summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp73
1 files changed, 53 insertions, 20 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d37916515..b4d6654b1 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -117,7 +117,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
* twice. */
// FIXME when ExprSets are online, use one of those to avoid
// duplicates in the above?
- // Actually, that doesn't work because you have to make sure
+ // Actually, that doesn't work because you have to make sure
// that the *last* occurrence is the one that gets processed first @CB
// This could be a big performance problem though because it requires
// traversing a DAG as a tree and that can really blow up @CB
@@ -132,6 +132,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
TheoryEngine::TheoryEngine(context::Context* ctxt) :
d_propEngine(NULL),
d_context(ctxt),
+ d_activeTheories(0),
d_theoryOut(this, ctxt),
d_hasShutDown(false),
d_incomplete(ctxt, false),
@@ -139,6 +140,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) :
for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
d_theoryTable[theoryId] = NULL;
+ d_theoryIsActive[theoryId] = false;
}
Rewriter::init();
@@ -150,7 +152,7 @@ TheoryEngine::~TheoryEngine() {
Assert(d_hasShutDown);
for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
- if(d_theoryTable[theoryId]) {
+ if(d_theoryTable[theoryId] != NULL) {
delete d_theoryTable[theoryId];
}
}
@@ -163,7 +165,7 @@ struct preprocess_stack_element {
bool children_added;
preprocess_stack_element(TNode node)
: node(node), children_added(false) {}
-};
+};/* struct preprocess_stack_element */
Node TheoryEngine::preprocess(TNode node) {
// Make sure the node is type-checked first (some rewrites depend on
@@ -198,24 +200,29 @@ void TheoryEngine::preRegister(TNode preprocessed) {
if (current.getKind() == kind::EQUAL) {
TheoryId theoryLHS = Theory::theoryOf(current[0]);
Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl;
+ markActive(theoryLHS);
d_theoryTable[theoryLHS]->preRegisterTerm(current);
// TheoryId theoryRHS = Theory::theoryOf(current[1]);
// if (theoryLHS != theoryRHS) {
+// markActive(theoryRHS);
// d_theoryTable[theoryRHS]->preRegisterTerm(current);
// Debug("register") << "preregistering " << current << " with " << theoryRHS << std::endl;
// }
// TheoryId typeTheory = Theory::theoryOf(current[0].getType());
// if (typeTheory != theoryLHS && typeTheory != theoryRHS) {
+// markActive(typeTheory);
// d_theoryTable[typeTheory]->preRegisterTerm(current);
// Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl;
// }
} else {
TheoryId theory = Theory::theoryOf(current);
Debug("register") << "preregistering " << current << " with " << theory << std::endl;
+ markActive(theory);
d_theoryTable[theory]->preRegisterTerm(current);
TheoryId typeTheory = Theory::theoryOf(current.getType());
if (theory != typeTheory) {
Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl;
+ markActive(typeTheory);
d_theoryTable[typeTheory]->preRegisterTerm(current);
}
}
@@ -248,7 +255,7 @@ bool TheoryEngine::check(theory::Theory::Effort effort) {
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasCheck) { \
+ if (theory::TheoryTraits<THEORY>::hasCheck && d_theoryIsActive[THEORY]) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \
if (!d_theoryOut.d_conflictNode.get().isNull()) { \
return false; \
@@ -271,7 +278,7 @@ void TheoryEngine::propagate() {
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasPropagate) { \
+ if (theory::TheoryTraits<THEORY>::hasPropagate && d_theoryIsActive[THEORY]) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \
}
@@ -359,13 +366,22 @@ Node TheoryEngine::getValue(TNode node) {
bool TheoryEngine::presolve() {
d_theoryOut.d_conflictNode = Node::null();
d_theoryOut.d_propagatedLiterals.clear();
+
try {
- for(unsigned i = 0; i < THEORY_LAST; ++ i) {
- d_theoryTable[i]->presolve();
- if(!d_theoryOut.d_conflictNode.get().isNull()) {
- return true;
- }
- }
+ // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ if (theory::TheoryTraits<THEORY>::hasPresolve && d_theoryIsActive[THEORY]) { \
+ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \
+ if(!d_theoryOut.d_conflictNode.get().isNull()) { \
+ return true; \
+ } \
+ }
+
+ // Presolve for each theory using the statement above
+ CVC4_FOR_EACH_THEORY
} catch(const theory::Interrupted&) {
Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl;
}
@@ -375,20 +391,37 @@ bool TheoryEngine::presolve() {
void TheoryEngine::notifyRestart() {
- for(unsigned i = 0; i < THEORY_LAST; ++ i) {
- if (d_theoryTable[i]) {
- d_theoryTable[i]->notifyRestart();
- }
+ // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_theoryIsActive[THEORY]) { \
+ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->notifyRestart(); \
}
-}
+ // notify each theory using the statement above
+ CVC4_FOR_EACH_THEORY
+}
void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
- for(unsigned i = 0; i < THEORY_LAST; ++ i) {
- if (d_theoryTable[i]) {
- d_theoryTable[i]->staticLearning(in, learned);
- }
+ // NOTE that we don't look at d_theoryIsActive[] here. First of
+ // all, we haven't done any pre-registration yet, so we don't know
+ // which theories are active. Second, let's give each theory a shot
+ // at doing something with the input formula, even if it wouldn't
+ // otherwise be active.
+
+ // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ if (theory::TheoryTraits<THEORY>::hasStaticLearning) { \
+ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->staticLearning(in, learned); \
}
+
+ // notify each theory using the statement above
+ CVC4_FOR_EACH_THEORY
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback