From 4d84681baf668906523d4a8f3543783d638fe1df Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 22 Feb 2022 11:46:44 -0600 Subject: [PATCH] Relax what is generated in the model from NL (#8113) This makes it so that we don't assign concrete values to equivalence classes with transcendental functions. It also removes some unused infrastructure. --- src/theory/arith/nl/cad_solver.cpp | 10 +---- src/theory/arith/nl/nl_model.cpp | 36 ---------------- src/theory/arith/nl/nl_model.h | 20 +-------- src/theory/arith/nl/nonlinear_extension.cpp | 17 +++----- src/theory/arith/nl/nonlinear_extension.h | 5 --- .../transcendental/transcendental_solver.cpp | 42 +++++++++++++++++++ .../nl/transcendental/transcendental_solver.h | 16 ++++++- src/theory/arith/theory_arith.cpp | 10 +++-- src/theory/arith/theory_arith.h | 2 + test/regress/regress0/arith/exp-in-model.smt2 | 5 +-- .../regress0/arith/issue7984-quant-trans.smt2 | 7 ++-- 11 files changed, 79 insertions(+), 91 deletions(-) diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 18071f3b2..57ea8c8ba 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -245,14 +245,8 @@ bool CadSolver::constructModelIfAvailable(std::vector& assertions) void CadSolver::addToModel(TNode var, TNode value) const { Trace("nl-cad") << "-> " << var << " = " << value << std::endl; - if (value.getType().isRealOrInt()) - { - d_model.addSubstitution(var, value); - } - else - { - d_model.addWitness(var, value); - } + Assert(value.getType().isRealOrInt()); + d_model.addSubstitution(var, value); } } // namespace nl diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index a28117d87..e236e3375 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -56,7 +56,6 @@ void NlModel::resetCheck() d_used_approx = false; d_check_model_solved.clear(); d_check_model_bounds.clear(); - d_check_model_witnesses.clear(); d_substitutions.clear(); } @@ -301,9 +300,6 @@ bool NlModel::addSubstitution(TNode v, TNode s) return false; } } - Assert(d_check_model_witnesses.find(v) == d_check_model_witnesses.end()) - << "We tried to add a substitution where we already had a witness term." - << std::endl; Subs tmp; tmp.add(v, s); for (auto& sub : d_substitutions.d_subs) @@ -351,23 +347,6 @@ bool NlModel::addBound(TNode v, TNode l, TNode u) return true; } -bool NlModel::addWitness(TNode v, TNode w) -{ - Trace("nl-ext-model") << "* check model witness : " << v << " -> " << w - << std::endl; - // should not set a witness for a value that is already set - if (d_substitutions.contains(v)) - { - Trace("nl-ext-model") << "...ERROR: setting witness for variable that " - "already has a constant value." - << std::endl; - Assert(false); - return false; - } - d_check_model_witnesses.emplace(v, w); - return true; -} - void NlModel::setUsedApproximate() { d_used_approx = true; } bool NlModel::usedApproximate() const { return d_used_approx; } @@ -886,11 +865,6 @@ bool NlModel::simpleCheckModelMsum(const std::map& msum, bool pol) } else { - Assert(d_check_model_witnesses.find(vc) - == d_check_model_witnesses.end()) - << "No variable should be assigned a witness term if we get " - "here. " - << vc << " is, though." << std::endl; Trace("nl-ext-cms-debug") << std::endl; Trace("nl-ext-cms") << " failed due to unknown bound for " << vc << std::endl; @@ -1044,7 +1018,6 @@ void NlModel::printModelValue(const char* c, Node n, unsigned prec) const void NlModel::getModelValueRepair( std::map& arithModel, std::map>& approximations, - std::map& witnesses, bool witnessToValue) { Trace("nl-model") << "NlModel::getModelValueRepair:" << std::endl; @@ -1089,11 +1062,6 @@ void NlModel::getModelValueRepair( Trace("nl-model") << v << " exact approximation is " << l << std::endl; } } - for (const auto& vw : d_check_model_witnesses) - { - Trace("nl-model") << vw.first << " witness is " << vw.second << std::endl; - witnesses.emplace(vw.first, vw.second); - } // Also record the exact values we used. An exact value can be seen as a // special kind approximation of the form (witness x. x = exact_value). // Notice that the above term gets rewritten such that the choice function @@ -1147,10 +1115,6 @@ bool NlModel::hasAssignment(Node v) const { return true; } - if (d_check_model_witnesses.find(v) != d_check_model_witnesses.end()) - { - return true; - } return (d_substitutions.contains(v)); } diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index e195aa9b2..27cb0f81d 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -133,13 +133,6 @@ class NlModel : protected EnvObj * bounds. */ bool addBound(TNode v, TNode l, TNode u); - /** - * Adds a model witness v -> w to the underlying theory model. - * The witness should only contain a single variable v and evaluate to true - * for exactly one value of v. The variable v is then (implicitly, - * declaratively) assigned to this single value that satisfies the witness w. - */ - bool addWitness(TNode v, TNode w); /** * Checks the current model based on solving for equalities, and using error * bounds on the Taylor approximation. @@ -182,14 +175,11 @@ class NlModel : protected EnvObj * 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; the mapping - * witnesses is filled with witness terms that are satisfied by a single - * value. + * v and w is a witness point that satisfies this predicate. */ void getModelValueRepair( std::map& arithModel, std::map>& approximations, - std::map& witnesses, bool witnessToValue); private: @@ -298,14 +288,6 @@ class NlModel : protected EnvObj * involves approximations of square roots. */ std::map> d_check_model_bounds; - /** - * witnesses for check model - * - * Stores witnesses for vatiables that define implicit variable assignments. - * For some variable v, we map to a formulas that is true for exactly one - * value of v. - */ - std::map d_check_model_witnesses; /** * The map from literals that our model construction solved, to the variable * that was solved for. Examples of such literals are: diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index b57c0d1db..bb360a542 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -49,7 +49,7 @@ NonlinearExtension::NonlinearExtension(Env& env, d_extTheoryCb(state.getEqualityEngine()), d_extTheory(env, d_extTheoryCb, d_im), d_model(env), - d_trSlv(d_env, d_im, d_model), + d_trSlv(d_env, d_astate, d_im, d_model), d_extState(d_im, d_model, d_env), d_factoringSlv(d_env, &d_extState), d_monomialBoundsSlv(d_env, &d_extState), @@ -277,11 +277,9 @@ void NonlinearExtension::checkFullEffort(std::map& arithModel, { Trace("nl-ext") << "interceptModel: do model repair" << std::endl; d_approximations.clear(); - d_witnesses.clear(); // modify the model values d_model.getModelValueRepair(arithModel, d_approximations, - d_witnesses, options().smt.modelWitnessValue); for (auto& am : arithModel) { @@ -292,6 +290,10 @@ void NonlinearExtension::checkFullEffort(std::map& arithModel, } } } + // must post-process model with transcendental solver, to ensure we don't + // assign values for equivalence classes with transcendental function + // applications + d_trSlv.postProcessModel(arithModel, termSet); } Node NonlinearExtension::getModelValue(TNode var) const @@ -304,10 +306,6 @@ Node NonlinearExtension::getModelValue(TNode var) const } return Node::null(); } - if (auto it = d_witnesses.find(var); it != d_witnesses.end()) - { - return it->second; - } return Node::null(); } @@ -326,11 +324,6 @@ bool NonlinearExtension::assertModel(TheoryModel* tm, TNode var) const } return true; } - if (auto it = d_witnesses.find(var); it != d_witnesses.end()) - { - tm->recordApproximation(var, it->second); - return true; - } return false; } diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 390dd72a3..dc7682f68 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -278,11 +278,6 @@ class NonlinearExtension : EnvObj * NlModel::getModelValueRepair. */ std::map> d_approximations; - /** - * The witnesses computed during collectModelInfo. For details, see - * NlModel::getModelValueRepair. - */ - std::map d_witnesses; }; /* class NonlinearExtension */ } // namespace nl diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 9f7e474bb..1448bdbd2 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -23,6 +23,7 @@ #include "expr/skolem_manager.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" +#include "theory/arith/arith_state.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" @@ -38,9 +39,11 @@ namespace nl { namespace transcendental { TranscendentalSolver::TranscendentalSolver(Env& env, + ArithState& state, InferenceManager& im, NlModel& m) : EnvObj(env), + d_astate(state), d_tstate(env, im, m), d_expSlv(env, &d_tstate), d_sineSlv(env, &d_tstate) @@ -443,6 +446,45 @@ int TranscendentalSolver::regionToConcavity(Kind k, int region) return 0; } +void TranscendentalSolver::postProcessModel(std::map& arithModel, + const std::set& termSet) +{ + Trace("nl-ext") << "TranscendentalSolver::postProcessModel" << std::endl; + std::unordered_set trReps; + for (const Node& n : termSet) + { + if (isTranscendentalKind(n.getKind())) + { + Node r = d_astate.getRepresentative(n); + trReps.insert(r); + } + } + if (trReps.empty()) + { + Trace("nl-ext") << "...no transcendental functions" << std::endl; + return; + } + std::vector rmFromModel; + for (auto& am : arithModel) + { + Node r = d_astate.getRepresentative(am.first); + if (trReps.find(r) != trReps.end()) + { + Trace("nl-ext") << "...erase value for " << am.first + << ", since approximate" << std::endl; + rmFromModel.push_back(am.first); + } + else + { + Trace("nl-ext") << "...keep model value for " << am.first << std::endl; + } + } + for (const Node& n : rmFromModel) + { + arithModel.erase(n); + } +} + } // namespace transcendental } // namespace nl } // namespace arith diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index c1a617b38..f8c7b8c9b 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -28,6 +28,7 @@ namespace cvc5 { namespace theory { namespace arith { +class ArithState; class InferenceManager; namespace nl { @@ -51,7 +52,10 @@ namespace transcendental { class TranscendentalSolver : protected EnvObj { public: - TranscendentalSolver(Env& env, InferenceManager& im, NlModel& m); + TranscendentalSolver(Env& env, + ArithState& state, + InferenceManager& im, + NlModel& m); ~TranscendentalSolver(); /** init last call @@ -148,6 +152,14 @@ class TranscendentalSolver : protected EnvObj */ void checkTranscendentalTangentPlanes(); + /** + * Post-process model. This ensures that the domain of arithModel does not + * contain terms that are equal to any transcendental function applications, + * as their values cannot be properly represented in the model. + */ + void postProcessModel(std::map& arithModel, + const std::set& termSet); + private: /** check transcendental function refinement for tf * @@ -178,6 +190,8 @@ class TranscendentalSolver : protected EnvObj */ int regionToConcavity(Kind k, int region); + /** A reference to the arithmetic state object */ + ArithState& d_astate; /** taylor degree * * Indicates that the degree of the polynomials in the Taylor approximation of diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 60f925e75..5218baf9b 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -49,7 +49,8 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation) d_nonlinearExtension(nullptr), d_opElim(d_env), d_arithPreproc(env, d_astate, d_im, d_pnm, d_opElim), - d_rewriter(d_opElim) + d_rewriter(d_opElim), + d_arithModelCacheSet(false) { // currently a cyclic dependency to TheoryArithPrivate d_astate.setParent(d_internal); @@ -193,6 +194,7 @@ void TheoryArith::postCheck(Effort level) if (Theory::fullEffort(level)) { d_arithModelCache.clear(); + d_arithModelCacheSet = false; std::set termSet; if (d_nonlinearExtension != nullptr) { @@ -370,16 +372,18 @@ eq::ProofEqEngine* TheoryArith::getProofEqEngine() void TheoryArith::updateModelCache(std::set& termSet) { - if (d_arithModelCache.empty()) + if (!d_arithModelCacheSet) { + d_arithModelCacheSet = true; collectAssertedTerms(termSet); d_internal->collectModelValues(termSet, d_arithModelCache); } } void TheoryArith::updateModelCache(const std::set& termSet) { - if (d_arithModelCache.empty()) + if (!d_arithModelCacheSet) { + d_arithModelCacheSet = true; d_internal->collectModelValues(termSet, d_arithModelCache); } } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 8f4819405..13f4f8ad7 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -180,6 +180,8 @@ class TheoryArith : public Theory { * used to augment the TheoryModel. */ std::map d_arithModelCache; + /** Is the above map computed? */ + bool d_arithModelCacheSet; };/* class TheoryArith */ diff --git a/test/regress/regress0/arith/exp-in-model.smt2 b/test/regress/regress0/arith/exp-in-model.smt2 index e6185da09..e63b24e26 100644 --- a/test/regress/regress0/arith/exp-in-model.smt2 +++ b/test/regress/regress0/arith/exp-in-model.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --check-model -; EXPECT: (error "Cannot run check-model on a model with approximate values.") -; EXIT: 1 +; COMMAND-LINE: -q +; EXPECT: sat (set-logic QF_UFNRAT) (set-option :produce-models true) (declare-fun b (Real) Real) diff --git a/test/regress/regress0/arith/issue7984-quant-trans.smt2 b/test/regress/regress0/arith/issue7984-quant-trans.smt2 index a6f31ac99..7252e11cf 100644 --- a/test/regress/regress0/arith/issue7984-quant-trans.smt2 +++ b/test/regress/regress0/arith/issue7984-quant-trans.smt2 @@ -1,8 +1,7 @@ -; COMMAND-LINE: --check-models -; EXPECT: (error "Cannot run check-model on a model with approximate values.") -; EXIT: 1 +; COMMAND-LINE: -q +; EXPECT: sat (set-logic QF_NRAT) (set-option :re-elim-agg true) (declare-fun r6 () Real) (assert (= 0.0 (cos r6))) -(check-sat) \ No newline at end of file +(check-sat) -- 2.30.2