summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/preprocessing/passes/miplib_trick.cpp1
-rw-r--r--src/preprocessing/passes/non_clausal_simp.cpp56
-rw-r--r--src/preprocessing/preprocessing_pass_context.cpp11
-rw-r--r--src/preprocessing/preprocessing_pass_context.h11
-rw-r--r--src/theory/arith/arith_ite_utils.cpp1
-rw-r--r--src/theory/combination_care_graph.cpp3
-rw-r--r--src/theory/combination_care_graph.h1
-rw-r--r--src/theory/combination_engine.cpp5
-rw-r--r--src/theory/combination_engine.h4
-rw-r--r--src/theory/model_manager.cpp14
-rw-r--r--src/theory/model_manager.h7
-rw-r--r--src/theory/model_manager_distributed.cpp7
-rw-r--r--src/theory/model_manager_distributed.h5
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/theory_model.cpp34
-rw-r--r--src/theory/theory_model.h25
-rw-r--r--test/regress/regress1/strings/issue5611-deq-norm-emp.smt24
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback