Minor cleaning of sygus term database (#3159)

4 files changed, 110 insertions, 129 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 9802ce049..fea2ce15a 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -17,6 +17,7 @@
 #include "expr/datatype.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
+#include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -230,7 +231,7 @@ int CegSingleInvSol::collectReconstructNodes(Node t, TypeNode stn, int& status)
     int carg = -1;
     int karg = -1;
     // first, do standard minimizations
-    Node min_t = d_qe->getTermDatabaseSygus()->minimizeBuiltinTerm( t );
+    Node min_t = minimizeBuiltinTerm(t);
     Trace("csi-rcons-debug") << "Minimized term is : " << min_t << std::endl;
     //check if op is in syntax sort
     carg = d_qe->getTermDatabaseSygus()->getOpConsNum( stn, min_t );
@@ -447,32 +448,6 @@ bool CegSingleInvSol::collectReconstructNodes(int pid,
   return true;
 }
 
-  /*
-  //flatten ITEs if necessary  TODO : carry assignment or move this elsewhere
-  if( t.getKind()==ITE ){
-    TypeNode cstn = tds->getArgType( dt[karg], 0 );
-    tds->registerSygusType( cstn );
-    Node prev_t;
-    while( !tds->hasKind( cstn, t[0].getKind() ) && t!=prev_t ){
-      prev_t = t;
-      Node exp_c = tds->expandBuiltinTerm( t[0] );
-      if( !exp_c.isNull() ){
-        t = NodeManager::currentNM()->mkNode( ITE, exp_c, t[1], t[2] );
-        Trace("csi-rcons-debug") << "Pre expand to " << t << std::endl;
-      }
-      t = flattenITEs( t, false );
-      if( t!=prev_t ){
-        Trace("csi-rcons-debug") << "Flatten ITE to " << t << std::endl;
-        std::map< Node, bool > sassign;
-        std::vector< Node > svars;
-        std::vector< Node > ssubs;
-        t = simplifySolutionNode( t, sassign, svars, ssubs, 0 );
-      }
-      Assert( t.getKind()==ITE );
-    }
-  }
-  */
-
 Node CegSingleInvSol::CegSingleInvSol::getReconstructedSolution(int id,
                                                                 bool mod_eq)
 {
@@ -765,16 +740,16 @@ Node CegSingleInvSol::builtinToSygusConst(Node c, TypeNode tn, int rcons_depth)
         if (rcons_depth < 1000)
         {
           // accelerated, recursive reconstruction of constants
-          Kind pk = tds->getPlusKind(TypeNode::fromType(dt.getSygusType()));
+          Kind pk = getPlusKind(TypeNode::fromType(dt.getSygusType()));
           if (pk != UNDEFINED_KIND)
           {
             int arg = tds->getKindConsNum(tn, pk);
             if (arg != -1)
             {
               Kind ck =
-                  tds->getComparisonKind(TypeNode::fromType(dt.getSygusType()));
+                  getComparisonKind(TypeNode::fromType(dt.getSygusType()));
               Kind pkm =
-                  tds->getPlusKind(TypeNode::fromType(dt.getSygusType()), true);
+                  getPlusKind(TypeNode::fromType(dt.getSygusType()), true);
               // get types
               Assert(dt[arg].getNumArgs() == 2);
               TypeNode tn1 = tds->getArgType(dt[arg], 0);
@@ -843,7 +818,7 @@ void CegSingleInvSol::registerType(TypeNode tn)
   const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
   TypeNode btn = TypeNode::fromType(dt.getSygusType());
   // for constant reconstruction
-  Kind ck = tds->getComparisonKind(btn);
+  Kind ck = getComparisonKind(btn);
   Node z = d_qe->getTermUtil()->getTypeValue(btn, 0);
 
   // iterate over constructors
@@ -1011,6 +986,98 @@ Node CegSingleInvSol::getGenericBase(TypeNode tn, const Datatype& dt, int c)
   d_generic_base[tn][c] = gr;
   return gr;
 }
+
+Node CegSingleInvSol::minimizeBuiltinTerm(Node n)
+{
+  Kind nk = n.getKind();
+  if ((nk != EQUAL && nk != LEQ && nk != LT && nk != GEQ && nk != GT)
+      || !n[0].getType().isReal())
+  {
+    return n;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  bool changed = false;
+  std::vector<Node> mon[2];
+  for (unsigned r = 0; r < 2; r++)
+  {
+    unsigned ro = r == 0 ? 1 : 0;
+    Node c;
+    Node nc;
+    if (n[r].getKind() == PLUS)
+    {
+      for (unsigned i = 0; i < n[r].getNumChildren(); i++)
+      {
+        if (ArithMSum::getMonomial(n[r][i], c, nc)
+            && c.getConst<Rational>().isNegativeOne())
+        {
+          mon[ro].push_back(nc);
+          changed = true;
+        }
+        else
+        {
+          if (!n[r][i].isConst() || !n[r][i].getConst<Rational>().isZero())
+          {
+            mon[r].push_back(n[r][i]);
+          }
+        }
+      }
+    }
+    else
+    {
+      if (ArithMSum::getMonomial(n[r], c, nc)
+          && c.getConst<Rational>().isNegativeOne())
+      {
+        mon[ro].push_back(nc);
+        changed = true;
+      }
+      else
+      {
+        if (!n[r].isConst() || !n[r].getConst<Rational>().isZero())
+        {
+          mon[r].push_back(n[r]);
+        }
+      }
+    }
+  }
+  if (changed)
+  {
+    Node nn[2];
+    for (unsigned r = 0; r < 2; r++)
+    {
+      nn[r] = mon[r].size() == 0
+                  ? nm->mkConst(Rational(0))
+                  : (mon[r].size() == 1 ? mon[r][0] : nm->mkNode(PLUS, mon[r]));
+    }
+    return nm->mkNode(n.getKind(), nn[0], nn[1]);
+  }
+  return n;
+}
+
+Kind CegSingleInvSol::getComparisonKind(TypeNode tn)
+{
+  if (tn.isInteger() || tn.isReal())
+  {
+    return LT;
+  }
+  else if (tn.isBitVector())
+  {
+    return BITVECTOR_ULT;
+  }
+  return UNDEFINED_KIND;
+}
+
+Kind CegSingleInvSol::getPlusKind(TypeNode tn, bool is_neg)
+{
+  if (tn.isInteger() || tn.isReal())
+  {
+    return is_neg ? MINUS : PLUS;
+  }
+  else if (tn.isBitVector())
+  {
+    return is_neg ? BITVECTOR_SUB : BITVECTOR_PLUS;
+  }
+  return UNDEFINED_KIND;
+}
 }
 }
 }
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
index d8239b530..c319080af 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
@@ -181,6 +181,18 @@ private:
                 std::vector<Node>& args,
                 int index_exc = -1,
                 int index_start = 0);
+  /** given a term, construct an equivalent smaller one that respects syntax */
+  Node minimizeBuiltinTerm(Node n);
+  /**
+   * Return the kind of "is less than" for type tn, where tn is either Int or
+   * BV.
+   */
+  static Kind getComparisonKind(TypeNode tn);
+  /**
+   * Return the kind of "plus" for type tn, or "minus" if is_neg is true, where
+   * tn is either Int or BV.
+   */
+  static Kind getPlusKind(TypeNode tn, bool is_neg = false);
 };
 
 
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index af8c93e45..208c8b9a0 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -1294,89 +1294,6 @@ bool TermDbSygus::canConstructKind(TypeNode tn,
   return false;
 }
 
-Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
-  if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) &&
-      ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){
-    bool changed = false;
-    std::vector< Node > mon[2];
-    for( unsigned r=0; r<2; r++ ){
-      unsigned ro = r==0 ? 1 : 0;
-      Node c;
-      Node nc;
-      if( n[r].getKind()==PLUS ){
-        for( unsigned i=0; i<n[r].getNumChildren(); i++ ){
-          if (ArithMSum::getMonomial(n[r][i], c, nc)
-              && c.getConst<Rational>().isNegativeOne())
-          {
-            mon[ro].push_back( nc );
-            changed = true;
-          }else{
-            if( !n[r][i].isConst() || !n[r][i].getConst<Rational>().isZero() ){
-              mon[r].push_back( n[r][i] );
-            }
-          }
-        }
-      }else{
-        if (ArithMSum::getMonomial(n[r], c, nc)
-            && c.getConst<Rational>().isNegativeOne())
-        {
-          mon[ro].push_back( nc );
-          changed = true;
-        }else{
-          if( !n[r].isConst() || !n[r].getConst<Rational>().isZero() ){
-            mon[r].push_back( n[r] );
-          }
-        }
-      }
-    }
-    if( changed ){
-      Node nn[2];
-      for( unsigned r=0; r<2; r++ ){
-        nn[r] = mon[r].size()==0 ? NodeManager::currentNM()->mkConst( Rational(0) ) : ( mon[r].size()==1 ? mon[r][0] : NodeManager::currentNM()->mkNode( PLUS, mon[r] ) );
-      }
-      return NodeManager::currentNM()->mkNode( n.getKind(), nn[0], nn[1] );
-    }
-  }
-  return n;
-}
-
-Node TermDbSygus::expandBuiltinTerm( Node t ){
-  if( t.getKind()==EQUAL ){
-    if( t[0].getType().isReal() ){
-      return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ),
-                                                    NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) );
-    }else if( t[0].getType().isBoolean() ){
-      return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
-                                                   NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
-    }
-  }else if( t.getKind()==ITE && t.getType().isBoolean() ){
-    return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
-                                                 NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) );
-  }
-  return Node::null();
-}
-
-
-Kind TermDbSygus::getComparisonKind( TypeNode tn ) {
-  if( tn.isInteger() || tn.isReal() ){
-    return LT;
-  }else if( tn.isBitVector() ){
-    return BITVECTOR_ULT;
-  }else{
-    return UNDEFINED_KIND;
-  }
-}
-
-Kind TermDbSygus::getPlusKind( TypeNode tn, bool is_neg ) {
-  if( tn.isInteger() || tn.isReal() ){
-    return is_neg ? MINUS : PLUS;
-  }else if( tn.isBitVector() ){
-    return is_neg ? BITVECTOR_SUB : BITVECTOR_PLUS;
-  }else{
-    return UNDEFINED_KIND;
-  }
-}
-
 bool TermDbSygus::involvesDivByZero( Node n, std::map< Node, bool >& visited ){
   if( visited.find( n )==visited.end() ){
     visited[n] = true;
@@ -1410,14 +1327,6 @@ bool TermDbSygus::involvesDivByZero( Node n ) {
   return involvesDivByZero( n, visited );
 }
 
-void doStrReplace(std::string& str, const std::string& oldStr, const std::string& newStr){
-  size_t pos = 0;
-  while((pos = str.find(oldStr, pos)) != std::string::npos){
-     str.replace(pos, oldStr.length(), newStr);
-     pos += newStr.length();
-  }
-}
-
 Node TermDbSygus::getAnchor( Node n ) {
   if( n.getKind()==APPLY_SELECTOR_TOTAL ){
     return getAnchor( n[0] );
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 2854ecab6..e0312c516 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -564,13 +564,6 @@ class TermDbSygus {
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
   Node getNormalized(TypeNode t, Node prog);
   unsigned getSygusTermSize( Node n );
-  /** given a term, construct an equivalent smaller one that respects syntax */
-  Node minimizeBuiltinTerm( Node n );
-  /** given a term, expand it into more basic components */
-  Node expandBuiltinTerm( Node n );
-  /** get comparison kind */
-  Kind getComparisonKind( TypeNode tn );
-  Kind getPlusKind( TypeNode tn, bool is_neg = false );
   /** involves div-by-zero */
   bool involvesDivByZero( Node n );
   /** get anchor */