как преобразовать выражение z3py в формат smtlib 2

Мой вопрос связан с: Z3: преобразовать выражение Z3py в SMT-LIB2?

Я пытаюсь преобразовать выражение z3py из в формат smtlib2. используя следующий скрипт, но после преобразования, когда я передаю результат на z3 или любой другой SMT, я получаю:

"Синтаксическая ошибка, непредвиденный let"

Есть ли способ привести его в формат smtlib2 с помощью z3py, чтобы мне не приходилось снова писать длинное выражение.

Ниже приведен код, который я использую для преобразования:

def convertor(f, status="unknown", name="benchmark", logic=""):
v = (Ast * 0)()
if isinstance(f, Solver):
a = f.assertions()
if len(a) == 0:
  f = BoolVal(True)
else:
  f = And(*a)
return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())

x = Int('x')
y = Int('y')
s = Solver()
s.add(x > 0)
s.add( x < 100000)
s.add(x==2*y)
print convertor(s, logic="QF_LIA")

и это вывод:

(set-info :status unknown)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(let (($x34 (= x (* 2 y))))
(let (($x31 (< x 100000)))
(let (($x10 (> x 0)))
(let (($x35 (and $x10 $x31 $x34)))
(assert $x35)))))
(check-sat)

python python-2.7 z3 z3py
person user3196876    schedule 24.03.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

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

Скорее всего, эта проблема из-за устаревшей версии Z3. Было множество исправлений, которые еще не попали в основную ветку и использовали нестабильную ветку (или предварительно скомпилированные ночные двоичные файлы здесь) я получаю другой вывод, который Z3 принимает без ошибок:

(set-info :status unknown)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(assert
(let (($x34 (= x (* 2 y))))
(let (($x31 (< x 100000)))
(let (($x10 (> x 0)))
(and $x10 $x31 $x34)))))
(check-sat)
person Christoph Wintersteiger    schedule 24.03.2014
comment
но проблема в том, что я передаю его другому SMT, и он говорит: синтаксическая ошибка пусть не определена. - person user3196876; 25.03.2014
comment
Я случайно скопировал не тот вывод, я обновил свой пост. - person Christoph Wintersteiger; 25.03.2014