diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-10 02:04:51 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-10 02:07:39 -0600 |
commit | 841b7951f41f399859afab13a81e04599308da61 (patch) | |
tree | 8c6eb70b498b0a01f00c1a77b96d00ff2f61c21b /src/theory/theory_engine.cpp | |
parent | 18fed5592fb769d12ba2901a0fdc00c5c02863b9 (diff) |
Add new method --quant-cf for finding conflicts eagerly for quantified formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c598fd01b..e55d6a9c9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -75,12 +75,18 @@ void TheoryEngine::finishInit() { void TheoryEngine::eqNotifyNewClass(TNode t){ d_quantEngine->addTermToDatabase( t ); + if( d_logicInfo.isQuantified() && options::quantConflictFind() ){ + d_quantEngine->getConflictFind()->newEqClass( t ); + } } void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){ //TODO: add notification to efficient E-matching - if (d_logicInfo.isQuantified()) { + if( d_logicInfo.isQuantified() ){ d_quantEngine->getEfficientEMatcher()->merge( t1, t2 ); + if( options::quantConflictFind() ){ + d_quantEngine->getConflictFind()->merge( t1, t2 ); + } } } @@ -89,7 +95,11 @@ void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){ } void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){ - + if( d_logicInfo.isQuantified() ){ + if( options::quantConflictFind() ){ + d_quantEngine->getConflictFind()->assertDisequal( t1, t2 ); + } + } } |