Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by default in...

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 04b918afce316fe1dd9423cdba10f697c6c5a838..9e704691a0724cdc18f71ef10ecfd2271c8c67f1 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -47,7 +47,7 @@ option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default fal
 option preSkolemQuant --pre-skolem-quant bool :read-write :default false
  apply skolemization eagerly to bodies of quantified formulas
 option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true
- apply skolemization to nested quantified formulass
+ apply skolemization to nested quantified formulas
 option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true
  apply skolemization to quantified formulas aggressively
 option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
@@ -118,10 +118,6 @@ option quantRepMode --quant-rep-mode=MODE  CVC4::theory::quantifiers::QuantRepMo
 option instRelevantCond --inst-rlv-cond bool :default false
  add relevancy conditions for instantiations
 
- 
-option eagerInstQuant --eager-inst-quant bool :default false
- apply quantifier instantiation eagerly
-
 option fullSaturateQuant --full-saturate-quant bool :default false :read-write
  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
 option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
@@ -293,8 +289,6 @@ option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false
   preregister ground instantiations in counterexample-based quantifier instantiation
 option cbqiMinBounds --cbqi-min-bounds bool :default false
   use minimally constrained lower/upper bound for counterexample-based quantifier instantiation
-option cbqiSymLia --cbqi-sym-lia bool :default false
-  use symbolic integer division in substitutions for counterexample-based quantifier instantiation
 option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false
   round up integer lower bounds in substitutions for counterexample-based quantifier instantiation
 option cbqiMidpoint --cbqi-midpoint bool :default false

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b7997a2041cccf71513cc4d3e02d687d28b2d792..19bc85e3e443e028251b37608231e37ab130d352 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1748,6 +1748,12 @@ void SmtEngine::setDefaults() {
       options::finiteModelFind.set( true );
     }
   }
+  //EPR
+  if( options::quantEpr() ){
+    if( !options::preSkolemQuant.wasSetByUser() ){
+      options::preSkolemQuant.set( true );
+    }
+  }
 
   //now, have determined whether finite model find is on/off
   //apply finite model finding options
@@ -1840,9 +1846,7 @@ void SmtEngine::setDefaults() {
       }
       if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){
         //only instantiation should happen at last call when model is avaiable
-        if( !options::instWhenMode.wasSetByUser() ){
-          options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
-        }
+        options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
       }
     }
   }

diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index d31851ec4930c6f80de57d2324caecf10d28304c..6eb91cbdf1992b2af02607e1f93a0b72d15c757d 100644 (file)
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -69,22 +69,20 @@ void CegInstantiator::computeProgVars( Node n ){
   }
 }
 
-bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
-                                          std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+bool CegInstantiator::isEligible( Node n ) {
+  //compute d_subs_fv, which program variables are contained in n, and determines if eligible
+  computeProgVars( n );
+  return d_inelig.find( n )==d_inelig.end();
+}
+
+bool CegInstantiator::doAddInstantiation( SolvedForm& sf, Node theta, unsigned i, unsigned effort,
                                           std::map< Node, Node >& cons, std::vector< Node >& curr_var ){
   if( i==d_vars.size() ){
     //solved for all variables, now construct instantiation
     if( !sf.d_has_coeff.empty() ){
-      if( options::cbqiSymLia() ){
-        //use symbolic solved forms
-        SolvedForm csf;
-        csf.copy( ssf );
-        return doAddInstantiationCoeff( csf, vars, btyp, 0, cons );
-      }else{
-        return doAddInstantiationCoeff( sf, vars, btyp, 0, cons );
-      }
+      return doAddInstantiationCoeff( sf, 0, cons );
     }else{
-      return doAddInstantiation( sf.d_subs, vars, cons );
+      return doAddInstantiation( sf.d_subs, sf.d_vars, cons );
     }
   }else{
     std::map< Node, std::map< Node, bool > > subs_proc;
@@ -122,19 +120,17 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
           Node n = it_eqc->second[k];
           if( n!=pv ){
             Trace("cbqi-inst-debug") << "...try based on equal term " << n << std::endl;
-            //compute d_subs_fv, which program variables are contained in n
-            computeProgVars( n );
             //must be an eligible term
-            if( d_inelig.find( n )==d_inelig.end() ){
+            if( isEligible( n ) ){
               Node ns;
               Node pv_coeff;  //coefficient of pv in the equality we solve (null is 1)
               bool proc = false;
               if( !d_prog_var[n].empty() ){
-                ns = applySubstitution( pvtn, n, sf, vars, pv_coeff, false );
+                ns = applySubstitution( pvtn, n, sf, pv_coeff, false );
                 if( !ns.isNull() ){
                   computeProgVars( ns );
                   //substituted version must be new and cannot contain pv
-                  proc = subs_proc[pv_coeff].find( ns )==subs_proc[pv_coeff].end() && d_prog_var[ns].find( pv )==d_prog_var[ns].end();
+                  proc = d_prog_var[ns].find( pv )==d_prog_var[ns].end();
                 }
               }else{
                 ns = n;
@@ -142,8 +138,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
               }
               if( proc ){
                 //try the substitution
-                subs_proc[ns][pv_coeff] = true;
-                if( doAddInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars,  btyp, theta, i, effort, cons, curr_var ) ){
+                if( tryDoAddInstantiationInc( ns, pv, pv_coeff, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
                   return true;
                 }
               }
@@ -167,7 +162,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
               for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
                 curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) );
               }
-              if( doAddInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+              if( doAddInstantiation( sf, theta, i, effort, cons, curr_var ) ){
                 return true;
               }else{
                 //cleanup
@@ -201,14 +196,12 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
         for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){
           Node n = it_reqc->second[kk];
           Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl;
-          //compute the variables in n
-          computeProgVars( n );
           //must be an eligible term
-          if( d_inelig.find( n )==d_inelig.end() ){
+          if( isEligible( n ) ){
             Node ns;
             Node pv_coeff;
             if( !d_prog_var[n].empty() ){
-              ns = applySubstitution( pvtn, n, sf, vars, pv_coeff );
+              ns = applySubstitution( pvtn, n, sf, pv_coeff );
               if( !ns.isNull() ){
                 computeProgVars( ns );
               }
@@ -274,7 +267,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
                         Node val = veq[1];
                         if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
                           subs_proc[val][veq_c] = true;
-                          if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                          if( doAddInstantiationInc( val, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var ) ){
                             return true;
                           }
                         }
@@ -288,11 +281,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
                     }
                   }
                   if( success ){
-                    if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
-                      subs_proc[val][veq_c] = true;
-                      if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                        return true;
-                      }
+                    if( tryDoAddInstantiationInc( val, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+                      return true;
                     }
                   }
                 }
@@ -343,14 +333,12 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
                   atom_lhs = Rewriter::rewrite( atom_lhs );
                   atom_rhs = d_zero;
                 }
-
-                computeProgVars( atom_lhs );
                 //must be an eligible term
-                if( d_inelig.find( atom_lhs )==d_inelig.end() ){
+                if( isEligible( atom_lhs ) ){
                   //apply substitution to LHS of atom
                   if( !d_prog_var[atom_lhs].empty() ){
                     Node atom_lhs_coeff;
-                    atom_lhs = applySubstitution( pvtn, atom_lhs, sf, vars, atom_lhs_coeff );
+                    atom_lhs = applySubstitution( pvtn, atom_lhs, sf, atom_lhs_coeff );
                     if( !atom_lhs.isNull() ){
                       computeProgVars( atom_lhs );
                       if( !atom_lhs_coeff.isNull() ){
@@ -460,11 +448,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
                           mbp_lit[index].push_back( lit );
                         }else{
                           //try this bound
-                          if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
-                            subs_proc[uval][veq_c] = true;
-                            if( doAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                              return true;
-                            }
+                          if( tryDoAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+                            return true;
                           }
                         }
                       }
@@ -492,7 +477,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
                         }
                         if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
                           subs_proc[uval][veq_c] = true;
-                          if( doAddInstantiationInc( uval, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                          if( doAddInstantiationInc( uval, pv, veq_c, 0, sf, theta, i, effort, cons, curr_var ) ){
                             return true;
                           }
                         }
@@ -529,7 +514,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
                   val = NodeManager::currentNM()->mkNode( UMINUS, val );
                   val = Rewriter::rewrite( val );
                 }
-                if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+                if( tryDoAddInstantiationInc( val, pv, Node::null(), 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
                   return true;
                 }
               }
@@ -623,11 +608,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
                   val = getModelBasedProjectionValue( pv, val, rr==0, mbp_coeff[rr][best], pv_value, t_values[rr][best], theta,
                                                       mbp_vts_coeff[rr][0][best], mbp_vts_coeff[rr][1][best] );
                   if( !val.isNull() ){
-                    if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){
-                      subs_proc[val][mbp_coeff[rr][best]] = true;
-                      if( doAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                        return true;
-                      }
+                    if( tryDoAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+                      return true;
                     }
                   }
                 }
@@ -640,11 +622,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
             Node c; //null (one) coefficient
             val = getModelBasedProjectionValue( pv, val, true, c, pv_value, d_zero, theta, Node::null(), Node::null() );
             if( !val.isNull() ){
-              if( subs_proc[val].find( c )==subs_proc[val].end() ){
-                subs_proc[val][c] = true;
-                if( doAddInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                  return true;
-                }
+              if( tryDoAddInstantiationInc( val, pv, c, 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+                return true;
               }
             }
           }
@@ -684,11 +663,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
             }
             Trace("cbqi-bound") << "Midpoint value : " << val << std::endl;
             if( !val.isNull() ){
-              if( subs_proc[val].find( Node::null() )==subs_proc[val].end() ){
-                subs_proc[val][Node::null()] = true;
-                if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                  return true;
-                }
+              if( tryDoAddInstantiationInc( val, pv, Node::null(), 0, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+                return true;
               }
             }
           }
@@ -705,11 +681,8 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
                   Node val = getModelBasedProjectionValue( pv, mbp_bounds[rr][j], rr==0, mbp_coeff[rr][j], pv_value, t_values[rr][j], theta,
                                                            mbp_vts_coeff[rr][0][j], mbp_vts_coeff[rr][1][j] );
                   if( !val.isNull() ){
-                    if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){
-                      subs_proc[val][mbp_coeff[rr][j]] = true;
-                      if( doAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
-                        return true;
-                      }
+                    if( tryDoAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, theta, i, effort, cons, curr_var, subs_proc ) ){
+                      return true;
                     }
                   }
                 }
@@ -738,7 +711,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
       //we only resort to values in the case of booleans
       Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() );
 #endif
-      if( doAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){
+      if( tryDoAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, theta, i, new_effort, cons, curr_var, subs_proc ) ){
         return true;
       }
     }
