diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 23 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 38 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.h | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_instantiation.cpp | 86 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 1 |
6 files changed, 63 insertions, 116 deletions
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<Rational>().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<QuantNameAttributeId, bool> 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; i<lems.size(); i++ ){ @@ -205,9 +187,7 @@ void CegConjecture::assign( Node q ) { Trace("cegqi") << "...finished, single invocation = " << isSingleInvocation() << std::endl; } -Node CegConjecture::getGuard() { - return !d_syntax_guided ? d_nsg_guard : d_ceg_si->getGuard(); -} +Node CegConjecture::getGuard() { return d_ceg_si->getGuard(); } bool CegConjecture::isSingleInvocation() const { return d_ceg_si->isSingleInvocation(); diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 0b6f0e1a8..25f063e06 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -101,8 +101,6 @@ public: Node getGuard(); /** is ground */ bool isGround() { return d_inner_vars.empty(); } - /** does this conjecture correspond to a syntax-guided synthesis input */ - bool isSyntaxGuided() const { return d_syntax_guided; } /** are we using single invocation techniques */ bool isSingleInvocation() const; /** preregister conjecture @@ -259,14 +257,6 @@ private: */ void printAndContinueStream(); //-------------------------------- end sygus stream - //-------------------------------- non-syntax guided (deprecated) - /** Whether we are syntax-guided (e.g. was the input in SyGuS format). - * This includes SyGuS inputs where no syntactic restrictions are provided. - */ - bool d_syntax_guided; - /** the guard for non-syntax-guided synthesis */ - Node d_nsg_guard; - //-------------------------------- end non-syntax guided (deprecated) /** candidate rewrite objects for each program variable * * This is used for the sygusRewSynth() option to synthesize new candidate diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index 378c2f1d7..b3cb98bc5 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -267,52 +267,52 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( !conj->needsRefinement() ){ Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl; - if( conj->isSyntaxGuided() ){ - std::vector< Node > clems; - conj->doSingleInvCheck( clems ); - if( !clems.empty() ){ - d_last_inst_si = true; - for( unsigned j=0; j<clems.size(); j++ ){ - Trace("cegqi-lemma") << "Cegqi::Lemma : single invocation instantiation : " << clems[j] << std::endl; - d_quantEngine->addLemma( 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; i<cclems.size(); i++ ){ - Node lem = cclems[i]; - 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{ - //this may happen if we eagerly unfold, simplify to true - Trace("cegqi-engine-debug") - << " ...FAILED to add candidate!" << std::endl; - } + std::vector<Node> 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<Node> 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 ); |