More unused code elimination (#2339)

9 files changed, 48 insertions, 255 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index a8e5d74b6..fe6764297 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -432,18 +432,6 @@ RewriteResponse DatatypesRewriter::rewriteTester(TNode in)
                            NodeManager::currentNM()->mkConst(true));
   }
   // could try dt.getNumConstructors()==2 && indexOf(in.getOperator())==1 ?
-  else if (!options::dtUseTesters())
-  {
-    unsigned tindex = indexOf(in.getOperator());
-    Trace("datatypes-rewrite-debug") << "Convert " << in << " to equality "
-                                     << in[0] << " " << tindex << std::endl;
-    Node neq = mkTester(in[0], tindex, dt);
-    Assert(neq != in);
-    Trace("datatypes-rewrite")
-        << "DatatypesRewriter::postRewrite: Rewrite tester " << in << " to "
-        << neq << std::endl;
-    return RewriteResponse(REWRITE_AGAIN_FULL, neq);
-  }
   return RewriteResponse(REWRITE_DONE, in);
 }
 
@@ -552,64 +540,19 @@ int DatatypesRewriter::isInstCons(Node t, Node n, const Datatype& dt)
 
 int DatatypesRewriter::isTester(Node n, Node& a)
 {
-  if (options::dtUseTesters())
-  {
-    if (n.getKind() == kind::APPLY_TESTER)
-    {
-      a = n[0];
-      return indexOf(n.getOperator());
-    }
-  }
-  else
+  if (n.getKind() == kind::APPLY_TESTER)
   {
-    if (n.getKind() == kind::EQUAL)
-    {
-      for (int i = 1; i >= 0; i--)
-      {
-        if (n[i].getKind() == kind::APPLY_CONSTRUCTOR)
-        {
-          const Datatype& dt =
-              Datatype::datatypeOf(n[i].getOperator().toExpr());
-          int ic = isInstCons(n[1 - i], n[i], dt);
-          if (ic != -1)
-          {
-            a = n[1 - i];
-            return ic;
-          }
-        }
-      }
-    }
+    a = n[0];
+    return indexOf(n.getOperator());
   }
   return -1;
 }
 
 int DatatypesRewriter::isTester(Node n)
 {
-  if (options::dtUseTesters())
+  if (n.getKind() == kind::APPLY_TESTER)
   {
-    if (n.getKind() == kind::APPLY_TESTER)
-    {
-      return indexOf(n.getOperator().toExpr());
-    }
-  }
-  else
-  {
-    if (n.getKind() == kind::EQUAL)
-    {
-      for (int i = 1; i >= 0; i--)
-      {
-        if (n[i].getKind() == kind::APPLY_CONSTRUCTOR)
-        {
-          const Datatype& dt =
-              Datatype::datatypeOf(n[i].getOperator().toExpr());
-          int ic = isInstCons(n[1 - i], n[i], dt);
-          if (ic != -1)
-          {
-            return ic;
-          }
-        }
-      }
-    }
+    return indexOf(n.getOperator().toExpr());
   }
   return -1;
 }
