Z3Opt C++ API: parse smtlib2 Formel aus Datei

Question

Gibt es eine Möglichkeit in der Z3Opt C++ API smtlib2 Datei zu analysieren? Also, im Grunde versuche ich, die Z3Opt-Formel in eine Datei zu schreiben und sie dann in einem anderen Programm zu lesen. Die einzige Funktion, die ich gefunden habe, um smtlib2-Dateien zu parsen, ist Z3_parse_smtlib2_file. Aber es ist keine Unterstützung erweiterten smtlib2 Format (mit maximize, minimize und assert-soft Operationen), die sie in z3opt tutorial beschreiben. Die z3-Konsolenversion akzeptiert dieses Format jedoch und ist nicht fehlgeschlagen. Es bedeutet, dass es einen Weg gibt, zu tun, was ich brauche. Könnte mir bitte jemand helfen?

Hier einige Beispiel zu erklären, was ich rede:

#include <iostream> 
#include <fstream> 
#include <z3/z3++.h> 

void dumpFormula() { 
    z3::context ctx; 
    auto&& opt = z3::optimize(ctx); 

    auto&& x = ctx.int_const("x"); 
    auto&& y = ctx.int_const("y"); 

    opt.add(x < 2); 
    opt.add((y - x) < 1); 
    opt.maximize(x + y); 

    std::ofstream out("output.smt2"); 
    out << opt << std::endl; 
    return; 
} 

void readDumpedFormula() { 
    z3::context ctx; 
    auto&& opt = z3::optimize(ctx); 
    z3::set_param("timeout", 1000); 


    Z3_ast a = Z3_parse_smtlib2_file(ctx, "output.smt2", 0, 0, 0, 0, 0, 0); 
    z3::expr e(ctx, a); 
    opt.add(e); 

    auto&& res = opt.check(); 
    switch (res) { 
     case z3::sat: std::cout << "Sat" << std::endl;break; 
     case z3::unsat: std::cout << "Unsat" << std::endl;break; 
     case z3::unknown: std::cout << "Unknown" << std::endl;break; 
    } 
    return; 
} 

int main() { 
    dumpFormula(); 
    readDumpedFormula(); 
    return 0; 
} 

Funktion dumpFormula() eine z3opt Formel erstellen und es in die Datei auszugeben. Hier ist 'output.smt2' file:

(declare-fun x() Int) 
(declare-fun y() Int) 
(assert (< x 2)) 
(assert (< (- y x) 1)) 
(maximize (+ x y)) 
(check-sat) 

Funktion readDumpedFormula() die Datei zu analysieren versucht, und diese Formel überprüfen. Aber alles, was ich bekomme, sind Fehler. Hier ist eine Ausgabe des Programms:

ungestützt

; maximieren Linie: 5 Position: 17

Sat

Answer 1

Dies ist eine etwas rezidivierende Frage. Der Parser, der über die API verfügbar gemacht wird, können Sie nur Formeln laden. Es verwendet ein Plugin-Modell, um dem Parser mitzuteilen, welche Befehle registriert sind. In der Version, in der die API verfügbar ist, enthalten die bereitgestellten Befehle nicht die Befehle für die Optimierung.

Scheint wirklich nach einem Feature zu fragen, das ein Optimierungsobjekt (symmetrisch, ein Solver-Objekt) nimmt und es mit Assertions und Objektiven aus einer Zeichenkette oder Datei auffüllt.

Sie könnten das Laden der Datei approximieren, indem Sie spezielle Prädikate maximieren, minimieren, soft-assert, bzw.. Parsen Sie dann die Datei mit diesen Assertions. Dann packen Sie die geparsten Assertionen nach und füttern Sie diese in ein Optimierungsobjekt.