Remove spurious theory methods calls (#4931)

This PR removes spurious theory method calls that are not implemented.

It also renames a common "propagate(TNode lit)" pattern to "propagateLit(TNode lit)" to avoid confusion with "propagate(Effort e)".

3 files changed, 13 insertions, 17 deletions

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 659f05ae8..629064d99 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -8,7 +8,7 @@ theory THEORY_ARRAYS ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_
 typechecker "theory/arrays/theory_arrays_type_rules.h"
 
 properties polite stable-infinite parametric
-properties check propagate presolve
+properties check presolve
 
 rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h"
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9c1e22940..d659aff11 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -414,14 +414,17 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs
 // T-PROPAGATION / REGISTRATION
 /////////////////////////////////////////////////////////////////////////////
 
-
-bool TheoryArrays::propagate(TNode literal)
+bool TheoryArrays::propagateLit(TNode literal)
 {
-  Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal  << ")" << std::endl;
+  Debug("arrays") << spaces(getSatContext()->getLevel())
+                  << "TheoryArrays::propagateLit(" << literal << ")"
+                  << std::endl;
 
   // If already in conflict, no more propagation
   if (d_conflict) {
-    Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl;
+    Debug("arrays") << spaces(getSatContext()->getLevel())
+                    << "TheoryArrays::propagateLit(" << literal
+                    << "): already in conflict" << std::endl;
     return false;
   }
 
@@ -861,12 +864,6 @@ void TheoryArrays::preRegisterTerm(TNode node)
   }
 }
 
-
-void TheoryArrays::propagate(Effort e)
-{
-  // direct propagation now
-}
-
 TrustNode TheoryArrays::explain(TNode literal)
 {
   Node explanation = explain(literal, NULL);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 2d09c55fe..24ebb4916 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -213,7 +213,7 @@ class TheoryArrays : public Theory {
   context::CDO<unsigned> d_literalsToPropagateIndex;
 
   /** Should be called to propagate the literal.  */
-  bool propagate(TNode literal);
+  bool propagateLit(TNode literal);
 
   /** Explain why this literal is true by adding assumptions */
   void explain(TNode literal, std::vector<TNode>& assumptions,
@@ -227,7 +227,6 @@ class TheoryArrays : public Theory {
 
  public:
   void preRegisterTerm(TNode n) override;
-  void propagate(Effort e) override;
   Node explain(TNode n, eq::EqProof* proof);
   TrustNode explain(TNode n) override;
 
@@ -306,9 +305,9 @@ class TheoryArrays : public Theory {
           << (value ? "true" : "false") << ")" << std::endl;
       // Just forward to arrays
       if (value) {
-        return d_arrays.propagate(predicate);
+        return d_arrays.propagateLit(predicate);
       }
-      return d_arrays.propagate(predicate.notNode());
+      return d_arrays.propagateLit(predicate.notNode());
     }
 
     bool eqNotifyTriggerTermEquality(TheoryId tag,
@@ -324,14 +323,14 @@ class TheoryArrays : public Theory {
           }
         }
         // Propagate equality between shared terms
-        return d_arrays.propagate(t1.eqNode(t2));
+        return d_arrays.propagateLit(t1.eqNode(t2));
       } else {
         if (t1.getType().isArray()) {
           if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
             return true;
           }
         }
-        return d_arrays.propagate(t1.eqNode(t2).notNode());
+        return d_arrays.propagateLit(t1.eqNode(t2).notNode());
       }
       return true;
     }