From c8d0db7ee9c48fadd19227d472f60ff0089c34da Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 2 Mar 2018 14:44:04 -0600 Subject: [PATCH] Simplify sygus wrt miniscoping (#1634) --- .../sygus/ce_guided_conjecture.cpp | 169 +++++++----------- .../quantifiers/sygus/ce_guided_conjecture.h | 12 +- src/theory/quantifiers/sygus/cegis.cpp | 12 +- src/theory/quantifiers/sygus/cegis.h | 9 +- 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; igetQuantAttributes()->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() ); - //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& lems) { bool CegConjecture::needsRefinement() { return !d_ce_sk.empty(); } + void CegConjecture::doCheck(std::vector& lems) { Assert(d_master != nullptr); @@ -301,7 +284,6 @@ void CegConjecture::doCheck(std::vector& 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& 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; igetSkolemize()->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 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 skolems; + d_qe->getSkolemize()->getSkolemConstants(ce_q, skolems); + Assert(d_inner_vars.size() == skolems.size()); + std::vector 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; kmkNode( 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 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& enums, return true; } -void Cegis::registerRefinementLemma(Node lem) +void Cegis::registerRefinementLemma(const std::vector& vars, + Node lem, + std::vector& 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& 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& candidates, std::vector& candidate_values, std::vector& 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& vars, + Node lem, + std::vector& 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& vars, + Node lem, + std::vector& lems) + { + } + protected: /** reference to quantifier engine */ QuantifiersEngine* d_qe; -- 2.30.2