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/theory/theory_model.cpp | |
parent | 7988675ce9666b6f2214b583d42b9fa8be52ae60 (diff) |
Return choice functions for approximate values in get-value (#3304)
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
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 |