Remove front-end support for Chain (#3767)

18 files changed, 36 insertions, 260 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 871cb2f99..1063452cb 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -893,7 +893,6 @@ install(FILES
           expr/array.h
           expr/array_store_all.h
           expr/ascription_type.h
-          expr/chain.h
           expr/datatype.h
           expr/emptyset.h
           expr/expr_iomanip.h
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 7bdc5008b..7f8fc8097 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -76,7 +76,6 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {VARIABLE, CVC4::Kind::BOUND_VARIABLE},
     {LAMBDA, CVC4::Kind::LAMBDA},
     {CHOICE, CVC4::Kind::CHOICE},
-    {CHAIN, CVC4::Kind::CHAIN},
     /* Boolean ------------------------------------------------------------- */
     {CONST_BOOLEAN, CVC4::Kind::CONST_BOOLEAN},
     {NOT, CVC4::Kind::NOT},
@@ -313,8 +312,6 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::BOUND_VARIABLE, VARIABLE},
         {CVC4::Kind::LAMBDA, LAMBDA},
         {CVC4::Kind::CHOICE, CHOICE},
-        {CVC4::Kind::CHAIN, CHAIN},
-        {CVC4::Kind::CHAIN_OP, CHAIN},
         /* Boolean --------------------------------------------------------- */
         {CVC4::Kind::CONST_BOOLEAN, CONST_BOOLEAN},
         {CVC4::Kind::NOT, NOT},
@@ -567,8 +564,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
 
 /* Set of kinds for indexed operators */
 const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds(
-    {CHAIN,
-     RECORD_UPDATE,
+    {RECORD_UPDATE,
      DIVISIBLE,
      BITVECTOR_REPEAT,
      BITVECTOR_ZERO_EXTEND,
@@ -1147,17 +1143,6 @@ std::string Op::getIndices() const
 }
 
 template <>
-Kind Op::getIndices() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  CVC4_API_CHECK(!d_expr->isNull())
-      << "Expecting a non-null internal expression. This Op is not indexed.";
-  Kind kind = intToExtKind(d_expr->getKind());
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN, kind) << "CHAIN";
-  return intToExtKind(d_expr->getConst<Chain>().getOperator());
-}
-
-template <>
 uint32_t Op::getIndices() const
 {
   CVC4_API_CHECK_NOT_NULL;
@@ -3195,18 +3180,6 @@ Op Solver::mkOp(Kind kind) const
   CVC4_API_SOLVER_TRY_CATCH_END
 }
 
-Op Solver::mkOp(Kind kind, Kind k) const
-{
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN, kind) << "CHAIN";
-
-  return Op(
-      kind,
-      *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get());
-
-  CVC4_API_SOLVER_TRY_CATCH_END;
-}
-
 Op Solver::mkOp(Kind kind, const std::string& arg) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 79c02c031..9820aeb19 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1927,15 +1927,6 @@ class CVC4_PUBLIC Solver
 
   /**
    * Create operator of kind:
-   *   - CHAIN
-   * See enum Kind for a description of the parameters.
-   * @param kind the kind of the operator
-   * @param k the kind argument to this operator
-   */
-  Op mkOp(Kind kind, Kind k) const;
-
-  /**
-   * Create operator of kind:
    *   - RECORD_UPDATE
    *   - DIVISIBLE (to support arbitrary precision integers)
    * See enum Kind for a description of the parameters.
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 213dec56a..dcb05be17 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -142,25 +142,6 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   CHOICE,
-  /**
-   * Chained operator.
-   * Parameters: 1
-   *   -[1]: Kind of the binary operation
-   * Create with:
-   *   mkOp(Kind opkind, Kind kind)
-
-   * Apply chained operation.
-   * Parameters: n > 1
-   *   -[1]: Op of kind CHAIN (represents a binary op)
-   *   -[2]..[n]: Arguments to that operator
-   * Create with:
-   *   mkTerm(Op op, Term child1, Term child2)
-   *   mkTerm(Op op, Term child1, Term child2, Term child3)
-   *   mkTerm(Op op, const std::vector<Term>& children)
-   * Turned into a conjunction of binary applications of the operator on
-   * adjoining parameters.
-   */
-  CHAIN,
 
   /* Boolean --------------------------------------------------------------- */
 
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index f6b48048f..8357102b0 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -7,7 +7,6 @@ libcvc4_add_sources(
   attribute.cpp
   attribute_internals.h
   attribute_unique_id.h
-  chain.h
   emptyset.cpp
   emptyset.h
   expr_iomanip.cpp
diff --git a/src/expr/chain.h b/src/expr/chain.h
deleted file mode 100644
index 9df819b4d..000000000
--- a/src/expr/chain.h
+++ /dev/null
@@ -1,51 +0,0 @@
-/*********************                                                        */
-/*! \file chain.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__CHAIN_H
-#define CVC4__CHAIN_H
-
-#include "expr/kind.h"
-#include <iostream>
-
-namespace CVC4 {
-
-/** A class to represent a chained, built-in operator. */
-class CVC4_PUBLIC Chain {
-  Kind d_kind;
-public:
-  explicit Chain(Kind k) : d_kind(k) { }
-  bool operator==(const Chain& ch) const { return d_kind == ch.d_kind; }
-  bool operator!=(const Chain& ch) const { return d_kind != ch.d_kind; }
-  Kind getOperator() const { return d_kind; }
-};/* class Chain */
-
-inline std::ostream& operator<<(std::ostream& out, const Chain& ch) CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& out, const Chain& ch) {
-  return out << ch.getOperator();
-}
-
-struct CVC4_PUBLIC ChainHashFunction {
-  size_t operator()(const Chain& ch) const {
-    return kind::KindHashFunction()(ch.getOperator());
-  }
-};/* struct ChainHashFunction */
-
-}/* CVC4 namespace */
-
-#endif  /* CVC4__CHAIN_H */
diff --git a/src/expr/chain.i b/src/expr/chain.i
deleted file mode 100644
index 8de1665ce..000000000
--- a/src/expr/chain.i
+++ /dev/null
@@ -1,12 +0,0 @@
-%{
-#include "expr/chain.h"
-%}
-
-%rename(equals) CVC4::Chain::operator==(const Chain&) const;
-%ignore CVC4::Chain::operator!=(const Chain&) const;
-
-%ignore CVC4::operator<<(std::ostream&, const Chain&);
-
-%rename(apply) CVC4::ChainHashFunction::operator()(const CVC4::Chain&) const;
-
-%include "expr/chain.h"
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 32d555718..664fa209d 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -515,6 +515,22 @@ Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args)
   return expr;
 }
 
