From 78b3f62746e95b915436c6a9bb57dab7be4d4fa4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 24 Sep 2019 20:56:21 -0500 Subject: Return choice functions for approximate values in get-value (#3304) --- src/theory/theory_model.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/theory/theory_model.cpp') 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::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 -- cgit v1.2.3