From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 4 Nov 2019 17:11:38 +0000 (-0600)
Subject: Eliminate deprecated utility function from sygus (#3431)
X-Git-Tag: cvc5-1.0.0~3862
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9854e505aeae1ac86ea75e98131dd8643349df60;p=cvc5.git

Eliminate deprecated utility function from sygus (#3431)
---

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 3a1ddc73c..aa0af6f1d 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -589,10 +589,9 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
   Node sbody = d_base_body.substitute(
       candidates.begin(), candidates.end(), vals.begin(), vals.end());
   Trace("cegis-sample-debug2") << "Sample " << sbody << std::endl;
-  // do eager unfolding
-  std::map<Node, Node> visited_n;
-  sbody = d_qe->getTermDatabaseSygus()->getEagerUnfold(sbody, visited_n);
-  Trace("cegis-sample") << "Sample (after unfolding): " << sbody << std::endl;
+  // do eager rewriting
+  sbody = Rewriter::rewrite(sbody);
+  Trace("cegis-sample") << "Sample (after rewriting): " << sbody << std::endl;
 
   NodeManager* nm = NodeManager::currentNM();
   for (unsigned i = 0, size = d_cegis_sampler.getNumSamplePoints(); i < size;
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 78f2f6a7e..7f48d30d8 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -540,8 +540,6 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   lem = Rewriter::rewrite(lem);
   // eagerly unfold applications of evaluation function
   Trace("cegqi-debug") << "pre-unfold counterexample : " << lem << std::endl;
-  std::map<Node, Node> visited_n;
-  lem = d_tds->getEagerUnfold(lem, visited_n);
   // record the instantiation
   // this is used for remembering the solution
   recordInstantiation(candidate_values);
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index d4ee11453..d17c343f4 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -1030,70 +1030,6 @@ Node TermDbSygus::unfold(Node en)
   return unfold(en, vtm, exp, false);
 }
 
-Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) {
-  std::map< Node, Node >::iterator itv = visited.find( n );
-  if( itv==visited.end() ){
-    Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl;
-    Node ret;
-    if (n.getKind() == DT_SYGUS_EVAL)
-    {
-      TypeNode tn = n[0].getType();
-      Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl;
-      if( tn.isDatatype() ){
-        const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-        if( dt.isSygus() ){ 
-          Trace("cegqi-eager") << "Unfold eager : " << n << std::endl;
-          Node bTerm = sygusToBuiltin( n[0], tn );
-          Trace("cegqi-eager") << "Built-in term : " << bTerm << std::endl;
-          std::vector< Node > vars;
-          std::vector< Node > subs;
-          Node var_list = Node::fromExpr( dt.getSygusVarList() );
-          Assert(var_list.getNumChildren() + 1 == n.getNumChildren());
-          for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
-            vars.push_back( var_list[j] );
-          }
-          for( unsigned j=1; j<n.getNumChildren(); j++ ){
-            Node nc = getEagerUnfold( n[j], visited );
-            subs.push_back( nc );
-            Assert(subs[j - 1].getType().isComparableTo(
-                var_list[j - 1].getType()));
-          }
-          Assert(vars.size() == subs.size());
-          bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-          Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl;
-          Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl;
-          Assert(n.getType().isComparableTo(bTerm.getType()));
-          ret = bTerm; 
-        }
-      }
-    }
-    if( ret.isNull() ){
-      if( n.getKind()!=FORALL ){
-        bool childChanged = false;
-        std::vector< Node > children;
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          Node nc = getEagerUnfold( n[i], visited );
-          childChanged = childChanged || n[i]!=nc;
-          children.push_back( nc );
-        }
-        if( childChanged ){
-          if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-            children.insert( children.begin(), n.getOperator() );
-          }
-          ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-        }
-      }
-      if( ret.isNull() ){
-        ret = n;
-      }
-    }
-    visited[n] = ret;
-    return ret;
-  }else{
-    return itv->second;
-  }
-}
-
 Node TermDbSygus::evaluateBuiltin(TypeNode tn,
                                   Node bn,
                                   std::vector<Node>& args,
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 68381fb2a..c591400e1 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -468,7 +468,6 @@ class TermDbSygus {
    * evaluation heads
    */
   Node unfold(Node en);
-  Node getEagerUnfold( Node n, std::map< Node, Node >& visited );
 };
 
 }/* CVC4::theory::quantifiers namespace */