Код дает неверный результат с ForAll, почему?

Я пытаюсь использовать квантификатор ForAll для b, поэтому формула a * b == b с каждым b даст мне в результате a == 1. Я реализовал это в приведенном ниже коде (Z3 python):

from z3 import *

a, b, a1 = BitVecs('a b a1', 32)

f = True
f = And(f, a1 == a * b)
f = And(f, a1 == b)

s = Solver()
s.add(ForAll(b, f))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

Я ожидал, что Z3 выдаст мне a = 1 на выходе, но вместо этого я получил Unsat. Любая идея о том, где проблема?

(Подозреваю, что неправильно использую ForAll, но не знаю, как это исправить)


python z3 z3py
person user311703    schedule 15.06.2013    source источник

Ответы (4)


arrow_upward
1
arrow_downward

Что Вы думаете об этом:

a, b, a1 = BitVecs('a b a1', 32)

f = True
f = And(f, a1 == a * b)
g= True
g = And(f, a1 == b)

s = Solver()
s.add(ForAll(b, ForAll(a1,f == g)))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat

выход:

a = 1

Другая форма:

a, b, a1 = BitVecs('a b a1', 32)

f = True
f = And(f, a1 == a * b)
g= True
g = And(g, a1 == b)

s = Solver()
s.add(ForAll(b, ForAll(a1,f == g)))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

выход:

a = 1
person Juan Ospina    schedule 16.06.2013
comment
Хуан, это работает, спасибо! Однако я бы изменил ForAll на ForAll([b, a1],f == g). Еще раз спасибо! - person user311703; 17.06.2013
comment
Кстати, у вас есть какие-либо предложения для исходного кода? В вашем коде представлена ​​новая формула g, тогда как в исходном коде есть только одна формула f. Спасибо. - person user311703; 17.06.2013

arrow_upward
0
arrow_downward

Что Вы думаете об этом:

a, b = BitVecs('a b', 32)

a1 = a*b
a2 = b


s = Solver()
s.add(ForAll(b, a1 == a2))

if s.check() == sat:
     print 'a =', s.model()[a]
else:
     print 'Unsat'

выход:

a = 1

Другой путь:

a, b = BitVecs('a b', 32)
a1 = a*b
a2 = b
f = True
f = And(f, a1 == a2)


s = Solver()
s.add(ForAll(b, f))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

выход:

a = 1
person Juan Ospina    schedule 15.06.2013
comment
Второе решение действительно интересное. Я никогда не думал, что можно просто так использовать a1 и a2, не объявляя a1 = BitVec(32). Но, похоже, это работает, что подтверждается вашим кодом. Есть объяснение этому???? - person user311703; 16.06.2013
comment
Кстати, мне все еще интересно, почему мой исходный код возвращает «Unsat». Есть идеи? Спасибо - person user311703; 16.06.2013

arrow_upward
0
arrow_downward

Вы просите Z3 (среди прочего) найти единственный a1, который равен b для всех значений b. Это невозможно. Ваша проблема не в Z3, а в базовой логике.

person Vladimir Klebanov    schedule 16.06.2013
comment
Владимир, у вас есть предложения по исправлению исходного кода? Хуан дал мне несколько советов, но этого все еще нет в исходном коде (в исходном вопросе). Спасибо! - person user311703; 17.06.2013

arrow_upward
0
arrow_downward

Если вы просто хотите проверить формулу a * b == b для всех возможных b. Вы можете использовать следующий код.

from z3 import *

a, b = BitVecs('a b', 32)
s = Solver()
s.add(ForAll(b, a * b == b))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

Этот код запускается в мгновение ока, но ваш код перегружает решатель и занимает относительно много времени для завершения.

person frogatto    schedule 23.05.2016