From abd0048cdb6cf4d2ee0a096c9f7a63a1f7f1d9c8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 26 Feb 2020 09:02:15 -0600 Subject: [PATCH] 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. --- src/options/smt_options.toml | 9 +++++++++ src/theory/arith/nl_model.cpp | 16 +++++++++++++--- src/theory/arith/nl_model.h | 8 +++++--- src/theory/arith/nonlinear_extension.cpp | 11 +++++++++-- src/theory/arith/nonlinear_extension.h | 7 +++++-- src/theory/theory_model.cpp | 5 +++++ src/theory/theory_model.h | 7 +++++++ test/regress/CMakeLists.txt | 1 + .../nl/issue3300-approx-sqrt-witness.smt2 | 11 +++++++++++ 9 files changed, 65 insertions(+), 10 deletions(-) create mode 100644 test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 024530224..88842faf7 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -419,6 +419,15 @@ header = "options/smt_options.h" read_only = true help = "in models, output uninterpreted sorts as datatype enumerations" +[[option]] + name = "modelWitnessChoice" + category = "regular" + long = "model-witness-choice" + type = "bool" + default = "false" + read_only = true + help = "in models, use a witness constant for choice functions" + [[option]] name = "regularChannelName" smt_name = "regular-output-channel" 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& arithModel, - std::map& approximations) +void NlModel::getModelValueRepair( + std::map& arithModel, + std::map>& 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& 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(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& arithModel, - std::map& approximations); + void getModelValueRepair( + std::map& arithModel, + std::map>& 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& a : d_approximations) + for (std::pair>& 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 d_cmiLemmas; std::vector d_cmiLemmasPp; - /** The approximations computed during collectModelInfo. */ - std::map d_approximations; + /** + * The approximations computed during collectModelInfo. For details, see + * NlModel::getModelValueRepair. + */ + std::map> d_approximations; /** have we successfully built the model in this SAT context? */ context::CDO 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 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b909817df..6acc6f7c8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1306,6 +1306,7 @@ set(regress_1_tests regress1/nl/exp1-lb.smt2 regress1/nl/exp_monotone.smt2 regress1/nl/factor_agg_s.smt2 + regress1/nl/issue3300-approx-sqrt-witness.smt2 regress1/nl/issue3441.smt2 regress1/nl/issue3617.smt2 regress1/nl/issue3656.smt2 diff --git a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 new file mode 100644 index 000000000..9bc47f925 --- /dev/null +++ b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 @@ -0,0 +1,11 @@ +; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/; s/((x (choice ((BOUND_VARIABLE Real)) (or (= BOUND_VARIABLE.*/SUCCESS/' +; COMMAND-LINE: --produce-models --model-witness-choice --no-check-models +; EXPECT: sat +; EXPECT: SUCCESS +(set-logic QF_NRA) +(set-info :status sat) +(declare-fun x () Real) +(assert (= (* x x) 2)) +(check-sat) +(get-value (x)) + -- 2.30.2