diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 36076ec3c..27feea60e 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -443,6 +443,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::ARCCOSECANT: case kind::ARCSECANT: case kind::ARCCOTANGENT: + case kind::PI: case kind::SQRT: case kind::MINUS: case kind::UMINUS: @@ -926,6 +927,7 @@ static string smtKindString(Kind k, Variant v) case kind::ARCCOSECANT: return "arccsc"; case kind::ARCSECANT: return "arcsec"; case kind::ARCCOTANGENT: return "arccot"; + case kind::PI: return "real.pi"; case kind::SQRT: return "sqrt"; case kind::MINUS: return "-"; case kind::UMINUS: return "-"; @@ -1309,6 +1311,15 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const } //print the model out << "(model" << endl; + // print approximations + if (m.hasApproximations()) + { + std::vector<std::pair<Expr, Expr> > approx = m.getApproximations(); + for (unsigned i = 0, size = approx.size(); i < size; i++) + { + out << "(approximation " << approx[i].second << ")" << std::endl; + } + } this->Printer::toStream(out, m); out << ")" << endl; //print the heap model, if it exists |