From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 17 May 2022 21:08:02 +0000 (-0500)
Subject: Minor cleanup of datatypes theory (#8791)
X-Git-Tag: cvc5-1.0.1~121
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6620e38d71051f8a4b40b2fae507749c7e7a2684;p=cvc5.git

Minor cleanup of datatypes theory (#8791)
---

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 19f18fde5..39239ba9f 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -360,8 +360,7 @@ TrustNode TheoryDatatypes::ppRewrite(TNode in, std::vector<SkolemLemma>& lems)
     }
     else
     {
-      nn = rew.size()==0 ? d_true :
-                ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
+      nn = NodeManager::currentNM()->mkAnd(rew);
     }
     if (in != nn)
     {
@@ -420,7 +419,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
     return;
   }
   Trace("datatypes-merge") << "Merge " << t1 << " " << t2 << std::endl;
-  Assert(areEqual(t1, t2));
+  Assert(d_equalityEngine->areEqual(t1, t2));
   TNode trep1 = t1;
   TNode trep2 = t2;
   EqcInfo* eqc2 = getOrMakeEqcInfo(t2);
@@ -463,11 +462,11 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
       }
       else
       {
-        Assert(areEqual(cons1, cons2));
+        Assert(d_equalityEngine->areEqual(cons1, cons2));
         // do unification
         for (size_t i = 0, nchild = cons1.getNumChildren(); i < nchild; i++)
         {
-          if (!areEqual(cons1[i], cons2[i]))
+          if (!d_equalityEngine->areEqual(cons1[i], cons2[i]))
           {
             Node eq = cons1[i].eqNode(cons2[i]);
             d_im.addPendingInference(eq, InferenceId::DATATYPES_UNIF, unifEq);
@@ -1216,13 +1215,12 @@ bool TheoryDatatypes::instantiate(EqcInfo* eqc, Node n)
   // instantiate this equivalence class
   eqc->d_inst = true;
   Node tt_cons = getInstantiateCons(tt, dt, index);
-  Node eq;
   if (tt == tt_cons)
   {
     // not necessary
     return false;
   }
-  eq = tt.eqNode(tt_cons);
+  Node eq = tt.eqNode(tt_cons);
   // Determine if the equality must be sent out as a lemma. Notice that
   // we  keep new equalities from the instantiate rule internal
   // as long as they are for datatype constructors that have no arguments that
@@ -1710,35 +1708,12 @@ void TheoryDatatypes::checkSplit()
   }
 }
 
-bool TheoryDatatypes::hasTerm(TNode a) { return d_equalityEngine->hasTerm(a); }
-
-bool TheoryDatatypes::areEqual( TNode a, TNode b ){
-  if( a==b ){
-    return true;
-  }else if( hasTerm( a ) && hasTerm( b ) ){
-    return d_equalityEngine->areEqual(a, b);
-  }else{
-    return false;
-  }
-}
-
-bool TheoryDatatypes::areDisequal( TNode a, TNode b ){
-  if( a==b ){
-    return false;
-  }else if( hasTerm( a ) && hasTerm( b ) ){
-    return d_equalityEngine->areDisequal(a, b, false);
-  }else{
-    //TODO : constants here?
-    return false;
-  }
-}
-
 TNode TheoryDatatypes::getRepresentative( TNode a ){
-  if( hasTerm( a ) ){
+  if (d_equalityEngine->hasTerm(a))
+  {
     return d_equalityEngine->getRepresentative(a);
-  }else{
-    return a;
   }
+  return a;
 }
 
 void TheoryDatatypes::printModelDebug( const char* c ){
@@ -1831,7 +1806,8 @@ std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit)
   bool pol = lit.getKind()!=NOT;
   if( atom.getKind()==APPLY_TESTER ){
     Node n = atom[0];
-    if( hasTerm( n ) ){
+    if (d_equalityEngine->hasTerm(n))
+    {
       Node r = d_equalityEngine->getRepresentative(n);
       EqcInfo * ei = getOrMakeEqcInfo( r, false );
       int l_index = getLabelIndex( ei, r );
@@ -1846,7 +1822,7 @@ std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit)
           Node lbl = getLabel( n );
           Assert(!lbl.isNull());
           exp_c.push_back( lbl );
-          Assert(areEqual(n, lbl[0]));
+          Assert(d_equalityEngine->areEqual(n, lbl[0]));
           eqToExplain = n.eqNode(lbl[0]);
         }
         d_equalityEngine->explainLit(eqToExplain, exp_c);
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index ed0501cef..a17f2290f 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -276,9 +276,6 @@ private:
 
  private:
   //equality queries
-  bool hasTerm( TNode a );
-  bool areEqual( TNode a, TNode b );
-  bool areDisequal( TNode a, TNode b );
   TNode getRepresentative( TNode a );
 
   /** Collect model values in m based on the relevant terms given by termSet */