Eliminate option for sygus UF evaluation functions (#2262)

9 files changed, 19 insertions, 68 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 443cd0bd0..8366fe4e1 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -256,48 +256,6 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt,
   Trace("dt-sygus-util") << "...return " << ret << std::endl;
   return ret;
 }
-Node DatatypesRewriter::mkSygusEvalApp(const std::vector<Node>& children)
-{
-  if (options::sygusEvalBuiltin())
-  {
-    return NodeManager::currentNM()->mkNode(DT_SYGUS_EVAL, children);
-  }
-  // otherwise, using APPLY_UF
-  Assert(!children.empty());
-  Assert(children[0].getType().isDatatype());
-  const Datatype& dt =
-      static_cast<DatatypeType>(children[0].getType().toType()).getDatatype();
-  Assert(dt.isSygus());
-  std::vector<Node> schildren;
-  schildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc()));
-  schildren.insert(schildren.end(), children.begin(), children.end());
-  return NodeManager::currentNM()->mkNode(APPLY_UF, schildren);
-}
-
-bool DatatypesRewriter::isSygusEvalApp(Node n)
-{
-  if (options::sygusEvalBuiltin())
-  {
-    return n.getKind() == DT_SYGUS_EVAL;
-  }
-  // otherwise, using APPLY_UF
-  if (n.getKind() != APPLY_UF || n.getNumChildren() == 0)
-  {
-    return false;
-  }
-  TypeNode tn = n[0].getType();
-  if (!tn.isDatatype())
-  {
-    return false;
-  }
-  const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
-  if (!dt.isSygus())
-  {
-    return false;
-  }
-  Node eval_op = Node::fromExpr(dt.getSygusEvaluationFunc());
-  return eval_op == n.getOperator();
-}
 
 RewriteResponse DatatypesRewriter::preRewrite(TNode in)
 {
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index b99c5fb53..7d91544e1 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -130,10 +130,6 @@ public:
  static Node mkSygusTerm(const Datatype& dt,
                          unsigned i,
                          const std::vector<Node>& children);
- /** make sygus evaluation function application */
- static Node mkSygusEvalApp(const std::vector<Node>& children);
- /** is sygus evaluation function */
- static bool isSygusEvalApp(Node n);
  /**
   * Get the builtin sygus operator for constructor term n of sygus datatype
   * type. For example, if n is the term C_+( d1, d2 ) where C_+ is a sygus
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 36cbb89fe..ac7467c00 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -32,7 +32,7 @@ void SygusEvalUnfold::registerEvalTerm(Node n)
 {
   Assert(options::sygusEvalUnfold());
   // is this a sygus evaluation function application?
-  if (!datatypes::DatatypesRewriter::isSygusEvalApp(n))
+  if (n.getKind() != DT_SYGUS_EVAL)
   {
     return;
   }
@@ -140,15 +140,13 @@ void SygusEvalUnfold::registerModelValue(Node a,
         }
         if (do_unfold)
         {
-          // TODO (#1949) : this is replicated for different values, possibly
-          // do better caching
+          // note that this is replicated for different values
           std::map<Node, Node> vtm;
           std::vector<Node> exp;
           vtm[n] = vn;
           eval_children.insert(
               eval_children.end(), it->second[i].begin(), it->second[i].end());
-          Node eval_fun =
-              datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children);
+          Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
           eval_children.resize(1);
           res = d_tds->unfold(eval_fun, vtm, exp);
           expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
@@ -158,11 +156,9 @@ void SygusEvalUnfold::registerModelValue(Node a,
           EvalSygusInvarianceTest esit;
           eval_children.insert(
               eval_children.end(), it->second[i].begin(), it->second[i].end());
-          Node conj =
-              datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children);
+          Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children);
           eval_children[0] = vn;
-          Node eval_fun =
-              datatypes::DatatypesRewriter::mkSygusEvalApp(eval_children);
+          Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
           res = d_tds->evaluateWithUnfolding(eval_fun);
           esit.init(conj, n, res);
           eval_children.resize(1);
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index efffa046f..deea1c261 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -268,6 +268,7 @@ Node CegGrammarConstructor::process(Node q,
 }
 
 Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars ){
+  NodeManager* nm = NodeManager::currentNM();
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
   std::stack<TNode> visit;
@@ -323,7 +324,7 @@ Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >&
       if (makeEvalFun)
       {
         // will make into an application of an evaluation function
-        ret = datatypes::DatatypesRewriter::mkSygusEvalApp(children);
+        ret = nm->mkNode(DT_SYGUS_EVAL, children);
       }
       else if (childChanged)
       {
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 56d2cf2b5..6a82b9dad 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -48,7 +48,7 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited,
     Node neval;
     Node n_output;
     bool neval_is_evalapp = false;
-    if (datatypes::DatatypesRewriter::isSygusEvalApp(n))
+    if (n.getKind() == DT_SYGUS_EVAL)
     {
       neval = n;
       if( hasPol ){
@@ -57,7 +57,7 @@ void CegConjecturePbe::collectExamples( Node n, std::map< Node, bool >& visited,
       neval_is_evalapp = true;
     }else if( n.getKind()==EQUAL && hasPol && !pol ){
       for( unsigned r=0; r<2; r++ ){
-        if (datatypes::DatatypesRewriter::isSygusEvalApp(n[r]))
+        if (n[r].getKind() == DT_SYGUS_EVAL)
         {
           neval = n[r];
           if( n[1-r].isConst() ){
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 71449029b..514f42fb1 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -463,7 +463,7 @@ Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates,
     if (it == visited.end())
     {
       visited[cur] = Node::null();
-      if (datatypes::DatatypesRewriter::isSygusEvalApp(cur))
+      if (cur.getKind() == DT_SYGUS_EVAL)
       {
         Node v = cur[0];
         if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 759ee6ffa..183f40b66 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -81,7 +81,7 @@ Node SygusUnifRl::purifyLemma(Node n,
   // We retrive model value now because purified node may not have a value
   Node nv = n;
   // Whether application of a function-to-synthesize
-  bool fapp = datatypes::DatatypesRewriter::isSygusEvalApp(n);
+  bool fapp = (n.getKind() == DT_SYGUS_EVAL);
   bool u_fapp = false;
   bool nu_fapp = false;
   if (fapp)
@@ -194,7 +194,7 @@ Node SygusUnifRl::purifyLemma(Node n,
       children[0] = new_f;
       Trace("sygus-unif-rl-purify-debug") << "Make sygus eval app " << children
                                           << std::endl;
-      np = datatypes::DatatypesRewriter::mkSygusEvalApp(children);
+      np = nm->mkNode(DT_SYGUS_EVAL, children);
       d_app_to_purified[nb] = np;
     }
     else
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 6e01ff084..3cbac1eaa 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -254,7 +254,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
     {
       echildren.push_back(sbv);
     }
-    Node eut = datatypes::DatatypesRewriter::mkSygusEvalApp(echildren);
+    Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren);
     Trace("sygus-unif-debug2") << "  Test evaluation of " << eut << "..."
                                << std::endl;
     eut = d_qe->getTermDatabaseSygus()->unfold(eut);
@@ -296,7 +296,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
         echildren[0] = sks[k];
         Trace("sygus-unif-debug2") << "...set eval dt to " << sks[k]
                                    << std::endl;
-        Node esk = datatypes::DatatypesRewriter::mkSygusEvalApp(echildren);
+        Node esk = nm->mkNode(DT_SYGUS_EVAL, echildren);
         vs.push_back(esk);
         Node tvar = nm->mkSkolem("templ", esk.getType());
         templ_var_index[tvar] = k;
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 99ab54a2c..54e731694 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -1557,7 +1557,7 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) {
 }
 
 Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) {
-  if (!datatypes::DatatypesRewriter::isSygusEvalApp(en))
+  if (en.getKind() != DT_SYGUS_EVAL)
   {
     Assert(en.isConst());
     return en;
@@ -1640,7 +1640,7 @@ Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Nod
       vtm[s] = ev[j];
     }
     cc.insert(cc.end(), args.begin(), args.end());
-    pre[j] = datatypes::DatatypesRewriter::mkSygusEvalApp(cc);
+    pre[j] = nm->mkNode(DT_SYGUS_EVAL, cc);
   }
   Node ret = mkGeneric(dt, i, pre);
   // if it is a variable, apply the substitution
@@ -1667,7 +1667,7 @@ Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) {
   if( itv==visited.end() ){
     Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl;
     Node ret;
-    if (datatypes::DatatypesRewriter::isSygusEvalApp(n))
+    if (n.getKind() == DT_SYGUS_EVAL)
     {
       TypeNode tn = n[0].getType();
       Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl;
@@ -1771,7 +1771,7 @@ Node TermDbSygus::evaluateWithUnfolding(
       visited.find(n);
   if( it==visited.end() ){
     Node ret = n;
-    while (datatypes::DatatypesRewriter::isSygusEvalApp(ret)
+    while (ret.getKind() == DT_SYGUS_EVAL
            && ret[0].getKind() == APPLY_CONSTRUCTOR)
     {
       ret = unfold( ret );
@@ -1806,7 +1806,7 @@ Node TermDbSygus::evaluateWithUnfolding( Node n ) {
 
 bool TermDbSygus::isEvaluationPoint(Node n) const
 {
-  if (!datatypes::DatatypesRewriter::isSygusEvalApp(n))
+  if (n.getKind() != DT_SYGUS_EVAL)
   {
     return false;
   }