change const are triggers from false to true in equality engines

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 90029495ba8449be7ee9b02399dfcb4edf055292..99f6e083685baeffe520d9b6fc8acc38638f69fa 100644 (file)
--- 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
@@ -34,7 +33,7 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa
     d_constraintDatabase(cd),
     d_setupLiteral(setup),
     d_avariables(avars),
-    d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", false)
+    d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true)
 {}
 
 ArithCongruenceManager::Statistics::Statistics():

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 94f3f573e4b71317ad4fb660cb7a2947c25b4b1e..c770fb7ae640dd3c5afe4748a729d7e28c62462a 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" , 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 616b20cfd5206785040a8823f095c8a726410289..9481b98943a90947cd72a6f58af33b846809b23d 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", 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 e803af3535fd900280884964d34719e1e8ec19c5..0c8d0fb6296cb7ca24bac001b584906487150d68 100644 (file)
--- 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 1892ecceb4626e1ad43a100eec9581406338ab22..565a5cd69af2a7953243482e38733e1293f7782c 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", 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 6d2dc3138e458469b9d3a7bedef91c0cb5eac05e..0a5b27772f5f87bbc9ca7f81f675ff09f1ac7e70 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", 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 11242569a8047b4775d117edf79bb6a0f7efee48..b00fdd6ee5dca274664a1f4d0c5d92b0e84f8d53 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", false),
+  d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true),
   d_conflict(c, false),
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),