Minor fixes and improvements to purify quant, relational triggers.

8 files changed, 58 insertions, 30 deletions

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 2b4854305..f4e8861dc 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -238,21 +238,19 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi
       Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern;
       Node t_match;
       if( pol ){
-        if (pat.getKind()==GT) {
-          Node r = NodeManager::currentNM()->mkConst( Rational(-1) );
-          t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
+        if( pat.getKind()==GT ){
+          t_match = NodeManager::currentNM()->mkNode(MINUS, t, qe->getTermDatabase()->d_one);
         }else{
           t_match = t;
         }
       }else{
-        if(pat.getKind()==EQUAL) {
-          Node r = NodeManager::currentNM()->mkConst( Rational(1) );
-          t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
+        if( pat.getKind()==EQUAL ){
+          Assert( t.getType().isReal() );
+          t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one);
         }else if( pat.getKind()==IFF ){
-          t_match = NodeManager::currentNM()->mkConst( !q->areEqual( NodeManager::currentNM()->mkConst(true), t ) );
+          t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) );
         }else if( pat.getKind()==GEQ ){
-          Node r = NodeManager::currentNM()->mkConst( Rational(1) );
-          t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
+          t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one);
         }else if( pat.getKind()==GT ){
           t_match = t;
         }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 8f055473d..1e2ac21a0 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -83,10 +83,10 @@ bool QuantifiersRewriter::isCube( Node n ){
   }
 }
 