@@ -634,21 +577,8 @@ unsigned DatatypesRewriter::indexOf(Node n)
 
 Node DatatypesRewriter::mkTester(Node n, int i, const Datatype& dt)
 {
-  if (options::dtUseTesters())
-  {
-    return NodeManager::currentNM()->mkNode(
-        kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), n);
-  }
-#ifdef CVC4_ASSERTIONS
-  Node ret = n.eqNode(DatatypesRewriter::getInstCons(n, dt, i));
-  Node a;
-  int ii = isTester(ret, a);
-  Assert(ii == i);
-  Assert(a == n);
-  return ret;
-#else
-  return n.eqNode(DatatypesRewriter::getInstCons(n, dt, i));
-#endif
+  return NodeManager::currentNM()->mkNode(
+      kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), n);
 }
 
 Node DatatypesRewriter::mkSplit(Node n, const Datatype& dt)
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index f886c6d3f..65df3a642 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -824,24 +824,6 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
         if( !cons1.isNull() && !cons2.isNull() ){
           Trace("datatypes-debug") << "  constructors : " << cons1 << " " << cons2 << std::endl;
           Node unifEq = cons1.eqNode( cons2 );
-          /*
-          std::vector< Node > exp;
-          std::vector< std::pair< TNode, TNode > > deq_cand;
-          bool conf = checkClashModEq( cons1, cons2, exp, deq_cand );
-          if( !conf ){
-            for( unsigned i=0; i<deq_cand.size(); i++ ){
-              if( d_equalityEngine.areDisequal( deq_cand[i].first, deq_cand[i].second, true ) ){
-                conf = true;
-                Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, deq_cand[i].first, deq_cand[i].second );
-                exp.push_back( eq.negate() );
-              }
-            }
-          }
-          if( conf ){
-            exp.push_back( unifEq );
-            d_conflictNode = explain( exp );
-          }
-         */
           std::vector< Node > rew;
           if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){
             d_conflictNode = explain( unifEq );
@@ -1747,41 +1729,41 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index
 void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
   //add constructor to equivalence class if not done so already
   int index = getLabelIndex( eqc, n );
-  if( index!=-1 && !eqc->d_inst ){
-    if( options::dtUseTesters() ){
-      Node exp;
-      Node tt;
-      if( !eqc->d_constructor.get().isNull() ){
-        exp = d_true;
-        tt = eqc->d_constructor;
-      }else{
-        exp = getLabel( n );
-        tt = exp[0];
-      }
-      const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
-      //instantiate this equivalence class
-      eqc->d_inst = true;
-      Node tt_cons = getInstantiateCons( tt, dt, index );
-      Node eq;
-      if( tt!=tt_cons ){
-        eq = tt.eqNode( tt_cons );
-        Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl;
-        d_pending.push_back( eq );
-        d_pending_exp[ eq ] = exp;
-        Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl;
-        Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl;
-        //eqc->d_inst.set( eq );
-        d_infer.push_back( eq );
-        d_infer_exp.push_back( exp );
-      }
-    }else{
-      eqc->d_inst = true;
-    }
-    //}
-    //else{
-    //  Debug("datatypes-inst") << "Do not instantiate" << std::endl;
-    //}
+  if (index == -1 || eqc->d_inst)
+  {
+    return;
+  }
+  Node exp;
+  Node tt;
+  if (!eqc->d_constructor.get().isNull())
+  {
+    exp = d_true;
+    tt = eqc->d_constructor;
+  }
+  else
+  {
+    exp = getLabel(n);
+    tt = exp[0];
+  }
+  const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
+  // instantiate this equivalence class
+  eqc->d_inst = true;
+  Node tt_cons = getInstantiateCons(tt, dt, index);
+  Node eq;
+  if (tt == tt_cons)
+  {
+    return;
   }
+  eq = tt.eqNode(tt_cons);
+  Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq
+                          << std::endl;
+  d_pending.push_back(eq);
+  d_pending_exp[eq] = exp;
+  Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl;
+  Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp
+                           << std::endl;
+  d_infer.push_back(eq);
+  d_infer_exp.push_back(exp);
 }
 
 void TheoryDatatypes::checkCycles() {
@@ -2197,38 +2179,6 @@ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) {
   }
 }
 
-bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ) {
-  if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) {
-    if( n1.getOperator() != n2.getOperator() ) {
-      return true;
-    } else {
-      Assert( n1.getNumChildren() == n2.getNumChildren() );
-      for( int i=0; i<(int)n1.getNumChildren(); i++ ) {
-        TNode nc1 = getEqcConstructor( n1[i] );
-        TNode nc2 = getEqcConstructor( n2[i] );
-        if( checkClashModEq( nc1, nc2, exp, deq_cand ) ) {
-          if( nc1!=n1[i] ){
-            exp.push_back( nc1.eqNode( n1[i] ) );
-          }
-          if( nc2!=n2[i] ){
-            exp.push_back( nc2.eqNode( n2[i] ) );
-          }
-          return true;
-        }
-      }
-    }
-  }else if( n1!=n2 ){
-    if( n1.isConst() && n2.isConst() ){
-      return true;
-    }else{
-      if( !areEqual( n1, n2 ) ){
-        deq_cand.push_back( std::pair< TNode, TNode >( n1, n2 ) );
-      }
-    }
-  }
-  return false;
-}
-
 void TheoryDatatypes::getRelevantTerms( std::set<Node>& termSet ) {
   // Compute terms appearing in assertions and shared terms
   std::set<Kind> irr_kinds;
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index e3a375b87..e06bb7408 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -330,8 +330,6 @@ private:
   void instantiate( EqcInfo* eqc, Node n );
   /** must communicate fact */
   bool mustCommunicateFact( Node n, Node exp );
-  /** check clash mod eq */
-  bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand );
   /** get relevant terms */
   void getRelevantTerms( std::set<Node>& termSet );
 private:
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index b3dc9965b..a8079f775 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -24,8 +24,6 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 
-#define USE_INDEX_ORDERING
-
 using namespace std;
 using namespace CVC4::kind;
 using namespace CVC4::context;
@@ -770,7 +768,7 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri
         }
       }
       Trace("fmf-eval-debug") << "Evaluate term " << n << " = ";
-      printRepresentativeDebug( "fmf-eval-debug", val );
+      Trace("fmf-eval-debug") << getRepresentative(val);
       Trace("fmf-eval-debug") << " (term " << val << "), depIndex = " << depIndex << std::endl;
     }
   }
@@ -859,7 +857,6 @@ struct sortGetMaxVariableNum {
 
 void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){
   if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
-#ifdef USE_INDEX_ORDERING
     //sort arguments in order of least significant vs. most significant variable in default ordering
     std::map< Node, std::vector< int > > argIndex;
     std::vector< Node > args;
@@ -889,30 +886,8 @@ void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){
       Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " ";
     }
     Debug("fmf-index-order") << std::endl;
-#else
-    d_eval_uf_use_default[n] = true;
-#endif
-  }
-}
-
-/*
-Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
-  std::vector< Node > children;
-  children.push_back(n.getOperator());
-  children.insert(children.end(), args.begin(), args.end());
-  Node nv = NodeManager::currentNM()->mkNode(APPLY_UF, children);
-  //make the term model specifically for nv
-  makeEvalUfModel( nv );
-  int argDepIndex;
-  if( d_eval_uf_use_default[nv] ){
-    return d_uf_model_tree[ n.getOperator() ].getValue( this, nv, argDepIndex );
-  }else{
-    return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex );
   }
 }
-*/
-
-
 
 FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
 FirstOrderModel(qe, c, name){
@@ -926,17 +901,6 @@ FirstOrderModelFmc::~FirstOrderModelFmc()
   }
 }
 
