Eingabeargumente von Z3_benchmark_to_smtlib_string()

Question

Ich versuche, die Funktion Z3_benchmark_to_smtlib_string() zu verwenden. Hier sind die Argumente, die ich verwende:

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 ? */ 

Jede Hilfe wäre willkommen.

Parallel dazu verwende ich meine Annahmen im laufenden Betrieb angezeigt wird, mit:

Z3_set_ast_print_mode (CTX, Z3_PRINT_SMTLIB2_COMPLIANT);

en bekommt seltsame Zeichen wie:? X21, x24, x37, (siehe unten). Irgendein Hinweis, um dieses Problem zu lösen?

Vielen Dank im Voraus,

AG

(let ((? X21 (bvand (_ bv582 32) (ite (= ((_ sign_extend 24) (_ bv98 8)) ((_ sign_extend 24) | MEM5 [8] |)) (? _ bv64 32) (_ BV0 32))))) (lassen ((x24 (bvand x21 (ite (bvsgt ((_ sign_extend 24) (_ bv98 8)) ((_ sign_extend 24) | MEM5 [8] |?)) (_ bv128 32) (_ BV0 32))))) (lassen ((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)) ((_ Vorzeichen_Extend 24) | Mem6 [8] |)) (_ bv128 32) (_ bv0 32))))))

Answer 1

Diese Funktion ist ziemlich alt. Es wurde erstellt, als SMT 2.0 nicht existierte. Ein SMT 1.0 Benchmark sieht wie folgt aus:

(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)) 
) 

Die Funktion, die Sie zur Herstellung einer Benchmark in diesem Format wurde gemeint verwenden. Aus diesem Grund haben wir Parameter wie name, logic, status usw. Sie entsprechen den Anmerkungen im obigen Beispiel. Darüber hinaus besteht ein SMT 1.0 Problem aus 0 oder mehr Annahmen und 1 Formel.

Wenn SMT 2.0 eingeführt wurde, wurde diese Methode 2.0-Format drucken Benchmarks in SMT erweitert, wenn wir eine exponentielle blowup zu vermeiden beim Drucken Formeln haben

Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT); 

Die seltsamen Zeichen sind nur Hilfs let Erklärungen verwendet. Beachten Sie, dass Z3-ASTs DAGs und keine Bäume sind. Es ist sehr einfach, eine DAG unter Verwendung der C-API zu erstellen, die viel freigegeben wird. Beispiel:

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) 
... 

Der AST a_100 ist ein sehr kompaktes Objekt im Speicher. Wenn wir versuchen, es als Baum ohne die zusätzlichen Deklarationen let zu drucken, wird die Ausgabe sehr groß sein.

Beachten Sie, dass die Ausgabe von dieser Funktion erzeugt wurde nie von Menschen verzehrt gemeint werden. Es wird hauptsächlich verwendet, um Benchmarks für das Repository SMT-LIB zu generieren.