From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 1 Mar 2022 02:19:02 +0000 (-0800)
Subject: Remove unused data members from `TheoryArrays` (#8197)
X-Git-Tag: cvc5-1.0.0~357
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=94dfcfbb9ac7bb3223c4c950038aa9f6d02cccb8;p=cvc5.git

Remove unused data members from `TheoryArrays` (#8197)
---

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 5a0e8f597..d7f36cde1 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -107,7 +107,6 @@ TheoryArrays::TheoryArrays(Env& env,
       d_defValues(context()),
       d_readTableContext(new context::Context()),
       d_arrayMerges(context()),
-      d_inCheckModel(false),
       d_dstrat(new TheoryArraysDecisionStrategy(this)),
       d_dstratInit(false)
 {
@@ -412,11 +411,6 @@ bool TheoryArrays::propagateLit(TNode literal)
     return false;
   }
 
-  // Propagate away
-  if (d_inCheckModel && context()->getLevel() != d_topLevel)
-  {
-    return true;
-  }
   bool ok = d_out->propagate(literal);
   if (!ok) {
     d_state.notifyInConflict();
@@ -2122,12 +2116,6 @@ bool TheoryArrays::dischargeLemmas()
 
 void TheoryArrays::conflict(TNode a, TNode b) {
   Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
-  if (d_inCheckModel)
-  {
-    // if in check model, don't send the conflict
-    d_state.notifyInConflict();
-    return;
-  }
   d_im.conflictEqConstantMerge(a, b);
 }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 7c7058049..636d7e8f5 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -445,10 +445,6 @@ class TheoryArrays : public Theory {
   void queueRowLemma(RowLemmaType lem);
   bool dischargeLemmas();
 
-  std::vector<Node> d_decisions;
-  bool d_inCheckModel;
-  int d_topLevel;
-
   /**
    * The decision strategy for the theory of arrays, which calls the
    * getNextDecisionEngineRequest function below.