diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index b2f047824..7958d977e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -106,11 +106,7 @@ class TheoryEngine { ++(d_engine->d_statistics.d_statLemma); d_engine->newLemma(node); } - void augmentingLemma(TNode node, bool) - throw(theory::Interrupted, AssertionException) { - ++(d_engine->d_statistics.d_statAugLemma); - d_engine->newAugmentingLemma(node); - } + void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) { d_explanationNode = explanationNode; @@ -322,12 +318,7 @@ public: } inline void newLemma(TNode node) { - d_propEngine->assertLemma(node); - } - - inline void newAugmentingLemma(TNode node) { - Node preprocessed = preprocess(node); - d_propEngine->assertFormula(preprocessed); + d_propEngine->assertLemma(preprocess(node)); } /** |