Sum () для значений с плавающей точкой в ​​Z3 - PullRequest
Новая
       106

Sum () для значений с плавающей точкой в ​​Z3

1 голос
/ 04 мая 2020

Я пытаюсь написать что-то, чтобы решить для переменного количества переменных с плавающей запятой, учитывая ожидаемое среднее. Тем не менее, я получаю это исключение при попытке запустить мой код.

z3.z3types.Z3Exception: b'Sort mismatch at argument #1 for function (declare-fun + (Int Int) Int) supplied sort is (_ FloatingPoint 8 24)'

Похоже, Sum() по некоторым причинам не работает со значениями с плавающей запятой. Это, или я просто делаю что-то не так.

Вот некоторый минимальный код воспроизведения: 

from z3 import *

l = [FP('x', Float32()), FP('y', Float32()), FP('z', Float32())]
s = Solver()
#s.add(Sum(l) == 100) # uncomment for exception
s.add(l[0] + l[1] + l[2] == 100)
s.check()
print(s.model())

1 Ответ

1 голос
/ 04 мая 2020

Вы не делаете ничего плохого. Просто метод Sum, экспортируемый API z3py, поддерживает только битовые векторы, целые числа и вещественные числа. В частности, он не допускает значения с плавающей точкой.

Нет причин, по которым это не следует делать, и вы можете зарегистрировать это как отсутствующую функцию в их системе отслеживания ошибок: https://github.com/Z3Prover/z3/issues

(Если вы сделаете это, вы также можете упомянуть, что у функции Product есть тот же недостаток, поэтому они могут исправить это вместе.)

Тем временем я рекомендую определить собственный метод. Примерно так: 

from z3 import *

import functools

def MySum(lst):
    return functools.reduce(lambda a, b: a + b, lst, 0);

l = [FP('x', Float32()), FP('y', Float32()), FP('z', Float32())]
s = Solver()
s.add(MySum(l) == 100)
s.check()
print(s.model())

Обратите внимание, что MySum является достаточно полиморфным c: его можно использовать для типов Int s, Real s, Float s, BitVec, и все будет работать Что он не делает, конечно, проверяет, чтобы убедиться, что вы передаете действительно то, что вы можете суммировать, например, не перечисления или какой-то другой тип данных. (И по сути, именно это пытается сделать внутренний метод API: он проверяет, имеет ли смысл то, что вы передаете, суммировать, за исключением того, что они пропустили регистр для чисел с плавающей запятой.)

...