diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 23 |
1 files changed, 0 insertions, 23 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() ){ |