Eliminate option for sygus UF evaluation functions (#2262)

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 8747c530eb079178768b2c798eabaa926b9ae077..ae61d5f339cd832f9167822c5e8d7c0c7ee60a06 100644 (file)
--- 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 c2cf80158512822894c30e845ce847cc7db7a6ec..a3519f405a0c0c8527eeb710622b355c85858795 100644 (file)
--- 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 0c521bb93646cfc14bf279fbb331dabbe1255078..2394a1b5d3ba90549a40c31e1d4b1406c6507ab7 100644 (file)
--- 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 443cd0bd002cbfc572b1c94a6f5374776fead137..8366fe4e1f74a2be0a5d99b407a06e8e90e08ca0 100644 (file)
--- 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 b99c5fb5341ce416263acec403ac406735f582fd..7d91544e12c6965ba73d1273436de11249e4cd2f 100644 (file)
--- 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 36cbb89fe5b8e64cdd23c63730e42f95c2d79349..ac7467c00e0b7fa2508ce8334fd6dd1c2ae4098f 100644 (file)
--- 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 efffa046fa996bec7914d63e00c54aac8b5bfc5a..deea1c26157659cb64188ee7e5f525ce00564322 100644 (file)
--- 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 56d2cf2b56012ce03a4d1cafe83807a8013903ef..6a82b9dadba99ba6e701e5dcf9a5177631fe6103 100644 (file)
--- 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 71449029b9609f00bdf8c7abcd434bcccf3eefcc..514f42fb1b76832e16a4f7a212bfe0d6e445c9a9 100644 (file)
--- 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 759ee6ffa15b6e664189230e3fe58ba13080d1f4..183f40b666e1c28109e500e5c823ac8538bacc70 100644 (file)
--- 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 6e01ff0843e22f7fde2d8b60d651e058c501d863..3cbac1eaaf8029bf0178852b26f614775fbce9e3 100644 (file)
--- 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 99ab54a2cbc57d736917ce73e8bf153aca3f4893..54e731694b3b7e298c0d26cf55cc20f31c621765 100644 (file)
--- 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;
   }