diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/ce_guided_single_inv.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 38 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 48 |
6 files changed, 74 insertions, 70 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index dce9c088c..f01efb5c4 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -87,16 +87,17 @@ void CegConjecture::initializeGuard( QuantifiersEngine * qe ){ if( !d_syntax_guided ){ //add immediate lemma Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() ); - Trace("cegqi") << "Add candidate lemma : " << lem << std::endl; + Trace("cegqi-lemma") << "Add candidate lemma : " << lem << std::endl; qe->getOutputChannel().lemma( lem ); }else if( d_ceg_si ){ - Node lem = d_ceg_si->getSingleInvLemma( d_guard ); - if( !lem.isNull() ){ - Trace("cegqi") << "Add single invocation lemma : " << lem << std::endl; - qe->getOutputChannel().lemma( lem ); + std::vector< Node > lems; + d_ceg_si->getSingleInvLemma( d_guard, lems ); + for( unsigned i=0; i<lems.size(); i++ ){ + Trace("cegqi-lemma") << "Add single invocation lemma " << i << " : " << lems[i] << std::endl; + qe->getOutputChannel().lemma( lems[i] ); if( Trace.isOn("cegqi-debug") ){ - lem = Rewriter::rewrite( lem ); - Trace("cegqi-debug") << "...rewritten : " << lem << std::endl; + Node rlem = Rewriter::rewrite( lems[i] ); + Trace("cegqi-debug") << "...rewritten : " << rlem << std::endl; } } } @@ -279,7 +280,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( !lems.empty() ){ d_last_inst_si = true; for( unsigned j=0; j<lems.size(); j++ ){ - Trace("cegqi-lemma") << "Single invocation lemma : " << lems[j] << std::endl; + Trace("cegqi-lemma") << "Single invocation instantiation lemma : " << lems[j] << std::endl; d_quantEngine->addLemma( lems[j] ); } d_statistics.d_cegqi_si_lemmas += lems.size(); diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index f122c63bb..c31ebd9ab 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -59,7 +59,7 @@ CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConje d_sol = new CegConjectureSingleInvSol( qe ); } -Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { +void CegConjectureSingleInv::getSingleInvLemma( Node guard, std::vector< Node >& lems ) { if( !d_single_inv.isNull() ) { d_single_inv_var.clear(); d_single_inv_sk.clear(); @@ -80,13 +80,10 @@ Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { inst = TermDb::simpleNegate( inst ); Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; - //copy variables to instantiator - d_cinst->d_vars.clear(); - d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); - - return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); - }else{ - return Node::null(); + //register with the instantiator + Node ginst = NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); + lems.push_back( ginst ); + d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk ); } } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 7df859337..8950b2642 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -113,8 +113,8 @@ public: std::map< Node, Node > d_trans_post; std::map< Node, std::vector< Node > > d_prog_templ_vars; public: - //get the single invocation lemma - Node getSingleInvLemma( Node guard ); + //get the single invocation lemma(s) + void getSingleInvLemma( Node guard, std::vector< Node >& lems ); //initialize void initialize( Node q ); //check diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 41c0e276b..073cba525 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -9,7 +9,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Implementation of cbqi instantiation strategies + ** \brief Implementation of counterexample-guided quantifier instantiation strategies **/ #include "theory/quantifiers/inst_strategy_cbqi.h" @@ -20,6 +20,7 @@ #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" +#include "util/ite_removal.h" using namespace std; using namespace CVC4; @@ -28,7 +29,6 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::arith; -using namespace CVC4::theory::datatypes; #define ARITH_INSTANTIATOR_USE_MINUS_DELTA //#define MBP_STRICT_ASSERTIONS @@ -1182,6 +1182,37 @@ void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, st subs_rhs.push_back( r ); } +void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) { + Assert( d_vars.empty() ); + d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() ); + IteSkolemMap iteSkolemMap; + d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); + Assert( 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; + d_aux_vars.push_back( i->first ); + } + for( unsigned i=0; i<lems.size(); i++ ){ + Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl; + Node rlem = lems[i]; + rlem = Rewriter::rewrite( rlem ); + Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; + //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( d_aux_vars.begin(), d_aux_vars.end(), lems[i][1][0] )!=d_aux_vars.end() ){ + Node v = lems[i][1][0]; + for( unsigned r=1; r<=2; r++ ){ + d_aux_eq[rlem[r]][v] = lems[i][r][1]; + Trace("cbqi-debug") << " " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl; + } + } + } + } + lems[i] = rlem; + } +} + //old implementation InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : @@ -1585,9 +1616,6 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q ); if( it==d_cinst.end() ){ CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true ); - for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){ - cinst->d_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) ); - } d_cinst[q] = cinst; return cinst; }else{ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 0056671be..f882da110 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -9,14 +9,14 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief instantiator_arith_instantiator + ** \brief counterexample-guided quantifier instantiation **/ #include "cvc4_private.h" -#ifndef __CVC4__INST_STRATEGT_CBQI_H -#define __CVC4__INST_STRATEGT_CBQI_H +#ifndef __CVC4__INST_STRATEGY_CBQI_H +#define __CVC4__INST_STRATEGY_CBQI_H #include "theory/quantifiers/instantiation_engine.h" #include "theory/arith/arithvar.h" @@ -30,10 +30,6 @@ namespace arith { class TheoryArith; } -namespace datatypes { - class TheoryDatatypes; -} - namespace quantifiers { class CegqiOutput @@ -64,6 +60,12 @@ private: std::map< Node, std::vector< Node > > d_curr_eqc; std::map< Node, Node > d_curr_rep; std::vector< Node > d_curr_arith_eqc; + //auxiliary variables + std::vector< Node > d_aux_vars; + //literals to equalities for aux vars + std::map< Node, std::map< Node, Node > > d_aux_eq; + //the CE variables + std::vector< Node > d_vars; private: //for adding instantiations during check void computeProgVars( Node n ); @@ -87,16 +89,12 @@ private: void addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ); public: CegInstantiator( QuantifiersEngine * qe, CegqiOutput * out, bool use_vts_delta = true, bool use_vts_inf = true ); - //the CE variables - std::vector< Node > d_vars; - //auxiliary variables - std::vector< Node > d_aux_vars; - //literals to equalities for aux vars - std::map< Node, std::map< Node, Node > > d_aux_eq; //check : add instantiations based on valuation of d_vars bool check(); //presolve for quantified formula void presolve( Node q ); + //register the counterexample lemma (stored in lems), modify vector + void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ); }; class InstStrategySimplex : public InstStrategy{ 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; } } |