Z3 считает модель несовместимой с аксиомами - PullRequest
Новая
       19

Z3 считает модель несовместимой с аксиомами

0 голосов
/ 18 января 2019

При запуске этого кода на Python 3.6.7 с модулем z3-solver (4.8.0.0) модель, возвращаемая z3, кажется, не подходит для аксиом. 

f = z3.Function('f', z3.IntSort(), z3.IntSort(), z3.IntSort())
x = z3.Int('x')
s = z3.Solver()
s.add(f(1, 10) == 42)
s.add(z3.ForAll([x], f(2, x) == f(1, x)))
s.check()
m = s.model()
print(m.eval(f(1, 10)))  # print 0
print(m.eval(f(2, 10)))  # print 0

Почему мы не получили 42, как мы могли ожидать? Есть ли проблема с аксиомами или функцией?

1 Ответ

0 голосов
/ 18 января 2019

Похоже, ваша установка может быть повреждена, так как я не могу повторить это: 

$ cat a.py
import z3
f = z3.Function('f', z3.IntSort(), z3.IntSort(), z3.IntSort())
x = z3.Int('x')
s = z3.Solver()
s.add(f(1, 10) == 42)
s.add(z3.ForAll([x], f(2, x) == f(1, x)))
print s.sexpr()
s.check()
m = s.model()
print(m.eval(f(1, 10)))  # print 0
print(m.eval(f(2, 10)))  # print 0

$ python a.py
(declare-fun f (Int Int) Int)
(assert (= (f 1 10) 42))
(assert (forall ((x Int)) (= (f 2 x) (f 1 x))))

42
42

Обратите внимание, что я добавил print s.sexpr() к вашему коду, и он красиво напечатал сгенерированный SMTLib. Вы видите то же самое?

...