@@ -747,9 +720,19 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::
   }
 }
 
+//cached version
+bool CegInstantiator::tryDoAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort,
+                                                std::map< Node, Node >& cons, std::vector< Node >& curr_var,
+                                                std::map< Node, std::map< Node, bool > >& subs_proc ) {
+  if( subs_proc[n].find( pv_coeff )==subs_proc[n].end() ){
+    subs_proc[n][pv_coeff] = true;
+    return doAddInstantiationInc( n, pv, pv_coeff, bt, sf, theta, i, effort, cons, curr_var );
+  }else{
+    return false;
+  }
+}
 
-bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
-                                             std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort,
                                              std::map< Node, Node >& cons, std::vector< Node >& curr_var ) {
   if( Trace.isOn("cbqi-inst") ){
     for( unsigned j=0; j<sf.d_subs.size(); j++ ){
@@ -791,16 +774,16 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int
       TNode tv = pv;
       TNode ts = n;
       Node a_pv_coeff;
-      Node new_subs = applySubstitution( vars[j].getType(), sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
+      Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_subs, a_coeff, a_has_coeff, a_var, a_pv_coeff, true );
       if( !new_subs.isNull() ){
         sf.d_subs[j] = new_subs;
         if( !a_pv_coeff.isNull() ){
           prev_coeff[j] = sf.d_coeff[j];
           if( sf.d_coeff[j].isNull() ){
-            Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), vars[j] )==sf.d_has_coeff.end() );
+            Assert( std::find( sf.d_has_coeff.begin(), sf.d_has_coeff.end(), sf.d_vars[j] )==sf.d_has_coeff.end() );
             //now has coefficient
-            new_has_coeff.push_back( vars[j] );
-            sf.d_has_coeff.push_back( vars[j] );
+            new_has_coeff.push_back( sf.d_vars[j] );
+            sf.d_has_coeff.push_back( sf.d_vars[j] );
             sf.d_coeff[j] = a_pv_coeff;
           }else{
             sf.d_coeff[j] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[j], a_pv_coeff ) );
@@ -819,19 +802,10 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int
     }else{
       Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl;
     }
