Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, minor changes.

5 files changed, 146 insertions, 104 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1397c10d3..5d6a913b0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1174,6 +1174,9 @@ void SmtEngine::setDefaults() {
     //must have finite model finding on
     options::finiteModelFind.set( true );
   }
+  if( options::recurseCbqi() ){
+    options::cbqi.set( true );
+  }
   if( options::fmfBoundInt() ){
     //must have finite model finding on
     options::finiteModelFind.set( true );
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index 0b75c4a77..c6a5f4227 100755
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -15,7 +15,7 @@
 

 #include "theory/quantifiers/ambqi_builder.h"

 #include "theory/quantifiers/term_database.h"

-

+#include "theory/quantifiers/options.h"

 

 using namespace std;

 using namespace CVC4;

@@ -148,48 +148,52 @@ void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsign
 }

 

 bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ) {

-  if( d_value==1 ){

-    //instantiations are all true : ignore this

-    return true;

-  }else{

-    if( depth==q[0].getNumChildren() ){

-      if( qe->addInstantiation( q, terms ) ){

-        Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;

-        inst++;

-        return true;

-      }else{

-        Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl;

-        //we are incomplete

-        return false;

-      }

+  if( inst==0 || !options::fmfOneInstPerRound() ){

+    if( d_value==1 ){

+      //instantiations are all true : ignore this

+      return true;

     }else{

-      bool osuccess = true;

-      TypeNode tn = m->getVariable( q, depth ).getType();

-      for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){

-        //get witness term

-        unsigned index = 0;

-        bool success;

-        do {

-          success = false;

-          index = getId( it->first, index );

-          if( index<32 ){

-            Assert( index<m->d_rep_set.d_type_reps[tn].size() );

-            terms[m->d_var_order[q][depth]] = m->d_rep_set.d_type_reps[tn][index];

-            //terms[depth] = m->d_rep_set.d_type_reps[tn][index];

-            if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){

-              //if we are incomplete, and have not yet added an instantiation, keep trying

-              index++;

-              Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl;

-            }else{

-              success = true;

+      if( depth==q[0].getNumChildren() ){

+        if( qe->addInstantiation( q, terms ) ){

+          Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl;

+          inst++;

+          return true;

+        }else{

+          Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl;

+          //we are incomplete

+          return false;

+        }

+      }else{

+        bool osuccess = true;

+        TypeNode tn = m->getVariable( q, depth ).getType();

+        for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){

+          //get witness term

+          unsigned index = 0;

+          bool success;

+          do {

+            success = false;

+            index = getId( it->first, index );

+            if( index<32 ){

+              Assert( index<m->d_rep_set.d_type_reps[tn].size() );

+              terms[m->d_var_order[q][depth]] = m->d_rep_set.d_type_reps[tn][index];

+              //terms[depth] = m->d_rep_set.d_type_reps[tn][index];

+              if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){

+                //if we are incomplete, and have not yet added an instantiation, keep trying

+                index++;

+                Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl;

+              }else{

+                success = true;

+              }

             }

-          }

-        }while( !success && index<32 );

-        //mark if we are incomplete

-        osuccess = osuccess && success;

+          }while( !success && index<32 );

+          //mark if we are incomplete

+          osuccess = osuccess && success;

+        }

+        return osuccess;

       }

-      return osuccess;

     }

+  }else{

+    return true;

   }

 }

 

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index f9b4dd588..fef6b38d1 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -34,6 +34,7 @@ using namespace CVC4::theory::datatypes;
 InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) :
     InstStrategy( ie ), d_th( th ), d_counter( 0 ){
   d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
+  d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
 }
 
 bool InstStrategySimplex::calculateShouldProcess( Node f ){
@@ -65,36 +66,33 @@ void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort
   ArithVariables::var_iterator vi, vend;
   for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
     ArithVar x = *vi;
-    if( d_th->d_internal->d_partialModel.hasEitherBound( x ) ){
-      Node n = avnm.asNode(x);
-
-      //collect instantiation constants
-      std::vector< Node > ics;
-      getInstantiationConstants( n, ics );
-      for( unsigned i=0; i<ics.size(); i++ ){
+    Node n = avnm.asNode(x);
 
-        NodeBuilder<> t(kind::PLUS);
-        if( n.getKind()==PLUS ){
-          for( int j=0; j<(int)n.getNumChildren(); j++ ){
-            addTermToRow( ics[i], x, n[j], t );
-          }
-        }else{
-          addTermToRow( ics[i], x, n, t );
-        }
-        d_instRows[ics[i]].push_back( x );
-        //this theory has constraints from f
-        Node f = TermDb::getInstConstAttr(ics[i]);
-        Debug("quant-arith") << "Has constraints from " << f << std::endl;
-        //set that we should process it
-        d_quantActive[ f ] = true;
-        //set tableaux term
-        if( t.getNumChildren()==0 ){
-          d_tableaux_term[ics[i]][x] = NodeManager::currentNM()->mkConst( Rational(0) );
-        }else if( t.getNumChildren()==1 ){
-          d_tableaux_term[ics[i]][x] = t.getChild( 0 );
-        }else{
-          d_tableaux_term[ics[i]][x] = t;
+    //collect instantiation constants
+    std::vector< Node > ics;
+    getInstantiationConstants( n, ics );
+    for( unsigned i=0; i<ics.size(); i++ ){
+      NodeBuilder<> t(kind::PLUS);
+      if( n.getKind()==PLUS ){
+        for( int j=0; j<(int)n.getNumChildren(); j++ ){
+          addTermToRow( ics[i], x, n[j], t );
         }
+      }else{
+        addTermToRow( ics[i], x, n, t );
+      }
+      d_instRows[ics[i]].push_back( x );
+      //this theory has constraints from f
+      Node f = TermDb::getInstConstAttr(ics[i]);
+      Debug("quant-arith") << "Has constraints from " << f << std::endl;
+      //set that we should process it
+      d_quantActive[ f ] = true;
+      //set tableaux term
+      if( t.getNumChildren()==0 ){
+        d_tableaux_term[ics[i]][x] = d_zero;
+      }else if( t.getNumChildren()==1 ){
+        d_tableaux_term[ics[i]][x] = t.getChild( 0 );
+      }else{
+        d_tableaux_term[ics[i]][x] = t;
       }
     }
   }
@@ -134,26 +132,50 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
   if( e<2 ){
     return STATUS_UNFINISHED;
   }else if( e==2 ){
-    //Notice() << f << std::endl;
-    //Notice() << "Num inst rows = " << d_th->d_instRows[f].size() << std::endl;
-    //Notice() << "Num inst constants = " << d_quantEngine->getNumInstantiationConstants( f ) << std::endl;
+    //the point instantiation
+    InstMatch m_point( f );
+    bool m_point_valid = true;
+    int lem = 0;
+    //scan over all instantiation rows
     for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
       Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
       Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
       for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
         ArithVar x = d_instRows[ic][j];
         if( !d_ceTableaux[ic][x].empty() ){
-          Debug("quant-arith-simplex") << "Check row " << ic << " " << x << std::endl;
+          if( Debug.isOn("quant-arith-simplex") ){
+            Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
+            Debug("quant-arith-simplex") << "  ";
+            for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
+              if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+              Debug("quant-arith-simplex") << it->first << " * " << it->second;
+            }
+            Debug("quant-arith-simplex") << " = ";
+            Node v = getTableauxValue( x, false );
+            Debug("quant-arith-simplex") << v << std::endl;
+            Debug("quant-arith-simplex") << "  term : " << d_tableaux_term[ic][x] << std::endl;
+            Debug("quant-arith-simplex") << "  ce-term : ";
+            for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
+              if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+              Debug("quant-arith-simplex") << it->first << " * " << it->second;
+            }
+            Debug("quant-arith-simplex") << std::endl;
+          }
           //instantiation row will be A*e + B*t = beta,
           // where e is a vector of terms , and t is vector of ground terms.
           // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
           // We will construct the term ( beta - B*t)/coeff to use for e_i.
           InstMatch m( f );
+          for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
+            if( f[0][k].getType().isInteger() ){
+              m.setValue( k, d_zero );
+            }
+          }
           //By default, choose the first instantiation constant to be e_i.
           Node var = d_ceTableaux[ic][x].begin()->first;
+          //if it is integer, we need to find variable with coefficent +/- 1
           if( var.getType().isInteger() ){
             std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
-            //try to find coefficent that is +/- 1
             while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
               ++it;
               if( it==d_ceTableaux[ic][x].end() ){
@@ -162,28 +184,35 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
                 var = it->first;
               }
             }
-            //otherwise, try one that divides all ground term coefficients? DO_THIS
+            //Otherwise, try one that divides all ground term coefficients?
+            //  Might be futile, if rewrite ensures gcd of coeffs is 1.
           }
           if( !var.isNull() ){
+            //add to point instantiation if applicable
+            if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
+              Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
+              Node v = getTableauxValue( x, false );
+              if( !var.getType().isInteger() || v.getType().isInteger() ){
+                m_point.setValue( i, v );
+              }else{
+                m_point_valid = false;
+              }
+            }
             Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
-            doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var );
+            if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
+              lem++;
+            }
           }else{
             Debug("quant-arith-simplex") << "Could not find var." << std::endl;
           }
