diff options
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 3 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.cpp | 19 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.h | 17 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 49 |
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) { |