diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 21:08:40 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-08 21:08:40 +0000 |
commit | b1d9707979074abb8fed7ad4e8a2b15648c69324 (patch) | |
tree | 236c83135c62a7499d1039fff94037950e05061e /src/theory/theory_engine.h | |
parent | 7b19de6b01d9a896560c39c9ef4a3731cf29b19d (diff) |
some more sat stuff for tim: assertions now go to theory_uf
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 */ |