Вопрос по string – Z3 со строковыми выражениями

2

Я пытаюсь использовать Z3, чтобы определить, является ли выражение выполнимым. Я мог бы легко сделать это, определив контекст, а затем переменные int_const и формулу. Чтобы вычислить выражение программно, вы должны написать все в коде. Допустим, логическое выражение задано в виде строки, что тогда? Например,

& quot; x == y & amp; & amp; ! x == z & quot;

будет выражаться в C API как:

context c;
expr x = c.int_const("x")
//Same for other variables
...
formula = (x == y) && (!x == z);
solver s(c);
s.add(formula);
//s.check() ...etc etc

Хорошо, я могу написать код для этой конкретной формулы, но как я могу сделать это программно с помощью строки. Я открыт для всего, что вы можете придумать.

Спасибо :)

Ваш Ответ

1   ответ
2

Я вижу следующие варианты:

1) вы можете реализовать свой собственный синтаксический анализатор и вызывать функции API Z3. Pro: вы можете использовать свой & quot; любимый & quot; язык для написания формул. Против: он "занят" Работа.

2) вы можете использовать APIZ3_parse_smtlib2_string, Против: ваши формулы должны быть в формате SMT 2.0. Например, вам придется написать(and (= x y) (not (= x y))) вместо(x == y) && !(x == z).

3) Вы можете использовать Z3 Python API и анализировать строки, используяeval функция в Python. Вот пример:

from z3 import *
# Creating x, y 
x = Int('x')
y = Int('y')

# Creating the formula using Python
f = And(x == y, Not(x == y))
print f

# Using eval to parse the string.
s = "And(x == y, Not(x == y))"
f2 = eval(s)
print f2

Кстати, этот скрипт не работает на rise4funhttp://rise4fun.com/z3py потому что функцияeval там не разрешено, но вы можете использовать приведенный выше скрипт в вашей локальной установке Z3.

Похожие вопросы