diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-27 17:27:57 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-27 17:27:57 +0200 |
commit | 0ddf1b9c74f2b2a78e0960b710c2edbdc5f8d02d (patch) | |
tree | 523a7c7ec9bfefd4297c5d8f56ef0ff474045d73 /src/theory/quantifiers/instantiation_engine.cpp | |
parent | d4a7b0cf0500e971c9c01e7628f3c1b567715059 (diff) |
Do ITE term bookkeeping when solving Sygus inputs. Add missing script from Sygus comp 2015. Fix bug 665 regarding strings rewriter for contains.
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 48 |
1 files changed, 14 insertions, 34 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 492b2dedf..699208fba 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers/inst_strategy_e_matching.h" #include "theory/quantifiers/inst_strategy_cbqi.h" #include "theory/quantifiers/trigger.h" -#include "util/ite_removal.h" using namespace std; using namespace CVC4; @@ -108,44 +107,25 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ 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; - lems.push_back( lem ); - d_quantEngine->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); - CegInstantiator * cinst = NULL; if( d_i_cegqi ){ - cinst = d_i_cegqi->getInstantiator( f ); - Assert( cinst->d_aux_vars.empty() ); - for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { - Trace("cbqi-debug") << " Auxiliary var (from ITE) : " << i->first << std::endl; - cinst->d_aux_vars.push_back( i->first ); + //must register with the instantiator + //must explicitly remove ITEs so that we record dependencies + std::vector< Node > ce_vars; + for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ + ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) ); } - } - for( unsigned i=0; i<lems.size(); i++ ){ - Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl; - if( !cinst ){ + std::vector< Node > lems; + lems.push_back( lem ); + CegInstantiator * cinst = d_i_cegqi->getInstantiator( f ); + cinst->registerCounterexampleLemma( lems, ce_vars ); + for( unsigned i=0; i<lems.size(); i++ ){ + Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl; d_quantEngine->addLemma( lems[i], false ); - }else{ - Node rlem = lems[i]; - rlem = Rewriter::rewrite( rlem ); - Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; - d_quantEngine->addLemma( rlem, false ); - //record the literals that imply auxiliary variables to be equal to terms - if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){ - if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){ - if( std::find( cinst->d_aux_vars.begin(), cinst->d_aux_vars.end(), lems[i][1][0] )!=cinst->d_aux_vars.end() ){ - Node v = lems[i][1][0]; - for( unsigned r=1; r<=2; r++ ){ - cinst->d_aux_eq[rlem[r]][v] = lems[i][r][1]; - Trace("cbqi-debug") << " " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl; - } - } - } - } } + }else{ + Trace("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; + d_quantEngine->addLemma( lem, false ); } - addedLemma = true; } } |