From 053ee7b8058eccb84b909920ff92975faeda996c Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 3 Aug 2018 15:34:17 -0500
Subject: Eliminate option for sygus UF evaluation functions (#2262)

---
 src/expr/datatype.cpp | 21 ---------------------
 src/expr/datatype.h   | 13 -------------
 2 files changed, 34 deletions(-)

(limited to 'src/expr')

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,
-- 
cgit v1.2.3