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.

diff --git a/.cproject b/.cproject
index cd310c4811d01626acfc3febba0a353f078d9fdd..fdbe0b29572680fc4d0a9a4ec66be265b6b4a5d8 100644 (file)
--- a/.cproject
+++ b/.cproject
@@ -18,7 +18,7 @@
                                        <folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath="">
                                                <toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base">
                                                        <targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/>
-                                                       <builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="3" superClass="cdt.managedbuild.target.gnu.builder.base">
+                                                       <builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="optimal" superClass="cdt.managedbuild.target.gnu.builder.base">
                                                                <outputEntries>
                                                                        <entry flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="outputPath" name=""/>
                                                                </outputEntries>

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index f2874f07509d405d391586cd9dc5f595668ed974..90029495ba8449be7ee9b02399dfcb4edf055292 100644 (file)
--- 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 8b313e124dd9e5867dc55e4966c1b83565a91531..94f3f573e4b71317ad4fb660cb7a2947c25b4b1e 100644 (file)
--- 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 938a93b8561b119a01cb910ec9e82fc99cd35d69..fc23347c635f059b186b7309aca15cb6ca52d76a 100644 (file)
--- 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 0429c3aab7580176114adf88e2e053777ab74e25..bf986a1389254a0fb26c7dbb8ccae29c9d799de1 100644 (file)
--- 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 2f8822b530643855e2c07084ef8fa5fb372bfde5..520ea5e70807bc04ce659cb44e7eb9a0d8f6a389 100755 (executable)
--- 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 >&
 \r
 ConjectureGenerator::ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ),\r
 d_notify( *this ),\r
-d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee"),\r
+d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),\r
 d_ee_conjectures( c ){\r
   d_fullEffortCount = 0;\r
   d_uequalityEngine.addFunctionKind( kind::APPLY_UF );\r

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index e229d3a6f9a401eee16bef04288fe9796564f918..1892ecceb4626e1ad43a100eec9581406338ab22 100644 (file)
--- 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 6e50cb82d07cdda883d8d91a934b4b4dc6215666..a4132635029d2582fe8b66e4e2bd0109e94c6366 100644 (file)
--- 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 67b055d33cc18dd403c52a1f498ca5e60ee8f992..a2eb58cdc3bd64dd119e326b810776c4ccba7c4f 100644 (file)
--- 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 9d91c096a6c19b48f3cf097882bda02225fe7cc2..22bf37470b424c0b05dfc1289aac657c5f42ee50 100644 (file)
--- 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 cb50bf355ce78a812de20359891aa969e406f71c..7d385c398a750ee7e239734e56214aec207d2c60 100644 (file)
--- 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 3b19270a48f3054fb0391997d18e1e72896b4383..42736a59b6a6fdf918d4eee9abeaead173a214aa 100644 (file)
--- 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 25092f37fb5ea28b3ef17fe4609bef93f832be33..a26947ed1f0ed8485ede3da9faeb173cf5f7ac85 100644 (file)
--- 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 8fa7d2dbc8aa6da8c5a034254659d8823c5c80e1..11242569a8047b4775d117edf79bb6a0f7efee48 100644 (file)
--- 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),