diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.cpp')
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index f5ebb33b1..0e6eb1581 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -64,24 +64,24 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve QuantNameAttribute qna; n.setAttribute(qna, true); } else if (attr == "sygus-synth-grammar") { - Assert( node_values.size()==1 ); + Assert(node_values.size() == 1); Trace("quant-attr-debug") << "Set sygus synth grammar " << n << " to " << node_values[0] << std::endl; SygusSynthGrammarAttribute ssg; n.setAttribute(ssg, node_values[0]); }else if( attr=="sygus-synth-fun-var-list" ){ - Assert( node_values.size()==1 ); + Assert(node_values.size() == 1); 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=="quant-inst-max-level" ){ - Assert( node_values.size()==1 ); + Assert(node_values.size() == 1); uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong(); Trace("quant-attr-debug") << "Set instantiation level " << n << " to " << lvl << std::endl; QuantInstLevelAttribute qila; n.setAttribute( qila, lvl ); }else if( attr=="rr-priority" ){ - Assert( node_values.size()==1 ); + Assert(node_values.size() == 1); uint64_t lvl = node_values[0].getConst<Rational>().getNumerator().getLong(); Trace("quant-attr-debug") << "Set rewrite rule priority " << n << " to " << lvl << std::endl; RrPriorityAttribute rrpa; @@ -296,7 +296,7 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){ } if( avar.getKind()==REWRITE_RULE ){ Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl; - Assert( i==0 ); + Assert(i == 0); qa.d_rr = avar; } } |