mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
add print to SMT-LIB format from solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
43269795c8
commit
b4600ffda0
|
@ -21,6 +21,7 @@ void demorgan() {
|
|||
// adding the negation of the conjecture as a constraint.
|
||||
s.add(!conjecture);
|
||||
std::cout << s << "\n";
|
||||
std::cout << s.to_smt2() << "\n";
|
||||
switch (s.check()) {
|
||||
case unsat: std::cout << "de-Morgan is valid\n"; break;
|
||||
case sat: std::cout << "de-Morgan is not valid\n"; break;
|
||||
|
|
|
@ -1314,6 +1314,26 @@ namespace z3 {
|
|||
expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
|
||||
expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
|
||||
friend std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
|
||||
|
||||
std::string to_smt2(char const* status = "unknown") {
|
||||
array<Z3_ast> es(assertions());
|
||||
Z3_ast const* fmls = es.ptr();
|
||||
Z3_ast fml = 0;
|
||||
unsigned sz = es.size();
|
||||
if (sz > 0) {
|
||||
--sz;
|
||||
fml = fmls[sz];
|
||||
}
|
||||
else {
|
||||
fml = ctx().bool_val(true);
|
||||
}
|
||||
return std::string(Z3_benchmark_to_smtlib_string(
|
||||
ctx(),
|
||||
"", "", status, "",
|
||||
sz,
|
||||
fmls,
|
||||
fml));
|
||||
}
|
||||
};
|
||||
|
||||
class goal : public object {
|
||||
|
|
Loading…
Reference in a new issue