4 files changed, 83 insertions, 5 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 1218f3809..da31d157f 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -300,6 +300,8 @@ operator TUPLE 1: "a tuple"
 
 operator LAMBDA 2 "lambda"
 
+parameterized CHAIN BUILTIN 2: "chain operator"
+
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
     ::CVC4::TypeConstantHashFunction \
@@ -342,6 +344,7 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
+typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
 
 constant SUBTYPE_TYPE \
     ::CVC4::Predicate \
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index f62140263..a23a1b8f2 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -51,6 +51,25 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) {
   return out;
 }
 
+Node TheoryBuiltinRewriter::blastChain(TNode in) {
+
+  Assert(in.getKind() == kind::CHAIN);
+
+  Kind chainedOp = in.getOperator().getConst<Kind>();
+
+  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;
+  }
+}
+
 }/* CVC4::theory::builtin namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index acf535388..b7199474b 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -32,22 +32,29 @@ namespace builtin {
 class TheoryBuiltinRewriter {
 
   static Node blastDistinct(TNode node);
+  static Node blastChain(TNode node);
 
 public:
 
-  static inline RewriteResponse postRewrite(TNode node) {
-    return RewriteResponse(REWRITE_DONE, node);
-  }
-
-  static inline RewriteResponse preRewrite(TNode node) {
+  static inline RewriteResponse doRewrite(TNode node) {
     switch(node.getKind()) {
     case kind::DISTINCT:
       return RewriteResponse(REWRITE_DONE, blastDistinct(node));
+    case kind::CHAIN:
+      return RewriteResponse(REWRITE_DONE, blastChain(node));
     default:
       return RewriteResponse(REWRITE_DONE, node);
     }
   }
 
+  static inline RewriteResponse postRewrite(TNode node) {
+    return doRewrite(node);
+  }
+
+  static inline RewriteResponse preRewrite(TNode node) {
+    return doRewrite(node);
+  }
+
   static inline void init() {}
   static inline void shutdown() {}
 
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index b7fd3c351..97af23f67 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -24,6 +24,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 #include "expr/expr.h"
+#include "theory/rewriter.h"
 
 #include <sstream>
 
@@ -168,6 +169,54 @@ public:
   }
 };/* class LambdaTypeRule */
 
+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 {
+      // Actually do the expansion to do the typechecking.
+      // Shouldn't be extra work to do this, since the rewriter
+      // keeps a cache.
+      tn = nodeManager->getType(Rewriter::rewrite(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 SortProperties {
 public:
   inline static bool isWellFounded(TypeNode type) {