API Z3 ast_to_string() с вычитанием

Проблема довольно проста. Я утверждаю следующее утверждение в Z3, используя интерфейс C API.

(assert(>= (xA 1) (- (yB 0) period))))

Теперь иногда мне нужно проверить, какие утверждения были отправлены, и результат в SatSolver. Я делаю это, создавая текстовый файл с помощью API ast_to_string(). Этот API возвращает мне приведенное выше заявление как -

(assert(>= (xA 1) (+ (yB 0) (* -1 period))))

Когда я загружаю этот файл в Sat Solver, он жалуется на ошибку -

(ошибка «ОШИБКА: строка 150, столбец 56: не удалось найти идентификатор -1».)

Итак, мне нужно вручную исправить все -1 в коде и запустить решатель спутников. Есть ли другой способ избежать этого?


z3
person Raj    schedule 31.05.2012    source источник
comment
Что вы подразумеваете под SatSolver? Зачем нужно проходить через текстовый файл? Нельзя ли просто вызвать его из API?   -  person Philippe    schedule 31.05.2012

Ответы (1)


arrow_upward
1
arrow_downward

Не забудьте установить:

Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);

перед использованием ast_to_string(), чтобы формулы вывода соответствовали формату SMTLIB 2.0.

person pad    schedule 31.05.2012
comment
Не очень решает проблему. Например, я получаю следующее на выходе - (assert(let ((?x28 (xA 1))) (>= ?x28 0))), поэтому в конечном итоге это убивает преимущество печати в файл. - person Raj; 31.05.2012
comment
Дело в том, что вывод парсится Z3 или нет. Наконец, SMTLIB — это машиночитаемый формат, а не человекочитаемый. - person pad; 31.05.2012