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?Z3Opt C++ API: parse smtlib2 Formel aus Datei
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
Es sieht so aus, als ob die Z3-Konsole eine andere Gruppe von Methoden verwendet als die C++ - API für Benutzer. Das Ausführen von Z3 mit GDB zeigt einen Trace durch 'main()' in 'main.cpp' nach' read_smtlib2_commands() 'in' smtlib_frontend.cpp' nach 'parse_smt2_commands()' in 'smt2parser.cpp'. Dies unterscheidet sich grundlegend von den Methoden in 'api_parsers.cpp'. –
@ DouglasB.Staple Ja. Ich habe auch darüber nachgedacht. Ich hoffte nur, dass es vielleicht eine Möglichkeit gibt, es in C++ API zu tun. – kivi