From: Andrew Reynolds Date: Tue, 4 Sep 2018 16:43:39 +0000 (-0500) Subject: Refactor ceg conjecture initialization (#2411) X-Git-Tag: cvc5-1.0.0~4691 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0daf3f9cd0939202d28f69aaca1757fa001924db;p=cvc5.git Refactor ceg conjecture initialization (#2411) --- diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index e3057da29..1d070417e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -70,6 +70,7 @@ void CegConjecture::assign( Node q ) { Assert( q.getKind()==FORALL ); Trace("cegqi") << "CegConjecture : assign : " << q << std::endl; d_quant = q; + NodeManager* nm = NodeManager::currentNM(); // pre-simplify the quantified formula based on the process utility d_simp_quant = d_ceg_proc->preSimplify(d_quant); @@ -163,10 +164,19 @@ void CegConjecture::assign( Node q ) { } // initialize the guard - if (d_ceg_si->getGuard().isNull()) + d_feasible_guard = nm->mkSkolem("G", nm->booleanType()); + d_feasible_guard = Rewriter::rewrite(d_feasible_guard); + d_feasible_guard = d_qe->getValuation().ensureLiteral(d_feasible_guard); + AlwaysAssert(!d_feasible_guard.isNull()); + // this must be called, both to ensure that the feasible guard is + // decided on with true polariy, but also to ensure that output channel + // has been used on this call to check. + d_qe->getOutputChannel().requirePhase(d_feasible_guard, true); + + if (isSingleInvocation()) { std::vector< Node > lems; - d_ceg_si->getInitialSingleInvLemma( lems ); + d_ceg_si->getInitialSingleInvLemma(d_feasible_guard, lems); for( unsigned i=0; igetOutputChannel().lemma( lems[i] ); @@ -176,10 +186,9 @@ void CegConjecture::assign( Node q ) { } } } - Assert( !getGuard().isNull() ); - Node gneg = getGuard().negate(); + Node gneg = d_feasible_guard.negate(); for( unsigned i=0; imkNode( OR, gneg, guarded_lemmas[i] ); + Node lem = nm->mkNode(OR, gneg, guarded_lemmas[i]); Trace("cegqi-lemma") << "Cegqi::Lemma : initial (guarded) lemma : " << lem << std::endl; d_qe->getOutputChannel().lemma( lem ); } @@ -187,7 +196,7 @@ void CegConjecture::assign( Node q ) { Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl; } -Node CegConjecture::getGuard() { return d_ceg_si->getGuard(); } +Node CegConjecture::getGuard() const { return d_feasible_guard; } bool CegConjecture::isSingleInvocation() const { return d_ceg_si->isSingleInvocation(); @@ -196,20 +205,25 @@ bool CegConjecture::isSingleInvocation() const { bool CegConjecture::needsCheck( std::vector< Node >& lem ) { if( isSingleInvocation() && !d_ceg_si->needsCheck() ){ return false; - }else{ - bool value; - 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 ); + } + bool value; + Assert(!d_feasible_guard.isNull()); + // non or fully single invocation : look at guard only + if (d_qe->getValuation().hasSatValue(d_feasible_guard, value)) + { + if (!value) + { + Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl; + return false; } - return true; } + else + { + Trace("cegqi-warn") << "WARNING: Guard " << d_feasible_guard + << " is not assigned!" << std::endl; + Assert(false); + } + return true; } @@ -563,7 +577,7 @@ Node CegConjecture::getStreamGuardedLemma(Node n) const Node CegConjecture::getNextDecisionRequest( unsigned& priority ) { // first, must try the guard // which denotes "this conjecture is feasible" - Node feasible_guard = getGuard(); + Node feasible_guard = d_feasible_guard; bool value; if( !d_qe->getValuation().hasSatValue( feasible_guard, value ) ) { priority = 0; diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 25f063e06..48d307f1e 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -97,8 +97,11 @@ public: * module to get synthesis solutions. */ void getSynthSolutions(std::map& sol_map, bool singleInvocation); - /** get guard, this is "G" in Figure 3 of Reynolds et al CAV 2015 */ - Node getGuard(); + /** + * The feasible guard whose semantics are "this conjecture is feasiable". + * This is "G" in Figure 3 of Reynolds et al CAV 2015. + */ + Node getGuard() const; /** is ground */ bool isGround() { return d_inner_vars.empty(); } /** are we using single invocation techniques */ @@ -132,6 +135,8 @@ public: private: /** reference to quantifier engine */ QuantifiersEngine * d_qe; + /** The feasible guard. */ + Node d_feasible_guard; /** single invocation utility */ std::unique_ptr d_ceg_si; /** utility for static preprocessing and analysis of conjectures */ diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index 1e0b36a3c..83a576d37 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -59,10 +59,10 @@ void CegInstantiation::check(Theory::Effort e, QEffort quant_e) d_waiting_conj = Node::null(); if (!d_conj->isAssigned()) { - if (!assignConjecture(q)) - { - return; - } + assignConjecture(q); + // assign conjecture always uses the output channel, we return and + // re-check here. + return; } } unsigned echeck = diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 39c3baf5c..7d8db8c03 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -49,12 +49,12 @@ CegConjectureSingleInv::CegConjectureSingleInv(QuantifiersEngine* qe, d_sip(new SingleInvocationPartition), d_sol(new CegConjectureSingleInvSol(qe)), d_cosi(new CegqiOutputSingleInv(this)), - d_cinst(NULL), + d_cinst(new CegInstantiator(d_qe, d_cosi, false, false)), d_c_inst_match_trie(NULL), - d_single_invocation(false) { - // third and fourth arguments set to (false,false) until we have solution - // reconstruction for delta and infinity - d_cinst = new CegInstantiator(d_qe, d_cosi, false, false); + d_single_invocation(false) +{ + // The third and fourth arguments of d_cosi set to (false,false) until we have + // solution reconstruction for delta and infinity. if (options::incrementalSolving()) { d_c_inst_match_trie = new inst::CDInstMatchTrie(qe->getUserContext()); @@ -65,51 +65,53 @@ CegConjectureSingleInv::~CegConjectureSingleInv() { if (d_c_inst_match_trie) { delete d_c_inst_match_trie; } - delete d_cinst; delete d_cosi; delete d_sol; // (new CegConjectureSingleInvSol(qe)), delete d_sip; // d_sip(new SingleInvocationPartition), } -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; - if( d_single_inv.getKind()==FORALL ){ - for( unsigned i=0; imkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" ); - d_single_inv_var.push_back( d_single_inv[0][i] ); - d_single_inv_sk.push_back( k ); - d_single_inv_sk_index[k] = i; - } - inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); - }else{ - inst = d_single_inv; - } - inst = TermUtil::simpleNegate( inst ); - Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; - - //register with the instantiator - 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; +void CegConjectureSingleInv::getInitialSingleInvLemma(Node g, + std::vector& lems) +{ + Assert(!g.isNull()); + Assert(!d_single_inv.isNull()); + // make for new var/sk + d_single_inv_var.clear(); + d_single_inv_sk.clear(); + Node inst; + NodeManager* nm = NodeManager::currentNM(); + if (d_single_inv.getKind() == FORALL) + { + for (unsigned i = 0, size = d_single_inv[0].getNumChildren(); i < size; i++) + { + std::stringstream ss; + ss << "k_" << d_single_inv[0][i]; + Node k = nm->mkSkolem(ss.str(), + d_single_inv[0][i].getType(), + "single invocation function skolem"); + d_single_inv_var.push_back(d_single_inv[0][i]); + d_single_inv_sk.push_back(k); + d_single_inv_sk_index[k] = i; } - d_cinst = new CegInstantiator( d_qe, d_cosi, false, false ); - d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk ); + inst = d_single_inv[1].substitute(d_single_inv_var.begin(), + d_single_inv_var.end(), + d_single_inv_sk.begin(), + d_single_inv_sk.end()); } + else + { + inst = d_single_inv; + } + inst = TermUtil::simpleNegate(inst); + Trace("cegqi-si") << "Single invocation initial lemma : " << inst + << std::endl; + + // register with the instantiator + Node ginst = nm->mkNode(OR, g.negate(), inst); + lems.push_back(ginst); + // make and register the instantiator + d_cinst.reset(new CegInstantiator(d_qe, d_cosi, false, false)); + d_cinst->registerCounterexampleLemma(lems, d_single_inv_sk); } void CegConjectureSingleInv::initialize( Node q ) { diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 00b50a4a1..09829e894 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -149,7 +149,7 @@ class CegConjectureSingleInv { // the instantiator's output channel CegqiOutputSingleInv* d_cosi; // the instantiator - CegInstantiator* d_cinst; + std::unique_ptr d_cinst; // list of skolems for each argument of programs std::vector d_single_inv_arg_sk; @@ -188,7 +188,6 @@ class CegConjectureSingleInv { bool d_single_invocation; // single invocation portion of quantified formula Node d_single_inv; - Node d_si_guard; // transition relation version per program std::map< Node, Node > d_trans_pre; std::map< Node, Node > d_trans_post; @@ -203,11 +202,17 @@ class CegConjectureSingleInv { // get simplified conjecture Node getSimplifiedConjecture() { return d_simp_quant; } - // get single invocation guard - Node getGuard() { return d_si_guard; } public: - //get the single invocation lemma(s) - void getInitialSingleInvLemma( std::vector< Node >& lems ); + /** get the single invocation lemma(s) + * + * This adds lemmas to lem that initializes this class for doing + * counterexample-guided instantiation for the synthesis conjecture. These + * lemmas correspond to the negation of the body of the (anti-skolemized) + * form of the conjecture for fresh skolems. + * + * Argument g is guard, for which all the above lemmas are guarded. + */ + void getInitialSingleInvLemma(Node g, std::vector& lems); // initialize this class for synthesis conjecture q void initialize( Node q ); /** finish initialize