Входные аргументы Z3_benchmark_to_smtlib_string () - PullRequest
Новая
       6

Входные аргументы Z3_benchmark_to_smtlib_string ()

2 голосов
/ 27 марта 2012

Я пытаюсь использовать функцию Z3_benchmark_to_smtlib_string (). Вот аргументы, которые я использую: 

Z3_benchmark_to_smtlib_string(
                   ctx,          /* this one is valid */
                   "test",       /* this one is random, I don't understand it */
                   "QF_UFBV",    /* I got this name from the smtlib website, valid ? */
                   "sat",        /* not sure about this one either */
                   NULL,         /* not sure about this one either */
                   nb_assumptions, /* should be ok */
                   assumptions,    /* should be ok too */
                   NULL);          /* not sure about this one, is this mandatory ? */

Любая помощь будет приветствоваться.

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

Z3_set_ast_print_mode (CTX, Z3_PRINT_SMTLIB2_COMPLIANT);

ru получает странные символы, такие как:? X21,? X24,? X37, (см. Ниже). Любая подсказка, чтобы решить эту проблему?

Заранее спасибо,

* 1014 А.Г. *

(let ((? X21 (bvand (_ bv582 32) (ite (= ((_ sign_extend 24) (_ bv98 8)) ((_ sign_extend 24) | Mem5 [8] |)) (_ bv64 32 ) (_ bv0 32))))) (let ((? x24 (bvand? x21 (ite (bvsgt ((_ sign_extend 24) (_ bv98 8))) ((_ sign_extend 24) | Mem5 [8] |)) (_ bv128 32) (_ bv0 32) )))) (let ((? x37 (bvand? x24 (ite (= ((_ sign_extend 24) (_ bv97 8)) ((_ sign_extend 24) | Mem6 [8] |)) (_ bv64 32) (_ bv0 32) )))) (bvand? x37 (ite (bvsgt ((_ sign_extend 24) (_ bv97 8)) ((_ sign_extend 24) | Mem6 [8] |)) (_ bv128 32) (_ bv0 32))))))

1 Ответ

2 голосов
/ 28 марта 2012

Эта функция довольно старая. Он был создан, когда SMT 2.0 не существовало. Тест SMT 1.0 выглядит так: 

(benchmark example
:status sat
:logic QF_LIA
:extrafuns ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int))
:assumption (>= (- x1 x2) 1)
:assumption (>= (- x1 x2) 3)
:assumption (= x3 x5)
:formula (= x2 (* 6 x4))
)

Функция, которую вы используете, предназначена для создания эталона в этом формате. Вот почему у нас есть такие параметры, как name, logic, status и т. Д. Они соответствуют аннотациям в примере выше. Кроме того, проблема SMT 1.0 состоит из 0 или более предположений и 1 формулы.

Когда был представлен SMT 2.0, этот метод был расширен для печати тестов в формате SMT 2.0, когда у нас есть 

Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);

Странные символы - это просто вспомогательные let объявления, используемые для исключения экспоненциального увеличения при печати формул. Обратите внимание, что Z3 AST являются DAG, а не деревьями. Создать группу обеспечения доступности баз данных с помощью API C, который имеет много общего, очень просто. Пример: 

 a_1 = Z3_mk_bvadd(b, c)
 a_2 = Z3_mk_bvmul(a1, a1)
 a_3 = Z3_mk_bvadd(a2, a2)
 a_4 = Z3_mk_bvmul(a3, a3)
 ...

AST a_100 - очень компактный объект в памяти. Если мы попытаемся напечатать его в виде дерева без использования вспомогательных объявлений let, результат будет очень большим.

Обратите внимание, что выходные данные, создаваемые этой функцией, никогда не предназначались для потребления людьми. Он в основном используется для генерации тестов для репозитория SMT-LIB .

...