-/*
-Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
-  Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;
-  for(unsigned i=0; i<args.size(); i++) {
-    args[i] = getUsedRepresentative(args[i]);
-  }
-  Assert( n.getKind()==APPLY_UF );
-  return d_models[n.getOperator()]->evaluate(this, args);
-}
-*/
-
 void FirstOrderModelFmc::processInitialize( bool ispre ) {
   if( ispre ){
     for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
@@ -1111,21 +1075,6 @@ Node FirstOrderModelAbs::getFunctionValue(Node op, const char* argPrefix ) {
   return Node::null();
 }
 
-/*
-Node FirstOrderModelAbs::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
-  Debug("qint-debug") << "get curr uf value " << n << std::endl;
-  if( d_models_valid[n] ){
-    TypeNode tn = n.getType();
-    if( tn.getNumChildren()>0 ){
-      tn = tn[tn.getNumChildren()-1];
-    }
-    return d_models[n]->evaluate( this, tn, args );
-  }else{
-    return Node::null();
-  }
-}
-*/
-
 void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) {
   if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){
     Node op = n.getKind()==APPLY_UF ? n.getOperator() : n;
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index fcc9cd060..d1b7eebb8 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -194,7 +194,7 @@ Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue(
     double score = (1.0 + static_cast<double>(d_value_pro_con[0][v].size()))
                    / (1.0 + static_cast<double>(d_value_pro_con[1][v].size()));
     Debug("fmf-model-cons-debug") << "  - score( ";
-    m->printRepresentativeDebug("fmf-model-cons-debug", v);
+    Debug("fmf-model-cons-debug") << m->getRepresentative(v);
     Debug("fmf-model-cons-debug") << " ) = " << score << std::endl;
     if (score > maxScore)
     {
@@ -213,7 +213,7 @@ Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue(
     {
       defaultVal = newDefaultVal;
       Debug("fmf-model-cons-debug") << "-> Change default value to ";
-      m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal);
+      Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal);
       Debug("fmf-model-cons-debug") << std::endl;
     }
     else
@@ -227,7 +227,7 @@ Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue(
   }
   // get the default term (this term must be defined non-ground in model)
   Debug("fmf-model-cons-debug") << "  Choose ";
-  m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal);
+  Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal);
   Debug("fmf-model-cons-debug")
       << " as default value (" << defaultTerm << ")" << std::endl;
   Debug("fmf-model-cons-debug")
@@ -437,7 +437,7 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
       fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val );
       fmig->d_uf_model_gen[op].makeModel( fmig, it->second );
       Debug("fmf-model-cons") << "Function " << op << " is the constant function ";
-      fmig->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val );
+      Debug("fmf-model-cons") << d_uf_prefs[op].d_const_val;
       Debug("fmf-model-cons") << std::endl;
       d_uf_model_constructed[op] = true;
     }else{
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 73d2de401..8c43e98ff 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -116,7 +116,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   }
   
   if( options::inferArithTriggerEq() ){
-    d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() );
+    d_eq_inference = new quantifiers::EqualityInference(c, false);
   }else{
     d_eq_inference = NULL;
   }
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 42818d581..34e1d455b 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -542,36 +542,6 @@ bool TheoryModel::areDisequal(TNode a, TNode b)
   }
 }
 
-//for debugging
-void TheoryModel::printRepresentativeDebug( const char* c, Node r ){
-  if( r.isNull() ){
-    Trace( c ) << "null";
-  }else if( r.getType().isBoolean() ){
-    if( areEqual( r, d_true ) ){
-      Trace( c ) << "true";
-    }else{
-      Trace( c ) << "false";
-    }
-  }else{
-    Trace( c ) << getRepresentative( r );
-  }
-}
-
-void TheoryModel::printRepresentative( std::ostream& out, Node r ){
-  Assert( !r.isNull() );
-  if( r.isNull() ){
-    out << "null";
-  }else if( r.getType().isBoolean() ){
-    if( areEqual( r, d_true ) ){
-      out  << "true";
-    }else{
-      out  << "false";
-    }
-  }else{
-    out << getRepresentative( r );
-  }
-}
-
 bool TheoryModel::areFunctionValuesEnabled() const
 {
   return d_enableFuncModels;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index ac0d686de..47d68a365 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -251,10 +251,6 @@ public:
   Expr getValue(Expr expr) const override;
   /** get cardinality for sort */
   Cardinality getCardinality(Type t) const override;
-  /** print representative debug function */
-  void printRepresentativeDebug( const char* c, Node r );
-  /** print representative function */
-  void printRepresentative( std::ostream& out, Node r );
 
   //---------------------------- function values
   /** a map from functions f to a list of all APPLY_UF terms with operator f */
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 3d656cf24..a3e058569 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -289,7 +289,7 @@ void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector
   }else{
     indent( out, ind );
     out << "return ";
-    m->printRepresentative( out, d_value );
+    out << m->getRepresentative(d_value);
     out << std::endl;
   }
 }