diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-08 16:28:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-08 16:28:22 -0500 |
commit | cfaa03f3db71dc2805b695f98b073431d0430e43 (patch) | |
tree | 29a005932e186354f2966603601982ca8448c89f /src/printer/smt2 | |
parent | f5e3739358b98d9a6ebc16fbc5aed9edee1483dc (diff) |
Infrastructure for approximations in model output (#1884)
Diffstat (limited to 'src/printer/smt2')
-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 |