From 7eff8fb5145752b100a9d04c834973e794d9a860 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 1 Jun 2021 13:58:49 -0500
Subject: [PATCH] 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.
---
 src/preprocessing/passes/ite_simp.cpp |  2 +-
 src/theory/arith/arith_ite_utils.cpp  | 12 ++++--------
 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)))
-- 
2.30.2