-          ////choose a new variable based on alternation strategy
-          //int index = d_counter%(int)d_th->d_ceTableaux[x].size();
-          //Node var;
-          //for( std::map< Node, Node >::iterator it = d_th->d_ceTableaux[x].begin(); it != d_th->d_ceTableaux[x].end(); ++it ){
-          //  if( index==0 ){
-          //    var = it->first;
-          //    break;
-          //  }
-          //  index--;
-          //}
-          //d_th->doInstantiation( f, d_th->d_tableaux_term[x], x, &m, var );
         }
       }
     }
+    if( lem==0 && m_point_valid ){
+      if( d_quantEngine->addInstantiation( f, m_point ) ){
+        Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
+      }
+    }
   }
   return STATUS_UNKNOWN;
 }
@@ -279,25 +308,30 @@ bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar
 
 bool InstStrategySimplex::doInstantiation2( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var, bool minus_delta ){
   // make term ( beta - term )/coeff
+  bool vIsInteger = var.getType().isInteger();
   Node beta = getTableauxValue( x, minus_delta );
-  Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
-  if( !d_ceTableaux[ic][x][var].isNull() ){
-    if( var.getType().isInteger() ){
-      Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
-      instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal );
-    }else{
-      Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst<Rational>() );
-      instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
+  if( !vIsInteger || beta.getType().isInteger() ){
+    Node instVal = NodeManager::currentNM()->mkNode( MINUS, beta, term );
+    if( !d_ceTableaux[ic][x][var].isNull() ){
+      if( vIsInteger ){
+        Assert( d_ceTableaux[ic][x][var]==NodeManager::currentNM()->mkConst( Rational(-1) ) );
+        instVal = NodeManager::currentNM()->mkNode( MULT, d_ceTableaux[ic][x][var], instVal );
+      }else{
+        Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_ceTableaux[ic][x][var].getConst<Rational>() );
+        instVal = NodeManager::currentNM()->mkNode( MULT, coeff, instVal );
+      }
     }
+    instVal = Rewriter::rewrite( instVal );
+    //use as instantiation value for var
+    int vn = var.getAttribute(InstVarNumAttribute());
+    m.setValue( vn, instVal );
+    Debug("quant-arith") << "Add instantiation " << m << std::endl;
+    return d_quantEngine->addInstantiation( f, m );
+  }else{
+    return false;
   }
