diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-24 20:56:21 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-24 20:56:21 -0500 |
commit | 78b3f62746e95b915436c6a9bb57dab7be4d4fa4 (patch) | |
tree | 57c36e4803b1be7919c5d7be0cafe33a60b2fd54 /src | |
parent | 7988675ce9666b6f2214b583d42b9fa8be52ae60 (diff) |
Return choice functions for approximate values in get-value (#3304)
Diffstat (limited to 'src')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 15 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 12 |
3 files changed, 20 insertions, 13 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e9e8f2ea0..37a73db2d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -541,8 +541,7 @@ void Smt2Printer::toStream(std::ostream& out, return; case kind::LAMBDA: - out << smtKindString(k, d_variant) << " "; - break; + case kind::CHOICE: out << smtKindString(k, d_variant) << " "; break; // arith theory case kind::PLUS: @@ -1026,6 +1025,7 @@ static string smtKindString(Kind k, Variant v) case kind::LAMBDA: return "lambda"; + case kind::CHOICE: return "choice"; // arith theory case kind::PLUS: return "+"; @@ -1345,15 +1345,8 @@ 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; - } - } + // don't need to print approximations since they are built into choice + // functions in the values of variables. this->Printer::toStream(out, m); out << ")" << endl; //print the heap model, if it exists diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fa318aaf1..305c36d13 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4212,8 +4212,10 @@ Expr SmtEngine::getValue(const Expr& ex) const || resultNode.getType().isSubtypeOf(expectedType), "Run with -t smt for details."); - // ensure it's a constant - Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst()); + // Ensure it's a constant, or a lambda (for uninterpreted functions), or + // a choice (for approximate values). + Assert(resultNode.getKind() == kind::LAMBDA + || resultNode.getKind() == kind::CHOICE || resultNode.isConst()); if(options::abstractValues() && resultNode.getType().isArray()) { resultNode = d_private->mkAbstractValue(resultNode); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index e0798aa3c..f65d3a203 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -256,6 +256,18 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const d_modelCache[n] = ret; return ret; } + // it might be approximate + std::map<Node, Node>::const_iterator ita = d_approximations.find(n); + if (ita != d_approximations.end()) + { + // If the value of n is approximate based on predicate P(n), we return + // choice z. P(z). + Node v = nm->mkBoundVar(n.getType()); + Node bvl = nm->mkNode(BOUND_VAR_LIST, v); + Node ret = nm->mkNode(CHOICE, bvl, ita->second.substitute(n, v)); + d_modelCache[n] = ret; + return ret; + } // must rewrite the term at this point ret = Rewriter::rewrite(n); // return the representative of the term in the equality engine, if it exists |