From 349131957e91150c24a9c69f5e1f04e34494b0c6 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 29 Apr 2010 23:42:41 +0000 Subject: [PATCH] Added the capability to construct expressions by passing the operator instead of the kind, i.e. Expr op = ..."f"... em.mkExpr(op, children); Operator kinds are automatically associated with the enclosing expression kind in the DSL and generated. --- src/expr/builtin_kinds | 7 +++++ src/expr/expr_manager_template.cpp | 26 ++++++++++++++++++ src/expr/expr_manager_template.h | 12 +++++++++ src/expr/metakind_template.h | 15 +++++++++++ src/expr/mkkind | 4 +-- src/expr/mkmetakind | 25 ++++++++++++------ src/expr/node_manager.h | 30 +++++++++++++++++++++ src/expr/type.cpp | 25 +++++++++++++++++- src/expr/type.h | 31 ++++++++++++++++++++++ src/expr/type_node.cpp | 17 ++++++++++++ src/expr/type_node.h | 9 +++++++ src/parser/parser.h | 2 +- src/parser/smt/Smt.g | 17 ++++++++---- src/theory/bv/kinds | 15 ++++++++++- src/theory/uf/kinds | 2 +- src/util/bitvector.cpp | 4 +++ src/util/bitvector.h | 42 +++++++++++++++++++++++++++++- 17 files changed, 263 insertions(+), 20 deletions(-) diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds index eb41c788e..1c24b045c 100644 --- a/src/expr/builtin_kinds +++ b/src/expr/builtin_kinds @@ -128,3 +128,10 @@ constant TYPE_CONSTANT \ "basic types" operator FUNCTION_TYPE 2: "function type" variable SORT_TYPE "sort type" + +constant BITVECTOR_TYPE \ + unsigned \ + ::CVC4::UnsignedHashStrategy \ + "util/bitvector.h" \ + "bit-vector type" + \ No newline at end of file diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 3480cc0e6..b957019fb 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -66,6 +66,11 @@ IntegerType ExprManager::integerType() const { return Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())); } +BitVectorType ExprManager::bitVectorType(unsigned size) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->bitVectorType(size))); +} + Expr ExprManager::mkExpr(Kind kind) { const unsigned n = 0; CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, @@ -161,6 +166,27 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector& children) { return Expr(this, d_nodeManager->mkNodePtr(kind, nodes)); } +Expr ExprManager::mkExpr(Expr opExpr, const std::vector& children) { + const unsigned n = children.size(); + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + + NodeManagerScope nms(d_nodeManager); + + vector nodes; + vector::const_iterator it = children.begin(); + vector::const_iterator it_end = children.end(); + while(it != it_end) { + nodes.push_back(it->getNode()); + ++it; + } + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), nodes)); +} + /** Make a function type from domain to range. */ FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) { NodeManagerScope nms(d_nodeManager); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 5ef6ef984..b3a1b68df 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -96,6 +96,9 @@ public: /** Get the type for integers */ IntegerType integerType() const; + /** The the type for bit-vectors */ + BitVectorType bitVectorType(unsigned size) const; + /** * Make a unary expression of a given kind (TRUE, FALSE,...). * @param kind the kind of expression @@ -163,6 +166,15 @@ public: */ Expr mkExpr(Kind kind, const std::vector& children); + /** + * Make an n-ary expression of given tre operator to appply and a vector of + * it's children + * @param opExpr the operator expression + * @param children the subexpressions + * @return the n-ary expression + */ + Expr mkExpr(Expr opExpr, const std::vector& children); + /** Create a constant of type T */ template Expr mkConst(const T&); diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index fda2801be..57bfc51e5 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -141,6 +141,21 @@ ${metakind_canbeatomic} return canBeAtomic[k]; }/* kindCanBeAtomic(k) */ + +/** + * Map a kind of the operator to the kind of the enclosing expression. For + * example, since the kind of functions is just VARIABLE, it should map + * VARIABLE to APPLY_UF. + */ +static inline Kind operatorKindToKind(Kind k) { + static const Kind kind2kind[] = { + kind::UNDEFINED_KIND, /* NULL_EXPR */ +${metakind_operatorKinds} + kind::UNDEFINED_KIND /* LAST_KIND */ + }; + + return kind2kind[k]; +} }/* CVC4::kind namespace */ namespace expr { diff --git a/src/expr/mkkind b/src/expr/mkkind index 294dc5d7e..d9c64b660 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -93,12 +93,12 @@ function nonatomic_operator { } function parameterized { - # parameterized K #children ["comment"] + # parameterized K1 K2 #children ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen - register_kind "$1" "$2" "$3" + register_kind "$1" "$3" "$4" } function constant { diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 84d18e218..e8f3724f1 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -46,6 +46,7 @@ metakind_constHashes= metakind_constPrinters= metakind_ubchildren= metakind_lbchildren= +metakind_operatorKinds= seen_theory=false seen_theory_builtin=false @@ -86,7 +87,7 @@ function variable { lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind VARIABLE "$1" 0 + register_metakind VARIABLE "$1" UNDEFINED_KIND 0 } function operator { @@ -95,7 +96,7 @@ function operator { lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind OPERATOR "$1" "$2" + register_metakind OPERATOR "$1" UNDEFINED_KIND "$2" } function nonatomic_operator { @@ -104,16 +105,16 @@ function nonatomic_operator { lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind NONATOMIC_OPERATOR "$1" "$2" + register_metakind NONATOMIC_OPERATOR "$1" UNDEFINED_KIND "$2" } function parameterized { - # parameterized K #children ["comment"] + # parameterized K1 K2 #children ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind PARAMETERIZED "$1" "$2" + register_metakind PARAMETERIZED "$1" "$2" "$3" } function constant { @@ -141,7 +142,7 @@ function constant { metakind_includes="${metakind_includes} #include \"$4\"" fi - register_metakind CONSTANT "$1" 0 + register_metakind CONSTANT "$1" UNDEFINED_KIND 0 metakind_constantMaps="${metakind_constantMaps} }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ @@ -206,7 +207,11 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > { function register_metakind { mk=$1 k=$2 - nc=$3 + k1=$3 + nc=$4 + + metakind_operatorKinds="${metakind_operatorKinds} kind::$k1, /* $k */ +"; if [ $mk = NONATOMIC_OPERATOR ]; then metakind_canbeatomic="${metakind_canbeatomic} false, /* $k */ @@ -289,6 +294,9 @@ while [ $# -gt 0 ]; do " metakind_canbeatomic="${metakind_canbeatomic} /* from $b */ +" + metakind_operatorKinds="${metakind_operatorKinds} + /* from $b */ " source "$kf" check_theory_seen @@ -308,7 +316,8 @@ for var in \ metakind_constHashes \ metakind_constPrinters \ metakind_ubchildren \ - metakind_lbchildren; do + metakind_lbchildren \ + metakind_operatorKinds; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 39c1c91b9..ab8199d1e 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -285,6 +285,12 @@ public: template Node* mkNodePtr(Kind kind, const std::vector >& children); + /** Create a node by applying an operator to the children */ + template + Node mkNode(TNode opNode, const std::vector >& children); + template + Node* mkNodePtr(TNode opNode, const std::vector >& children); + /** * Create a variable with the given name and type. NOTE that no * lookup is done on the name. If you mkVar("a", type) and then @@ -454,6 +460,9 @@ public: /** Get the (singleton) type for sorts. */ inline TypeNode kindType(); + /** Get the type of bitvectors of size size */ + inline TypeNode bitVectorType(unsigned size); + /** * Make a function type from domain to range. * @@ -624,6 +633,10 @@ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst(KIND_TYPE)); } +inline TypeNode NodeManager::bitVectorType(unsigned size) { + return TypeNode(mkTypeConst(kind::BITVECTOR_TYPE)); +} + /** Make a function type from domain to range. */ inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) { std::vector sorts; @@ -845,6 +858,23 @@ inline Node* NodeManager::mkNodePtr(Kind kind, return NodeBuilder<>(this, kind).append(children).constructNodePtr(); } +// N-ary version for operators +template +inline Node NodeManager::mkNode(TNode opNode, + const std::vector >& + children) { + Assert(kind::metaKindOf(opNode.getKind()) == kind::metakind::PARAMETERIZED); + return NodeBuilder<>(this, kind::operatorKindToKind(opNode.getKind())).append(children); +} + +template +inline Node* NodeManager::mkNodePtr(TNode opNode, + const std::vector >& + children) { + return NodeBuilder<>(this, kind::operatorKindToKind(opNode.getKind())).constructNodePtr(); +} + + // N-ary version for types inline TypeNode NodeManager::mkTypeNode(Kind kind, const std::vector& children) { return NodeBuilder<>(this, kind).append(children).constructTypeNode(); diff --git a/src/expr/type.cpp b/src/expr/type.cpp index c76349fe3..faadfb0a6 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -120,13 +120,26 @@ bool Type::isReal() const { return d_typeNode->isInteger(); } -/** Cast to a integer type */ +/** Cast to a real type */ Type::operator RealType() const throw (AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isReal()); return RealType(*this); } +/** Is this the bit-vector type? */ +bool Type::isBitVector() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isBitVector(); +} + +/** Cast to a bit-vector type */ +Type::operator BitVectorType() const throw (AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isBitVector()); + return BitVectorType(*this); +} + /** Is this a function type? */ bool Type::isFunction() const { NodeManagerScope nms(d_nodeManager); @@ -214,6 +227,12 @@ RealType::RealType(const Type& t) throw (AssertionException) Assert(isReal()); } +BitVectorType::BitVectorType(const Type& t) throw (AssertionException) +: Type(t) +{ + Assert(isBitVector()); +} + FunctionType::FunctionType(const Type& t) throw (AssertionException) : Type(t) { @@ -233,4 +252,8 @@ SortType::SortType(const Type& t) throw (AssertionException) } +unsigned BitVectorType::getSize() const { + return d_typeNode->getBitVectorSize(); +} + }/* CVC4 namespace */ diff --git a/src/expr/type.h b/src/expr/type.h index c61b67f77..f513ef5de 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -34,6 +34,7 @@ class TypeNode; class BooleanType; class IntegerType; class RealType; +class BitVectorType; class FunctionType; class KindType; class SortType; @@ -152,6 +153,18 @@ public: */ operator RealType() const throw (AssertionException); + /** + * Is this the bit-vector type? + * @return true if the type is a bit-vector type + */ + bool isBitVector() const; + + /** + * Cast this type to a bit-vector type + * @return the BitVectorType + */ + operator BitVectorType() const throw (AssertionException); + /** * Is this a function type? * @return true if the type is a Boolean type @@ -278,6 +291,24 @@ public: KindType(const Type& type) throw (AssertionException); }; + +/** + * Class encapsulating the bit-vector type. + */ +class CVC4_PUBLIC BitVectorType : public Type { + +public: + + /** Construct from the base type */ + BitVectorType(const Type& type) throw (AssertionException); + + /** + * Returns the size of the bit-vector type. + * @return the width of the bit-vector type (> 0) + */ + unsigned getSize() const; +}; + /** * Output operator for types * @param out the stream to output to diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 08e50844b..b935c837e 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -67,4 +67,21 @@ bool TypeNode::isKind() const { return getKind() == kind::TYPE_CONSTANT && getConst() == KIND_TYPE; } +/** Is this a bit-vector type */ +bool TypeNode::isBitVector() const { + return getKind() == kind::BITVECTOR_TYPE; +} + +/** Is this a bit-vector type of size size */ +bool TypeNode::isBitVector(unsigned size) const { + return getKind() == kind::BITVECTOR_TYPE && getConst() == size; +} + +/** Get the size of this bit-vector type */ +unsigned TypeNode::getBitVectorSize() const { + Assert(isBitVector()); + return getConst(); +} + + }/* CVC4 namespace */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 12df5513f..1d32fffda 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -314,6 +314,15 @@ public: function types. */ bool isPredicate() const; + /** Is this a bit-vector type */ + bool isBitVector() const; + + /** Is this a bit-vector type of size size */ + bool isBitVector(unsigned size) const; + + /** Get the size of this bit-vector type */ + unsigned getBitVectorSize() const; + /** Is this a sort kind */ bool isSort() const; diff --git a/src/parser/parser.h b/src/parser/parser.h index a84021c10..f56ec03ac 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -13,7 +13,7 @@ ** A collection of state for use by parser implementations. **/ -#include "cvc4parser_private.h" +#include "cvc4parser_public.h" #ifndef __CVC4__PARSER__PARSER_STATE_H #define __CVC4__PARSER__PARSER_STATE_H diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 2dd680f09..5cd94ec0d 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -178,6 +178,7 @@ annotatedFormula[CVC4::Expr& expr] Kind kind; std::string name; std::vector args; /* = getExprVector(); */ + Expr op; /* Operator expression FIXME: move away kill it */ } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK @@ -195,14 +196,12 @@ annotatedFormula[CVC4::Expr& expr] // Semantic predicate not necessary if parenthesized subexpressions // are disallowed - // { isFunction(LT(2)->getText()) }? - + // { isFunction(LT(2)->getText()) }? LPAREN_TOK - functionSymbol[expr] - { args.push_back(expr); } + parameterizedOperator[op] annotatedFormulas[args,expr] RPAREN_TOK // TODO: check arity - { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); } + { expr = MK_EXPR(op,args); } | /* An ite expression */ LPAREN_TOK ITE_TOK @@ -283,10 +282,18 @@ builtinOp[CVC4::Kind& kind] | STAR_TOK { $kind = CVC4::kind::MULT; } | TILDE_TOK { $kind = CVC4::kind::UMINUS; } | MINUS_TOK { $kind = CVC4::kind::MINUS; } + // Bit-vectors // NOTE: Theory operators go here /* TODO: lt, gt, plus, minus, etc. */ ; +/** + * Matches an operator. + */ +parameterizedOperator[CVC4::Expr& op] + : functionSymbol[op] + ; + /** * Matches a (possibly undeclared) predicate identifier (returning the string). * @param check what kind of check to do with the symbol diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 8a4c6b6f7..aeb425474 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -10,4 +10,17 @@ constant CONST_BITVECTOR \ ::CVC4::BitVector \ ::CVC4::BitVectorHashStrategy \ "util/bitvector.h" \ - "a fixed-width bit-vector constant" \ No newline at end of file + "a fixed-width bit-vector constant" + +operator BITVECTOR_CONCAT 2 "bit-vector concatenation" +constant BITVECTOR_EXTRACT_OP \ + ::CVC4::BitVectorExtract \ + ::CVC4::BitVectorExtractHashStrategy \ + "util/bitvector.h" \ + "operator for the bit-vector extract" + +parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 2 "disequality" + + + + \ No newline at end of file diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 8cbf975f2..f95bfb582 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -6,4 +6,4 @@ theory ::CVC4::theory::uf::TheoryUF "theory_uf.h" -parameterized APPLY_UF 1: "uninterpreted function application" +parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index bea06f71a..125065118 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -13,4 +13,8 @@ std::ostream& operator <<(std::ostream& os, const BitVector& bv) { return os << bv.toString(); } +std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) { + return os << "[" << bv.high << ":" << bv.low << "]"; +} + } diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 3859fa407..e1c0131d9 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -85,14 +85,54 @@ public: } }; +/** + * Hash function for the BitVector constants. + */ struct BitVectorHashStrategy { static inline size_t hash(const BitVector& bv) { return bv.hash(); } }; -std::ostream& operator <<(std::ostream& os, const BitVector& bv); +/** + * The structure representing the extraction operation for bit-vectors. The + * operation map bit-vectors to bit-vector of size high - low + 1 + * by taking the bits at indices high ... low + */ +struct BitVectorExtract { + /** The high bit of the range for this extract */ + unsigned high; + /** The low bit of the range for this extract */ + unsigned low; + + bool operator == (const BitVectorExtract& extract) const { + return high == extract.high && low == extract.low; + } +}; +/** + * Hash function for the BitVectorExtract objects. + */ +class BitVectorExtractHashStrategy { +public: + static size_t hash(const BitVectorExtract& extract) { + size_t hash = extract.low; + hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2); + return hash; + } +}; + +/** + * Hash function for the unsigned integers. + */ +struct UnsignedHashStrategy { + static inline size_t hash(unsigned x) { + return (size_t)x; + } +}; + +std::ostream& operator <<(std::ostream& os, const BitVector& bv); +std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv); } -- 2.30.2