Significant work on bounded integer quantification to handle non-trivial bounds. Refactoring of InstConstantAttribute to be internal to TermDb.

1 files changed, 3 insertions, 3 deletions

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 9843cd09e..c68623baa 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -65,7 +65,7 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) {
 
 void TheoryQuantifiers::preRegisterTerm(TNode n) {
   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
-  if( n.getKind()==FORALL && !n.hasAttribute(InstConstantAttribute()) ){
+  if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){
     getQuantifiersEngine()->registerQuantifier( n );
   }
 }
@@ -149,7 +149,7 @@ Node TheoryQuantifiers::getNextDecisionRequest(){
 
 void TheoryQuantifiers::assertUniversal( Node n ){
   Assert( n.getKind()==FORALL );
-  if( !n.hasAttribute(InstConstantAttribute()) ){
+  if( !TermDb::hasInstConstAttr(n) ){
     getQuantifiersEngine()->registerQuantifier( n );
     getQuantifiersEngine()->assertNode( n );
   }
@@ -157,7 +157,7 @@ void TheoryQuantifiers::assertUniversal( Node n ){
 
 void TheoryQuantifiers::assertExistential( Node n ){
   Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
-  if( !n[0].hasAttribute(InstConstantAttribute()) ){
+  if( !TermDb::hasInstConstAttr(n[0]) ){
     if( d_skolemized.find( n )==d_skolemized.end() ){
       Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] );
       NodeBuilder<> nb(kind::OR);