diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-02 14:44:04 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-02 14:44:04 -0600 |
commit | c8d0db7ee9c48fadd19227d472f60ff0089c34da (patch) | |
tree | ad8b35763f65e53f96cb9574f3392fd870c0c1e0 | |
parent | 356319744514261f06afced5ee975d49abe83eb4 (diff) |
Simplify sygus wrt miniscoping (#1634)
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 169 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.h | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_module.h | 17 |
5 files changed, 102 insertions, 117 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index ac0982c4e..3e71eedad 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -36,18 +36,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -// recursion is not an issue since OR nodes are flattened by the (quantifiers) rewriter -// this function is for sanity since solution correctness in SyGuS depends on fully miniscoping based on this function -void collectDisjuncts( Node n, std::vector< Node >& d ) { - if( n.getKind()==OR ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - collectDisjuncts( n[i], d ); - } - }else{ - d.push_back( n ); - } -} - CegConjecture::CegConjecture(QuantifiersEngine* qe) : d_qe(qe), d_ceg_si(new CegConjectureSingleInv(qe, this)), @@ -141,18 +129,12 @@ void CegConjecture::assign( Node q ) { if (d_qe->getQuantAttributes()->isSygus(q)) { - collectDisjuncts( d_base_inst, d_base_disj ); - Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; - //store the inner variables for each disjunct - for( unsigned j=0; j<d_base_disj.size(); j++ ){ - Trace("cegqi") << " " << j << " : " << d_base_disj[j] << std::endl; - d_inner_vars_disj.push_back( std::vector< Node >() ); - //if the disjunct is an existential, store it - if( d_base_disj[j].getKind()==NOT && d_base_disj[j][0].getKind()==FORALL ){ - for( unsigned k=0; k<d_base_disj[j][0][0].getNumChildren(); k++ ){ - d_inner_vars.push_back( d_base_disj[j][0][0][k] ); - d_inner_vars_disj[j].push_back( d_base_disj[j][0][0][k] ); - } + // if the base instantiation is an existential, store its variables + if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL) + { + for (const Node& v : d_base_inst[0][0]) + { + d_inner_vars.push_back(v); } } d_syntax_guided = true; @@ -247,6 +229,7 @@ void CegConjecture::doBasicCheck(std::vector< Node >& lems) { bool CegConjecture::needsRefinement() { return !d_ce_sk.empty(); } + void CegConjecture::doCheck(std::vector<Node>& lems) { Assert(d_master != nullptr); @@ -301,7 +284,6 @@ void CegConjecture::doCheck(std::vector<Node>& lems) return; } Assert( d_ce_sk.empty() ); - d_ce_sk.push_back( std::vector< Node >() ); }else{ if( !constructed_cand ){ return; @@ -310,30 +292,33 @@ void CegConjecture::doCheck(std::vector<Node>& lems) std::vector< Node > ic; ic.push_back( d_quant.negate() ); - std::vector< Node > d; - collectDisjuncts( inst, d ); - Assert( d.size()==d_base_disj.size() ); + //immediately skolemize inner existentials - for( unsigned i=0; i<d.size(); i++ ){ - Node dr = Rewriter::rewrite( d[i] ); - if( dr.getKind()==NOT && dr[0].getKind()==FORALL ){ - if( constructed_cand ){ - ic.push_back(d_qe->getSkolemize()->getSkolemizedBody(dr[0]).negate()); - } - if( sk_refine ){ - Assert( !isGround() ); - d_ce_sk.back().push_back( dr[0] ); - } - }else{ - if( constructed_cand ){ - ic.push_back( dr ); - if( !d_inner_vars_disj[i].empty() ){ - Trace("cegqi-debug") << "*** quantified disjunct : " << d[i] << " simplifies to " << dr << std::endl; - } - } - if( sk_refine ){ - d_ce_sk.back().push_back( Node::null() ); - } + Node instr = Rewriter::rewrite(inst); + if (instr.getKind() == NOT && instr[0].getKind() == FORALL) + { + if (constructed_cand) + { + ic.push_back(d_qe->getSkolemize()->getSkolemizedBody(instr[0]).negate()); + } + if (sk_refine) + { + Assert(!isGround()); + d_ce_sk.push_back(instr[0]); + } + } + else + { + if (constructed_cand) + { + // use the instance itself + ic.push_back(instr); + } + if (sk_refine) + { + // we add null so that one test of the conjecture for the empty + // substitution is checked + d_ce_sk.push_back(Node::null()); } } if( constructed_cand ){ @@ -360,69 +345,45 @@ void CegConjecture::doRefine( std::vector< Node >& lems ){ std::vector< Node > sk_vars; std::vector< Node > sk_subs; //collect the substitution over all disjuncts - for( unsigned k=0; k<d_ce_sk[0].size(); k++ ){ - Node ce_q = d_ce_sk[0][k]; - if( !ce_q.isNull() ){ - Assert( !d_inner_vars_disj[k].empty() ); - std::vector<Node> skolems; - d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems); - Assert(d_inner_vars_disj[k].size() == skolems.size()); - std::vector< Node > model_values; - getModelValues(skolems, model_values); - sk_vars.insert( sk_vars.end(), d_inner_vars_disj[k].begin(), d_inner_vars_disj[k].end() ); - sk_subs.insert( sk_subs.end(), model_values.begin(), model_values.end() ); - }else{ - if( !d_inner_vars_disj[k].empty() ){ - //denegrate case : quantified disjunct was trivially true and does not need to be refined - //add trivial substitution (in case we need substitution for previous cex's) - for( unsigned i=0; i<d_inner_vars_disj[k].size(); i++ ){ - sk_vars.push_back( d_inner_vars_disj[k][i] ); - sk_subs.push_back( getModelValue( d_inner_vars_disj[k][i] ) ); // will return dummy value - } - } - } - } - - //for conditional evaluation + Node ce_q = d_ce_sk[0]; + if (!ce_q.isNull()) + { + std::vector<Node> skolems; + d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems); + Assert(d_inner_vars.size() == skolems.size()); + std::vector<Node> model_values; + getModelValues(skolems, model_values); + sk_vars.insert(sk_vars.end(), d_inner_vars.begin(), d_inner_vars.end()); + sk_subs.insert(sk_subs.end(), model_values.begin(), model_values.end()); + } + else + { + Assert(d_inner_vars.empty()); + } + std::vector< Node > lem_c; - Assert( d_ce_sk[0].size()==d_base_disj.size() ); - std::vector< Node > inst_cond_c; Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl; - for( unsigned k=0; k<d_ce_sk[0].size(); k++ ){ - Node ce_q = d_ce_sk[0][k]; - Trace("cegqi-refine-debug") << " For counterexample point, disjunct " << k << " : " << ce_q << " " << d_base_disj[k] << std::endl; - Node c_disj; - if( !ce_q.isNull() ){ - Assert( d_base_disj[k].getKind()==kind::NOT && d_base_disj[k][0].getKind()==kind::FORALL ); - c_disj = d_base_disj[k][0][1]; - }else{ - if( d_inner_vars_disj[k].empty() ){ - c_disj = d_base_disj[k].negate(); - }else{ - //denegrate case : quantified disjunct was trivially true and does not need to be refined - Trace("cegqi-refine-debug") << "*** skip " << d_base_disj[k] << std::endl; - } - } - if( !c_disj.isNull() ){ - //compute the body, inst_cond - //standard CEGIS refinement : plug in values, assert that d_candidates must satisfy entire specification - lem_c.push_back( c_disj ); - } + Trace("cegqi-refine-debug") + << " For counterexample point : " << ce_q << std::endl; + Node base_lem; + if (!ce_q.isNull()) + { + Assert(d_base_inst.getKind() == kind::NOT + && d_base_inst[0].getKind() == kind::FORALL); + base_lem = d_base_inst[0][1]; } + else + { + base_lem = d_base_inst.negate(); + } + Assert( sk_vars.size()==sk_subs.size() ); - - Node base_lem = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( AND, lem_c ); - + Trace("cegqi-refine") << "doRefine : construct and finalize lemmas..." << std::endl; - - + base_lem = base_lem.substitute( sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end() ); base_lem = Rewriter::rewrite( base_lem ); - d_master->registerRefinementLemma(base_lem); - - Node lem = - NodeManager::currentNM()->mkNode(OR, getGuard().negate(), base_lem); - lems.push_back( lem ); + d_master->registerRefinementLemma(sk_vars, base_lem, lems); d_ce_sk.clear(); } diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 9f3335ee2..8ab871d08 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -160,14 +160,14 @@ private: * this is the formula exists y. P( d_candidates, y ). */ Node d_base_inst; - /** expand base inst to disjuncts */ - std::vector< Node > d_base_disj; /** list of variables on inner quantification */ std::vector< Node > d_inner_vars; - std::vector< std::vector< Node > > d_inner_vars_disj; - /** current extential quantifeirs whose couterexamples we must refine */ - std::vector< std::vector< Node > > d_ce_sk; - + /** + * The set of current existentially quantified formulas whose couterexamples + * we must refine. This may be added to during calls to doCheck(). The model + * values for skolems of these formulas are analyzed during doRefine(). + */ + std::vector<Node> d_ce_sk; /** the asserted (negated) conjecture */ Node d_quant; diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index a571c85fb..b778b90be 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -150,9 +150,19 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, return true; } -void Cegis::registerRefinementLemma(Node lem) +void Cegis::registerRefinementLemma(const std::vector<Node>& vars, + Node lem, + std::vector<Node>& lems) { d_refinement_lemmas.push_back(lem); + // Make the refinement lemma and add it to lems. + // This lemma is guarded by the parent's guard, which has the semantics + // "this conjecture has a solution", hence this lemma states: + // if the parent conjecture has a solution, it satisfies the specification + // for the given concrete point. + Node rlem = + NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem); + lems.push_back(rlem); } void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 2cb668fa1..358b50536 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -56,8 +56,13 @@ class Cegis : public SygusModule const std::vector<Node>& candidates, std::vector<Node>& candidate_values, std::vector<Node>& lems) override; - /** register refinement lemma */ - virtual void registerRefinementLemma(Node lem) override; + /** register refinement lemma + * + * This function stores lem as a refinement lemma, and adds it to lems. + */ + virtual void registerRefinementLemma(const std::vector<Node>& vars, + Node lem, + std::vector<Node>& lems) override; private: /** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */ diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 230ea7a61..0a3fa9995 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -81,7 +81,7 @@ class SygusModule * If this function returns true, it adds to candidate_values a list of terms * of the same length and type as candidates that are candidate solutions * to the synthesis conjecture in question. This candidate { v } will then be - * tested by testing the (un)satisfiablity of P( v, k' ) for fresh k' by the + * tested by testing the (un)satisfiablity of P( v, cex ) for fresh cex by the * caller. * * This function may also add lemmas to lems, which are sent out as lemmas @@ -102,10 +102,19 @@ class SygusModule * value { v } to candidate_values for candidates = { k }. This function is * called if the base instantiation of the synthesis conjecture has a model * under this substitution. In particular, in the above example, this function - * is called when the refinement lemma P( v, k' ) has a model. The argument - * lem in the call to this function is P( v, k' ). + * is called when the refinement lemma P( v, cex ) has a model M. In calls to + * this function, the argument vars is cex and lem is P( k, cex^M ). + * + * This function may also add lemmas to lems, which are sent out as lemmas + * on the output channel of quantifiers by the caller. For an example of + * such lemmas, see Cegis::registerRefinementLemma. */ - virtual void registerRefinementLemma(Node lem) {} + virtual void registerRefinementLemma(const std::vector<Node>& vars, + Node lem, + std::vector<Node>& lems) + { + } + protected: /** reference to quantifier engine */ QuantifiersEngine* d_qe; |