Eliminate option for sygus UF evaluation functions (#2262)

12 files changed, 19 insertions, 111 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 8747c530e..ae61d5f33 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -154,23 +154,6 @@ void Datatype::resolve(ExprManager* em,
     }
     d_record = new Record(fields);
   }
-  
-  //make the sygus evaluation function
-  if( isSygus() ){
-    PrettyCheckArgument(d_params.empty(), this, "sygus types cannot be parametric");
-    NodeManager* nm = NodeManager::fromExprManager(em);
-    std::string name = "eval_" + getName();
-    std::vector<TypeNode> evalType;
-    evalType.push_back(TypeNode::fromType(d_self));
-    if( !d_sygus_bvl.isNull() ){
-      for(size_t j = 0; j < d_sygus_bvl.getNumChildren(); ++j) {
-        evalType.push_back(TypeNode::fromType(d_sygus_bvl[j].getType()));
-      }
-    }
-    evalType.push_back(TypeNode::fromType(d_sygus_type));
-    TypeNode eval_func_type = nm->mkFunctionType(evalType);
-    d_sygus_eval = nm->mkSkolem(name, eval_func_type, "sygus evaluation function").toExpr();    
-  }
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
@@ -683,10 +666,6 @@ bool Datatype::getSygusAllowAll() const {
   return d_sygus_allow_all;
 }
 
-Expr Datatype::getSygusEvaluationFunc() const {
-  return d_sygus_eval;
-}
-
 bool Datatype::involvesExternalType() const{
   return d_involvesExt;
 }
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index c2cf80158..a3519f405 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -920,17 +920,6 @@ public:
    * to setSygus).
    */
   bool getSygusAllowAll() const;
-  /** get sygus evaluation function
-   *
-   * This gets the evaluation function for this datatype
-   * for the deep embedding. This is a function of type:
-   *   D x T1 x ... x Tn -> T
-   * where:
-   *   D is the datatype type for this datatype,
-   *   T1...Tn are the types of the variables in getSygusVarList(),
-   *   T is getSygusType().
-   */
-  Expr getSygusEvaluationFunc() const;
 
   /** involves external type
    * Get whether this datatype has a subfield
@@ -979,8 +968,6 @@ public:
   bool d_sygus_allow_const;
   /** whether all terms are allowed as solutions */
   bool d_sygus_allow_all;
-  /** the evaluation function for this sygus datatype */
-  Expr d_sygus_eval;
 
   /** the cardinality of this datatype
   * "mutable" because computing the cardinality can be expensive,
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 0c521bb93..2394a1b5d 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -184,12 +184,3 @@ header = "options/datatypes_options.h"
   default    = "-1"
   read_only  = true
   help       = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)"
-
-[[option]]
-  name       = "sygusEvalBuiltin"
-  category   = "regular"
-  long       = "sygus-eval-builtin"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "use builtin kind for evaluation functions in sygus"
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;
   }