diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
commit | d7dc7c2b3038b862af5ea55e7cf6b1fc4e1fe684 (patch) | |
tree | d6c229a2659bfcb3cdf7c7c786414ecc1e59e61c /src/theory/quantifiers/instantiation_engine.cpp | |
parent | 1ec95c559074ed7575a0165deb16fcee45920e9f (diff) |
Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 3dad74044..6cf64407f 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -102,7 +102,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //add counterexample lemma lem = Rewriter::rewrite( lem ); Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; - + //must explicitly remove ITEs so that we record dependencies IteSkolemMap iteSkolemMap; std::vector< Node > lems; @@ -140,7 +140,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } } } - + addedLemma = true; } } @@ -289,6 +289,9 @@ bool InstantiationEngine::checkComplete() { void InstantiationEngine::registerQuantifier( Node f ){ if( d_quantEngine->hasOwnership( f, this ) ){ + for( unsigned i=0; i<d_instStrategies.size(); ++i ){ + d_instStrategies[i]->registerQuantifier( f ); + } //Notice() << "do cbqi " << f << " ? " << std::endl; if( options::cbqi() ){ Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); |