Упрощение выражения с использованием переменных в конечной области

Тактика ctx-solver-simplify работает только для логических переменных, поэтому как мне поступить с переменными в конечной области (например, какую тактику использовать)? Например, если z может принимать только 3 значения 0,1,2, то как упростить Or(z==0,z==1,z==2) до true?

Кроме того, даже для логических выражений тактика ctx-solver-simplify не упрощается полностью. Например:

x,y,z = z3.Bools('x y z')
c1 = z3.And(x==True,y==True,z==True)
c2 = z3.And(x==True,y==True,z==False)
c3 = z3.And(x==True,y==False,z==True)
c4 = z3.And(x==True,y==True,z==False)
z3.Tactic('ctx-solver-simplify')(z3.Or([c1,c2,c3,c4]))
[[Or(And(x, z), And(x == True, y == True, z == False))]]

Как мне получить что-то вроде And(x, Or(z, y)) ?

Спасибо !


simplify z3 z3py
person Vu Nguyen    schedule 10.03.2015    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Приведение булевых (или других задач конечной области) к минимальной форме является трудной задачей. Тактика ctx-solver-simplify является одним из самых дорогих упрощений, но она не доходит до доказуемо наименьшей формы.

Задачи из других областей (например, перечисления вроде z \in {0, 1, 2}) должны быть сначала преобразованы в логические значения, чтобы использовать эту тактику, но, возможно, другие тактики будут лучше подходить, и, возможно, кодирование бит-векторов будет лучше. помогите тоже.

person Christoph Wintersteiger    schedule 21.03.2015