From 201ae337e8e1531d1ae68a0ae536e34850edecd3 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 1 Dec 2015 15:02:08 +0100 Subject: [PATCH] More work on --cegqi-si-partial, incomplete. --- src/Makefile.am | 2 + .../quantifiers/ce_guided_instantiation.cpp | 126 +++++++++++++----- .../quantifiers/ce_guided_instantiation.h | 26 ++-- .../quantifiers/ce_guided_single_inv.cpp | 93 +++++++++++-- src/theory/quantifiers/ce_guided_single_inv.h | 18 ++- .../quantifiers/ce_guided_single_inv_ei.cpp | 47 +++++++ .../quantifiers/ce_guided_single_inv_ei.h | 43 ++++++ 7 files changed, 287 insertions(+), 68 deletions(-) create mode 100644 src/theory/quantifiers/ce_guided_single_inv_ei.cpp create mode 100644 src/theory/quantifiers/ce_guided_single_inv_ei.h diff --git a/src/Makefile.am b/src/Makefile.am index 3c482413b..fe38ddf71 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -333,6 +333,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/ce_guided_single_inv.cpp \ theory/quantifiers/ce_guided_single_inv_sol.h \ theory/quantifiers/ce_guided_single_inv_sol.cpp \ + theory/quantifiers/ce_guided_single_inv_ei.h \ + theory/quantifiers/ce_guided_single_inv_ei.cpp \ theory/quantifiers/local_theory_ext.h \ theory/quantifiers/local_theory_ext.cpp \ theory/quantifiers/fun_def_process.h \ diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index f11153f5f..dcbfba3ff 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -78,22 +78,23 @@ void CegConjecture::assign( Node q ) { } void CegConjecture::initializeGuard( QuantifiersEngine * qe ){ - if( isAssigned() && d_guard.isNull() ){ - d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); - //specify guard behavior - d_guard = qe->getValuation().ensureLiteral( d_guard ); - AlwaysAssert( !d_guard.isNull() ); - qe->getOutputChannel().requirePhase( d_guard, true ); + if( isAssigned() ){ if( !d_syntax_guided ){ - //add immediate lemma - Node lem = NodeManager::currentNM()->mkNode( OR, d_guard.negate(), d_base_inst.negate() ); - Trace("cegqi-lemma") << "Add candidate lemma : " << lem << std::endl; - qe->getOutputChannel().lemma( lem ); - }else if( d_ceg_si ){ + if( d_nsg_guard.isNull() ){ + d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); + d_nsg_guard = qe->getValuation().ensureLiteral( d_nsg_guard ); + AlwaysAssert( !d_nsg_guard.isNull() ); + qe->getOutputChannel().requirePhase( d_nsg_guard, true ); + //add immediate lemma + Node lem = NodeManager::currentNM()->mkNode( OR, d_nsg_guard.negate(), d_base_inst.negate() ); + Trace("cegqi-lemma") << "Cegqi::Lemma : non-syntax-guided : " << lem << std::endl; + qe->getOutputChannel().lemma( lem ); + } + }else if( d_ceg_si->d_si_guard.isNull() ){ std::vector< Node > lems; - d_ceg_si->getInitialSingleInvLemma( d_guard, lems ); + d_ceg_si->getInitialSingleInvLemma( lems ); for( unsigned i=0; igetOutputChannel().lemma( lems[i] ); if( Trace.isOn("cegqi-debug") ){ Node rlem = Rewriter::rewrite( lems[i] ); @@ -101,6 +102,7 @@ void CegConjecture::initializeGuard( QuantifiersEngine * qe ){ } } } + Assert( !getGuard().isNull() ); } } @@ -117,7 +119,7 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { d_lits[i] = lit; Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() ); - Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl; + Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness split : " << lem << std::endl; qe->getOutputChannel().lemma( lem ); qe->getOutputChannel().requirePhase( lit, true ); @@ -128,7 +130,7 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { lem_c.push_back( NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, d_candidates[j], c ) ); } Node hlem = NodeManager::currentNM()->mkNode( OR, lit.negate(), lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ) ); - Trace("cegqi-lemma") << "Fairness expansion (dt-height-pred) : " << hlem << std::endl; + Trace("cegqi-lemma") << "Cegqi::Lemma : Fairness expansion (dt-height-pred) : " << hlem << std::endl; qe->getOutputChannel().lemma( hlem ); } return lit; @@ -138,6 +140,10 @@ Node CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) { } } +Node CegConjecture::getGuard() { + return !d_syntax_guided ? d_nsg_guard : d_ceg_si->d_si_guard; +} + CegqiFairMode CegConjecture::getCegqiFairMode() { return isSingleInvocation() ? CEGQI_FAIR_NONE : options::ceGuidedInstFair(); } @@ -150,8 +156,52 @@ bool CegConjecture::isFullySingleInvocation() { return d_ceg_si->isFullySingleInvocation(); } -bool CegConjecture::needsCheck() { - return !isSingleInvocation() || d_ceg_si->needsCheck(); +bool CegConjecture::needsCheck( std::vector< Node >& lem ) { + if( isSingleInvocation() && !d_ceg_si->needsCheck() ){ + return false; + }else{ + bool value; + if( !isSingleInvocation() || isFullySingleInvocation() ){ + Assert( !getGuard().isNull() ); + // non or fully single invocation : look at guard only + if( d_qe->getValuation().hasSatValue( getGuard(), value ) ) { + if( !value ){ + Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl; + return false; + } + }else{ + Assert( false ); + } + }else{ + // not fully single invocation : infeasible if overall specification is infeasible + Assert( !d_ceg_si->d_full_guard.isNull() ); + if( d_qe->getValuation().hasSatValue( d_ceg_si->d_full_guard, value ) ) { + if( !value ){ + Trace("cegqi-nsi") << "NSI : found full specification is infeasible." << std::endl; + return false; + }else{ + Assert( !d_ceg_si->d_si_guard.isNull() ); + if( d_qe->getValuation().hasSatValue( d_ceg_si->d_si_guard, value ) ) { + if( !value ){ + if( !d_ceg_si->d_single_inv_exp.isNull() ){ + //this should happen infrequently : only if cegqi determines infeasibility of a false candidate before E-matching does + Trace("cegqi-nsi") << "NSI : current single invocation lemma was infeasible, block assignment upon which conjecture was based." << std::endl; + Node l = NodeManager::currentNM()->mkNode( OR, d_ceg_si->d_full_guard.negate(), d_ceg_si->d_single_inv_exp ); + lem.push_back( l ); + d_ceg_si->initializeNextSiConjecture(); + } + return false; + } + }else{ + Assert( false ); + } + } + }else{ + Assert( false ); + } + } + return true; + } } void CegConjecture::preregisterConjecture( Node q ) { @@ -168,29 +218,30 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) { } unsigned CegInstantiation::needsModel( Theory::Effort e ) { - return QuantifiersEngine::QEFFORT_MODEL; + return d_conj->d_ceg_si->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL; } void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { - if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){ + unsigned echeck = d_conj->d_ceg_si->isSingleInvocation() ? QuantifiersEngine::QEFFORT_STANDARD : QuantifiersEngine::QEFFORT_MODEL; + if( quant_e==echeck ){ Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl; Trace("cegqi-engine-debug") << std::endl; bool active = false; - bool feasible = false; bool value; if( d_quantEngine->getValuation().hasSatValue( d_conj->d_assert_quant, value ) ) { active = value; }else{ Trace("cegqi-engine-debug") << "...no value for quantified formula." << std::endl; } - if( d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) { - feasible = value; - }else{ - Trace("cegqi-engine-debug") << "...no value for guard." << std::endl; - } - Trace("cegqi-engine-debug") << "Current conjecture status : active : " << active << " feasible : " << feasible << std::endl; - if( active && feasible && d_conj->needsCheck() ){ + Trace("cegqi-engine-debug") << "Current conjecture status : active : " << active << std::endl; + std::vector< Node > lem; + if( active && d_conj->needsCheck( lem ) ){ checkCegConjecture( d_conj ); + }else{ + for( unsigned i=0; igetOutputChannel().lemma( lem[i] ); + } } Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl; } @@ -241,9 +292,14 @@ Node CegInstantiation::getNextDecisionRequest() { if( d_conj->isAssigned() ){ d_conj->initializeGuard( d_quantEngine ); std::vector< Node > req_dec; - req_dec.push_back( d_conj->d_guard ); - if( d_conj->d_ceg_si && !d_conj->d_ceg_si->d_ns_guard.isNull() ){ - req_dec.push_back( d_conj->d_ceg_si->d_ns_guard ); + req_dec.push_back( d_conj->getGuard() ); + if( d_conj->d_ceg_si ){ + if( !d_conj->d_ceg_si->d_full_guard.isNull() ){ + req_dec.push_back( d_conj->d_ceg_si->d_full_guard ); + } + if( !d_conj->d_ceg_si->d_ns_guard.isNull() ){ + req_dec.push_back( d_conj->d_ceg_si->d_ns_guard ); + } } for( unsigned i=0; iaddLemma( lems[j] ); } d_statistics.d_cegqi_si_lemmas += lems.size(); @@ -313,7 +369,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } if( !lems.empty() ){ for( unsigned j=0; jaddLemma( lems[j] ); } Trace("cegqi-engine") << " ...refine size." << std::endl; @@ -353,7 +409,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Node lem = NodeManager::currentNM()->mkNode( OR, ic ); lem = Rewriter::rewrite( lem ); d_last_inst_si = false; - Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl; + Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem << std::endl; d_quantEngine->addLemma( lem ); ++(d_statistics.d_cegqi_lemmas_ce); Trace("cegqi-engine") << " ...find counterexample." << std::endl; @@ -399,9 +455,9 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { } if( success ){ Node lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ); - lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), lem ); + lem = NodeManager::currentNM()->mkNode( OR, conj->getGuard().negate(), lem ); lem = Rewriter::rewrite( lem ); - Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl; + Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl; Trace("cegqi-engine") << " ...refine candidate." << std::endl; d_quantEngine->addLemma( lem ); ++(d_statistics.d_cegqi_lemmas_refine); diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 82c57b3d8..6fcfdbc58 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -37,16 +37,10 @@ public: Node d_assert_quant; /** quantified formula (after processing) */ Node d_quant; - /** guard */ - Node d_guard; /** base instantiation */ Node d_base_inst; /** expand base inst to disjuncts */ std::vector< Node > d_base_disj; - /** guard split */ - Node d_guard_split; - /** is syntax-guided */ - bool d_syntax_guided; /** list of constants for quantified formula */ std::vector< Node > d_candidates; /** list of variables on inner quantification */ @@ -54,22 +48,20 @@ public: std::vector< std::vector< Node > > d_inner_vars_disj; /** list of terms we have instantiated candidates with */ std::map< int, std::vector< Node > > d_candidate_inst; - /** initialize guard */ - void initializeGuard( QuantifiersEngine * qe ); /** measure term */ Node d_measure_term; /** measure sum size */ int d_measure_term_size; /** refine count */ unsigned d_refine_count; - /** assign */ - void assign( Node q ); - /** is assigned */ - bool isAssigned() { return !d_quant.isNull(); } /** current extential quantifeirs whose couterexamples we must refine */ std::vector< std::vector< Node > > d_ce_sk; /** single invocation utility */ CegConjectureSingleInv * d_ceg_si; +public: //non-syntax guided (deprecated) + /** guard */ + bool d_syntax_guided; + Node d_nsg_guard; public: //for fairness /** the cardinality literals */ std::map< int, Node > d_lits; @@ -77,6 +69,8 @@ public: //for fairness context::CDO< int > d_curr_lit; /** allocate literal */ Node getLiteral( QuantifiersEngine * qe, int i ); + /** get guard */ + Node getGuard(); /** is ground */ bool isGround() { return d_inner_vars.empty(); } /** fairness */ @@ -86,9 +80,15 @@ public: //for fairness /** is single invocation */ bool isFullySingleInvocation(); /** needs check */ - bool needsCheck(); + bool needsCheck( std::vector< Node >& lem ); /** preregister conjecture */ void preregisterConjecture( Node q ); + /** initialize guard */ + void initializeGuard( QuantifiersEngine * qe ); + /** assign */ + void assign( Node q ); + /** is assigned */ + bool isAssigned() { return !d_quant.isNull(); } }; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index c9f71b76a..f309ae0cd 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/ce_guided_single_inv.h" #include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/quantifiers/ce_guided_single_inv_ei.h" #include "theory/theory_engine.h" #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" @@ -52,17 +53,31 @@ CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConje }else{ d_c_inst_match_trie = NULL; } - CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this ); + d_cosi = new CegqiOutputSingleInv( this ); // third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity - d_cinst = new CegInstantiator( qe, cosi, false, false ); + d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); d_sol = new CegConjectureSingleInvSol( qe ); d_sip = new SingleInvocationPartition; + + if( options::cegqiSingleInvPartial() ){ + d_ei = new CegEntailmentInfer( qe, d_sip ); + }else{ + d_ei = NULL; + } } -void CegConjectureSingleInv::getInitialSingleInvLemma( Node guard, std::vector< Node >& lems ) { +void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems ) { + Assert( d_si_guard.isNull() ); + //single invocation guard + d_si_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); + d_si_guard = d_qe->getValuation().ensureLiteral( d_si_guard ); + AlwaysAssert( !d_si_guard.isNull() ); + d_qe->getOutputChannel().requirePhase( d_si_guard, true ); + if( !d_single_inv.isNull() ) { + //make for new var/sk d_single_inv_var.clear(); d_single_inv_sk.clear(); Node inst; @@ -83,8 +98,13 @@ void CegConjectureSingleInv::getInitialSingleInvLemma( Node guard, std::vector< Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; //register with the instantiator - Node ginst = NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); + Node ginst = NodeManager::currentNM()->mkNode( OR, d_si_guard.negate(), inst ); lems.push_back( ginst ); + //make and register the instantiator + if( d_cinst ){ + delete d_cinst; + } + d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk ); } } @@ -162,13 +182,12 @@ void CegConjectureSingleInv::initialize( Node q ) { if( !d_sip->d_conjuncts[1].empty() ){ singleInvocation = false; if( options::cegqiSingleInvPartial() ){ - /* TODO : this enables partially single invocation techniques + //this enables partially single invocation techniques d_nsingle_inv = d_sip->getNonSingleInvocation(); d_nsingle_inv = TermDb::simpleNegate( d_nsingle_inv ); d_full_inv = d_sip->getFullSpecification(); d_full_inv = TermDb::simpleNegate( d_full_inv ); singleInvocation = true; - */ }else if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ //if we are doing invariant templates, then construct the template std::map< Node, bool > has_inv; @@ -287,11 +306,33 @@ void CegConjectureSingleInv::initialize( Node q ) { //just invoke the presolve now d_cinst->presolve( d_single_inv ); } - if( !d_nsingle_inv.isNull() ){ + if( !isFullySingleInvocation() ){ //initialize information as next single invocation conjecture initializeNextSiConjecture(); Trace("cegqi-si") << "Non-single invocation formula is : " << d_nsingle_inv << std::endl; Trace("cegqi-si") << "Full specification is : " << d_full_inv << std::endl; + //add full specification lemma : will use for testing infeasibility/deriving entailments + d_full_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GF", NodeManager::currentNM()->booleanType() ) ); + d_full_guard = d_qe->getValuation().ensureLiteral( d_full_guard ); + AlwaysAssert( !d_full_guard.isNull() ); + d_qe->getOutputChannel().requirePhase( d_full_guard, true ); + Node fbvl; + if( !d_sip->d_all_vars.empty() ){ + fbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, d_sip->d_all_vars ); + } + std::vector< Node > flem_c; + for( unsigned i=0; id_conjuncts[2].size(); i++ ){ + Node flemi = d_sip->d_conjuncts[2][i]; + if( !fbvl.isNull() ){ + flemi = NodeManager::currentNM()->mkNode( FORALL, fbvl, flemi ); + } + flem_c.push_back( flemi ); + } + Node flem = flem_c.empty() ? d_qe->getTermDatabase()->d_true : ( flem_c.size()==1 ? flem_c[0] : NodeManager::currentNM()->mkNode( AND, flem_c ) ); + flem = NodeManager::currentNM()->mkNode( OR, d_full_guard.negate(), flem ); + flem = Rewriter::rewrite( flem ); + Trace("cegqi-lemma") << "Cegqi::Lemma : full specification " << flem << std::endl; + d_qe->getOutputChannel().lemma( flem ); } }else{ Trace("cegqi-si") << "Formula is not single invocation." << std::endl; @@ -435,6 +476,23 @@ Node CegConjectureSingleInv::addDeepEmbedding( Node n, std::map< Node, Node >& v } void CegConjectureSingleInv::initializeNextSiConjecture() { + Trace("cegqi-nsi") << "NSI : initialize next candidate conjecture..." << std::endl; + if( d_single_inv.isNull() ){ + if( d_ei->getEntailedConjecture( d_single_inv, d_single_inv_exp ) ){ + Trace("cegqi-nsi") << "NSI : got : " << d_single_inv << std::endl; + Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl; + }else{ + Trace("cegqi-nsi") << "NSI : failed to construct next conjecture." << std::endl; + Notice() << "Incomplete due to --cegqi-si-partial." << std::endl; + exit( 10 ); + } + }else{ + //initial call + Trace("cegqi-nsi") << "NSI : have : " << d_single_inv << std::endl; + Assert( d_single_inv_exp.isNull() ); + } + + d_si_guard = Node::null(); d_ns_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GS", NodeManager::currentNM()->booleanType() ) ); d_ns_guard = d_qe->getValuation().ensureLiteral( d_ns_guard ); AlwaysAssert( !d_ns_guard.isNull() ); @@ -481,10 +539,6 @@ bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){ Trace("cegqi-engine-debug") << "Rewrite based on vts symbols..." << std::endl; lem = d_qe->getTermDatabase()->rewriteVtsSymbols( lem ); } - //add guard if not fully single invocation - if( !isFullySingleInvocation() ){ - lem = NodeManager::currentNM()->mkNode( OR, d_ns_guard.negate(), lem ); - } Trace("cegqi-engine-debug") << "Rewrite..." << std::endl; lem = Rewriter::rewrite( lem ); Trace("cegqi-si") << "Single invocation lemma : " << lem << std::endl; @@ -554,14 +608,25 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) { } }else if( !isFullySingleInvocation() ){ //create next candidate conjecture - Trace("cegqi-nsi") << "NSI : create next candidate conjecture..." << std::endl; - exit( 10 ); + Assert( d_ei!=NULL ); + //construct d_single_inv + d_single_inv = Node::null(); + initializeNextSiConjecture(); + return; } d_curr_lemmas.clear(); //call check for instantiator d_cinst->check(); //add lemmas - lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() ); + //add guard if not fully single invocation + if( !isFullySingleInvocation() ){ + Assert( !d_ns_guard.isNull() ); + for( unsigned i=0; imkNode( OR, d_ns_guard.negate(), d_curr_lemmas[i] ) ); + } + }else{ + lems.insert( lems.end(), d_curr_lemmas.begin(), d_curr_lemmas.end() ); + } } } diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index f058cf196..dfa0554d0 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -29,6 +29,7 @@ namespace quantifiers { class CegConjecture; class CegConjectureSingleInv; +class CegEntailmentInfer; class CegqiOutputSingleInv : public CegqiOutput { @@ -52,15 +53,15 @@ private: QuantifiersEngine * d_qe; CegConjecture * d_parent; CegConjectureSingleInvSol * d_sol; + CegEntailmentInfer * d_ei; //the instantiator + CegqiOutputSingleInv * d_cosi; CegInstantiator * d_cinst; //for recognizing templates for invariant synthesis Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ); // partially single invocation Node removeDeepEmbedding( Node n, std::vector< Node >& progs, std::vector< TypeNode >& types, int& type_valid, std::map< Node, Node >& visited ); Node addDeepEmbedding( Node n, std::map< Node, Node >& visited ); - //initialize next candidate si conjecture - void initializeNextSiConjecture(); //presolve void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ); void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); @@ -104,12 +105,15 @@ public: Node d_quant; // single invocation portion of quantified formula Node d_single_inv; + Node d_si_guard; // non-single invocation portion of quantified formula Node d_nsingle_inv; + Node d_ns_guard; // full version quantified formula Node d_full_inv; - // current guard - Node d_ns_guard; + Node d_full_guard; + //explanation for current single invocation conjecture + Node d_single_inv_exp; // transition relation version per program std::map< Node, Node > d_trans_pre; std::map< Node, Node > d_trans_post; @@ -120,7 +124,7 @@ public: std::map< Node, Node > d_prog_to_eval_op; public: //get the single invocation lemma(s) - void getInitialSingleInvLemma( Node guard, std::vector< Node >& lems ); + void getInitialSingleInvLemma( std::vector< Node >& lems ); //initialize void initialize( Node q ); //check @@ -134,11 +138,13 @@ public: // is single invocation bool isSingleInvocation() { return !d_single_inv.isNull(); } // is single invocation - bool isFullySingleInvocation() { return d_nsingle_inv.isNull(); } + bool isFullySingleInvocation() { return !d_single_inv.isNull() && d_nsingle_inv.isNull(); } //needs check bool needsCheck(); /** preregister conjecture */ void preregisterConjecture( Node q ); + //initialize next candidate si conjecture (if not fully single invocation) + void initializeNextSiConjecture(); }; // partitions any formulas given to it into single invocation/non-single invocation diff --git a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp new file mode 100644 index 000000000..18252e190 --- /dev/null +++ b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp @@ -0,0 +1,47 @@ +/********************* */ +/*! \file ce_guided_single_inv_ei.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief utility for inferring entailments for cegqi + ** + **/ + +#include "theory/quantifiers/ce_guided_single_inv_ei.h" +#include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/theory_engine.h" +#include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/quant_util.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace std; + +namespace CVC4 { + +CegEntailmentInfer::CegEntailmentInfer( QuantifiersEngine * qe, SingleInvocationPartition * sip ) : d_qe( qe ), d_sip( sip ) { + +} + +bool CegEntailmentInfer::getEntailedConjecture( Node& conj, Node& exp ) { + if( Trace.isOn("cegqi-ei") ){ + Trace("cegqi-ei") << "Infer new conjecture from : " << std::endl; + d_sip->debugPrint( "cegqi-ei" ); + Trace("cegqi-ei") << "Current assertions : " << std::endl; + d_qe->getTheoryEngine()->printAssertions("cegqi-ei"); + } + + + return false; +} + +} \ No newline at end of file diff --git a/src/theory/quantifiers/ce_guided_single_inv_ei.h b/src/theory/quantifiers/ce_guided_single_inv_ei.h new file mode 100644 index 000000000..0645c406a --- /dev/null +++ b/src/theory/quantifiers/ce_guided_single_inv_ei.h @@ -0,0 +1,43 @@ +/********************* */ +/*! \file ce_guided_single_inv_ei.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief utility for inferring entailments for cegqi + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_ENTAILMENT_INFERENCE_H +#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_ENTAILMENT_INFERENCE_H + + +#include "theory/quantifiers/ce_guided_single_inv.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class CegEntailmentInfer { +private: + QuantifiersEngine * d_qe; + SingleInvocationPartition * d_sip; +public: + CegEntailmentInfer( QuantifiersEngine * qe, SingleInvocationPartition * sip ); + virtual ~CegEntailmentInfer(){} + + bool getEntailedConjecture( Node& conj, Node& exp ); +}; + + +} +} +} + +#endif -- 2.30.2