-    if( options::cbqiSymLia() && pv_coeff.isNull() ){
-      //apply simple substitutions also to sym_subs
-      prev_sym_subs[j] = ssf.d_subs[j];
-      ssf.d_subs[j] = ssf.d_subs[j].substitute( a_var.begin(), a_var.end(), a_subs.begin(), a_subs.end() );
-      ssf.d_subs[j] = Rewriter::rewrite( ssf.d_subs[j] );
-    }
   }
   if( success ){
     Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl;
-    vars.push_back( pv );
-    btyp.push_back( bt );
-    sf.push_back( pv, n, pv_coeff );
-    ssf.push_back( pv, n, pv_coeff );
+    sf.push_back( pv, n, pv_coeff, bt );
     Node new_theta = theta;
     if( !pv_coeff.isNull() ){
       if( new_theta.isNull() ){
@@ -848,16 +822,13 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int
       is_cv = true;
     }
     Trace("cbqi-inst-debug2") << "Recurse..." << std::endl;
-    success = doAddInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
+    success = doAddInstantiation( sf, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
     if( !success ){
       Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
       if( is_cv ){
         curr_var.push_back( pv );
       }
-      sf.pop_back( pv, n, pv_coeff );
-      ssf.pop_back( pv, n, pv_coeff );
-      vars.pop_back();
-      btyp.pop_back();
+      sf.pop_back( pv, n, pv_coeff, bt );
     }
   }
   if( success ){
@@ -874,29 +845,23 @@ bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int
     for( unsigned i=0; i<new_has_coeff.size(); i++ ){
       sf.d_has_coeff.pop_back();
     }
-    for( std::map< int, Node >::iterator it = prev_sym_subs.begin(); it != prev_sym_subs.end(); it++ ){
-      ssf.d_subs[it->first] = it->second;
-    }
     return false;
   }
 }
 
-bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp,
-                                             unsigned j, std::map< Node, Node >& cons ) {
-
-
+bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, unsigned j, std::map< Node, Node >& cons ) {
   if( j==sf.d_has_coeff.size() ){
-    return doAddInstantiation( sf.d_subs, vars, cons );
+    return doAddInstantiation( sf.d_subs, sf.d_vars, cons );
   }else{
-    Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() );
-    unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin();
+    Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), sf.d_has_coeff[j] )!=sf.d_vars.end() );
+    unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), sf.d_has_coeff[j] )-sf.d_vars.begin();
     Node prev = sf.d_subs[index];
     Assert( !sf.d_coeff[index].isNull() );
-    Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << vars[index] << " = " << sf.d_subs[index] << std::endl;
-    Assert( vars[index].getType().isInteger() );
+    Trace("cbqi-inst-debug") << "Normalize substitution for " << sf.d_coeff[index] << " * " << sf.d_vars[index] << " = " << sf.d_subs[index] << std::endl;
+    Assert( sf.d_vars[index].getType().isInteger() );
     //must ensure that divisibility constraints are met
     //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful
