From bf863b1f3cee791585e2c04e5f40afcadcdf113c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 20 Aug 2018 18:40:40 -0500 Subject: Remove support for prototype (non-sygus) synthesis (#2338) --- src/theory/quantifiers/quantifiers_attributes.cpp | 23 ------ src/theory/quantifiers/quantifiers_attributes.h | 21 +++--- .../quantifiers/sygus/ce_guided_conjecture.cpp | 38 +++------- .../quantifiers/sygus/ce_guided_conjecture.h | 10 --- .../quantifiers/sygus/ce_guided_instantiation.cpp | 86 +++++++++++----------- src/theory/quantifiers/theory_quantifiers.cpp | 1 - 6 files changed, 63 insertions(+), 116 deletions(-) (limited to 'src/theory') diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index e8e93dc0f..dde6dc4a9 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -74,10 +74,6 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve Trace("quant-attr-debug") << "Set sygus synth fun var list to " << n << " to " << node_values[0] << std::endl; SygusSynthFunVarListAttribute ssfvla; n.setAttribute( ssfvla, node_values[0] ); - }else if( attr=="synthesis" ){ - Trace("quant-attr-debug") << "Set synthesis " << n << std::endl; - SynthesisAttribute ca; - n.setAttribute( ca, true ); }else if( attr=="quant-inst-max-level" ){ Assert( node_values.size()==1 ); uint64_t lvl = node_values[0].getConst().getNumerator().getLong(); @@ -238,12 +234,6 @@ void QuantAttributes::computeAttributes( Node q ) { } d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); } - if( d_qattr[q].d_synthesis ){ - if( d_quantEngine->getCegInstantiation()==NULL ){ - Trace("quant-warn") << "WARNING : ceg instantiation is null, and we have : " << q << std::endl; - } - d_quantEngine->setOwner( q, d_quantEngine->getCegInstantiation(), 2 ); - } } void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ @@ -282,10 +272,6 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ << " for " << q << std::endl; qa.d_name = avar; } - if( avar.getAttribute(SynthesisAttribute()) ){ - Trace("quant-attr") << "Attribute : synthesis : " << q << std::endl; - qa.d_synthesis = true; - } if( avar.hasAttribute(QuantInstLevelAttribute()) ){ qa.d_qinstLevel = avar.getAttribute(QuantInstLevelAttribute()); Trace("quant-attr") << "Attribute : quant inst level " << qa.d_qinstLevel << " : " << q << std::endl; @@ -355,15 +341,6 @@ bool QuantAttributes::isSygus( Node q ) { } } -bool QuantAttributes::isSynthesis( Node q ) { - std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); - if( it==d_qattr.end() ){ - return false; - }else{ - return it->second.d_synthesis; - } -} - int QuantAttributes::getQuantInstLevel( Node q ) { std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); if( it==d_qattr.end() ){ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 16de5fd2e..918269bbe 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -57,10 +57,6 @@ struct QuantNameAttributeId }; typedef expr::Attribute QuantNameAttribute; -/** Attribute true for quantifiers that are synthesis conjectures */ -struct SynthesisAttributeId {}; -typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute; - struct InstLevelAttributeId { }; @@ -87,8 +83,17 @@ namespace quantifiers { struct QAttributes { public: - QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false), - d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){} + QAttributes() + : d_hasPattern(false), + d_conjecture(false), + d_axiom(false), + d_sygus(false), + d_rr_priority(-1), + d_qinstLevel(-1), + d_quant_elim(false), + d_quant_elim_partial(false) + { + } ~QAttributes(){} /** does the quantified formula have a pattern? */ bool d_hasPattern; @@ -104,8 +109,6 @@ struct QAttributes Node d_fundef_f; /** is this formula marked as a sygus conjecture? */ bool d_sygus; - /** is this formula marked as a synthesis (non-sygus) conjecture? */ - bool d_synthesis; /** if a rewrite rule, then this is the priority value for the rewrite rule */ int d_rr_priority; /** stores the maximum instantiation level allowed for this quantified formula @@ -192,8 +195,6 @@ public: bool isFunDef( Node q ); /** is sygus conjecture */ bool isSygus( Node q ); - /** is synthesis conjecture */ - bool isSynthesis( Node q ); /** get instantiation level */ int getQuantInstLevel( Node q ); /** get rewrite rule priority */ diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 31a76d933..e3057da29 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -50,8 +50,7 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe) d_master(nullptr), d_set_ce_sk_vars(false), d_repair_index(0), - d_refine_count(0), - d_syntax_guided(false) + d_refine_count(0) { if (options::sygusSymBreakPbe() || options::sygusUnifPbe()) { @@ -153,36 +152,19 @@ void CegConjecture::assign( Node q ) { Assert(d_master != nullptr); } - if (d_qe->getQuantAttributes()->isSygus(q)) + Assert(d_qe->getQuantAttributes()->isSygus(q)); + // if the base instantiation is an existential, store its variables + if (d_base_inst.getKind() == NOT && d_base_inst[0].getKind() == FORALL) { - // 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]) { - for (const Node& v : d_base_inst[0][0]) - { - d_inner_vars.push_back(v); - } + d_inner_vars.push_back(v); } - d_syntax_guided = true; - } - else if (d_qe->getQuantAttributes()->isSynthesis(q)) - { - d_syntax_guided = false; - }else{ - Assert( false ); } // initialize the guard - if( !d_syntax_guided ){ - if( d_nsg_guard.isNull() ){ - d_nsg_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); - d_nsg_guard = d_qe->getValuation().ensureLiteral( d_nsg_guard ); - AlwaysAssert( !d_nsg_guard.isNull() ); - d_qe->getOutputChannel().requirePhase( d_nsg_guard, true ); - // negated base as a guarded lemma - guarded_lemmas.push_back( d_base_inst.negate() ); - } - }else if( d_ceg_si->getGuard().isNull() ){ + if (d_ceg_si->getGuard().isNull()) + { std::vector< Node > lems; d_ceg_si->getInitialSingleInvLemma( lems ); for( unsigned i=0; iisSyntaxGuided() ){ - std::vector< Node > clems; - conj->doSingleInvCheck( clems ); - if( !clems.empty() ){ - d_last_inst_si = true; - for( unsigned j=0; jaddLemma( clems[j] ); - } - d_statistics.d_cegqi_si_lemmas += clems.size(); - Trace("cegqi-engine") << " ...try single invocation." << std::endl; - return; - } - - Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; - std::vector< Node > cclems; - conj->doCheck(cclems); - bool addedLemma = false; - for( unsigned i=0; iaddLemma( lem ) ){ - ++(d_statistics.d_cegqi_lemmas_ce); - addedLemma = true; - }else{ - //this may happen if we eagerly unfold, simplify to true - Trace("cegqi-engine-debug") - << " ...FAILED to add candidate!" << std::endl; - } + std::vector clems; + conj->doSingleInvCheck(clems); + if (!clems.empty()) + { + d_last_inst_si = true; + for (const Node& lem : clems) + { + Trace("cegqi-lemma") + << "Cegqi::Lemma : single invocation instantiation : " << lem + << std::endl; + d_quantEngine->addLemma(lem); } - if( addedLemma ){ - Trace("cegqi-engine") << " ...check for counterexample." << std::endl; + d_statistics.d_cegqi_si_lemmas += clems.size(); + Trace("cegqi-engine") << " ...try single invocation." << std::endl; + return; + } + + Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; + std::vector cclems; + conj->doCheck(cclems); + bool addedLemma = false; + for (const Node& lem : cclems) + { + d_last_inst_si = false; + Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem + << std::endl; + if (d_quantEngine->addLemma(lem)) + { + ++(d_statistics.d_cegqi_lemmas_ce); + addedLemma = true; }else{ - if( conj->needsRefinement() ){ - //immediately go to refine candidate - checkCegConjecture( conj ); - return; - } - } + // this may happen if we eagerly unfold, simplify to true + Trace("cegqi-engine-debug") + << " ...FAILED to add candidate!" << std::endl; + } + } + if (addedLemma) + { + Trace("cegqi-engine") << " ...check for counterexample." << std::endl; }else{ - Assert( aq==q ); - Trace("cegqi-engine") << " *** Check candidate phase (non-SyGuS)." << std::endl; - std::vector< Node > lems; - conj->doBasicCheck(lems); - Assert(lems.empty()); + if (conj->needsRefinement()) + { + // immediately go to refine candidate + checkCegConjecture(conj); + return; + } } }else{ Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl; diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 842671a5e..2ab45aa96 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -47,7 +47,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output out.handleUserAttribute("quant-name", this); out.handleUserAttribute("sygus-synth-grammar", this); out.handleUserAttribute( "sygus-synth-fun-var-list", this ); - out.handleUserAttribute( "synthesis", this ); out.handleUserAttribute( "quant-inst-max-level", this ); out.handleUserAttribute( "rr-priority", this ); out.handleUserAttribute( "quant-elim", this ); -- cgit v1.2.3