Improve relevant domain computation for arithmetic, full saturation strategy. Simply E-matching trigger selection, do not use non-trivial triggers unless necessary. Add option to strings.

1 files changed, 119 insertions, 72 deletions

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 49bbe5680..88793358e 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -34,15 +34,9 @@ void RelevantDomain::RDomain::merge( RDomain * r ) {
   d_terms.clear();
 }
 
-void RelevantDomain::RDomain::addTerm( Node t, bool nonGround ) {
-  if( !nonGround ){
-    if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
-      d_terms.push_back( t );
-    }
-  }else{
-    if( std::find( d_ng_terms.begin(), d_ng_terms.end(), t )==d_ng_terms.end() ){
-      d_ng_terms.push_back( t );
-    }
+void RelevantDomain::RDomain::addTerm( Node t ) {
+  if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){
+    d_terms.push_back( t );
   }
 }
 
@@ -79,13 +73,13 @@ RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_
    d_is_computed = false;
 }
 
-RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i ) {
+RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i, bool getParent ) {
   if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){
     d_rel_doms[n][i] = new RDomain;
     d_rn_map[d_rel_doms[n][i]] = n;
     d_ri_map[d_rel_doms[n][i]] = i;
   }
-  return d_rel_doms[n][i]->getParent();
+  return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i];
 }
 
 void RelevantDomain::reset(){
@@ -100,11 +94,11 @@ void RelevantDomain::compute(){
         it2->second->reset();
       }
     }
-    for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
-      Node f = d_model->getAssertedQuantifier( i );
-      Node icf = d_qe->getTermDatabase()->getInstConstantBody( f );
+    for( int i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
+      Node q = d_model->getAssertedQuantifier( i );
+      Node icf = d_qe->getTermDatabase()->getInstConstantBody( q );
       Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
-      computeRelevantDomain( icf, true, true );
+      computeRelevantDomain( q, icf, true, true );
     }
 
     Trace("rel-dom-debug") << "account for ground terms" << std::endl;
@@ -145,7 +139,7 @@ void RelevantDomain::compute(){
   }
 }
 
-void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
+void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool pol ) {
   Node op = d_qe->getTermDatabase()->getOperator( n );
   for( unsigned i=0; i<n.getNumChildren(); i++ ){
     if( !op.isNull() ){
@@ -158,51 +152,29 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) {
         computeRelevantDomainOpCh( rf, n[i] );
       }
     }
-    //TODO
     if( n[i].getKind()!=FORALL ){
       bool newHasPol;
       bool newPol;
       QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
-      computeRelevantDomain( n[i], newHasPol, newPol );
+      computeRelevantDomain( q, n[i], newHasPol, newPol );
     }
   }
 
-  if( n.getKind()==EQUAL || n.getKind()==GEQ ){
-    int varCount = 0;
-    std::vector< RDomain * > rds;
-    int varCh = -1;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( n[i].getKind()==INST_CONSTANT ){
-        Node q = d_qe->getTermDatabase()->getInstConstAttr( n[i] );
-        unsigned id = n[i].getAttribute(InstVarNumAttribute());
-        rds.push_back( getRDomain( q, id ) );
-        varCount++;
-        varCh = i;
-      }else{
-        rds.push_back( NULL );
-      }
-    }
-    if( varCount==2 ){
-      //merge the two relevant domains
-      if( ( !hasPol || pol ) && rds[0]!=rds[1] ){
-        rds[0]->merge( rds[1] );
+  if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) && TermDb::hasInstConstAttr( n ) ){
+    //compute the information for what this literal does
+    computeRelevantDomainLit( q, hasPol, pol, n );
+    if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
+      Assert( d_rel_dom_lit[hasPol][pol][n].d_rd[0]!=NULL && d_rel_dom_lit[hasPol][pol][n].d_rd[1]!=NULL );
+      RDomain * rd1 = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent();
+      RDomain * rd2 = d_rel_dom_lit[hasPol][pol][n].d_rd[1]->getParent();
+      if( rd1!=rd2 ){
+        rd1->merge( rd2 );
       }
-    }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) << ", 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 );
-      }
-      //the positive occurence adds other terms
-      if( ( !hasPol || pol ) && n[0].getType().isInteger() ){
-        if( n.getKind()==EQUAL ){
-          for( unsigned i=0; i<2; i++ ){
-            rds[varCh]->addTerm( QuantArith::offset( n[oCh], i==0 ? 1 : -1 ), ng  );
-          }
-        }else if( n.getKind()==GEQ ){
-          rds[varCh]->addTerm( QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 ), ng );
+    }else{
+      if( d_rel_dom_lit[hasPol][pol][n].d_rd[0]!=NULL ){
+        RDomain * rd = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent();
+        for( unsigned i=0; i<d_rel_dom_lit[hasPol][pol][n].d_val.size(); i++ ){
+          rd->addTerm( d_rel_dom_lit[hasPol][pol][n].d_val[i] );
         }
       }
     }