-    Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], vars[index] );
+    Node eq_lhs = NodeManager::currentNM()->mkNode( MULT, sf.d_coeff[index], sf.d_vars[index] );
     Node eq_rhs = sf.d_subs[index];
     Node eq = eq_lhs.eqNode( eq_rhs );
     eq = Rewriter::rewrite( eq );
@@ -904,20 +869,20 @@ bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node
     std::map< Node, Node > msum;
     if( QuantArith::getMonomialSumLit( eq, msum ) ){
       Node veq;
-      if( QuantArith::isolate( vars[index], msum, veq, EQUAL, true )!=0 ){
+      if( QuantArith::isolate( sf.d_vars[index], msum, veq, EQUAL, true )!=0 ){
         Node veq_c;
-        if( veq[0]!=vars[index] ){
+        if( veq[0]!=sf.d_vars[index] ){
           Node veq_v;
           if( QuantArith::getMonomial( veq[0], veq_c, veq_v ) ){
-            Assert( veq_v==vars[index] );
+            Assert( veq_v==sf.d_vars[index] );
           }
         }
         sf.d_subs[index] = veq[1];
         if( !veq_c.isNull() ){
           sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c );
-          Trace("cbqi-inst-debug") << "...bound type is : " << btyp[index] << std::endl;
+          Trace("cbqi-inst-debug") << "...bound type is : " << sf.d_btyp[index] << std::endl;
           //intger division rounding up if from a lower bound
-          if( btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
+          if( sf.d_btyp[index]==1 && options::cbqiRoundUpLowerLia() ){
             sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index],
               NodeManager::currentNM()->mkNode( ITE,
                 NodeManager::currentNM()->mkNode( EQUAL,
@@ -927,24 +892,8 @@ bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node
             );
           }
         }
-        Trace("cbqi-inst-debug") << "...normalize integers : " << vars[index] << " -> " << sf.d_subs[index] << std::endl;
-        if( options::cbqiSymLia() ){
-          //must apply substitution to previous subs
-          std::vector< Node > curr_var;
-          std::vector< Node > curr_subs;
-          curr_var.push_back( vars[index] );
-          curr_subs.push_back( sf.d_subs[index] );
-          for( unsigned k=0; k<index; k++ ){
-            Node prevs = sf.d_subs[k];
-            sf.d_subs[k] = sf.d_subs[k].substitute( curr_var.begin(), curr_var.end(), curr_subs.begin(), curr_subs.end() );
-            if( prevs!=sf.d_subs[k] ){
-              Trace("cbqi-inst-debug2") << "      rewrite " << vars[k] << " -> " << prevs << " to ";
-              sf.d_subs[k] = Rewriter::rewrite( sf.d_subs[k] );
-              Trace("cbqi-inst-debug2") << sf.d_subs[k] << std::endl;
-            }
-          }
-        }
-        if( doAddInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){
+        Trace("cbqi-inst-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl;
+        if( doAddInstantiationCoeff( sf, j+1, cons ) ){
           return true;
         }
       }
@@ -1176,14 +1125,11 @@ bool CegInstantiator::check() {
   processAssertions();
   for( unsigned r=0; r<2; r++ ){
     SolvedForm sf;
-    SolvedForm ssf;
-    std::vector< Node > vars;
-    std::vector< int > btyp;
     Node theta;
     std::map< Node, Node > cons;
     std::vector< Node > curr_var;
     //try to add an instantiation
-    if( doAddInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
+    if( doAddInstantiation( sf, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
       return true;
     }
   }
@@ -1236,16 +1182,16 @@ void CegInstantiator::presolve( Node q ) {
   //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing
   //only if no nested quantifiers
   if( !QuantifiersRewriter::containsQuantifiers( q[1] ) ){
-    std::vector< Node > vars;
+    std::vector< Node > ps_vars;
     std::map< Node, std::vector< Node > > teq;
     for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      vars.push_back( q[0][i] );
+      ps_vars.push_back( q[0][i] );
       teq[q[0][i]].clear();
     }
     collectPresolveEqTerms( q[1], teq );
     std::vector< Node > terms;
     std::vector< Node > conj;
-    getPresolveEqConjuncts( vars, terms, teq, q, conj );
+    getPresolveEqConjuncts( ps_vars, terms, teq, q, conj );
 
     if( !conj.empty() ){
       Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
@@ -1410,10 +1356,8 @@ void CegInstantiator::processAssertions() {
     std::vector< Node > akeep;
     for( unsigned i=0; i<it->second.size(); i++ ){
       Node n = it->second[i];
-      //compute the variables in assertion
-      computeProgVars( n );
       //must be an eligible term
-      if( d_inelig.find( n )==d_inelig.end() ){
+      if( isEligible( n ) ){
         //must contain at least one variable
         if( !d_prog_var[n].empty() ){
           Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;

diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index 3d7bbcb5525d54d51774f35e5475c7514387cb8e..5b89420276ae7bac609ef02d0b61a3c68552348b 100644 (file)
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -38,6 +38,8 @@ public:
   virtual bool addLemma( Node lem ) = 0;
 };
 
+class Instantiator;
+
 class CegInstantiator {
 private:
   QuantifiersEngine * d_qe;
@@ -72,55 +74,53 @@ private:
   void collectCeAtoms( Node n, std::map< Node, bool >& visited );
   //for adding instantiations during check
   void computeProgVars( Node n );
+  // is eligible 
+  bool isEligible( Node n );
   //solved form, involves substitution with coefficients
   class SolvedForm {
   public:
+    std::vector< Node > d_vars;
     std::vector< Node > d_subs;
     std::vector< Node > d_coeff;
+    std::vector< int > d_btyp;
     std::vector< Node > d_has_coeff;
     void copy( SolvedForm& sf ){
       d_subs.insert( d_subs.end(), sf.d_subs.begin(), sf.d_subs.end() );
       d_coeff.insert( d_coeff.end(), sf.d_coeff.begin(), sf.d_coeff.end() );
       d_has_coeff.insert( d_has_coeff.end(), sf.d_has_coeff.begin(), sf.d_has_coeff.end() );
     }
-    void push_back( Node pv, Node n, Node pv_coeff ){
+    void push_back( Node pv, Node n, Node pv_coeff, int bt ){
+      d_vars.push_back( pv );
       d_subs.push_back( n );
       d_coeff.push_back( pv_coeff );
+      d_btyp.push_back( bt );
       if( !pv_coeff.isNull() ){
         d_has_coeff.push_back( pv );
       }
     }
-    void pop_back( Node pv, Node n, Node pv_coeff ){
+    void pop_back( Node pv, Node n, Node pv_coeff, int bt ){
+      d_vars.pop_back();
       d_subs.pop_back();
       d_coeff.pop_back();
+      d_btyp.pop_back();
       if( !pv_coeff.isNull() ){
         d_has_coeff.pop_back();
       }
     }
   };
-  /*
-  class MbpBound {
-  public:
-    Node d_bound;
-    Node d_coeff;
-    Node d_vts_coeff[2];
-    Node d_lit;
-  };
-  */
   // effort=0 : do not use model value, 1: use model value, 2: one must use model value
-  bool doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
-                         std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
-                         std::map< Node, Node >& cons, std::vector< Node >& curr_var );
-  bool doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
-                            std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
-                            std::map< Node, Node >& cons, std::vector< Node >& curr_var );
-  bool doAddInstantiationCoeff( SolvedForm& sf,
-                              std::vector< Node >& vars, std::vector< int >& btyp,
-                              unsigned j, std::map< Node, Node >& cons );
+  bool doAddInstantiation( SolvedForm& sf, Node theta, unsigned i, unsigned effort,
+                           std::map< Node, Node >& cons, std::vector< Node >& curr_var );
+  bool tryDoAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort,
+                                 std::map< Node, Node >& cons, std::vector< Node >& curr_var,
+                                 std::map< Node, std::map< Node, bool > >& subs_proc );
+  bool doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, Node theta, unsigned i, unsigned effort,
+                              std::map< Node, Node >& cons, std::vector< Node >& curr_var );
+  bool doAddInstantiationCoeff( SolvedForm& sf, unsigned j, std::map< Node, Node >& cons );
   bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons );
   Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons );
-  Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) {
-    return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff );
+  Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, Node& pv_coeff, bool try_coeff = true ) {
+    return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, sf.d_vars, pv_coeff, try_coeff );
   }
   Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& subs, std::vector< Node >& coeff, std::vector< Node >& has_coeff,
                           std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true );
@@ -142,6 +142,26 @@ public:
   void registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars );
 };
 
+
+/*
+// an instantiator for individual variables
+class InstantiatorVar {
+public:
+  
+  void postProcessInstantiation( SolvedForm& sf );
+};
+*/
+
+/*
+class MbpBound {
+public:
+  Node d_bound;
+  Node d_coeff;
+  Node d_vts_coeff[2];
+  Node d_lit;
+};
+*/
+
 }
 }
 }

diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index b3df9ca5ded0a9c0e4f5f76300bbca1a9b765d79..ceae3e4c8363d1e7fd15bc350e1071bf16440d46 100644 (file)
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -388,23 +388,6 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif
   return addedLemmas;
 }
 
-int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
-  Assert( options::eagerInstQuant() );
-  if( !d_match_pattern.isNull() ){
-    InstMatch m( f );
-    if( getMatch( f, t, m, qe ) ){
-      if( qe->addInstantiation( f, m ) ){
-        return 1;
-      }
-    }
-  }else{
-    for( unsigned i=0; i<d_children.size(); i++ ){
-      d_children[i]->addTerm( f, t, qe );
-    }
-  }
-  return 0;
-}
-
 
 InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ) {
   std::vector< Node > pats;
@@ -716,22 +699,6 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe,
   }
 }
 
