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