-int QuantifiersRewriter::getPurifyId( Node n, std::vector< Node >& args ){
+int QuantifiersRewriter::getPurifyId( Node n ){
   if( inst::Trigger::isAtomicTriggerKind( n.getKind() ) ){
     return 1;
-  }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE || !TermDb::containsTerms( n, args ) ){
+  }else if( TermDb::isBoolConnective( n.getKind() ) || n.getKind()==EQUAL || n.getKind()==BOUND_VARIABLE || !TermDb::hasBoundVarAttr( n ) ){
     return 0;
   }else{
     return -1;
@@ -768,7 +768,7 @@ Node QuantifiersRewriter::computeProcessIte( Node body, Node ipl ){
   return body;
 }
 
-bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ) {
+bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ) {
   if( TermDb::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){
     return false;
   }else{
@@ -776,7 +776,7 @@ bool QuantifiersRewriter::isVariableElim( Node v, Node s, std::vector< Node >& a
       std::map< Node, std::vector< int > >::iterator it = var_parent.find( v );
       if( it!=var_parent.end() ){
         Assert( !it->second.empty() );
-        int id = getPurifyId( s, args );
+        int id = getPurifyId( s );
         return it->second.size()==1 && it->second[0]==id;
       }
     }
@@ -790,7 +790,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
     for( unsigned i=0; i<2; i++ ){
       std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[i] );
       if( ita!=args.end() ){
-        if( isVariableElim( lit[i], lit[1-i], args, var_parent ) ){
+        if( isVariableElim( lit[i], lit[1-i], var_parent ) ){
           Trace("var-elim-quant") << "Variable eliminate based on equality : " << lit[i] << " -> " << lit[1-i] << std::endl;
           vars.push_back( lit[i] );
           subs.push_back( lit[1-i] );
@@ -809,7 +809,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
             Node veq_c;
             Node val;
             int ires = QuantArith::isolate( itm->first, msum, veq_c, val, EQUAL );
-            if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, args, var_parent ) ){
+            if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val, var_parent ) ){
               Trace("var-elim-quant") << "Variable eliminate based on solved equality : " << itm->first << " -> " << val << std::endl;
               vars.push_back( itm->first );
               subs.push_back( val );
@@ -1689,17 +1689,17 @@ Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args,
     return it->second;
   }else{
     Node ret = body;
-    if( body.getNumChildren()>0 && body.getKind()!=FORALL && TermDb::containsTerms( ret, args ) ){
+    if( body.getNumChildren()>0 && body.getKind()!=FORALL && TermDb::hasBoundVarAttr( ret ) ){
       std::vector< Node > children;
       bool childrenChanged = false;
-      int id = getPurifyId( body, args );
+      int id = getPurifyId( body );
       for( unsigned i=0; i<body.getNumChildren(); i++ ){
         Node bi;
         if( body.getKind()==EQUAL && i==1 ){
-          int cid = getPurifyId( children[0], args );
+          int cid = getPurifyId( children[0] );
           bi = computePurify2( body[i], args, visited, var_to_term, var_parent, cid );
           if( children[0].getKind()==BOUND_VARIABLE ){
-            cid = getPurifyId( bi, args );
+            cid = getPurifyId( bi );
             if( cid!=0 && std::find( var_parent[children[0]].begin(), var_parent[children[0]].end(), cid )==var_parent[children[0]].end() ){
               var_parent[children[0]].push_back( id );
             }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 607fd9191..daf5a8bad 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -31,7 +31,7 @@ public:
   static bool isClause( Node n );
   static bool isLiteral( Node n );
   static bool isCube( Node n );
-  static int getPurifyId( Node n, std::vector< Node >& args );
+  static int getPurifyId( Node n );
 private:
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
   static Node mkForAll( std::vector< Node >& args, Node body, Node ipl );
@@ -41,7 +41,7 @@ private:
   static Node computeClause( Node n );
   static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
   static bool isConditionalVariableElim( Node n, int pol=0 );
-  static bool isVariableElim( Node v, Node s, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent );
+  static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent );
   static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs,
                                       std::map< Node, std::vector< int > >& var_parent );
   static Node computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term,
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 8e3304b6a..49bbe5680 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -56,12 +56,12 @@ RelevantDomain::RDomain * RelevantDomain::RDomain::getParent() {
   }
 }
 
-void RelevantDomain::RDomain::removeRedundantTerms( FirstOrderModel * fm ) {
+void RelevantDomain::RDomain::removeRedundantTerms( QuantifiersEngine * qe ) {
   std::map< Node, Node > rterms;
   for( unsigned i=0; i<d_terms.size(); i++ ){
     Node r = d_terms[i];
     if( !TermDb::hasInstConstAttr( d_terms[i] ) ){
-      r = fm->getRepresentative( d_terms[i] );
+      r = qe->getEqualityQuery()->getRepresentative( d_terms[i] );
     }
     if( rterms.find( r )==rterms.end() ){
       rterms[r] = d_terms[i];
@@ -132,7 +132,7 @@ void RelevantDomain::compute(){
         RDomain * r = it2->second;
         RDomain * rp = r->getParent();
         if( r==rp ){
-          r->removeRedundantTerms( d_model );
+          r->removeRedundantTerms( d_qe );
           for( unsigned i=0; i<r->d_terms.size(); i++ ){
             Trace("rel-dom") << r->d_terms[i] << " ";
           }
@@ -190,7 +190,7 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
     }else if( varCount==1 ){
       int oCh = varCh==0 ? 1 : 0;
       bool ng = d_qe->getTermDatabase()->hasInstConstAttr( n[oCh] );
-      Trace("rel-dom-debug") << "...add term " << n[oCh] << ", is ground = " << (!ng) << std::endl;
+      Trace("rel-dom-debug") << "...add term " << n[oCh] << ", is ground = " << (!ng) << ", pol = " << pol << ", hasPol = " << hasPol << ", kind = " << n.getKind() << std::endl;
       //the negative occurrence adds the term to the domain
       if( !hasPol || !pol ){
         rds[varCh]->addTerm( n[oCh], ng );
@@ -202,7 +202,6 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
             rds[varCh]->addTerm( QuantArith::offset( n[oCh], i==0 ? 1 : -1 ), ng  );
           }
         }else if( n.getKind()==GEQ ){
-          Node nt = QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 );
           rds[varCh]->addTerm( QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 ), ng );
         }
       }
@@ -228,6 +227,7 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
   }
 }
 
+/*
 Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) {
   RDomain * rf = getRDomain( f, i );
   Trace("rel-dom-debug") << "Get relevant domain " << rf << " " << r << std::endl;
@@ -248,3 +248,4 @@ Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) {
     return r;
   }
 }
+*/
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 7d1c60f80..25c821e10 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -37,7 +37,7 @@ private:
     void merge( RDomain * r );
     void addTerm( Node t, bool nonGround = false );
     RDomain * getParent();
-    void removeRedundantTerms( FirstOrderModel * fm );
+    void removeRedundantTerms( QuantifiersEngine * qe );
     bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); }
   };
   std::map< Node, std::map< int, RDomain * > > d_rel_doms;
@@ -56,7 +56,7 @@ public:
   void compute();
 
   RDomain * getRDomain( Node n, int i );
-  Node getRelevantTerm( Node f, int i, Node r );
+  //Node getRelevantTerm( Node f, int i, Node r );
 };/* class RelevantDomain */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index e41af5e2d..79e62a6cd 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -699,6 +699,29 @@ bool TermDb::hasInstConstAttr( Node n ) {
   return !getInstConstAttr(n).isNull();
 }
 
+Node TermDb::getBoundVarAttr( Node n ) {
+  if (!n.hasAttribute(BoundVarAttribute()) ){
+    Node bv;
+    if( n.getKind()==BOUND_VARIABLE ){
+      bv = n;
+    }else{
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        bv = getBoundVarAttr(n[i]);
+        if( !bv.isNull() ){
+          break;
+        }
+      }
+    }
+    BoundVarAttribute bva;
+    n.setAttribute(bva, bv);
+  }
+  return n.getAttribute(BoundVarAttribute());
+}
+
+bool TermDb::hasBoundVarAttr( Node n ) {
+  return !getBoundVarAttr(n).isNull();
+}
+
 /** get the i^th instantiation constant of q */
 Node TermDb::getInstantiationConstant( Node q, int i ) const {
   std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index f809aa5b8..8ce6aeaf0 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -59,6 +59,9 @@ typedef expr::Attribute< NoMatchAttributeId,
 struct InstConstantAttributeId {};
 typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute;
 
+struct BoundVarAttributeId {};
+typedef expr::Attribute<BoundVarAttributeId, Node> BoundVarAttribute;
+
 struct InstLevelAttributeId {};
 typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
 
@@ -262,6 +265,8 @@ public:
 
   static Node getInstConstAttr( Node n );
   static bool hasInstConstAttr( Node n );
+  static Node getBoundVarAttr( Node n );
+  static bool hasBoundVarAttr( Node n );
 
 
 //for skolem
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 1f332e909..fdfa77b02 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -250,9 +250,10 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
     if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
       Node rtr;
       bool do_negate = hasPol && pol;
+      bool is_arith = n[0].getType().isReal();
       for( unsigned i=0; i<2; i++) {
         if( n[1-i].getKind()==INST_CONSTANT ){
-          if( isUsableTrigger(n[i], f) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) ){
+          if( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) && ( !do_negate || is_arith ) ){
             rtr = n;
             break;
           }
@@ -263,7 +264,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
           }
         }
       }
-      if( n[0].getType().isInteger() ){
+      if( is_arith ){
         //try to rearrange?
         std::map< Node, Node > m;
         if( QuantArith::getMonomialSumLit(n, m) ){