diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 09:02:15 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-26 09:02:15 -0600 |
commit | abd0048cdb6cf4d2ee0a096c9f7a63a1f7f1d9c8 (patch) | |
tree | cffa12338950b4d7b5bfc43e78849684b6058e30 /src/theory | |
parent | 50c31e61ab240ccd551a0aea732f8b9a88d7fb32 (diff) |
Support for witnessing choice in models (#3781)
Fixes #3300.
This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/nl_model.cpp | 16 | ||||
-rw-r--r-- | src/theory/arith/nl_model.h | 8 | ||||
-rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 11 | ||||
-rw-r--r-- | src/theory/arith/nonlinear_extension.h | 7 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 5 | ||||
-rw-r--r-- | src/theory/theory_model.h | 7 |
6 files changed, 44 insertions, 10 deletions
diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index 8a4145552..929eb4acc 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -1247,8 +1247,9 @@ void NlModel::printModelValue(const char* c, Node n, unsigned prec) const } } -void NlModel::getModelValueRepair(std::map<Node, Node>& arithModel, - std::map<Node, Node>& approximations) +void NlModel::getModelValueRepair( + std::map<Node, Node>& arithModel, + std::map<Node, std::pair<Node, Node>>& approximations) { // Record the approximations we used. This code calls the // recordApproximation method of the model, which overrides the model @@ -1266,8 +1267,17 @@ void NlModel::getModelValueRepair(std::map<Node, Node>& arithModel, if (l != u) { Node pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); - approximations[v] = pred; Trace("nl-model") << v << " approximated as " << pred << std::endl; + Node witness; + if (options::modelWitnessChoice()) + { + // witness is the midpoint + witness = nm->mkNode( + MULT, nm->mkConst(Rational(1, 2)), nm->mkNode(PLUS, l, u)); + witness = Rewriter::rewrite(witness); + Trace("nl-model") << v << " witness is " << witness << std::endl; + } + approximations[v] = std::pair<Node, Node>(pred, witness); } else { diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl_model.h index 66c5d89c1..354f6f71c 100644 --- a/src/theory/arith/nl_model.h +++ b/src/theory/arith/nl_model.h @@ -180,10 +180,12 @@ class NlModel * The mapping arithModel is updated by this method to map arithmetic terms v * to their (exact) value that was computed during checkModel; the mapping * approximations is updated to store approximate values in the form of a - * predicate over v. + * pair (P, w), where P is a predicate that describes the possible values of + * v and w is a witness point that satisfies this predicate. */ - void getModelValueRepair(std::map<Node, Node>& arithModel, - std::map<Node, Node>& approximations); + void getModelValueRepair( + std::map<Node, Node>& arithModel, + std::map<Node, std::pair<Node, Node>>& approximations); private: /** The current model */ diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 6c04268db..acae404ba 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -1304,9 +1304,16 @@ void NonlinearExtension::check(Theory::Effort e) { // Otherwise, we will answer SAT. The values that we approximated are // recorded as approximations here. TheoryModel* tm = d_containing.getValuation().getModel(); - for (std::pair<const Node, Node>& a : d_approximations) + for (std::pair<const Node, std::pair<Node, Node>>& a : d_approximations) { - tm->recordApproximation(a.first, a.second); + if (a.second.second.isNull()) + { + tm->recordApproximation(a.first, a.second.first); + } + else + { + tm->recordApproximation(a.first, a.second.first, a.second.second); + } } } } diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index ddca284a4..338ae6611 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -480,8 +480,11 @@ class NonlinearExtension { */ std::vector<Node> d_cmiLemmas; std::vector<Node> d_cmiLemmasPp; - /** The approximations computed during collectModelInfo. */ - std::map<Node, Node> d_approximations; + /** + * The approximations computed during collectModelInfo. For details, see + * NlModel::getModelValueRepair. + */ + std::map<Node, std::pair<Node, Node>> d_approximations; /** have we successfully built the model in this SAT context? */ context::CDO<bool> d_builtModel; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index c6055ede9..399695131 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -598,6 +598,11 @@ void TheoryModel::recordApproximation(TNode n, TNode pred) // model cache is invalid d_modelCache.clear(); } +void TheoryModel::recordApproximation(TNode n, TNode pred, Node witness) +{ + Node predDisj = NodeManager::currentNM()->mkNode(OR, n.eqNode(witness), pred); + recordApproximation(n, predDisj); +} void TheoryModel::setUsingModelCore() { d_using_model_core = true; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 0914987cc..d2ce63ac5 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -215,6 +215,13 @@ public: * construction process. */ void recordApproximation(TNode n, TNode pred); + /** + * Same as above, but with a witness constant. This ensures that the + * approximation predicate is of the form (or (= n witness) pred). This + * is useful if the user wants to know a possible concrete value in + * the range of the predicate. + */ + void recordApproximation(TNode n, TNode pred, Node witness); /** set unevaluate/semi-evaluated kind * * This informs this model how it should interpret applications of terms with |