summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/arith/congruence_manager.cpp2
-rw-r--r--src/theory/arrays/theory_arrays.cpp6
-rw-r--r--src/theory/bv/bv_subtheory_core.cpp2
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp2
-rwxr-xr-xsrc/theory/quantifiers/conjecture_generator.cpp2
-rw-r--r--src/theory/sets/theory_sets_private.cpp2
-rw-r--r--src/theory/shared_terms_database.cpp2
-rw-r--r--src/theory/strings/theory_strings.cpp2
-rw-r--r--src/theory/theory_engine.cpp4
-rw-r--r--src/theory/theory_model.cpp2
-rw-r--r--src/theory/uf/equality_engine.cpp8
-rw-r--r--src/theory/uf/equality_engine.h7
-rw-r--r--src/theory/uf/theory_uf.cpp2
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),
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback