Преобразование объектов ast (или решателя) z3 C++ API в строку SMTLIB

Я играю с z3 и другими решателями SMT и хочу изучить случаи, когда другие решатели, такие как boolector, побеждают z3 и наоборот. Для этой цели мне нужен способ преобразования объявлений и утверждений в формат SMT-LIB2, который могут распознавать другие решатели SMT.

Например, для этого примера

void print_as_smtlib2_string() {
    context c;
    expr x = c.int_const("x");
    expr y = c.int_const("y");
    solver s(c);

    s.add(x >= 1);
    s.add(y < x + 3);
    std::cout << s.check() << "\n";

    Z3_set_ast_print_mode(c, Z3_PRINT_SMTLIB_COMPLIANT);

    std::cout << "\nSolver is:\n";
    std::cout << s << "\n";
}

Я получаю что-то вроде: сидел

Решатель: (решатель (>= x 1) (‹ y (+ x 3)))

Вместо этого я хочу что-то вроде этого (ссылка на rise4fun: http://rise4fun.com/Z3/aznC8):

(declare-const x Int)
(declare-const y Int)
(assert (>= x 1))
(assert (< y (+ x 3)))
(check-sat)

Я пробовал функции C API, такие как Z3_set_ast_print_mode, Z3_ast_to_string, но безуспешно. Я просмотрел Z3_benchmark_to_smtlib_string, но этот пост Входные аргументы Z3_benchmark_to_smtlib_string() предполагает, что он поддерживает только SMTLIB 1.0.


c++ api z3 smt
person Tushar    schedule 28.03.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Z3_benchmark_to_smtlib_string — единственная функция Z3 для этой цели. Как и сообщение, на которое вы ссылаетесь, оно было расширено до SMTLIB2. Как говорит Лео в своем ответе на этот пост, это старая функция, которая редко используется, и она может не поддерживать сброс всех функций (например, параметров решателей). Недавно был также другой пост, касающийся этой функции и проблем/ошибок в более старых версиях Z3 (см. -smtlib-2-format">здесь).

person Christoph Wintersteiger    schedule 31.03.2014