-int InstMatchGeneratorMulti::addTerm( Node q, Node t, QuantifiersEngine* qe ){
-  Assert( options::eagerInstQuant() );
-  int addedLemmas = 0;
-  for( int i=0; i<(int)d_children.size(); i++ ){
-    Node t_op = qe->getTermDatabase()->getMatchOperator( t );
-    if( ((InstMatchGenerator*)d_children[i])->d_match_pattern_op==t_op ){
-      InstMatch m( q );
-      //if it produces a match, then process it with the rest
-      if( ((InstMatchGenerator*)d_children[i])->getMatch( q, t, m, qe ) ){
-        processNewMatch( qe, m, i, addedLemmas );
-      }
-    }
-  }
-  return addedLemmas;
-}
-
 InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe ) : d_f( q ), d_match_pattern( pat ) {
   if( d_match_pattern.getKind()==NOT ){
     d_match_pattern = d_match_pattern[0];
@@ -841,20 +808,6 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
   }
 }
 
-int InstMatchGeneratorSimple::addTerm( Node q, Node t, QuantifiersEngine* qe ){
-  //for eager instantiation only
-  Assert( options::eagerInstQuant() );
-  InstMatch m( q );
-  for( unsigned i=0; i<t.getNumChildren(); i++ ){
-    if( d_match_pattern[i].getKind()==INST_CONSTANT ){
-      m.setValue(d_var_num[i], t[i]);
-    }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){
-      return 0;
-    }
-  }
-  return qe->addInstantiation( q, m ) ? 1 : 0;
-}
-
 int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) {
   Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
   unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );

diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 65c5a14277f4c1ab985a8c21d01433f7e281852f..c238e3c4e5b28910ede9744234b4076fd3d720a9 100644 (file)
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -42,8 +42,6 @@ public:
   virtual bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) = 0;
   /** add instantiations directly */
   virtual int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
-  /** add ground term t, called when t is added to term db */
-  virtual int addTerm( Node q, Node t, QuantifiersEngine* qe ) { return 0; }
   /** set active add */
   virtual void setActiveAdd( bool val ) {}
   /** get active score */
@@ -113,8 +111,6 @@ public:
   bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
   /** add instantiations */
   int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t */
-  int addTerm( Node q, Node t, QuantifiersEngine* qe );
 
   bool d_active_add;
   void setActiveAdd( bool val );
@@ -205,8 +201,6 @@ public:
   bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; }
   /** add instantiations */
   int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t */
-  int addTerm( Node q, Node t, QuantifiersEngine* qe );
 };/* class InstMatchGeneratorMulti */
 
 /** smart (single)-trigger implementation */
@@ -240,8 +234,6 @@ public:
   bool getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return false; }
   /** add instantiations */
   int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
-  /** add ground term t, possibly add instantiations */
-  int addTerm( Node q, Node t, QuantifiersEngine* qe );
   /** get active score */
   int getActiveScore( QuantifiersEngine * qe );
 };/* class InstMatchGeneratorSimple */

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a34ad116a2dc6911d0a92feffceba4dc303e5617..dee4952bd36fdbefe03704c117b96ed3a1629292 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -175,17 +175,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
           if( d_sygus_tdb ){
             d_sygus_tdb->registerEvalTerm( n );
           }