+api::Term Parser::mkChain(api::Kind k, const std::vector<api::Term>& args)
+{
+  if (args.size() == 2)
+  {
+    // if this is the case exactly 1 pair will be generated so the
+    // AND is not required
+    return d_solver->mkTerm(k, args[0], args[1]);
+  }
+  std::vector<api::Term> children;
+  for (size_t i = 0, nargsmo = args.size() - 1; i < nargsmo; i++)
+  {
+    children.push_back(d_solver->mkTerm(k, args[i], args[i + 1]));
+  }
+  return d_solver->mkTerm(api::AND, children);
+}
+
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch (type) {
     case SYM_VARIABLE:
diff --git a/src/parser/parser.h b/src/parser/parser.h
index ecf1e2961..cd70fde0f 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -24,6 +24,7 @@
 #include <set>
 #include <string>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "expr/expr_stream.h"
 #include "expr/kind.h"
@@ -677,6 +678,16 @@ public:
    */
   Expr mkHoApply(Expr expr, std::vector<Expr>& args);
 
+  /** make chain
+   *
+   * Given a kind k and argument terms t_1, ..., t_n, this returns the
+   * conjunction of:
+   *  (k t_1 t_2) .... (k t_{n-1} t_n)
+   * It is expected that k is a kind denoting a predicate, and args is a list
+   * of terms of size >= 2 such that the terms above are well-typed.
+   */
+  api::Term mkChain(api::Kind k, const std::vector<api::Term>& args);
+
   /**
    * Add an operator to the current legal set.
    *
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index f3b66643a..11dedb259 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1887,7 +1887,9 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args)
                || kind == kind::LEQ || kind == kind::GEQ)
       {
         /* "chainable", but CVC4 internally only supports 2 args */
-        return em->mkExpr(em->mkConst(Chain(kind)), args);
+        api::Term ret =
+            mkChain(intToExtKind(kind), api::exprVectorToTerms(args));
+        return ret.getExpr();
       }
     }
 
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 71a3e4bee..bf699ae3c 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -326,7 +326,9 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector<Expr>& args)
           || kind == kind::LEQ || kind == kind::GEQ)
       {
         /* "chainable", but CVC4 internally only supports 2 args */
-        return em->mkExpr(em->mkConst(Chain(kind)), args);
+        api::Term ret =
+            mkChain(intToExtKind(kind), api::exprVectorToTerms(args));
+        return ret.getExpr();
       }
     }
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index f8448f1e9..f3f43220c 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -283,8 +283,8 @@ void CvcPrinter::toStream(
       out << ")";
       return;
       break;
-    case kind::CHAIN:
-    case kind::DISTINCT: // chain and distinct not supported directly in CVC4, blast them away with the rewriter
+    case kind::DISTINCT:
+      // distinct not supported directly, blast it away with the rewriter
       toStream(out, theory::Rewriter::rewrite(n), depth, types, true);
       return;
     case kind::SORT_TYPE:
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index bfdaf7852..8153d6856 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -193,9 +193,6 @@ void Smt2Printer::toStream(std::ostream& out,
     case kind::BUILTIN:
       out << smtKindString(n.getConst<Kind>(), d_variant);
       break;
-    case kind::CHAIN_OP:
-      out << smtKindString(n.getConst<Chain>().getOperator(), d_variant);
-      break;
     case kind::CONST_RATIONAL: {
       const Rational& r = n.getConst<Rational>();
       toStreamRational(
@@ -474,7 +471,6 @@ void Smt2Printer::toStream(std::ostream& out,
     out << smtKindString(k, d_variant) << " ";
     parametricTypeChildren = true;
     break;
-  case kind::CHAIN: break;
   case kind::FUNCTION_TYPE:
     out << "->";
     for (Node nc : n)
@@ -1027,7 +1023,6 @@ static string smtKindString(Kind k, Variant v)
     // builtin theory
   case kind::EQUAL: return "=";
   case kind::DISTINCT: return "distinct";
-  case kind::CHAIN: break;
   case kind::SEXPR: break;
 
     // bool theory
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 88a53062a..7e2ed84b1 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -1050,42 +1050,6 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term,
     return;
   }
 
-  case kind::CHAIN: {
-    // LFSC doesn't allow declarations with variable numbers of
-    // arguments, so we have to flatten chained operators, like =.
-    Kind op = term.getOperator().getConst<Chain>().getOperator();
-    std::string op_str;
-    bool booleanCase = false;
-    if (op==kind::EQUAL && term[0].getType().isBoolean()) {
-      booleanCase = term[0].getType().isBoolean();
-      op_str = "iff";
-    } else {
-      op_str = utils::toLFSCKind(op);
-    }
-    size_t n = term.getNumChildren();
-    std::ostringstream paren;
-    for(size_t i = 1; i < n; ++i) {
-      if(i + 1 < n) {
-        os << "(" << utils::toLFSCKind(kind::AND) << " ";
-        paren << ")";
-      }
-      os << "(" << op_str << " ";
-      if (booleanCase && printsAsBool(term[i - 1])) os << "(p_app ";
-      printBoundTerm(term[i - 1], os, map);
-      if (booleanCase && printsAsBool(term[i - 1])) os << ")";
-      os << " ";
-      if (booleanCase && printsAsBool(term[i])) os << "(p_app ";
-      printBoundTerm(term[i], os, map);
-      if (booleanCase && printsAsBool(term[i])) os << ")";
-      os << ")";
-      if(i + 1 < n) {
-        os << " ";
-      }
-    }
-    os << paren.str();
-    return;
-  }
-
   default: Unhandled() << k;
   }
 }
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) {