-  instVal = Rewriter::rewrite( instVal );
-  //use as instantiation value for var
-  int vn = var.getAttribute(InstVarNumAttribute());
-  m.setValue( vn, instVal );
-  Debug("quant-arith") << "Add instantiation " << m << std::endl;
-  return d_quantEngine->addInstantiation( f, m );
 }
-
+/*
 Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
   if( d_th->d_internal->d_partialModel.hasArithVar(n) ){
     ArithVar v = d_th->d_internal->d_partialModel.asArithVar( n );
@@ -306,7 +340,7 @@ Node InstStrategySimplex::getTableauxValue( Node n, bool minus_delta ){
     return NodeManager::currentNM()->mkConst( Rational(0) );
   }
 }
-
+*/
 Node InstStrategySimplex::getTableauxValue( ArithVar v, bool minus_delta ){
   const Rational& delta = d_th->d_internal->d_partialModel.getDelta();
   DeltaRational drv = d_th->d_internal->d_partialModel.getAssignment( v );
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index c70c90b29..a446c8b35 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -55,7 +55,7 @@ private:
   /** ce tableaux */
   std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_ceTableaux;
   /** get value */
-  Node getTableauxValue( Node n, bool minus_delta = false );
+  //Node getTableauxValue( Node n, bool minus_delta = false );
   Node getTableauxValue( arith::ArithVar v, bool minus_delta = false );
   /** do instantiation */
   bool doInstantiation( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var );
@@ -67,7 +67,8 @@ private:
 private:
   /** */
   int d_counter;
-  /** negative one */
+  /** constants */
+  Node d_zero;
   Node d_negOne;
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 38db10feb..f02a3bce1 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -82,7 +82,7 @@ option fullSaturateQuant --full-saturate-quant bool :default false
 option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
  choose literal matching mode
 
-option cbqi --enable-cbqi bool :default false
+option cbqi --enable-cbqi bool :read-write :default false
  turns on counterexample-based quantifier instantiation
 
 option recurseCbqi --cbqi-recurse bool :default false