PARSER_STATE->warning(ss.str());
}
// do nothing
- } else if(attr==":axiom" || attr==":conjecture" || attr==":fun-def" ||
- attr==":sygus" || attr==":synthesis") {
+ }
+ else if (attr==":axiom" || attr==":conjecture" || attr==":fun-def")
+ {
if(hasValue) {
std::stringstream ss;
ss << "warning: Attribute " << attr
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();
}
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 ){
<< " 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;
}
}
-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() ){
};
typedef expr::Attribute<QuantNameAttributeId, bool> QuantNameAttribute;
-/** Attribute true for quantifiers that are synthesis conjectures */
-struct SynthesisAttributeId {};
-typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute;
-
struct InstLevelAttributeId
{
};
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;
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
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 */
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())
{
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++ ){
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();
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
*/
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
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;
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 );
projects / cvc5.git / commitdiff