-
-          if( options::eagerInstQuant() ){
-            for( unsigned i=0; i<n.getNumChildren(); i++ ){
-              if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
-                int addedLemmas = 0;
-                for( unsigned i=0; i<d_op_triggers[op].size(); i++ ){
-                  addedLemmas += d_op_triggers[op][i]->addTerm( n );
-                }
-              }
-            }
-          }
         }
       }else{
         setTermInactive( n );

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index d0bcd3a695cbf11a83ee792a0eedc4c3a9302e7c..3017238caffe19b2d95f74392fe7f34161e7a00f 100644 (file)
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -76,12 +76,6 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
     ++(qe->d_statistics.d_multi_triggers);
   }
   //Notice() << "Trigger : " << (*this) << "  for " << f << std::endl;
-  if( options::eagerInstQuant() ){
-    for( int i=0; i<(int)d_nodes.size(); i++ ){
-      Node op = qe->getTermDatabase()->getMatchOperator( d_nodes[i] );
-      qe->getTermDatabase()->registerTrigger( this, op );
-    }
-  }
   Trace("trigger-debug") << "Finished making trigger." << std::endl;
 }
 
@@ -107,10 +101,6 @@ bool Trigger::getMatch( Node f, Node t, InstMatch& m ){
   return ((InstMatchGenerator*)d_mg)->getMatch( f, t, m, d_quantEngine );
 }
 
-int Trigger::addTerm( Node t ){
-  return d_mg->addTerm( d_f, t, d_quantEngine );
-}
-
 Node Trigger::getInstPattern(){
   return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
 }

diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 6d7bf1f4db881ce3411338474c3e86111c0676f6..6316273313cb1d6e0399620c59778d97dbfb86bb 100644 (file)
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -72,8 +72,6 @@ class Trigger {
       Currently the trigger should not be a multi-trigger.
   */
   bool getMatch( Node f, Node t, InstMatch& m);
-  /** add ground term t, called when t is added to the TermDb */
-  int addTerm( Node t );
   /** return whether this is a multi-trigger */
   bool isMultiTrigger() { return d_nodes.size()>1; }
   /** get inst pattern list */

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index fbfdb856e283fefb991adfff9ca5369f0766ac45..ec20d1edeadf223565d5c639c6b03d5b47f62544 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -794,10 +794,7 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within
   if( !d_presolve || !options::incrementalSolving() ){
     std::set< Node > added;
     getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
-    //maybe have triggered instantiations if we are doing eager instantiation
-    if( options::eagerInstQuant() ){
-      flushLemmas();
-    }
+    
     //added contains also the Node that just have been asserted in this branch
     if( d_quant_rel ){
       for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){