diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-07-18 13:08:56 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-07-18 13:08:56 -0500 |
| commit | d0ec84da973d3ba7054b61fd620a1eba0d459a48 (patch) | |
| tree | 0e7c4882b35ad327d0956f7b0887437896cb6dd1 /src/theory/quantifiers/quantifiers_attributes.cpp | |
| parent | 004bcc12f592991db93ffd92cfb5925940c80980 (diff) | |
Fix quantifier instantiation bug in cbqi, add default priorities in rewrite engine.
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 5bdce5fac..909c9c388 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -32,6 +32,10 @@ void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){ Trace("quant-attr") << "Set conjecture " << n << std::endl; ConjectureAttribute ca; n.setAttribute( ca, true ); + }else if( attr=="rr_priority" ){ + //Trace("quant-attr") << "Set rr priority " << n << std::endl; + //RrPriorityAttribute rra; + } }else{ for( size_t i=0; i<n.getNumChildren(); i++ ){ |