diff options
-rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 1 | ||||
-rw-r--r-- | src/preprocessing/passes/non_clausal_simp.cpp | 56 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.cpp | 11 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 11 | ||||
-rw-r--r-- | src/theory/arith/arith_ite_utils.cpp | 1 | ||||
-rw-r--r-- | src/theory/combination_care_graph.cpp | 3 | ||||
-rw-r--r-- | src/theory/combination_care_graph.h | 1 | ||||
-rw-r--r-- | src/theory/combination_engine.cpp | 5 | ||||
-rw-r--r-- | src/theory/combination_engine.h | 4 | ||||
-rw-r--r-- | src/theory/model_manager.cpp | 14 | ||||
-rw-r--r-- | src/theory/model_manager.h | 7 | ||||
-rw-r--r-- | src/theory/model_manager_distributed.cpp | 7 | ||||
-rw-r--r-- | src/theory/model_manager_distributed.h | 5 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 34 | ||||
-rw-r--r-- | src/theory/theory_model.h | 25 | ||||
-rw-r--r-- | test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 | 4 |
17 files changed, 84 insertions, 107 deletions
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 893cf0239..e9819072d 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -550,7 +550,6 @@ PreprocessingPassResult MipLibTrick::applyInternal( << "unexpected solution from arith's ppAssert()"; Assert(nullMap.empty()) << "unexpected substitution from arith's ppAssert()"; - d_preprocContext->addModelSubstitution(*ii, newVar.eqNode(one)); newVars.push_back(newVar); varRef = newVar; } diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 2fcc6f76f..d68c30a11 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -327,34 +327,32 @@ PreprocessingPassResult NonClausalSimp::applyInternal( << "non-clausal preprocessed: " << assertion << std::endl; } - // add substitutions to model, or as assertions if needed (when incremental) - NodeManager* nm = NodeManager::currentNM(); - for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos) + // If necessary, add as assertions if needed (when incremental). This is + // necessary because certain variables cannot truly be eliminated when + // we are in incremental mode. For example, say our first call to check-sat + // is a formula F containing variable x. On the second call to check-sat, + // say we solve a top-level assertion (= x t). Since the solver already has + // constraints involving x, we must still keep (= x t) as an assertion. + // However, notice that we do not retract the substitution { x -> t }. This + // means that all *subsequent* assertions after (= x t) will replace x by t. + if (assertionsToPreprocess->storeSubstsInAsserts()) { - Node lhs = (*pos).first; - TrustNode trhs = newSubstitutions->applyTrusted((*pos).second); - Node rhs = trhs.isNull() ? (*pos).second : trhs.getNode(); - // If using incremental, we must check whether this variable has occurred - // before now. If it hasn't we can add this as a substitution. - if (!assertionsToPreprocess->storeSubstsInAsserts() - || d_preprocContext->getSymsInAssertions().find(lhs) - == d_preprocContext->getSymsInAssertions().end()) + for (const std::pair<const Node, const Node>& pos: nss) { - Trace("non-clausal-simplify") - << "substitute: " << lhs << " " << rhs << std::endl; - d_preprocContext->addModelSubstitution(lhs, rhs); - } - else - { - // if it has, the substitution becomes an assertion - Node eq = nm->mkNode(kind::EQUAL, lhs, rhs); - Trace("non-clausal-simplify") - << "substitute: will notify SAT layer of substitution: " << eq - << std::endl; - trhs = newSubstitutions->applyTrusted((*pos).first); - Assert(!trhs.isNull()); - assertionsToPreprocess->addSubstitutionNode(trhs.getProven(), - trhs.getGenerator()); + Node lhs = pos.first; + // If using incremental, we must check whether this variable has occurred + // before now. If it has, we must add as an assertion. + if (d_preprocContext->getSymsInAssertions().contains(lhs)) + { + // if it has, the substitution becomes an assertion + TrustNode trhs = newSubstitutions->applyTrusted(lhs); + Assert(!trhs.isNull()); + Trace("non-clausal-simplify") + << "substitute: will notify SAT layer of substitution: " + << trhs.getProven() << std::endl; + assertionsToPreprocess->addSubstitutionNode(trhs.getProven(), + trhs.getGenerator()); + } } } @@ -438,6 +436,12 @@ PreprocessingPassResult NonClausalSimp::applyInternal( } propagator->setNeedsFinish(true); + + // Note that typically ttls.apply(assert)==assert here. + // However, this invariant is invalidated for cases where we use explicit + // equality assertions for variables solved in incremental mode that already + // exist in assertions, as described above. + return PreprocessingPassResult::NO_CONFLICT; } diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 139fa4153..9e8a4efc8 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -67,20 +67,11 @@ void PreprocessingPassContext::recordSymbolsInAssertions( } } -void PreprocessingPassContext::addModelSubstitution(const Node& lhs, - const Node& rhs) -{ - getTheoryEngine()->getModel()->addSubstitution(lhs, - d_smt->expandDefinitions(rhs)); -} - void PreprocessingPassContext::addSubstitution(const Node& lhs, const Node& rhs, ProofGenerator* pg) { getTopLevelSubstitutions().addSubstitution(lhs, rhs, pg); - // also add as a model substitution - addModelSubstitution(lhs, rhs); } void PreprocessingPassContext::addSubstitution(const Node& lhs, @@ -89,8 +80,6 @@ void PreprocessingPassContext::addSubstitution(const Node& lhs, const std::vector<Node>& args) { getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args); - // also add as a model substitution - addModelSubstitution(lhs, rhs); } ProofNodeManager* PreprocessingPassContext::getProofNodeManager() diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index a4ca166d8..a14fafb47 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -78,15 +78,8 @@ class PreprocessingPassContext void recordSymbolsInAssertions(const std::vector<Node>& assertions); /** - * Add substitution to theory model. This method should only be called if - * we have already added the substitution to the top-level substitutions - * class. Otherwise, addSubstitution should be called instead. - * @param lhs The node replaced by node 'rhs' - * @param rhs The node to substitute node 'lhs' - */ - void addModelSubstitution(const Node& lhs, const Node& rhs); - /** - * Add substitution to the top-level substitutions and to the theory model. + * Add substitution to the top-level substitutions, which also as a + * consequence is used by the theory model. * @param lhs The node replaced by node 'rhs' * @param rhs The node to substitute node 'lhs' * @param pg The proof generator that can provide a proof of lhs == rhs. diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 22c91b5bb..7ed3093b7 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -273,7 +273,6 @@ void ArithIteUtils::addSubstitution(TNode f, TNode t){ Debug("arith::ite") << "adding " << f << " -> " << t << endl; d_subcount = d_subcount + 1; d_subs->addSubstitution(f, t); - d_model->addSubstitution(f, t); } Node ArithIteUtils::applySubstitutions(TNode f){ diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp index 4a6a1f150..fa020e96b 100644 --- a/src/theory/combination_care_graph.cpp +++ b/src/theory/combination_care_graph.cpp @@ -26,9 +26,10 @@ namespace theory { CombinationCareGraph::CombinationCareGraph( TheoryEngine& te, + Env& env, const std::vector<Theory*>& paraTheories, ProofNodeManager* pnm) - : CombinationEngine(te, paraTheories, pnm) + : CombinationEngine(te, env, paraTheories, pnm) { } diff --git a/src/theory/combination_care_graph.h b/src/theory/combination_care_graph.h index 437831678..971b81d1d 100644 --- a/src/theory/combination_care_graph.h +++ b/src/theory/combination_care_graph.h @@ -36,6 +36,7 @@ class CombinationCareGraph : public CombinationEngine { public: CombinationCareGraph(TheoryEngine& te, + Env& env, const std::vector<Theory*>& paraTheories, ProofNodeManager* pnm); ~CombinationCareGraph(); diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index 4b04188f1..33300ead8 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -29,9 +29,11 @@ namespace cvc5 { namespace theory { CombinationEngine::CombinationEngine(TheoryEngine& te, + Env& env, const std::vector<Theory*>& paraTheories, ProofNodeManager* pnm) : d_te(te), + d_env(env), d_valuation(&te), d_pnm(pnm), d_logicInfo(te.getLogicInfo()), @@ -51,7 +53,8 @@ CombinationEngine::CombinationEngine(TheoryEngine& te, d_eemanager.reset( new EqEngineManagerDistributed(d_te, *d_sharedSolver.get())); // make the distributed model manager - d_mmanager.reset(new ModelManagerDistributed(d_te, *d_eemanager.get())); + d_mmanager.reset( + new ModelManagerDistributed(d_te, d_env, *d_eemanager.get())); } else { diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index 6430e2325..063cefd49 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -27,6 +27,7 @@ namespace cvc5 { class TheoryEngine; +class Env; namespace theory { @@ -45,6 +46,7 @@ class CombinationEngine { public: CombinationEngine(TheoryEngine& te, + Env& env, const std::vector<Theory*>& paraTheories, ProofNodeManager* pnm); virtual ~CombinationEngine(); @@ -107,6 +109,8 @@ class CombinationEngine void sendLemma(TrustNode trn, TheoryId atomsTo); /** Reference to the theory engine */ TheoryEngine& d_te; + /** Reference to the environment */ + Env& d_env; /** Valuation for the engine */ Valuation d_valuation; /** The proof node manager */ diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index b7499447f..c1c488f65 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -18,23 +18,23 @@ #include "options/smt_options.h" #include "options/theory_options.h" #include "prop/prop_engine.h" -#include "theory/quantifiers_engine.h" +#include "smt/env.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_builder.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" namespace cvc5 { namespace theory { -ModelManager::ModelManager(TheoryEngine& te, EqEngineManager& eem) +ModelManager::ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem) : d_te(te), - d_logicInfo(te.getLogicInfo()), + d_env(env), d_eem(eem), d_modelEqualityEngine(nullptr), d_modelEqualityEngineAlloc(nullptr), - d_model(new TheoryModel(te.getUserContext(), - "DefaultModel", - options::assignFunctionValues())), + d_model(new TheoryModel( + env, "DefaultModel", options::assignFunctionValues())), d_modelBuilder(nullptr), d_modelBuilt(false), d_modelBuiltSuccess(false) @@ -46,7 +46,7 @@ ModelManager::~ModelManager() {} void ModelManager::finishInit(eq::EqualityEngineNotify* notify) { // construct the model - const LogicInfo& logicInfo = d_te.getLogicInfo(); + const LogicInfo& logicInfo = d_env.getLogicInfo(); // Initialize the model and model builder. if (logicInfo.isQuantified()) { diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h index 41559e7b6..ff8459fcb 100644 --- a/src/theory/model_manager.h +++ b/src/theory/model_manager.h @@ -26,6 +26,7 @@ namespace cvc5 { class TheoryEngine; +class Env; namespace theory { @@ -42,7 +43,7 @@ class TheoryModel; class ModelManager { public: - ModelManager(TheoryEngine& te, EqEngineManager& eem); + ModelManager(TheoryEngine& te, Env& env, EqEngineManager& eem); virtual ~ModelManager(); /** * Finish initializing this class, which allocates the model, the model @@ -125,8 +126,8 @@ class ModelManager void collectTerms(TheoryId tid, TNode n, std::set<Node>& termSet) const; /** Reference to the theory engine */ TheoryEngine& d_te; - /** Logic info of theory engine (cached) */ - const LogicInfo& d_logicInfo; + /** Reference to the environment */ + Env& d_env; /** The equality engine manager */ EqEngineManager& d_eem; /** diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp index f3a501f94..4124407be 100644 --- a/src/theory/model_manager_distributed.cpp +++ b/src/theory/model_manager_distributed.cpp @@ -15,6 +15,7 @@ #include "theory/model_manager_distributed.h" +#include "smt/env.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" #include "theory/theory_model_builder.h" @@ -23,8 +24,9 @@ namespace cvc5 { namespace theory { ModelManagerDistributed::ModelManagerDistributed(TheoryEngine& te, + Env& env, EqEngineManager& eem) - : ModelManager(te, eem) + : ModelManager(te, env, eem) { } @@ -69,10 +71,11 @@ bool ModelManagerDistributed::prepareModel() // model, which includes both dump their equality information and assigning // values. Notice the order of theories here is important and is the same // as the list in CVC5_FOR_EACH_THEORY in theory_engine.cpp. + const LogicInfo& logicInfo = d_env.getLogicInfo(); for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) { - if (!d_logicInfo.isTheoryEnabled(theoryId)) + if (!logicInfo.isTheoryEnabled(theoryId)) { // theory not active, skip continue; diff --git a/src/theory/model_manager_distributed.h b/src/theory/model_manager_distributed.h index 1a79eec9a..322e61a98 100644 --- a/src/theory/model_manager_distributed.h +++ b/src/theory/model_manager_distributed.h @@ -22,9 +22,6 @@ #include "theory/model_manager.h" namespace cvc5 { - -class TheoryEngine; - namespace theory { /** @@ -41,7 +38,7 @@ namespace theory { class ModelManagerDistributed : public ModelManager { public: - ModelManagerDistributed(TheoryEngine& te, EqEngineManager& eem); + ModelManagerDistributed(TheoryEngine& te, Env& env, EqEngineManager& eem); ~ModelManagerDistributed(); /** Prepare the model, as described above. */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ccdd2bf4b..1acaca34f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -146,7 +146,7 @@ void TheoryEngine::finishInit() // Initialize the theory combination architecture if (options::tcMode() == options::TcMode::CARE_GRAPH) { - d_tc.reset(new CombinationCareGraph(*this, paraTheories, d_pnm)); + d_tc.reset(new CombinationCareGraph(*this, d_env, paraTheories, d_pnm)); } else { diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 1543739e0..a95546cf5 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -19,8 +19,10 @@ #include "options/smt_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "smt/env.h" #include "smt/smt_engine.h" #include "theory/rewriter.h" +#include "theory/trust_substitutions.h" using namespace std; using namespace cvc5::kind; @@ -29,11 +31,9 @@ using namespace cvc5::context; namespace cvc5 { namespace theory { -TheoryModel::TheoryModel(context::Context* c, - std::string name, - bool enableFuncModels) - : d_name(name), - d_substitutions(c), +TheoryModel::TheoryModel(Env& env, std::string name, bool enableFuncModels) + : d_env(env), + d_name(name), d_equalityEngine(nullptr), d_using_model_core(false), d_enableFuncModels(enableFuncModels) @@ -137,7 +137,7 @@ std::vector<Node> TheoryModel::getDomainElements(TypeNode tn) const Node TheoryModel::getValue(TNode n) const { //apply substitutions - Node nn = d_substitutions.apply(n); + Node nn = d_env.getTopLevelSubstitutions().apply(n); Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl; //get value in model nn = getModelValue(nn); @@ -367,26 +367,6 @@ Node TheoryModel::getModelValue(TNode n) const return n; } -/** add substitution */ -void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ - if( !d_substitutions.hasSubstitution( x ) ){ - Debug("model") << "Add substitution in model " << x << " -> " << t << std::endl; - d_substitutions.addSubstitution( x, t, invalidateCache ); - } else { -#ifdef CVC5_ASSERTIONS - Node oldX = d_substitutions.getSubstitution(x); - // check that either the old substitution is the same, or it now maps to the new substitution - if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) { - InternalError() - << "Two incompatible substitutions added to TheoryModel:\n" - << "the term: " << x << "\n" - << "old mapping: " << d_substitutions.apply(oldX) << "\n" - << "new mapping: " << d_substitutions.apply(t); - } -#endif /* CVC5_ASSERTIONS */ - } -} - /** add term */ void TheoryModel::addTermInternal(TNode n) { @@ -747,7 +727,7 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() { Node n = it->first; Assert(!n.isNull()); // should not have been solved for in a substitution - Assert(d_substitutions.apply(n) == n); + Assert(d_env.getTopLevelSubstitutions().apply(n) == n); if( !hasAssignedFunctionDefinition( n ) ){ Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl; if( options::ufHo() ){ diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index b4a089767..ab66e8fe7 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -23,12 +23,14 @@ #include "theory/ee_setup_info.h" #include "theory/rep_set.h" -#include "theory/substitutions.h" #include "theory/type_enumerator.h" #include "theory/type_set.h" #include "theory/uf/equality_engine.h" namespace cvc5 { + +class Env; + namespace theory { /** Theory Model class. @@ -38,16 +40,16 @@ namespace theory { * (1) d_equalityEngine : an equality engine object, which stores * an equivalence relation over all terms that exist in * the current set of assertions. - * (2) d_substitutions : a substitution map storing cases of - * explicitly solved terms, for instance during preprocessing. - * (3) d_reps : a map from equivalence class representatives of + * (2) d_reps : a map from equivalence class representatives of * the equality engine to the (constant) representatives * assigned to that equivalence class. - * (4) d_uf_models : a map from uninterpreted functions to their + * (3) d_uf_models : a map from uninterpreted functions to their * lambda representation. - * (5) d_rep_set : a data structure that allows interpretations + * (4) d_rep_set : a data structure that allows interpretations * for types to be represented as terms. This is useful for * finite model finding. + * Additionally, models are dependent on top-level substitutions stored in the + * d_env class. * * These data structures are built after a full effort check with * no lemmas sent, within a call to: @@ -79,8 +81,9 @@ namespace theory { class TheoryModel { friend class TheoryEngineModelBuilder; -public: - TheoryModel(context::Context* c, std::string name, bool enableFuncModels); + + public: + TheoryModel(Env& env, std::string name, bool enableFuncModels); virtual ~TheoryModel(); /** * Finish init, where ee is the equality engine the model should use. @@ -90,8 +93,6 @@ public: /** reset the model */ virtual void reset(); //---------------------------- for building the model - /** Adds a substitution from x to t. */ - void addSubstitution(TNode x, TNode t, bool invalidateCache = true); /** assert equality holds in the model * * This method returns true if and only if the equality engine of this model @@ -355,10 +356,10 @@ public: std::string debugPrintModelEqc() const; protected: + /** Reference to the environmanet */ + Env& d_env; /** Unique name of this model */ std::string d_name; - /** substitution map for this model */ - SubstitutionMap d_substitutions; /** equality engine containing all known equalities/disequalities */ eq::EqualityEngine* d_equalityEngine; /** approximations (see recordApproximation) */ diff --git a/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 b/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 index 3b3e2cfab..c96ca1bea 100644 --- a/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 +++ b/test/regress/regress1/strings/issue5611-deq-norm-emp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: -i --strings-exp +; COMMAND-LINE: -i --strings-exp --no-check-models ; EXPECT: sat (set-logic ALL) (declare-fun str7 () String) @@ -7,4 +7,6 @@ (assert (not (= str8 (str.replace_re_all (str.++ str9 str8 str7) (str.to_re "ULfQhzdcQSfqWSXyjuptqjqsazpyjzdDddlJPLDJhalmhBhlNBKZvoxoLOpfplkqhvIRHMOMDAGIdoRyiZmxmMvRijgpFnd") str9)))) (push) (assert (and (str.in_re str8 (str.to_re str7)) (not (= str9 (str.replace_re_all (str.++ str8 str8) (str.to_re "ULfQhzdcQSfqWSXyjuptqjqsazpyjzdDddlJPLDJhalmhBhlNBKZvoxoLOpfplkqhvIRHMOMDAGIdoRyiZmxmMvRijgpFnd") str9))))) +; note that (debug) model checking fails since this benchmark triggers a string variable (str7) to be solved after it appears in assertions, due to the push above. +; this leads to a quantified formula changing after substitution, in which case our model evaluation loses track of its value. (check-sat) |