Z3 дает неожиданный UNSAT для всех формул

У меня есть фрагмент кода z3py ниже

I = Int('I')
x = Int('x')
a = Int('a')
O = Bool('O')
constraint1 = Implies(x==0,O)
constraint2 = Implies(And(x >= 6, O), x ==6)

test = And(constraint1,constraint2,(O == I <= a), I==x)
s = Solver()
s.add(ForAll([x],test))
result = s.check()
print result
if result == sat:
    print s.model()

Он должен сделать вывод о правильности инварианта O через предоставленный набор соединений. В этом случае я предоставил соединение I == x, поэтому все, что нужно сделать z3, это угадать константу a как 6, чтобы дать правильный инвариант O == (x <= 6), который удовлетворяет предложениям рога. Однако я продолжаю получать UNSAT. Есть идеи, почему?


logic z3 z3py theorem-proving
person wrahman    schedule 03.09.2016    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Ограничения не выполняются.

У вас есть формула вида Forall x . And(.... , I == x) Последняя конъюнкция влечет Forall x . I == x, что не соответствует действительности, поскольку I взято из бесконечного набора чисел, так что это не тот случай, когда каждый x в этом бесконечном наборе равен I.

person Nikolaj Bjorner    schedule 03.09.2016
comment
Да, ты прав. Я предполагаю, что я пытаюсь сказать z3, чтобы он знал, что я теперь являюсь значением-заполнителем для x и количественно оценивается ForAll. Другими словами, моя формула должна читаться как ForAll I. And(....) из отображения I == x Любые предложения о том, как это сделать, будут очень признательны. - person wrahman; 04.09.2016