Adding an option to the equality engine constructor to treat all constants as

trigger terms. I've disabled constants as triggers for all equality engines
except for the shared terms engine where it is needed.

13 files changed, 24 insertions, 19 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index f2874f075..90029495b 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -34,7 +34,7 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa
     d_constraintDatabase(cd),
     d_setupLiteral(setup),
     d_avariables(avars),
-    d_ee(d_notify, c, "theory::arith::ArithCongruenceManager")
+    d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", false)
 {}
 
 ArithCongruenceManager::Statistics::Statistics():
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 8b313e124..94f3f573e 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -61,15 +61,15 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_numGetModelValConflicts("theory::arrays::number of getModelVal conflicts", 0),
   d_numSetModelValSplits("theory::arrays::number of setModelVal splits", 0),
   d_numSetModelValConflicts("theory::arrays::number of setModelVal conflicts", 0),
-  d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"),
+  d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , false),
   d_ppFacts(u),
   //  d_ppCache(u),
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),
   d_isPreRegistered(c),
-  d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual"),
+  d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", false),
   d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"),
+  d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", false),
   d_conflict(c, false),
   d_backtracker(c),
   d_infoMap(c, &d_backtracker),
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 938a93b85..fc23347c6 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -32,7 +32,7 @@ using namespace CVC4::theory::bv::utils;
 CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_notify(*this),
-    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
+    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV", false),
     d_slicer(new Slicer()),
     d_isComplete(c, true),
     d_useSlicer(false),
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 0429c3aab..bf986a138 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -46,7 +46,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_infer(c),
   d_infer_exp(c),
   d_notify( *this ),
-  d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"),
+  d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", false),
   d_labels( c ),
   d_selector_apps( c ),
   //d_consEqc( c ),
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 2f8822b53..520ea5e70 100755
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -81,7 +81,7 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >&
 

 ConjectureGenerator::ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ),

 d_notify( *this ),

-d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee"),

+d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),

 d_ee_conjectures( c ){

   d_fullEffortCount = 0;

   d_uequalityEngine.addFunctionKind( kind::APPLY_UF );

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index e229d3a6f..1892ecceb 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1086,7 +1086,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
                                      context::UserContext* u):
   d_external(external),
   d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"),
+  d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate", false),
   d_trueNode(NodeManager::currentNM()->mkConst<bool>(true)),
   d_falseNode(NodeManager::currentNM()->mkConst<bool>(false)),
   d_conflict(c),
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 6e50cb82d..a41326350 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -29,7 +29,7 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Co
 , d_alreadyNotifiedMap(context)
 , d_registeredEqualities(context)
 , d_EENotify(*this)
-, d_equalityEngine(d_EENotify, context, "SharedTermsDatabase")
+, d_equalityEngine(d_EENotify, context, "SharedTermsDatabase", true)
 , d_theoryEngine(theoryEngine)
 , d_inConflict(context, false)
 {
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 67b055d33..a2eb58cdc 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -37,7 +37,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
   : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
   RMAXINT(LONG_MAX),
   d_notify( *this ),
-  d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"),
+  d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", false),
   d_conflict(c, false),
   d_infer(c),
   d_infer_exp(c),
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 9d91c096a..22bf37470 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -74,7 +74,7 @@ void TheoryEngine::finishInit() {
   if (d_logicInfo.isQuantified()) {
     d_quantEngine->finishInit();
     Assert(d_masterEqualityEngine == 0);
-    d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master");
+    d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master", false);
 
     for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
       if (d_theoryTable[theoryId]) {
@@ -1201,7 +1201,7 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
 }
 
 Node TheoryEngine::getModelValue(TNode var) {
-  if(var.isConst()) return var;  // FIXME: HACK!!!
+  if (var.isConst()) return var;  // FIXME: HACK!!!
   Assert(d_sharedTerms.isShared(var));
   return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
 }
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index cb50bf355..7d385c398 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -34,7 +34,7 @@ TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncM
   d_false = NodeManager::currentNM()->mkConst( false );
 
   d_eeContext = new context::Context();
-  d_equalityEngine = new eq::EqualityEngine(d_eeContext, name);
+  d_equalityEngine = new eq::EqualityEngine(d_eeContext, name, false);
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine->addFunctionKind(kind::APPLY_UF);
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 3b19270a4..42736a59b 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -79,7 +79,7 @@ EqualityEngine::~EqualityEngine() throw(AssertionException) {
 }
 
 
-EqualityEngine::EqualityEngine(context::Context* context, std::string name)
+EqualityEngine::EqualityEngine(context::Context* context, std::string name, bool constantsAreTriggers)
 : ContextNotifyObj(context)
 , d_masterEqualityEngine(0)
 , d_context(context)
@@ -93,6 +93,7 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name)
 , d_subtermEvaluatesSize(context, 0)
 , d_stats(name)
 , d_inPropagate(false)
+, d_constantsAreTriggers(constantsAreTriggers)
 , d_triggerDatabaseSize(context, 0)
 , d_triggerTermSetUpdatesSize(context, 0)
 , d_deducedDisequalitiesSize(context, 0)
@@ -103,7 +104,7 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name)
   init();
 }
 
-EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name)
+EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name, bool constantsAreTriggers)
 : ContextNotifyObj(context)
 , d_masterEqualityEngine(0)
 , d_context(context)
@@ -117,6 +118,7 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c
 , d_subtermEvaluatesSize(context, 0)
 , d_stats(name)
 , d_inPropagate(false)
+, d_constantsAreTriggers(constantsAreTriggers)
 , d_triggerDatabaseSize(context, 0)
 , d_triggerTermSetUpdatesSize(context, 0)
 , d_deducedDisequalitiesSize(context, 0)
@@ -308,7 +310,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
     // We set this here as this only applies to actual terms, not the
     // intermediate application terms
     d_isBoolean[result] = true;
-  } else if (d_isConstant[result]) {
+  } else if (d_constantsAreTriggers && d_isConstant[result]) {
     // Non-Boolean constants are trigger terms for all tags
     EqualityNodeId tId = getNodeId(t);
     // Setup the new set 
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 25092f37f..a26947ed1 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -165,12 +165,12 @@ public:
   /**
    * Initialize the equality engine, given the notification class.
    */
-  EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name);
+  EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name, bool constantsAreTriggers);
 
   /**
    * Initialize the equality engine with no notification class.
    */
-  EqualityEngine(context::Context* context, std::string name);
+  EqualityEngine(context::Context* context, std::string name, bool constantsAreTriggers);
 
   /**
    * Just a destructor.
@@ -554,6 +554,9 @@ private:
     }
   };/* struct EqualityEngine::TriggerTermSet */
 
+  /** Are the constants triggers */
+  bool d_constantsAreTriggers;
+
   /** The information about trigger terms is stored in this easily maintained memory. */
   char* d_triggerDatabase;
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 8fa7d2dbc..11242569a 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -34,7 +34,7 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel&
   /* The strong theory solver can be notified by EqualityEngine::init(),
    * so make sure it's initialized first. */
   d_thss(NULL),
-  d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
+  d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", false),
   d_conflict(c, false),
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),