@@ -220,32 +192,107 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
     if( rf!=rq ){
       rq->merge( rf );
     }
-  }else if( !d_qe->getTermDatabase()->hasInstConstAttr( n ) ){
+  }else if( !TermDb::hasInstConstAttr( n ) ){
     Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl;
     //term to add
     rf->addTerm( 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;
-  if( !d_qe->getEqualityQuery()->getEngine()->hasTerm( r ) || rf->hasTerm( r ) ){
-    return r;
-  }else{
-    Node rr = d_model->getRepresentative( r );
-    eq::EqClassIterator eqc( rr, d_qe->getEqualityQuery()->getEngine() );
-    while( !eqc.isFinished() ){
-      Node en = (*eqc);
-      if( rf->hasTerm( en ) ){
-        return en;
+void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ) {
+  if( d_rel_dom_lit[hasPol][pol].find( n )==d_rel_dom_lit[hasPol][pol].end() ){
+    d_rel_dom_lit[hasPol][pol][n].d_merge = false;
+    int varCount = 0;
+    int varCh = -1;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( n[i].getKind()==INST_CONSTANT ){
+        d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain( q, n[i].getAttribute(InstVarNumAttribute()), false );
+        varCount++;
+        varCh = i;
+      }else{
+        d_rel_dom_lit[hasPol][pol][n].d_rd[i] = NULL;
       }
-      ++eqc;
     }
-    //otherwise, may be equal to some non-ground term
-
-    return r;
+    
+    Node r_add;
+    bool varLhs = true;
+    if( varCount==2 ){
+      d_rel_dom_lit[hasPol][pol][n].d_merge = true;
+    }else{
+      if( varCount==1 ){
+        r_add = n[1-varCh];
+        varLhs = (varCh==0);
+        d_rel_dom_lit[hasPol][pol][n].d_rd[0] = d_rel_dom_lit[hasPol][pol][n].d_rd[varCh];
+        d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
+      }else{
+        //solve the inequality for one/two variables, if possible
+        std::map< Node, Node > msum;
+        if( QuantArith::getMonomialSumLit( n, msum ) ){
+          Node var;
+          Node var2;
+          bool hasNonVar = false;
+          for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+            if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){
+              if( var.isNull() ){
+                var = it->first;
+              }else if( var2.isNull() ){
+                var2 = it->first;
+              }else{
+                hasNonVar = true;
+              }
+            }else{
+              hasNonVar = true;
+            }
+          }
+          if( !var.isNull() ){
+            if( var2.isNull() ){
+              //single variable solve
+              Node veq_c;
+              Node val;
+              int ires = QuantArith::isolate( var, msum, veq_c, val, n.getKind() );
+              if( ires!=0 ){
+                if( veq_c.isNull() ){
+                  r_add = val;
+                  varLhs = (ires==1);
+                  d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false );
+                  d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
+                }
+              }
+            }else if( !hasNonVar ){
+              //merge the domains
+              d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false );
+              d_rel_dom_lit[hasPol][pol][n].d_rd[1] = getRDomain( q, var2.getAttribute(InstVarNumAttribute()), false );
+              d_rel_dom_lit[hasPol][pol][n].d_merge = true;
+            }
+          }
+        }
+      }
+    }
+    if( d_rel_dom_lit[hasPol][pol][n].d_merge ){
+      //do not merge if constant negative polarity
+      if( hasPol && !pol ){
+        d_rel_dom_lit[hasPol][pol][n].d_merge = false;
+      }
+    }else if( !r_add.isNull() && !TermDb::hasInstConstAttr( r_add ) ){
+      Trace("rel-dom-debug") << "...add term " << r_add << ", pol = " << pol << ", kind = " << n.getKind() << std::endl;
+      //the negative occurrence adds the term to the domain
+      if( !hasPol || !pol ){
+        d_rel_dom_lit[hasPol][pol][n].d_val.push_back( r_add );
+      }
+      //the positive occurence adds other terms
+      if( ( !hasPol || pol ) && n[0].getType().isInteger() ){
+        if( n.getKind()==EQUAL ){
+          for( unsigned i=0; i<2; i++ ){
+            d_rel_dom_lit[hasPol][pol][n].d_val.push_back( QuantArith::offset( r_add, i==0 ? 1 : -1 )  );
+          }
+        }else if( n.getKind()==GEQ ){
+          d_rel_dom_lit[hasPol][pol][n].d_val.push_back( QuantArith::offset( r_add, varLhs ? 1 : -1 ) );
+        }
+      }
+    }else{
+      d_rel_dom_lit[hasPol][pol][n].d_rd[0] = NULL;
+      d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
+    }
   }
 }
-*/
+