From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 12 Sep 2016 19:45:38 +0000 (-0500)
Subject: Remove old implementation of cbqi
X-Git-Tag: cvc5-1.0.0~6028^2~55
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=685b1f3769decafbff1c5b929d4ce01169ff9d81;p=cvc5.git

Remove old implementation of cbqi
---

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 606e33d75..2e9aa00cc 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -275,8 +275,6 @@ option sygusDirectEval --sygus-direct-eval bool :default true
   direct unfolding of evaluation functions
   
 # approach applied to general quantified formulas
-option cbqiSplx --cbqi-splx bool :read-write :default false
- turns on old implementation of counterexample-based quantifier instantiation
 option cbqi --cbqi bool :read-write :default false
  turns on counterexample-based quantifier instantiation
 option recurseCbqi --cbqi-recurse bool :default true
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 93e62f79d..c9f80c2aa 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1825,10 +1825,6 @@ void SmtEngine::setDefaults() {
       options::cbqi.set( true );
     }
   }
-  if( options::cbqiSplx() ){
-    //implies more general option
-    options::cbqi.set( true );
-  }
   if( options::cbqi() ){
     //must rewrite divk
     if( !options::rewriteDivk.wasSetByUser()) {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 3e414ca6d..51bbd67f3 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -25,10 +25,6 @@
 namespace CVC4 {
 namespace theory {
 
-namespace quantifiers {
-  class InstStrategySimplex;
-}
-
 namespace arith {
 
 /**
@@ -38,7 +34,6 @@ namespace arith {
  */
 class TheoryArith : public Theory {
 private:
-  friend class quantifiers::InstStrategySimplex;
   friend class TheoryArithPrivate;
 
   TheoryArithPrivate* d_internal;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index edc3a5bc0..ed7efe008 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -70,9 +70,6 @@
 
 namespace CVC4 {
 namespace theory {
-namespace quantifiers {
-  class InstStrategySimplex;
-}
 namespace arith {
 
 class BranchCutInfo;
@@ -93,7 +90,6 @@ class InferBoundsResult;
  */
 class TheoryArithPrivate {
 private:
-  friend class quantifiers::InstStrategySimplex;
 
   static const uint32_t RESET_START = 2;
 
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 3d4b6a333..82f45916c 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -334,7 +334,7 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis
 
 void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
-    if( !options::cbqiAll() && !options::cbqiSplx() ){
+    if( !options::cbqiAll() ){
       //take full ownership of the quantified formula
       d_quantEngine->setOwner( q, this );
       
@@ -495,7 +495,7 @@ int InstStrategyCbqi::hasNonCbqiVariable( Node q ){
     if( tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() ){
       handled = 0;
     }else if( tn.isDatatype() ){
-      handled = !options::cbqiSplx() ? 0 : -1;
+      handled = 0;
     }else if( tn.isSort() ){
       QuantEPR * qepr = d_quantEngine->getQuantEPR();
       if( qepr!=NULL ){
@@ -592,325 +592,6 @@ Node InstStrategyCbqi::getNextDecisionRequest(){
 
 
 
-
-//old implementation
-
-InstStrategySimplex::InstStrategySimplex( TheoryArith* th, QuantifiersEngine* ie ) : InstStrategyCbqi( ie ), d_th( th ), d_counter( 0 ){
-  d_negOne = NodeManager::currentNM()->mkConst( Rational(-1) );
-  d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
-}
-
-void getInstantiationConstants( Node n, std::vector< Node >& ics ){
-  if( n.getKind()==INST_CONSTANT ){
-    if( std::find( ics.begin(), ics.end(), n )==ics.end() ){
-      ics.push_back( n );
-    }
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      getInstantiationConstants( n[i], ics );
-    }
-  }
-}
-
-
-void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
-  Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
-  d_quantActive.clear();
-  d_instRows.clear();
-  d_tableaux_term.clear();
-  d_tableaux.clear();
-  d_ceTableaux.clear();
-  //search for instantiation rows in simplex tableaux
-  ArithVariables& avnm = d_th->d_internal->d_partialModel;
-  ArithVariables::var_iterator vi, vend;
-  for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
-    ArithVar x = *vi;
-    Node n = avnm.asNode(x);
-
-    //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;
-      }
-    }
-  }
-  //print debug
-  if( Debug.isOn("quant-arith-debug") ){
-    Debug("quant-arith-debug") << std::endl;
-    debugPrint( "quant-arith-debug" );
-  }
-  d_counter++;
-}
-
-void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder<>& t ){
-  if( n.getKind()==MULT ){
-    if( TermDb::hasInstConstAttr(n[1]) && n[0].getKind()==CONST_RATIONAL ){
-      if( n[1]==i ){
-        d_ceTableaux[i][x][ n[1] ] = n[0];
-      }else{
-        d_tableaux_ce_term[i][x][ n[1] ] = n[0];
-      }
-    }else{
-      d_tableaux[i][x][ n[1] ] = n[0];
-      t << n;
-    }
-  }else{
-    if( TermDb::hasInstConstAttr(n) ){
-      if( n==i ){
-        d_ceTableaux[i][x][ n ] = Node::null();
-      }else{
-        d_tableaux_ce_term[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
-      }
-    }else{
-      d_tableaux[i][x][ n ] = NodeManager::currentNM()->mkConst( Rational(1) );
-      t << n;
-    }
-  }
-}
-
-void InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
-  if( e==0 ){
-    if( d_quantActive.find( f )!=d_quantActive.end() ){
-      //the point instantiation
-      InstMatch m_point( f );
-      bool m_point_valid = true;
-      int lem = 0;
-      //scan over all instantiation rows
-      for( unsigned 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( unsigned j=0; j<d_instRows[ic].size(); j++ ){
-          ArithVar x = d_instRows[ic][j];
-          if( !d_ceTableaux[ic][x].empty() ){
-            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();
-              while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
-                ++it;
-                if( it==d_ceTableaux[ic][x].end() ){
-                  var = Node::null();
-                }else{
-                  var = it->first;
-                }
-              }
-              //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;
-              if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
-                lem++;
-              }
-            }else{
-              Debug("quant-arith-simplex") << "Could not find var." << std::endl;
-            }
-          }
-        }
-      }
-      if( lem==0 && m_point_valid ){
-        if( d_quantEngine->addInstantiation( f, m_point ) ){
-          Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
-        }
-      }
-    }
-  }
-}
-
-
-void InstStrategySimplex::debugPrint( const char* c ){
-  ArithVariables& avnm = d_th->d_internal->d_partialModel;
-  ArithVariables::var_iterator vi, vend;
-  for(vi = avnm.var_begin(), vend = avnm.var_end(); vi != vend; ++vi ){
-    ArithVar x = *vi;
-    Node n = avnm.asNode(x);
-    //if( ((TheoryArith*)getTheory())->d_partialModel.hasEitherBound( x ) ){
-      Debug(c) << x << " : " << n << ", bounds = ";
-      if( d_th->d_internal->d_partialModel.hasLowerBound( x ) ){
-        Debug(c) << d_th->d_internal->d_partialModel.getLowerBound( x );
-      }else{
-        Debug(c) << "-infty";
-      }
-      Debug(c) << " <= ";
-      Debug(c) << d_th->d_internal->d_partialModel.getAssignment( x );
-      Debug(c) << " <= ";
-      if( d_th->d_internal->d_partialModel.hasUpperBound( x ) ){
-        Debug(c) << d_th->d_internal->d_partialModel.getUpperBound( x );
-      }else{
-        Debug(c) << "+infty";
-      }
-      Debug(c) << std::endl;
-      //Debug(c) << "   Term = " << d_tableaux_term[x] << std::endl;
-      //Debug(c) << "   ";
-      //for( std::map< Node, Node >::iterator it2 = d_tableaux[x].begin(); it2 != d_tableaux[x].end(); ++it2 ){
-      //  Debug(c) << "( " << it2->first << ", " << it2->second << " ) ";
-      //}
-      //for( std::map< Node, Node >::iterator it2 = d_ceTableaux[x].begin(); it2 != d_ceTableaux[x].end(); ++it2 ){
-      //  Debug(c) << "(CE)( " << it2->first << ", " << it2->second << " ) ";
-      //}
-      //for( std::map< Node, Node >::iterator it2 = d_tableaux_ce_term[x].begin(); it2 != d_tableaux_ce_term[x].end(); ++it2 ){
-      //  Debug(c) << "(CE-term)( " << it2->first << ", " << it2->second << " ) ";
-      //}
-      //Debug(c) << std::endl;
-    //}
-  }
-  Debug(c) << std::endl;
-
-  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-    Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
-    Debug(c) << f << std::endl;
-    Debug(c) << "   Inst constants: ";
-    for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
-      if( j>0 ){
-        Debug( c ) << ", ";
-      }
-      Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
-    }
-    Debug(c) << std::endl;
-    for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
-      Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
-      Debug(c) << "   Instantiation rows for " << ic << " : ";
-      for( unsigned k=0; k<d_instRows[ic].size(); k++ ){
-        if( k>0 ){
-          Debug(c) << ", ";
-        }
-        Debug(c) << d_instRows[ic][k];
-      }
-      Debug(c) << std::endl;
-    }
-  }
-}
-
-//say instantiation row x for quantifier f is coeff*var + A*t[e] + term = beta,
-// where var is an instantiation constant from f,
-// t[e] is a vector of terms containing instantiation constants from f,
-// and term is a ground term (c1*t1 + ... + cn*tn).
-// We construct the term ( beta - term )/coeff to use as an instantiation for var.
-bool InstStrategySimplex::doInstantiation( Node f, Node ic, Node term, ArithVar x, InstMatch& m, Node var ){
-  //first try +delta
-  if( doInstantiation2( f, ic, term, x, m, var ) ){
-    ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith);
-    return true;
-  }else{
-#ifdef ARITH_INSTANTIATOR_USE_MINUS_DELTA
-    //otherwise try -delta
-    if( doInstantiation2( f, ic, term, x, m, var, true ) ){
-      ++(d_quantEngine->d_statistics.d_instantiations_cbqi_arith);
-      return true;
-    }else{
-      return false;
-    }
-#else
-    return false;
-#endif
-  }
-}
-
-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 );
-  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{
-        Assert( d_ceTableaux[ic][x][var].getKind()==CONST_RATIONAL );
-        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;
-  }
-}
-/*
-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 );
-    return getTableauxValue( v, minus_delta );
-  }else{
-    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 );
-  Rational qmodel = drv.substituteDelta( minus_delta ? -delta : delta );
-  return mkRationalNode(qmodel);
-}
-
-
-
 //new implementation
 
 bool CegqiOutputInstStrategy::doAddInstantiation( std::vector< Node >& subs ) {
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index e88842822..18f4f4a31 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -109,50 +109,6 @@ public:
   Node getNextDecisionRequest();
 };
 
-
-class InstStrategySimplex : public InstStrategyCbqi {
-protected:
-  /** reference to theory arithmetic */
-  arith::TheoryArith* d_th;
-  /** quantifiers we should process */
-  std::map< Node, bool > d_quantActive;
-  /** delta */
-  std::map< TypeNode, Node > d_deltas;
-  /** for each quantifier, simplex rows */
-  std::map< Node, std::vector< arith::ArithVar > > d_instRows;
-  /** tableaux */
-  std::map< Node, std::map< arith::ArithVar, Node > > d_tableaux_term;
-  std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux_ce_term;
-  std::map< Node, std::map< arith::ArithVar, std::map< Node, Node > > > d_tableaux;
-  /** 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( arith::ArithVar v, bool minus_delta = false );
-  /** do instantiation */
-  bool doInstantiation( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var );
-  bool doInstantiation2( Node f, Node ic, Node term, arith::ArithVar x, InstMatch& m, Node var, bool minus_delta = false );
-  /** add term to row */
-  void addTermToRow( Node ic, arith::ArithVar x, Node n, NodeBuilder<>& t );
-  /** print debug */
-  void debugPrint( const char* c );
-private:
-  /** */
-  int d_counter;
-  /** constants */
-  Node d_zero;
-  Node d_negOne;
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  void process( Node f, Theory::Effort effort, int e );
-public:
-  InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
-  ~InstStrategySimplex() throw() {}
-  /** identify */
-  std::string identify() const { return std::string("Simplex"); }
-};
-
-
 //generalized counterexample guided quantifier instantiation
 
 class InstStrategyCegqi;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 7c1fd82d3..dc3f0cdd5 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -225,15 +225,10 @@ void QuantifiersEngine::finishInit(){
     d_modules.push_back(  d_inst_engine );
   }
   if( options::cbqi() ){
-    if( options::cbqiSplx() ){
-      d_i_cbqi = new quantifiers::InstStrategySimplex( (arith::TheoryArith*)getTheoryEngine()->theoryOf( THEORY_ARITH ), this );
-      d_modules.push_back( d_i_cbqi );
-    }else{
-      d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
-      d_modules.push_back( d_i_cbqi );
-      if( options::cbqiModel() ){
-        needsBuilder = true;
-      }
+    d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
+    d_modules.push_back( d_i_cbqi );
+    if( options::cbqiModel() ){
+      needsBuilder = true;
     }
   }
   if( options::ceGuidedInst() ){