diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-01 13:58:49 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-01 13:58:49 -0500 |
commit | 7eff8fb5145752b100a9d04c834973e794d9a860 (patch) | |
tree | e12f2704467c6d6629eecb6d56c29e8933e5b908 /src | |
parent | 320c48b1c82feb7a5d55af39d0cdbb7a1c2c6ff2 (diff) |
Use top-level substitutions in ITE simp (#6651)
With this PR, we use the central top-level substitutions instance in the ITE simplification preprocessing pass. Previously the ITE simplification pass maintained its own copy of the substitutions.
Since the top-level substitutions now are the authority on models, this led to model failures after this change: ac8cf53#diff-30677c5a1752b1d0e83ef25fd2cfb8949576ea42cf7821fe0ac00ebbd0122f8aL276.
This PR corrects the issue.
This is required for SMT-COMP.
Diffstat (limited to 'src')
-rw-r--r-- | src/preprocessing/passes/ite_simp.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/arith_ite_utils.cpp | 12 | ||||
-rw-r--r-- | src/theory/arith/arith_ite_utils.h | 6 |
3 files changed, 7 insertions, 13 deletions
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index e0a57ae5b..5bfb2a79f 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -154,7 +154,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) *(d_iteUtilities.getContainsVisitor()); arith::ArithIteUtils aiteu(contains, d_preprocContext->getUserContext(), - theory_engine->getModel()); + d_preprocContext->getTopLevelSubstitutions().get()); bool anyItes = false; for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 7ed3093b7..99b95719f 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -145,22 +145,18 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){ ArithIteUtils::ArithIteUtils( preprocessing::util::ContainsTermITEVisitor& contains, context::Context* uc, - TheoryModel* model) + SubstitutionMap& subs) : d_contains(contains), - d_subs(NULL), - d_model(model), + d_subs(subs), d_one(1), d_subcount(uc, 0), d_skolems(uc), d_implies(), d_orBinEqs() { - d_subs = new SubstitutionMap(uc); } ArithIteUtils::~ArithIteUtils(){ - delete d_subs; - d_subs = NULL; } void ArithIteUtils::clear(){ @@ -272,12 +268,12 @@ unsigned ArithIteUtils::getSubCount() const{ 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_subs.addSubstitution(f, t); } Node ArithIteUtils::applySubstitutions(TNode f){ AlwaysAssert(!options::incrementalSolving()); - return d_subs->apply(f); + return d_subs.apply(f); } Node ArithIteUtils::selectForCmp(Node n) const{ diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index cd1014e38..ba7a23479 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -40,14 +40,12 @@ class ContainsTermITEVisitor; namespace theory { class SubstitutionMap; -class TheoryModel; namespace arith { class ArithIteUtils { preprocessing::util::ContainsTermITEVisitor& d_contains; - SubstitutionMap* d_subs; - TheoryModel* d_model; + SubstitutionMap& d_subs; typedef std::unordered_map<Node, Node> NodeMap; // cache for reduce vars @@ -76,7 +74,7 @@ class ArithIteUtils { public: ArithIteUtils(preprocessing::util::ContainsTermITEVisitor& contains, context::Context* userContext, - TheoryModel* model); + SubstitutionMap& subs); ~ArithIteUtils(); //(ite ?v_2 ?v_1 (ite ?v_3 (- ?v_1 128) (- ?v_1 256))) |