Remove front-end support for Chain (#3767)

4 files changed, 0 insertions, 94 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 15891dfad..c90419def 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -300,13 +300,6 @@ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, sec
 
 operator CHOICE 2 "a Hilbert choice (epsilon) expression; first parameter is a BOUND_VAR_LIST, second is the Hilbert choice body"
 
-parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjunction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator"
-constant CHAIN_OP \
-    ::CVC4::Chain \
-    ::CVC4::ChainHashFunction \
-    "expr/chain.h" \
-    "the chained operator; payload is an instance of the CVC4::Chain class"
-
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
     ::CVC4::TypeConstantHashFunction \
@@ -334,8 +327,6 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 typerule CHOICE ::CVC4::theory::builtin::ChoiceTypeRule
-typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
-typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
 
 # lambda expressions that are isomorphic to array constants can be considered constants
 construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index d9fe2fecc..15c312080 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -18,7 +18,6 @@
 #include "theory/builtin/theory_builtin_rewriter.h"
 
 #include "expr/attribute.h"
-#include "expr/chain.h"
 #include "expr/node_algorithm.h"
 #include "theory/rewriter.h"
 
@@ -53,24 +52,6 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) {
   return out;
 }
 
-Node TheoryBuiltinRewriter::blastChain(TNode in) {
-  Assert(in.getKind() == kind::CHAIN);
-
-  Kind chainedOp = in.getOperator().getConst<Chain>().getOperator();
-
-  if(in.getNumChildren() == 2) {
-    // if this is the case exactly 1 pair will be generated so the
-    // AND is not required
-    return NodeManager::currentNM()->mkNode(chainedOp, in[0], in[1]);
-  } else {
-    NodeBuilder<> conj(kind::AND);
-    for(TNode::iterator i = in.begin(), j = i + 1; j != in.end(); ++i, ++j) {
-      conj << NodeManager::currentNM()->mkNode(chainedOp, *i, *j);
-    }
-    return conj;
-  }
-}
-
 RewriteResponse TheoryBuiltinRewriter::postRewrite(TNode node) {
   if( node.getKind()==kind::LAMBDA ){
     Trace("builtin-rewrite") << "Rewriting lambda " << node << "..." << std::endl;
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index 60a8f29f0..4b75d7e3a 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -32,18 +32,6 @@ class TheoryBuiltinRewriter : public TheoryRewriter
   static Node blastDistinct(TNode node);
 
  public:
-  /**
-   * Takes a chained application of a binary operator and returns a conjunction
-   * of binary applications of that operator.
-   *
-   * For example:
-   *
-   * (= x y z) ---> (and (= x y) (= y z))
-   *
-   * @param node A node that is a chained application of a binary operator
-   * @return A conjunction of binary applications of the chained operator
-   */
-  static Node blastChain(TNode node);
 
   static inline RewriteResponse doRewrite(TNode node)
   {
@@ -51,7 +39,6 @@ class TheoryBuiltinRewriter : public TheoryRewriter
     {
       case kind::DISTINCT:
         return RewriteResponse(REWRITE_DONE, blastDistinct(node));
-      case kind::CHAIN: return RewriteResponse(REWRITE_DONE, blastChain(node));
       default: return RewriteResponse(REWRITE_DONE, node);
     }
   }
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index bb88b64ee..d49edbc8c 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -194,59 +194,6 @@ class ChoiceTypeRule
   }
 }; /* class ChoiceTypeRule */
 
-class ChainTypeRule {
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    Assert(n.getKind() == kind::CHAIN);
-
-    if(!check) {
-      return nodeManager->booleanType();
-    }
-
-    TypeNode tn;
-    try {
-      tn = nodeManager->getType(TheoryBuiltinRewriter::blastChain(n), check);
-    } catch(TypeCheckingExceptionPrivate& e) {
-      std::stringstream ss;
-      ss << "Cannot typecheck the expansion of chained operator `" << n.getOperator() << "':"
-         << std::endl;
-      // indent the sub-exception for clarity
-      std::stringstream ss2;
-      ss2 << e;
-      std::string eStr = ss2.str();
-      for(size_t i = eStr.find('\n'); i != std::string::npos; i = eStr.find('\n', i)) {
-        eStr.insert(++i, "| ");
-      }
-      ss << "| " << eStr;
-      throw TypeCheckingExceptionPrivate(n, ss.str());
-    }
-
-    // This check is intentionally != booleanType() rather than
-    // !(...isBoolean()): if we ever add a type compatible with
-    // Boolean (pseudobooleans or whatever), we have to revisit
-    // the above "!check" case where booleanType() is returned
-    // directly.  Putting this check here will cause a failure if
-    // it's ever relevant.
-    if(tn != nodeManager->booleanType()) {
-      std::stringstream ss;
-      ss << "Chains can only be formed over predicates; "
-         << "the operator here returns `" << tn << "', expected `"
-         << nodeManager->booleanType() << "'.";
-      throw TypeCheckingExceptionPrivate(n, ss.str());
-    }
-
-    return nodeManager->booleanType();
-  }
-};/* class ChainTypeRule */
-
-class ChainedOperatorTypeRule {
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    Assert(n.getKind() == kind::CHAIN_OP);
-    return nodeManager->getType(nodeManager->operatorOf(n.getConst<Chain>().getOperator()), check);
-  }
-};/* class ChainedOperatorTypeRule */
-
 class SortProperties {
  public:
   inline static bool isWellFounded(TypeNode type) {