From 1ce8e28d5976e1ab30099cb9e6943514497d2980 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Tue, 4 May 2010 03:42:56 +0000 Subject: [PATCH] Type-checking classes and hooks (not tested yet). --- src/expr/Makefile.am | 1 + src/expr/builtin_type_rules.h | 51 +++++ src/expr/expr_manager_template.cpp | 10 +- src/expr/expr_manager_template.h | 3 +- src/expr/expr_template.cpp | 24 ++- src/expr/expr_template.h | 42 +++- src/expr/node.cpp | 21 ++ src/expr/node.h | 43 ++++- src/expr/node_manager.cpp | 191 +++++++++++++++++++ src/expr/node_manager.h | 10 +- src/expr/type.cpp | 1 + src/expr/type.h | 3 + src/theory/arith/Makefile.am | 1 + src/theory/arith/theory_arith_type_rules.h | 74 +++++++ src/theory/booleans/Makefile.am | 3 +- src/theory/booleans/theory_bool_type_rules.h | 56 ++++++ src/theory/bv/Makefile.am | 3 +- src/theory/bv/theory_bv_type_rules.h | 170 +++++++++++++++++ src/theory/uf/Makefile.am | 3 +- src/theory/uf/theory_uf_type_rules.h | 47 +++++ src/util/bitvector.h | 4 + src/util/exception.h | 3 +- test/unit/expr/expr_public.h | 17 +- 23 files changed, 749 insertions(+), 32 deletions(-) create mode 100644 src/expr/builtin_type_rules.h create mode 100644 src/theory/arith/theory_arith_type_rules.h create mode 100644 src/theory/booleans/theory_bool_type_rules.h create mode 100644 src/theory/bv/theory_bv_type_rules.h create mode 100644 src/theory/uf/theory_uf_type_rules.h diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index ef51b9c83..c3c3fccf6 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -10,6 +10,7 @@ libexpr_la_SOURCES = \ node.cpp \ type_node.h \ type_node.cpp \ + builtin_type_rules.h \ node_builder.h \ @srcdir@/expr.h \ type.h \ diff --git a/src/expr/builtin_type_rules.h b/src/expr/builtin_type_rules.h new file mode 100644 index 000000000..2a6b43b22 --- /dev/null +++ b/src/expr/builtin_type_rules.h @@ -0,0 +1,51 @@ +/********************* */ +/** builtin_type_rules.cpp + ** Original author: dejan + ** Major contributors: none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BUILTIN_TYPE_RULES_H_ +#define __CVC4__BUILTIN_TYPE_RULES_H_ + +#include "expr/node.h" +#include "expr/type_node.h" +#include "expr/expr.h" + +namespace CVC4 { + +class EqualityTypeRule { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingException) { + if (n[0].getType() != n[1].getType()) { + throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type"); + } + return nodeManager->booleanType(); + } +}; + +class DistinctTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) { + TNode::iterator child_it = n.begin(); + TNode::iterator child_it_end = n.end(); + TypeNode firstType = (*child_it).getType(); + for (++child_it; child_it != child_it_end; ++child_it) { + if ((*child_it).getType() != firstType) { + throw TypeCheckingExceptionPrivate(n, "Not all arguments are of the same type"); + } + } + return nodeManager->booleanType(); + } +}; + +} + +#endif /* __CVC4__BUILTIN_TYPE_RULES_H_ */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index b957019fb..03a54d49b 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -229,9 +229,15 @@ SortType ExprManager::mkSort(const std::string& name) { return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))); } -Type ExprManager::getType(const Expr& e) { +Type ExprManager::getType(const Expr& e) throw (TypeCheckingException) { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode()))); + Type t; + try { + t = Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode()))); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(Expr(this, new Node(e.getNode())), e.getMessage()); + } + return t; } Expr ExprManager::mkVar(const std::string& name, const Type& type) { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index b3a1b68df..16d1b4534 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -22,6 +22,7 @@ #include "expr/kind.h" #include "expr/type.h" +#include "expr/expr.h" ${includes} @@ -208,7 +209,7 @@ public: SortType mkSort(const std::string& name); /** Get the type of an expression */ - Type getType(const Expr& e); + Type getType(const Expr& e) throw (TypeCheckingException); // variables are special, because duplicates are permitted Expr mkVar(const std::string& name, const Type& type); diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index ba7032e34..a1be2ece8 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -14,6 +14,7 @@ **/ #include "expr/expr.h" +#include "expr/expr_manager.h" #include "expr/node.h" #include "util/Assert.h" @@ -26,7 +27,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 30 "${template}" +#line 31 "${template}" using namespace CVC4::kind; @@ -37,6 +38,25 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) { return out; } +TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message) +: Exception(message), d_expr(new Expr(expr)) +{ +} + +TypeCheckingException::~TypeCheckingException() throw () { + delete d_expr; +} + +std::string TypeCheckingException::toString() const { + std::stringstream ss; + ss << "Error type-checking " << d_expr << ": " << d_msg; + return ss.str(); +} + +Expr TypeCheckingException::getExpression() const { + return *d_expr; +} + Expr::Expr() : d_node(new Node), d_exprManager(NULL) { @@ -129,7 +149,7 @@ Expr Expr::getOperator() const { return Expr(d_exprManager, new Node(d_node->getOperator())); } -Type Expr::getType() const { +Type Expr::getType() const throw (TypeCheckingException) { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); return d_exprManager->getType(*this); diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 0e960358f..914d47959 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -15,12 +15,10 @@ #include "cvc4_public.h" -// circular dependency: force expr_manager.h first -#include "expr/expr_manager.h" - #ifndef __CVC4__EXPR_H #define __CVC4__EXPR_H +#include "expr/type.h" #include #include #include @@ -31,7 +29,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 35 "${template}" +#line 33 "${template}" namespace CVC4 { @@ -39,6 +37,40 @@ namespace CVC4 { template class NodeTemplate; +class Expr; + +/** + * Exception thrown in the case of type-checking errors. + */ +class TypeCheckingException : public Exception { + +private: + + /** The expression responsible for the error */ + Expr* d_expr; + +protected: + + TypeCheckingException(): Exception() {} + TypeCheckingException(const Expr& expr, std::string message); + +public: + + /** Destructor */ + ~TypeCheckingException() throw (); + + /** + * Get the Node that caused the type-checking to fail. + * @return the node + */ + Expr getExpression() const; + + /** Returns the message corresponding to the type-checking failure */ + std::string toString() const; + + friend class ExprManager; +}; + /** * Class encapsulating CVC4 expressions and methods for constructing new * expressions. @@ -144,7 +176,7 @@ public: /** Returns the type of the expression, if it has been computed. * Returns NULL if the type of the expression is not known. */ - Type getType() const; + Type getType() const throw (TypeCheckingException); /** * Returns the string representation of the expression. diff --git a/src/expr/node.cpp b/src/expr/node.cpp index bf1997381..7ebea8a70 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -26,4 +26,25 @@ namespace expr { const int NodeSetDepth::s_iosIndex = std::ios_base::xalloc(); }/* CVC4::expr namespace */ + + +TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, std::string message) +: Exception(message), d_node(new Node(node)) +{ +} + +TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () { + delete d_node; +} + +std::string TypeCheckingExceptionPrivate::toString() const { + std::stringstream ss; + ss << "Error type-checking " << d_node << ": " << d_msg; + return ss.str(); +} + +Node TypeCheckingExceptionPrivate::getNode() const { + return *d_node; +} + }/* CVC4 namespace */ diff --git a/src/expr/node.h b/src/expr/node.h index f8d9117c7..d3e8792ed 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -26,8 +26,10 @@ #include #include +#include "type.h" #include "expr/kind.h" #include "expr/metakind.h" +#include "expr/expr.h" #include "util/Assert.h" #include "util/output.h" @@ -39,6 +41,43 @@ class NodeManager; template class NodeTemplate; +/** + * Exception thrown during the type-checking phase, it can be + * thrown by node.getType(). + */ +class TypeCheckingExceptionPrivate : public Exception { + +private: + + /** The node repsonsible for the failure */ + NodeTemplate* d_node; + +protected: + + TypeCheckingExceptionPrivate(): Exception() {} + +public: + + /** + * Construct the exception with the problematic node and the message + * @param node the problematic node + * @param message the message explaining the failure + */ + TypeCheckingExceptionPrivate(NodeTemplate node, std::string message); + + /** Destructor */ + ~TypeCheckingExceptionPrivate() throw (); + + /** + * Get the Node that caused the type-checking to fail. + * @return the node + */ + NodeTemplate getNode() const; + + /** Returns the message corresponding to the type-checking failure */ + std::string toString() const; +}; + /** * The Node class encapsulates the NodeValue with reference counting. */ @@ -247,7 +286,7 @@ public: * Returns the type of this node. * @return the type */ - TypeNode getType() const; + TypeNode getType() const throw (CVC4::TypeCheckingExceptionPrivate); /** * Returns the kind of this node. @@ -814,7 +853,7 @@ inline bool NodeTemplate::hasOperator() const { } template -TypeNode NodeTemplate::getType() const { +TypeNode NodeTemplate::getType() const throw (CVC4::TypeCheckingExceptionPrivate) { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 4f0e0ff76..171c75186 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -17,6 +17,12 @@ #include "node_manager.h" +#include "expr/builtin_type_rules.h" +#include "theory/booleans/theory_bool_type_rules.h" +#include "theory/uf/theory_uf_type_rules.h" +#include "theory/arith/theory_arith_type_rules.h" +#include "theory/bv/theory_bv_type_rules.h" + #include using namespace std; @@ -169,4 +175,189 @@ void NodeManager::reclaimZombies() { } }/* NodeManager::reclaimZombies() */ +TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) { + TypeNode typeNode; + bool hasType = getAttribute(n, TypeAttr(), typeNode); + if (!hasType) { + // Infer the type + switch (n.getKind()) { + case kind::EQUAL: + typeNode = CVC4::EqualityTypeRule::computeType(this, n); + break; + case kind::DISTINCT: + typeNode = CVC4::DistinctTypeRule::computeType(this, n); + break; + case kind::CONST_BOOLEAN: + typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n); + break; + case kind::NOT: + typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n); + break; + case kind::AND: + typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n); + break; + case kind::IFF: + typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n); + break; + case kind::IMPLIES: + typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n); + break; + case kind::OR: + typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n); + break; + case kind::XOR: + typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n); + break; + case kind::ITE: + typeNode = CVC4::theory::boolean::IteTypeRule::computeType(this, n); + break; + case kind::APPLY_UF: + typeNode = CVC4::theory::uf::UfTypeRule::computeType(this, n); + break; + case kind::PLUS: + typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n); + break; + case kind::MULT: + typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n); + break; + case kind::MINUS: + typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n); + break; + case kind::UMINUS: + typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n); + break; + case kind::CONST_RATIONAL: + typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n); + break; + case kind::CONST_INTEGER: + typeNode = CVC4::theory::arith::ArithConstantTypeRule::computeType(this, n); + break; + case kind::LT: + typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n); + break; + case kind::LEQ: + typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n); + break; + case kind::GT: + typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n); + break; + case kind::GEQ: + typeNode = CVC4::theory::arith::ArithPredicateTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_CONST: + typeNode = CVC4::theory::bv::BitVectorConstantTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_AND: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_OR: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_XOR: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_NOT: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_NAND: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_NOR: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_XNOR: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_COMP: + typeNode = CVC4::theory::bv::BitVectorCompRule::computeType(this, n); + break; + case kind::BITVECTOR_MULT: + typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n); + break; + case kind::BITVECTOR_PLUS: + typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n); + break; + case kind::BITVECTOR_SUB: + typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n); + break; + case kind::BITVECTOR_NEG: + typeNode = CVC4::theory::bv::BitVectorArithRule::computeType(this, n); + break; + case kind::BITVECTOR_UDIV: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_UREM: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_SDIV: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_SREM: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_SMOD: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_SHL: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_LSHR: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_ASHR: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_ROTATE_LEFT: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_ROTATE_RIGHT: + typeNode = CVC4::theory::bv::BitVectorFixedWidthTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_ULT: + typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_ULE: + typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_UGT: + typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_UGE: + typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_SLT: + typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_SLE: + typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_SGT: + typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_SGE: + typeNode = CVC4::theory::bv::BitVectorPredicateTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_EXTRACT: + typeNode = CVC4::theory::bv::BitVectorExtractTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_CONCAT: + typeNode = CVC4::theory::bv::BitVectorConcatRule::computeType(this, n); + break; + case kind::BITVECTOR_REPEAT: + typeNode = CVC4::theory::bv::BitVectorRepeatTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_ZERO_EXTEND: + typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n); + break; + case kind::BITVECTOR_SIGN_EXTEND: + typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n); + break; + default: + Unimplemented(); + } + setAttribute(n, TypeAttr(), typeNode); + } + return typeNode; +} + }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5cb19bc89..53abdb703 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -21,6 +21,7 @@ #include "expr/attribute.h" #include "expr/node.h" #include "expr/type_node.h" +#include "expr/expr.h" #ifndef __CVC4__NODE_MANAGER_H #define __CVC4__NODE_MANAGER_H @@ -507,7 +508,7 @@ public: /** * Get the type for the given node. */ - inline TypeNode getType(TNode n); + TypeNode getType(TNode n) throw (TypeCheckingExceptionPrivate); /** * Returns true if this node is atomic (has no more Boolean structure) @@ -673,13 +674,6 @@ NodeManager::mkPredicateType(const std::vector& sorts) { return mkTypeNode(kind::FUNCTION_TYPE, sortNodes); } -inline TypeNode NodeManager::getType(TNode n) { - TypeNode typeNode; - getAttribute(n, TypeAttr(), typeNode); - // TODO: Type computation - return typeNode; -} - inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); if(find == d_nodeValuePool.end()) { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index faadfb0a6..521e177d3 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -14,6 +14,7 @@ **/ #include "expr/node_manager.h" +#include "expr/expr_manager.h" #include "expr/type.h" #include "expr/type_node.h" #include "expr/type_constant.h" diff --git a/src/expr/type.h b/src/expr/type.h index f513ef5de..137dbfff3 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -29,7 +29,10 @@ namespace CVC4 { class NodeManager; +class ExprManager; class TypeNode; +template +class NodeTemplate; class BooleanType; class IntegerType; diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 7c3e76d0a..0428bf84e 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -8,6 +8,7 @@ noinst_LTLIBRARIES = libarith.la libarith_la_SOURCES = \ theory_arith.h \ theory_arith.cpp \ + theory_arith_type_rules.h \ arith_rewriter.h \ arith_rewriter.cpp \ arith_utilities.h \ diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h new file mode 100644 index 000000000..e97af08ee --- /dev/null +++ b/src/theory/arith/theory_arith_type_rules.h @@ -0,0 +1,74 @@ +/********************* */ +/** theory_arith_type_rules.cpp + ** Original author: dejan + ** Major contributors: none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_ARITH_TYPE_RULES_H_ +#define __CVC4__THEORY_ARITH_TYPE_RULES_H_ + +namespace CVC4 { +namespace theory { +namespace arith { + + +class ArithConstantTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType(); + return nodeManager->integerType(); + } +}; + +class ArithOperatorTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode integerType = nodeManager->integerType(); + TypeNode realType = nodeManager->realType(); + TNode::iterator child_it = n.begin(); + TNode::iterator child_it_end = n.end(); + bool isInteger = true; + for(; child_it != child_it_end; ++child_it) { + TypeNode childType = (*child_it).getType(); + if (!childType.isInteger()) isInteger = false; + if(childType != integerType && childType != realType) { + throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic subterm"); + } + } + return (isInteger ? integerType : realType); + } +}; + +class ArithPredicateTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode integerType = nodeManager->integerType(); + TypeNode realType = nodeManager->realType(); + TypeNode lhsType = n[0].getType(); + if (lhsType != integerType && lhsType != realType) { + throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side"); + } + TypeNode rhsType = n[1].getType(); + if (rhsType != integerType && rhsType != realType) { + throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side"); + } + return nodeManager->booleanType(); + } +}; + +} +} +} + +#endif /* THEORY_ARITH_TYPE_RULES_H_ */ diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index 690299630..a1b3e097a 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libbooleans.la libbooleans_la_SOURCES = \ - theory_bool.h + theory_bool.h \ + theory_bool_type_rules.h EXTRA_DIST = kinds diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h new file mode 100644 index 000000000..4cfc2f87f --- /dev/null +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -0,0 +1,56 @@ +/********************* */ +/** theory_bool_type_rules.cpp + ** Original author: dejan + ** Major contributors: none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_BOOL_TYPE_RULES_H_ +#define __CVC4__THEORY_BOOL_TYPE_RULES_H_ + +namespace CVC4 { +namespace theory { +namespace boolean { + +class BooleanTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode booleanType = nodeManager->booleanType(); + TNode::iterator child_it = n.begin(); + TNode::iterator child_it_end = n.end(); + for(; child_it != child_it_end; ++child_it) + if((*child_it).getType() != booleanType) { + throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression"); + } + return booleanType; + } +}; + +class IteTypeRule { + public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingException) { + TypeNode booleanType = nodeManager->booleanType(); + if (n[0].getType() != booleanType) { + throw TypeCheckingExceptionPrivate(n, "condition of ITE is not Boolean"); + } + TypeNode iteType = n[1].getType(); + if (iteType != n[2].getType()) { + throw TypeCheckingExceptionPrivate(n, "both branches of the ITE must be of the same type"); + } + return iteType; + } +}; + +} // boolean namespace +} // theory namespace +} // CVC4 namespace + +#endif /* __CVC4__THEORY_BOOL_TYPE_RULES_H_ */ diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index d90472fd3..6f9a51dc3 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libbv.la libbv_la_SOURCES = \ - theory_bv.h + theory_bv.h \ + theory_bv_type_rules.h EXTRA_DIST = kinds diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h new file mode 100644 index 000000000..c9a7c1f2c --- /dev/null +++ b/src/theory/bv/theory_bv_type_rules.h @@ -0,0 +1,170 @@ +/********************* */ +/** theory_bv_types.h + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Bitvector theory. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ +#define __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ + +namespace CVC4 { +namespace theory { +namespace bv { + +class BitVectorConstantTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + return nodeManager->bitVectorType(n.getConst().getSize()); + } +}; + +class BitVectorCompRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode lhs = n[0].getType(); + TypeNode rhs = n[1].getType(); + if (!lhs.isBitVector() || lhs != rhs) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + } + return nodeManager->bitVectorType(1); + } +}; + +class BitVectorArithRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + unsigned maxWidth = 0; + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + // TODO: optimize unary neg + for (; it != it_end; ++ it) { + TypeNode t = (*it).getType(); + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + if (maxWidth < t.getBitVectorSize()) maxWidth = t.getBitVectorSize(); + } + return nodeManager->bitVectorType(maxWidth); + } +}; + +class BitVectorFixedWidthTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + TypeNode t = (*it).getType(); + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + for (++ it; it != it_end; ++ it) { + if ((*it).getType() != t) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + } + } + return t; + } +}; + +class BitVectorPredicateTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode lhsType = n[0].getType(); + if (!lhsType.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + TypeNode rhsType = n[1].getType(); + if (lhsType != rhsType) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms of the same width"); + } + return nodeManager->booleanType(); + } +}; + +class BitVectorExtractTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode t = n[0].getType(); + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + BitVectorExtract extractInfo = n.getOperator().getConst(); + if (extractInfo.high < extractInfo.low) { + throw TypeCheckingExceptionPrivate(n, "high extract index is smaller than the low extract index"); + } + if (extractInfo.high >= t.getBitVectorSize()) { + throw TypeCheckingExceptionPrivate(n, "high extract index is bigger than the size of the bit-vector"); + } + return nodeManager->bitVectorType(extractInfo.high - extractInfo.low + 1); + } +}; + +class BitVectorConcatRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + unsigned size = 0; + TNode::iterator it = n.begin(); + TNode::iterator it_end = n.end(); + for (; it != it_end; ++ it) { + TypeNode t = n[0].getType(); + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + size += t.getBitVectorSize(); + } + return nodeManager->bitVectorType(size); + } +}; + +class BitVectorRepeatTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode t = n[0].getType(); + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + unsigned repeatAmount = n.getOperator().getConst(); + return nodeManager->bitVectorType(repeatAmount * t.getBitVectorSize()); + } +}; + +class BitVectorExtendTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TypeNode t = n[0].getType(); + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + unsigned extendAmount = n.getKind() == kind::BITVECTOR_SIGN_EXTEND ? + (unsigned) n.getOperator().getConst() : + (unsigned) n.getOperator().getConst(); + + return nodeManager->bitVectorType(extendAmount + t.getBitVectorSize()); + } +}; + +} +} +} + +#endif /* __CVC4__EXPR_TYPE_THEORY_BV_TYPE_RULES_H_ */ diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index e0aa3a1df..e40359521 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -9,6 +9,7 @@ libuf_la_SOURCES = \ ecdata.h \ ecdata.cpp \ theory_uf.h \ - theory_uf.cpp + theory_uf.cpp \ + theory_uf_type_rules.h EXTRA_DIST = kinds diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h new file mode 100644 index 000000000..8c05591d6 --- /dev/null +++ b/src/theory/uf/theory_uf_type_rules.h @@ -0,0 +1,47 @@ +/********************* */ +/** theory_uf_type_rules.h + ** Original author: dejan + ** Major contributors: none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY_UF_TYPE_RULES_H_ +#define __CVC4__THEORY_UF_TYPE_RULES_H_ + +namespace CVC4 { +namespace theory { +namespace uf { + +class UfTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n) + throw (TypeCheckingException) { + TNode f = n.getOperator(); + TypeNode fType = f.getType(); + if (n.getNumChildren() != fType.getNumChildren() - 1) { + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); + } + TNode::iterator argument_it = n.begin(); + TNode::iterator argument_it_end = n.end(); + TypeNode::iterator argument_type_it = fType.begin(); + for(; argument_it != argument_it_end; ++argument_it) + if((*argument_it).getType() != *argument_type_it) { + throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + } + return fType.getRangeType(); + } +}; + +} +} +} + + +#endif /* THEORY_UF_TYPE_RULES_H_ */ diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 1ab13230b..879680fd7 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -83,6 +83,10 @@ public: std::string toString(unsigned int base = 2) const { return d_value.get_str(base); } + + unsigned getSize() const { + return d_size; + } }; /** diff --git a/src/util/exception.h b/src/util/exception.h index 862597bae..48dcf1244 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -34,7 +34,8 @@ public: virtual ~Exception() throw() {} // NON-VIRTUAL METHOD for setting and printing the error message void setMessage(const std::string& msg) { d_msg = msg; } - // Printing: feel free to redefine toString(). When inherited, + std::string getMessage() const { return d_msg; } + // Printing: feel free to redefine toString(). When inherited, // it's recommended that this method print the type of exception // before the actual message. virtual std::string toString() const { return d_msg; } diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index f40e32ef9..d483a86f4 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -258,14 +258,15 @@ public: TS_ASSERT(a->getType() == d_em->booleanType()); TS_ASSERT(b->getType() == d_em->booleanType()); - TS_ASSERT(c->getType().isNull()); - TS_ASSERT(mult->getType().isNull()); - TS_ASSERT(plus->getType().isNull()); - TS_ASSERT(d->getType().isNull()); - TS_ASSERT(i1->getType().isNull()); - TS_ASSERT(i2->getType().isNull()); - TS_ASSERT(r1->getType().isNull()); - TS_ASSERT(r2->getType().isNull()); +// TODO: Type-checking exceptions +// TS_ASSERT(c->getType().isNull()); +// TS_ASSERT(mult->getType().isNull()); +// TS_ASSERT(plus->getType().isNull()); +// TS_ASSERT(d->getType().isNull()); +// TS_ASSERT(i1->getType().isNull()); +// TS_ASSERT(i2->getType().isNull()); +// TS_ASSERT(r1->getType().isNull()); +// TS_ASSERT(r2->getType().isNull()); } void testToString() { -- 2.30.2