Инвариантная индукция над роговыми предложениями с Z3py

Question

В настоящее время я использую Z3py для вывода некоторых инвариантов, которые кодируются как совокупность роговых предложений, в то же время предоставляя шаблон для инварианта. Сначала я начинаю с простого примера, если вы видите фрагмент кода ниже.

x = 0; 
while(x < 5){ 
    x += 1 
} 
assert(x == 5) 

Это приводит к роговых положений

х = 0 => Inv (х)

< х 5/\ Inv (х) => Inv (х + 1)

Не (х < 5)/\ Inv (х) => х = 5

инвариант здесь х < = 5.

Я предоставил шаблон для инварианта формы a * x + b < = c , так что все решатели должны угадать набор значений для a, b и c, которые могут уменьшиться до x < = 5 .

Однако, когда я кодирую его, я все время становлюсь неустойчивым. Если попытаться утвердить Not (x == 5), я получу a = 2, b = 1/8 и c = 2, что не имеет для меня никакого смысла в качестве контрпримера.

Я предоставляю свой код ниже и был бы благодарен за помощь в исправлении моей кодировки.

x = Real('x') 
x_2 = Real('x_2') 
a = Real('a') 
b = Real('b') 
c = Real('c') 
s = Solver() 
s.add(ForAll([x],And(
Implies(x == 0 , a*x + b <= c), 
Implies(And(x_2 == x + 1, x < 5, a*x + b <= c), a*x_2 + b <= c), 
Implies(And(a*x + b <= c, Not(x < 5)), x==5) 
))) 
if (s.check() == sat): 
    print(s.model()) 

Редактировать: он становится для меня незнакомцем. Если я удалю определение x_2 и просто замените x_2 на (x + 1) во втором предложении horn, а также удалю x_2 = x_2 + 1, я получаю unsat ли я пишу Not (x == 5) или x == 5 в заключительном пункте рога.

Answer 1

Существовали две вещи, предотвращающие исходную кодировку из работы:

1) Это не представляется возможным удовлетворить x_2 == x + 1 для всех x для одного значения x_2. Таким образом, если вы собираетесь написать x_2 == x + 1, то и x, и x_2 необходимо количественно оценить.

2) Несколько удивительно, что эта проблема выполняется в целых числах, но не в действиях. Вы можете увидеть проблему с предложением x < 5 /\ Inv(x) => Inv(x + 1). Если x является целым числом, то это выполняется x <= 5. Однако, если x разрешено быть любой реальной стоимостью, тогда вы можете получить x == 4.5, который удовлетворяет как x < 5, так и x <= 5, но не x + 1 <= 5, поэтому Inv(x) = (x <= 5) не удовлетворяет этой проблеме в действиях.

Кроме того, вам может быть полезно определить Inv(x), он немного очищает код. Вот кодирование вашей проблемы с этими изменениями:

from z3 import * 

# Changing these from 'Int' to 'Real' changes the problem from sat to unsat. 
x = Int('x') 
x_2 = Int('x_2') 
a = Int('a') 
b = Int('b') 
c = Int('c') 

def Inv(x): 
    return a*x + b <= c 

s = Solver() 

# I think this is the simplest encoding for your problem. 
clause1 = Implies(x == 0 , Inv(x)) 
clause2 = Implies(And(x < 5, Inv(x)), Inv(x + 1)) 
clause3 = Implies(And(Inv(x), Not(x < 5)), x == 5) 
s.add(ForAll([x], And(clause1, clause2, clause3))) 

# Alternatively, if clause2 is specified with x_2, then x_2 needs to be 
# universally quantified. Note the ForAll([x, x_2]... 
#clause2 = Implies(And(x_2 == x + 1, x < 5, Inv(x)), Inv(x_2)) 
#s.add(ForAll([x, x_2], And(clause1, clause2, clause3))) 

# Print result all the time, to avoid confusing unknown with unsat. 
result = s.check() 
print result 
if (result == sat): 
    print(s.model()) 

Еще одна вещь: это немного странно для меня, чтобы написать a*x + b <= c в качестве шаблона, потому что это то же самое, как a*x <= d для некоторого целого d.