From 7de44af3d352fe9f622945f8a61b2b1b4e6d8b49 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 25 Feb 2022 10:45:41 -0600 Subject: [PATCH] Remove approximations infrastructure from model (#8166) We now allow partial specifications. Recording approximations is arithmetic specific, and if necessary could be added as a post-processing analysis e.g. during check-model. --- src/options/smt_options.toml | 9 ---- src/theory/arith/nl/nl_model.cpp | 22 ++-------- src/theory/arith/nl/nl_model.h | 10 +---- src/theory/arith/nl/nonlinear_extension.cpp | 44 +------------------ src/theory/arith/nl/nonlinear_extension.h | 16 ------- src/theory/arith/theory_arith.cpp | 7 --- src/theory/theory_model.cpp | 38 ---------------- src/theory/theory_model.h | 37 ---------------- src/theory/theory_model_builder.cpp | 5 --- .../nl/issue3300-approx-sqrt-witness.smt2 | 2 +- 10 files changed, 7 insertions(+), 183 deletions(-) diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 739f898f1..e37d84d1a 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -383,15 +383,6 @@ name = "SMT Layer" name = "none" help = "(default) do not print declarations of uninterpreted elements in models." - -[[option]] - name = "modelWitnessValue" - category = "regular" - long = "model-witness-value" - type = "bool" - default = "false" - help = "in models, use a witness constant for choice functions" - [[option]] name = "foreignTheoryRewrite" category = "regular" diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index e236e3375..c566758be 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -1015,10 +1015,7 @@ void NlModel::printModelValue(const char* c, Node n, unsigned prec) const } } -void NlModel::getModelValueRepair( - std::map& arithModel, - std::map>& approximations, - bool witnessToValue) +void NlModel::getModelValueRepair(std::map& arithModel) { Trace("nl-model") << "NlModel::getModelValueRepair:" << std::endl; // If we extended the model with entries x -> 0 for unconstrained values, @@ -1031,29 +1028,16 @@ void NlModel::getModelValueRepair( // recordApproximation method of the model, which overrides the model // values for variables that we solved for, using techniques specific to // this class. - NodeManager* nm = NodeManager::currentNM(); for (const std::pair>& cb : d_check_model_bounds) { Node l = cb.second.first; Node u = cb.second.second; - Node pred; Node v = cb.first; if (l != u) { - pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); - Trace("nl-model") << v << " approximated as " << pred << std::endl; - Node witness; - if (witnessToValue) - { - // witness is the midpoint - witness = nm->mkNode(MULT, - nm->mkConst(CONST_RATIONAL, Rational(1, 2)), - nm->mkNode(ADD, l, u)); - witness = rewrite(witness); - Trace("nl-model") << v << " witness is " << witness << std::endl; - } - approximations[v] = std::pair(pred, witness); + Trace("nl-model") << v << " is in interval " << l << "..." << u + << std::endl; } else { diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index 27cb0f81d..265e270db 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -172,15 +172,9 @@ class NlModel : protected EnvObj * call to checkModel above. * * 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 - * 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. + * to their (exact) value that was computed during checkModel. */ - void getModelValueRepair( - std::map& arithModel, - std::map>& approximations, - bool witnessToValue); + void getModelValueRepair(std::map& arithModel); private: /** Cache for concrete model values */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index bb360a542..a26dbf173 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -276,19 +276,8 @@ void NonlinearExtension::checkFullEffort(std::map& arithModel, if (res == Result::Sat::SAT) { Trace("nl-ext") << "interceptModel: do model repair" << std::endl; - d_approximations.clear(); // modify the model values - d_model.getModelValueRepair(arithModel, - d_approximations, - options().smt.modelWitnessValue); - for (auto& am : arithModel) - { - Node val = getModelValue(am.first); - if (!val.isNull()) - { - am.second = val; - } - } + d_model.getModelValueRepair(arithModel); } // must post-process model with transcendental solver, to ensure we don't // assign values for equivalence classes with transcendental function @@ -296,37 +285,6 @@ void NonlinearExtension::checkFullEffort(std::map& arithModel, d_trSlv.postProcessModel(arithModel, termSet); } -Node NonlinearExtension::getModelValue(TNode var) const -{ - if (auto it = d_approximations.find(var); it != d_approximations.end()) - { - if (it->second.second.isNull()) - { - return it->second.first; - } - return Node::null(); - } - return Node::null(); -} - -bool NonlinearExtension::assertModel(TheoryModel* tm, TNode var) const -{ - if (auto it = d_approximations.find(var); it != d_approximations.end()) - { - const auto& approx = it->second; - if (approx.second.isNull()) - { - tm->recordApproximation(var, approx.first); - } - else - { - tm->recordApproximation(var, approx.first, approx.second); - } - return true; - } - return false; -} - Result::Sat NonlinearExtension::modelBasedRefinement(const std::set& termSet) { ++(d_stats.d_mbrRuns); diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index dc7682f68..0c94bbc08 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -111,16 +111,6 @@ class NonlinearExtension : EnvObj void checkFullEffort(std::map& arithModel, const std::set& termSet); - /** - * Retrieve the model value for the given variable. It may be either an - * arithmetic term or a witness. - */ - Node getModelValue(TNode var) const; - /** - * Assert the model for the given variable to the theory model. - */ - bool assertModel(TheoryModel* tm, TNode var) const; - /** Does this class need a call to check(...) at last call effort? */ bool hasNlTerms() const { return d_hasNlTerms; } @@ -272,12 +262,6 @@ class NonlinearExtension : EnvObj /** The strategy for the nonlinear extension. */ Strategy d_strategy; - - /** - * The approximations computed during collectModelInfo. For details, see - * NlModel::getModelValueRepair. - */ - std::map> d_approximations; }; /* class NonlinearExtension */ } // namespace nl diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4480fdbb3..26e3c52f1 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -292,13 +292,6 @@ bool TheoryArith::collectModelValues(TheoryModel* m, { continue; } - if (d_nonlinearExtension != nullptr) - { - if (d_nonlinearExtension->assertModel(m, p.first)) - { - continue; - } - } // maps to constant of comparable type Assert(p.first.getType().isComparableTo(p.second.getType())); if (m->assertEquality(p.first, p.second, true)) diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 36502101b..58bd32995 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -80,8 +80,6 @@ void TheoryModel::reset(){ d_modelCache.clear(); d_sep_heap = Node::null(); d_sep_nil_eq = Node::null(); - d_approximations.clear(); - d_approx_list.clear(); d_reps.clear(); d_assignExcSet.clear(); d_aesMaster.clear(); @@ -110,13 +108,6 @@ bool TheoryModel::getHeapModel(Node& h, Node& neq) const return true; } -bool TheoryModel::hasApproximations() const { return !d_approx_list.empty(); } - -std::vector > TheoryModel::getApproximations() const -{ - return d_approx_list; -} - std::vector TheoryModel::getDomainElements(TypeNode tn) const { // must be an uninterpreted sort @@ -277,18 +268,6 @@ Node TheoryModel::getModelValue(TNode n) const 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 - // witness z. P(z). - Node v = nm->mkBoundVar(n.getType()); - Node bvl = nm->mkNode(BOUND_VAR_LIST, v); - Node answer = nm->mkNode(WITNESS, bvl, ita->second.substitute(n, v)); - d_modelCache[n] = answer; - return answer; - } // must rewrite the term at this point ret = rewrite(n); // return the representative of the term in the equality engine, if it exists @@ -588,23 +567,6 @@ bool TheoryModel::hasAssignmentExclusionSets() const return !d_assignExcSet.empty(); } -void TheoryModel::recordApproximation(TNode n, TNode pred) -{ - Trace("model-builder-debug") - << "Record approximation : " << n << " satisfies the predicate " << pred - << std::endl; - Assert(d_approximations.find(n) == d_approximations.end()); - Assert(pred.getType().isBoolean()); - d_approximations[n] = pred; - d_approx_list.push_back(std::pair(n, 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); -} bool TheoryModel::isUsingModelCore() const { return d_using_model_core; } void TheoryModel::setUsingModelCore() { diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index b476ddfef..e1ddef5d4 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -186,35 +186,6 @@ class TheoryModel : protected EnvObj std::vector& eset); /** have any assignment exclusion sets been created? */ bool hasAssignmentExclusionSets() const; - /** record approximation - * - * This notifies this model that the value of n was approximated in this - * model such that the predicate pred (involving n) holds. For example, - * for transcendental functions, we may determine an error bound on the - * value of a transcendental function, say c-e <= y <= c+e where - * c and e are constants. We call this function with n set to sin( x ) and - * pred set to c-e <= sin( x ) <= c+e. - * - * If recordApproximation is called at least once during the model - * construction process, then check-model is not guaranteed to succeed. - * However, there are cases where we can establish the input is satisfiable - * without constructing an exact model. For example, if x=.77, sin(x)=.7, and - * say we have computed c=.7 and e=.01 as an approximation in the above - * example, then we may reason that the set of assertions { sin(x)>.6 } is - * satisfiable, albiet without establishing an exact (irrational) value for - * sin(x). - * - * This function is simply for bookkeeping, it does not affect the model - * 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 @@ -305,10 +276,6 @@ class TheoryModel : protected EnvObj bool getHeapModel(Node& h, Node& neq) const; //---------------------------- end separation logic - /** is the list of approximations non-empty? */ - bool hasApproximations() const; - /** get approximations */ - std::vector > getApproximations() const; /** get domain elements for uninterpreted sort t */ std::vector getDomainElements(TypeNode t) const; /** get the representative set object */ @@ -374,10 +341,6 @@ class TheoryModel : protected EnvObj std::string d_name; /** equality engine containing all known equalities/disequalities */ eq::EqualityEngine* d_equalityEngine; - /** approximations (see recordApproximation) */ - std::map d_approximations; - /** list of all approximations */ - std::vector > d_approx_list; /** a set of kinds that are unevaluated */ std::unordered_set d_unevaluated_kinds; /** a set of kinds that are semi-evaluated */ diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index fc1d5ee9e..367bf557a 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -1124,11 +1124,6 @@ void TheoryEngineModelBuilder::postProcessModel(bool incomplete, TheoryModel* m) void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm) { - if (tm->hasApproximations()) - { - // models with approximations may fail the assertions below - return; - } eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); std::map::iterator itMap; // Check that every term evaluates to its representative in the model diff --git a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 index 5348fb239..3a4a23dbb 100644 --- a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 +++ b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 @@ -1,5 +1,5 @@ ; SCRUBBER: sed -e 's/((x (_ real_algebraic_number .*/((x (_ real_algebraic_number/' -; COMMAND-LINE: --produce-models --model-witness-value --no-check-models +; COMMAND-LINE: --produce-models --no-check-models ; REQUIRES: poly ; EXPECT: sat ; EXPECT: ((x (_ real_algebraic_number -- 2.30.2