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)".

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 659f05ae8d33e0c85e9ef2c632ea70f1eb64fe7e..629064d9910149a25e004a778eb703d88af2cde1 100644 (file)
--- 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 9c1e22940f1b3dfa2b06b8f9ef95f08ffb98211c..d659aff11b1e3ef8902f064e640edc0616430b02 100644 (file)
--- 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 2d09c55fe4fdd36ebf42192aa45ebc1ee26dc415..24ebb4916223c5dd24d3ca39916bf2fb168a07b6 100644 (file)
--- 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;
     }

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 4b80529d2068938e71139ab43a47956c871cf98b..26bff20b7515851afb9d97261359cb0f7beb5bab 100644 (file)
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -7,7 +7,7 @@
 theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h"
 typechecker "theory/datatypes/theory_datatypes_type_rules.h"
 
-properties check presolve parametric propagate
+properties check parametric
 
 rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatypes_rewriter.h"
 

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 08ec4322e3cd725a3ecf361fa9630fce13a66d1d..65264bb3f7458c086b4498328007ba64a72dcd0d 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -701,11 +701,6 @@ TrustNode TheoryDatatypes::expandDefinition(Node n)
   return TrustNode::null();
 }
 
-void TheoryDatatypes::presolve()
-{
-  Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
-}
-
 TrustNode TheoryDatatypes::ppRewrite(TNode in)
 {
   Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
@@ -739,17 +734,14 @@ void TheoryDatatypes::addSharedTerm(TNode t) {
   Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
 }
 
-/** propagate */
-void TheoryDatatypes::propagate(Effort effort){
-
-}
-
-/** propagate */
-bool TheoryDatatypes::propagate(TNode literal){
-  Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal  << ")" << std::endl;
+bool TheoryDatatypes::propagateLit(TNode literal)
+{
+  Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal << ")"
+                         << std::endl;
   // If already in conflict, no more propagation
   if (d_conflict) {
-    Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal << "): already in conflict" << std::endl;
+    Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal
+                           << "): already in conflict" << std::endl;
     return false;
   }
   Trace("dt-prop") << "dtPropagate " << literal << std::endl;

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 0465a7788c1aa4c99b7b9d7bcfb3dd7cd6ff2507..137aae4695e6d936749d165f507dda48bcc32a9b 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -62,9 +62,9 @@ class TheoryDatatypes : public Theory {
     {
       Debug("dt") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
-        return d_dt.propagate(predicate);
+        return d_dt.propagateLit(predicate);
       }
-      return d_dt.propagate(predicate.notNode());
+      return d_dt.propagateLit(predicate.notNode());
     }
     bool eqNotifyTriggerTermEquality(TheoryId tag,
                                      TNode t1,
@@ -73,10 +73,9 @@ class TheoryDatatypes : public Theory {
     {
       Debug("dt") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
-        return d_dt.propagate(t1.eqNode(t2));
-      } else {
-        return d_dt.propagate(t1.eqNode(t2).notNode());
+        return d_dt.propagateLit(t1.eqNode(t2));
       }
+      return d_dt.propagateLit(t1.eqNode(t2).notNode());
     }
     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
     {
@@ -270,9 +269,7 @@ private:
   //--------------------------------- end initialization
 
   /** propagate */
-  void propagate(Effort effort) override;
-  /** propagate */
-  bool propagate(TNode literal);
+  bool propagateLit(TNode literal);
   /** explain */
   void addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions );
   void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions );
@@ -293,7 +290,6 @@ private:
   void preRegisterTerm(TNode n) override;
   TrustNode expandDefinition(Node n) override;
   TrustNode ppRewrite(TNode n) override;
-  void presolve() override;
   void addSharedTerm(TNode t) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   bool collectModelInfo(TheoryModel* m) override;

diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds
index 235b6117291fc13e0218acac8d63ed0ea9370080..7a3fb00a42ac4fa7e3e6397403667e5c10713c8d 100644 (file)
--- a/src/theory/sep/kinds
+++ b/src/theory/sep/kinds
@@ -8,7 +8,7 @@ theory THEORY_SEP ::CVC4::theory::sep::TheorySep "theory/sep/theory_sep.h"
 typechecker "theory/sep/theory_sep_type_rules.h"
 
 properties polite stable-infinite parametric
-properties check propagate presolve
+properties check presolve
 
 rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h"
 

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index f75eb44726e196e59a710902c4d4c2d9074af734..cf3cf2f9aaeb14b56ac0fdc727e2083ab06dd0c5 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -111,13 +111,13 @@ Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstit
 // T-PROPAGATION / REGISTRATION
 /////////////////////////////////////////////////////////////////////////////
 
-
-bool TheorySep::propagate(TNode literal)
+bool TheorySep::propagateLit(TNode literal)
 {
-  Debug("sep") << "TheorySep::propagate(" << literal  << ")" << std::endl;
+  Debug("sep") << "TheorySep::propagateLit(" << literal << ")" << std::endl;
   // If already in conflict, no more propagation
   if (d_conflict) {
-    Debug("sep") << "TheorySep::propagate(" << literal << "): already in conflict" << std::endl;
+    Debug("sep") << "TheorySep::propagateLit(" << literal
+                 << "): already in conflict" << std::endl;
     return false;
   }
   bool ok = d_out->propagate(literal);
@@ -146,11 +146,6 @@ void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
   }
 }
 
-
-void TheorySep::propagate(Effort e){
-
-}
-
 TrustNode TheorySep::explain(TNode literal)
 {
   Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl;

diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index b178b97db39a8af437ceae194d34eece1d4dcd78..bbb37a3a28751c3c087ae8243bc333db7447311b 100644 (file)
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -105,13 +105,12 @@ class TheorySep : public Theory {
 
  private:
   /** 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);
 
  public:
-  void propagate(Effort e) override;
   TrustNode explain(TNode n) override;
 
  public:
@@ -163,9 +162,9 @@ class TheorySep : public Theory {
       // Just forward to sep
       if (value)
       {
-        return d_sep.propagate(predicate);
+        return d_sep.propagateLit(predicate);
       }
-      return d_sep.propagate(predicate.notNode());
+      return d_sep.propagateLit(predicate.notNode());
     }
     bool eqNotifyTriggerTermEquality(TheoryId tag,
                                      TNode t1,
@@ -178,13 +177,9 @@ class TheorySep : public Theory {
       if (value)
       {
         // Propagate equality between shared terms
-        return d_sep.propagate(t1.eqNode(t2));
+        return d_sep.propagateLit(t1.eqNode(t2));
       }
-      else
-      {
-        return d_sep.propagate(t1.eqNode(t2).notNode());
-      }
-      return true;
+      return d_sep.propagateLit(t1.eqNode(t2).notNode());
     }
 
     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 452acfea060f817090b378e054d38df54c92476e..d3c42ef276525d1b127d59c108fa71b4586e5c90 100644 (file)
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -12,7 +12,7 @@ rewriter ::CVC4::theory::sets::TheorySetsRewriter \
     "theory/sets/theory_sets_rewriter.h"
 
 properties parametric
-properties check propagate presolve
+properties check presolve
 
 # constants
 constant EMPTYSET \

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 2627f72e33d6076d597efaa14bcdecdff8f132fa..647a7bb47cff1b91765dcaa1d34a3fac20239e48 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -196,10 +196,6 @@ void TheorySets::presolve() {
   d_internal->presolve();
 }
 
-void TheorySets::propagate(Effort e) {
-  d_internal->propagate(e);
-}
-
 bool TheorySets::isEntailed( Node n, bool pol ) {
   return d_internal->isEntailed( n, pol );
 }

diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 36e6ac65d97cd8c632d85ec777a6302a97403114..9e04b89a7f9a1b5e77b13c838b52704ac2f68ab4 100644 (file)
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -70,7 +70,6 @@ class TheorySets : public Theory
   TrustNode expandDefinition(Node n) override;
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
   void presolve() override;
-  void propagate(Effort) override;
   bool isEntailed(Node n, bool pol);
  private:
   /** Functions to handle callbacks from equality engine */

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f7c7ae7f933572a0a6a78a59bac4737630b20aab..3c94146060f1e41a44283b7e5a2c8dc99f2e2d34 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1392,8 +1392,6 @@ Node mkAnd(const std::vector<TNode>& conjunctions)
   return conjunction;
 } /* mkAnd() */
 
-void TheorySetsPrivate::propagate(Theory::Effort effort) {}
-
 bool TheorySetsPrivate::propagate(TNode literal)
 {
   Debug("sets-prop") << " propagate(" << literal << ")" << std::endl;

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 9a786598cee71f55571bc104ebd218f299271793..af780eadce729eec517c691edd72393c2e247af9 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -219,8 +219,6 @@ class TheorySetsPrivate {
 
   void presolve();
 
-  void propagate(Theory::Effort);
-
   /** get default output channel */
   OutputChannel* getOutputChannel();
   /** get the valuation */

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 131a48ae9b669640ff53261df3afddb8f1600666..78c6ab1f1d9ad15234eea5da4be0458de5ee3305 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -6,7 +6,7 @@
 
 theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
 
-properties check parametric propagate presolve
+properties check parametric presolve
 
 rewriter ::CVC4::theory::strings::SequencesRewriter "theory/strings/sequences_rewriter.h"
 

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6d81c742a1b3de5ef21aaaddad448529cdac2610..e427963540c3372a9344bb8d6358a06b90e4b55a 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -181,16 +181,15 @@ EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) {
   return EQUALITY_UNKNOWN;
 }
 
-void TheoryStrings::propagate(Effort e) {
-  // direct propagation now
-}
-
-bool TheoryStrings::propagate(TNode literal) {
-  Debug("strings-propagate") << "TheoryStrings::propagate(" << literal  << ")" << std::endl;
+bool TheoryStrings::propagateLit(TNode literal)
+{
+  Debug("strings-propagate")
+      << "TheoryStrings::propagateLit(" << literal << ")" << std::endl;
   // If already in conflict, no more propagation
   if (d_state.isInConflict())
   {
-    Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << "): already in conflict" << std::endl;
+    Debug("strings-propagate") << "TheoryStrings::propagateLit(" << literal
+                               << "): already in conflict" << std::endl;
     return false;
   }
   // Propagate out

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index da48ece90396c4bc4488c3fc72f7da9007937a48..8a1afe6b36882f1385019b55417fb8d936772631 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -84,8 +84,6 @@ class TheoryStrings : public Theory {
   //--------------------------------- end initialization
   /** Identify this theory */
   std::string identify() const override;
-  /** Propagate */
-  void propagate(Effort e) override;
   /** Explain */
   TrustNode explain(TNode literal) override;
   /** Get current substitution */
@@ -130,9 +128,9 @@ class TheoryStrings : public Theory {
     {
       Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
-        return d_str.propagate(predicate);
+        return d_str.propagateLit(predicate);
       }
-      return d_str.propagate(predicate.notNode());
+      return d_str.propagateLit(predicate.notNode());
     }
     bool eqNotifyTriggerTermEquality(TheoryId tag,
                                      TNode t1,
@@ -141,10 +139,9 @@ class TheoryStrings : public Theory {
     {
       Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
-        return d_str.propagate(t1.eqNode(t2));
-      } else {
-        return d_str.propagate(t1.eqNode(t2).notNode());
+        return d_str.propagateLit(t1.eqNode(t2));
       }
+      return d_str.propagateLit(t1.eqNode(t2).notNode());
     }
     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
     {
@@ -175,7 +172,7 @@ class TheoryStrings : public Theory {
     SolverState& d_state;
   };/* class TheoryStrings::NotifyClass */
   /** propagate method */
-  bool propagate(TNode literal);
+  bool propagateLit(TNode literal);
   /** compute care graph */
   void computeCareGraph() override;
   /**

diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 109e6d0a1766856732aee5aa54f4b1dca342ec51..9564899feaab547e42a05bc13f50092600277fbb 100644 (file)
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -8,7 +8,7 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h"
 typechecker "theory/uf/theory_uf_type_rules.h"
 
 properties stable-infinite parametric
-properties check propagate ppStaticLearn presolve
+properties check ppStaticLearn presolve
 
 rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
 parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function"

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 0b97d8a5da1f51e774d397b6d162868f6417d246..29014d33fc2acee7fd2bce7cc9c76a656545ff46 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -261,11 +261,14 @@ void TheoryUF::preRegisterTerm(TNode node) {
   }
 }/* TheoryUF::preRegisterTerm() */
 
-bool TheoryUF::propagate(TNode literal) {
-  Debug("uf::propagate") << "TheoryUF::propagate(" << literal  << ")" << std::endl;
+bool TheoryUF::propagateLit(TNode literal)
+{
+  Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal << ")"
+                         << std::endl;
   // If already in conflict, no more propagation
   if (d_conflict) {
-    Debug("uf::propagate") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
+    Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal
+                           << "): already in conflict" << std::endl;
     return false;
   }
   // Propagate out
@@ -276,12 +279,6 @@ bool TheoryUF::propagate(TNode literal) {
   return ok;
 }/* TheoryUF::propagate(TNode) */
 
-void TheoryUF::propagate(Effort effort) {
-  //if (d_thss != NULL) {
-  //  return d_thss->propagate(effort);
-  //}
-}
-
 void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) {
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 7d17fdb8684bb4d10310718d2b7cabc93cf6ed88..8efaf79e3359466fa1f2d704f93f437c46b31897 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -49,10 +49,9 @@ public:
     {
       Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
-        return d_uf.propagate(predicate);
-      } else {
-       return d_uf.propagate(predicate.notNode());
+        return d_uf.propagateLit(predicate);
       }
+      return d_uf.propagateLit(predicate.notNode());
     }
 
     bool eqNotifyTriggerTermEquality(TheoryId tag,
@@ -62,10 +61,9 @@ public:
     {
       Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
-        return d_uf.propagate(t1.eqNode(t2));
-      } else {
-        return d_uf.propagate(t1.eqNode(t2).notNode());
+        return d_uf.propagateLit(t1.eqNode(t2));
       }
+      return d_uf.propagateLit(t1.eqNode(t2).notNode());
     }
 
     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
@@ -119,7 +117,7 @@ private:
    * Should be called to propagate the literal. We use a node here
    * since some of the propagated literals are not kept anywhere.
    */
-  bool propagate(TNode literal);
+  bool propagateLit(TNode literal);
 
   /**
    * Explain why this literal is true by adding assumptions
@@ -189,8 +187,6 @@ private:
   void addSharedTerm(TNode n) override;
   void computeCareGraph() override;
 
-  void propagate(Effort effort) override;
-
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
   std::string identify() const override { return "THEORY_UF"; }