Z3 не может обнаружить противоречивое утверждение с экзистенциальным квантификатором - PullRequest
Новая
       3

Z3 не может обнаружить противоречивое утверждение с экзистенциальным квантификатором

0 голосов
/ 08 октября 2018

Я создал противоречивую программу z3.Я добавил несколько ограничений, затем добавил противоречивое утверждение с экзистенциальным квантификатором (Exists([_x1,_y1,_z1],Implies(And(_CV1+_CE1<=_z1,And(_CE1<=_x1,_x1<_y1)),And(ForAll([_n1],Implies(And(_n1>=_x1,_n1<_y1),_z1+_f(_n1)<a)),_z1+_y1>=a)))) 

a=Int('a')
c=Int('c')
b=Int('b')
_n=Int('_n')
_CV1=Int('_CV1')
_CS1=Int('_CS1')
_CE1=Int('_CE1')
_x1=Int('_x1')
_y1=Int('_y1')
_z1=Int('_z1')
_n1=Int('_n1')
_f=Function('_f',IntSort(),IntSort())
_s=Solver()
_s.set("timeout",50000)
_s.add(ForAll([_n],Implies(_n>=0, _f(_n)==_n)))
_s.add(_CS1>=0)
_s.add(_CE1>_CS1)
_s.add(ForAll([_n1],Implies(And(_n1>=_CS1,_n1<_CE1),_CV1+_f(_n1)<a)))
_s.add(_CV1+_CE1>=a)  
_s.add(Exists([_x1,_y1,_z1],Implies(And(_CV1+_CE1<=_z1,And(_CE1<=_x1,_x1<_y1)),And(ForAll([_n1],Implies(And(_n1>=_x1,_n1<_y1),_z1+_f(_n1)<a)),_z1+_y1>=a))))

z3, возвращаем следующий контрпример 

[_y1!1 = 1,_x1!2 = 5,a = 1,_CS1 = 0,_CE1 = 1,_CV1 = 0,_z1!0 = 0,_f = [0 -> 0, else -> Var(0)]]

Существует ограничение _x1<_y1в следствии утверждения с экзистенциальным квантификатором.Странно контрпример _y1!1 = 1,_x1!2 = 5.Я не могу понять, почему он возвращает эти значения.

Если я удаляю экзистенциальный квантор, построенный по следующему запросу, это приводит к противоречию.

_s.add(_CS1>=0)
_s.add(_CE1>_CS1)
_s.add(ForAll([_n1],Implies(And(_n1>=_CS1,_n1<_CE1),_CV1+_f(_n1)<a)))
_s.add(_CV1+_CE1>=a)  
_s.add(_x1>=_CE1)
_s.add(_y1>_x1)
_s.add(_CV1+_CE1<=_z1)
_s.add(ForAll([_n1],Implies(And(_n1>=_x1,_n1<_y1),_z1+_f(_n1)<a)))
_s.add(_z1+_y1>=a)

Не могли бы вы помочь мне понять, почему первая программа z3 не возвращает желаемый результат.Пожалуйста, укажите, если я делаю какую-либо ошибку?

...