diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 076ea4d2d..5453aab93 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -60,7 +60,8 @@ class TheoryEngine { d_engine = &engine; } - void conflict(TNode, bool) throw(theory::Interrupted) { + void conflict(TNode conflictNode, bool) throw(theory::Interrupted) { + Debug("theory") << "conflict(" << conflictNode << ")" << std::endl; } void propagate(TNode, bool) throw(theory::Interrupted) { @@ -107,8 +108,22 @@ public: * @returns the theory, or NULL if the TNode is * of built-in type. */ - theory::Theory* theoryOf(TNode n) { - return theoryOfTable[n]; + theory::Theory* theoryOf(const TNode& node) { + return theoryOfTable[node]; + } + + /** + * Assert the formula to the apropriate theory. + * @param node the assertion + */ + inline void assertFact(const TNode& node) { + Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + theory::Theory* theory = theoryOf(node); + if (theory != NULL) theory->assertFact(node); + } + + inline void check(theory::Theory::Effort effort) { + d_uf.check(effort); } };/* class TheoryEngine */ |