Merge pull request #71 from kbansal/const-are-triggers

change const are triggers from false to true in equality engines

Performance comparison:
   https://www.starexec.org/starexec/secure/details/job.jsp?id=6941

Bug opened for testcase that became much worse:
  http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=621

7 files changed, 8 insertions, 9 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 186914500..99f6e0836 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -1,4 +1,3 @@
-/*********************                                                        */
 /*! \file congruence_manager.cpp
  ** \verbatim
  ** Original author: Tim King
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 94f3f573e..c770fb7ae 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" , false),
+  d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP" , true),
   d_ppFacts(u),
   //  d_ppCache(u),
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),
   d_isPreRegistered(c),
-  d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", false),
+  d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual", true),
   d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", false),
+  d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays", true),
   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 616b20cfd..9481b9894 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", false),
+    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV", true),
     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 e803af353..0c8d0fb62 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -49,7 +49,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", false),
+  d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes", true),
   d_labels( c ),
   d_selector_apps( c ),
   //d_consEqc( c ),
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 1892ecceb..565a5cd69 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", false),
+  d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate", true),
   d_trueNode(NodeManager::currentNM()->mkConst<bool>(true)),
   d_falseNode(NodeManager::currentNM()->mkConst<bool>(false)),
   d_conflict(c),
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6d2dc3138..0a5b27772 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", false),
+  d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings", true),
   d_conflict(c, false),
   d_infer(c),
   d_infer_exp(c),
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 11242569a..b00fdd6ee 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", false),
+  d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true),
   d_conflict(c, false),
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),