From 1c5ad02344b9041cab9dd275ae69c953c31c6b8d Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Sun, 2 May 2010 02:20:17 +0000 Subject: [PATCH] smt parser for bit-vectors --- src/expr/builtin_kinds | 4 +- src/expr/node_manager.h | 2 +- src/expr/type_node.cpp | 4 +- src/parser/antlr_input.h | 11 ++++ src/parser/smt/Smt.g | 95 ++++++++++++++++++++++++++++- src/theory/bv/kinds | 68 +++++++++++++++++++-- src/util/bitvector.h | 51 ++++++++++++++-- test/regress/regress0/bv/test00.smt | 49 +++++++++++++++ 8 files changed, 268 insertions(+), 16 deletions(-) create mode 100644 test/regress/regress0/bv/test00.smt diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds index 1c24b045c..5ce38f5fd 100644 --- a/src/expr/builtin_kinds +++ b/src/expr/builtin_kinds @@ -130,8 +130,8 @@ operator FUNCTION_TYPE 2: "function type" variable SORT_TYPE "sort type" constant BITVECTOR_TYPE \ - unsigned \ - ::CVC4::UnsignedHashStrategy \ + ::CVC4::BitVectorSize \ + "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \ "util/bitvector.h" \ "bit-vector type" \ No newline at end of file diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 8243bd6da..5cb19bc89 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -634,7 +634,7 @@ inline TypeNode NodeManager::kindType() { } inline TypeNode NodeManager::bitVectorType(unsigned size) { - return TypeNode(mkTypeConst(kind::BITVECTOR_TYPE)); + return TypeNode(mkTypeConst(BitVectorSize(size))); } /** Make a function type from domain to range. */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b935c837e..da16000ce 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -74,13 +74,13 @@ bool TypeNode::isBitVector() const { /** Is this a bit-vector type of size size */ bool TypeNode::isBitVector(unsigned size) const { - return getKind() == kind::BITVECTOR_TYPE && getConst() == size; + return getKind() == kind::BITVECTOR_TYPE && getConst() == size; } /** Get the size of this bit-vector type */ unsigned TypeNode::getBitVectorSize() const { Assert(isBitVector()); - return getConst(); + return getConst(); } diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 1d6f5f790..441d2a0b3 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -134,6 +134,8 @@ public: /** Retrieve the text associated with a token. */ inline static std::string tokenText(pANTLR3_COMMON_TOKEN token); + /** Retrieve an unsigned from the text of a token */ + inline static unsigned tokenToUnsigned( pANTLR3_COMMON_TOKEN token ); /** Retrieve an Integer from the text of a token */ inline static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token ); /** Retrieve a Rational from the text of a token */ @@ -180,6 +182,15 @@ std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) { return txt; } +unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) { + unsigned result; + std::stringstream ss; + ss << tokenText(token); + ss >> result; + return result; +} + + Integer AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) { Integer i( tokenText(token) ); return i; diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index bc2ecb661..dde5d26eb 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -94,7 +94,8 @@ setLogic(Parser *parser, const std::string& name) { parser->mkSort("U"); } else if(name == "QF_LRA"){ parser->defineType("Real", parser->getExprManager()->realType()); - } else{ + } else if(name == "QF_BV"){ + } else { // NOTE: Theory types go here Unhandled(name); } @@ -270,6 +271,7 @@ builtinOp[CVC4::Kind& kind] | IFF_TOK { $kind = CVC4::kind::IFF; } | EQUAL_TOK { $kind = CVC4::kind::EQUAL; } | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; } + // NOTE: Theory operators go here | GREATER_THAN_TOK { $kind = CVC4::kind::GT; } | GREATER_THAN_TOK EQUAL_TOK @@ -283,7 +285,35 @@ builtinOp[CVC4::Kind& kind] | TILDE_TOK { $kind = CVC4::kind::UMINUS; } | MINUS_TOK { $kind = CVC4::kind::MINUS; } // Bit-vectors - // NOTE: Theory operators go here + | CONCAT_TOK { $kind = CVC4::kind::BITVECTOR_CONCAT; } + | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; } + | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; } + | BVXOR_TOK { $kind = CVC4::kind::BITVECTOR_XOR; } + | BVNOT_TOK { $kind = CVC4::kind::BITVECTOR_NOT; } + | BVNAND_TOK { $kind = CVC4::kind::BITVECTOR_NAND; } + | BVNOR_TOK { $kind = CVC4::kind::BITVECTOR_NOR; } + | BVXNOR_TOK { $kind = CVC4::kind::BITVECTOR_XNOR; } + | BVCOMP_TOK { $kind = CVC4::kind::BITVECTOR_COMP; } + | BVMUL_TOK { $kind = CVC4::kind::BITVECTOR_MULT; } + | BVADD_TOK { $kind = CVC4::kind::BITVECTOR_PLUS; } + | BVSUB_TOK { $kind = CVC4::kind::BITVECTOR_SUB; } + | BVNEG_TOK { $kind = CVC4::kind::BITVECTOR_NEG; } + | BVUDIV_TOK { $kind = CVC4::kind::BITVECTOR_UDIV; } + | BVUREM_TOK { $kind = CVC4::kind::BITVECTOR_UREM; } + | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; } + | BVSREM_TOK { $kind = CVC4::kind::BITVECTOR_SREM; } + | BVSMOD_TOK { $kind = CVC4::kind::BITVECTOR_SMOD; } + | BVSHL_TOK { $kind = CVC4::kind::BITVECTOR_SHL; } + | BVLSHR_TOK { $kind = CVC4::kind::BITVECTOR_LSHR; } + | BVASHR_TOK { $kind = CVC4::kind::BITVECTOR_ASHR; } + | BVULT_TOK { $kind = CVC4::kind::BITVECTOR_ULT; } + | BVULE_TOK { $kind = CVC4::kind::BITVECTOR_ULE; } + | BVUGT_TOK { $kind = CVC4::kind::BITVECTOR_UGT; } + | BVUGE_TOK { $kind = CVC4::kind::BITVECTOR_UGE; } + | BVSLT_TOK { $kind = CVC4::kind::BITVECTOR_SLT; } + | BVSLE_TOK { $kind = CVC4::kind::BITVECTOR_SLE; } + | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; } + | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; } /* TODO: lt, gt, plus, minus, etc. */ ; @@ -292,6 +322,25 @@ builtinOp[CVC4::Kind& kind] */ parameterizedOperator[CVC4::Expr& op] : functionSymbol[op] + | bitVectorOperator[op] + ; + +/** + * Matches a bit-vector operator (the ones parametrized by numbers) + */ +bitVectorOperator[CVC4::Expr& op] + : EXTRACT_TOK '[' n1 = NUMERAL_TOK ':' n2 = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), AntlrInput::tokenToUnsigned($n2))); } + | REPEAT_TOK '[' n = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); } + | ZERO_EXTEND_TOK '[' n = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); } + | SIGN_EXTEND_TOK '[' n = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); } + | ROTATE_LEFT_TOK '[' n = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); } + | ROTATE_RIGHT_TOK '[' n = NUMERAL_TOK ']' + { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); } ; /** @@ -319,7 +368,7 @@ functionSymbol[CVC4::Expr& fun] } : functionName[name,CHECK_DECLARED] { PARSER_STATE->checkFunction(name); - fun = PARSER_STATE->getVariable(name); } + fun = PARSER_STATE->getVariable(name); } ; /** @@ -394,6 +443,9 @@ sortSymbol returns [CVC4::Type t] } : sortName[name,CHECK_NONE] { $t = PARSER_STATE->getSort(name); } + | BITVECTOR_TOK '[' NUMERAL_TOK ']' { + $t = EXPR_MANAGER->bitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_TOK)); + } ; /** @@ -503,6 +555,43 @@ STAR_TOK : '*'; TILDE_TOK : '~'; XOR_TOK : 'xor'; +// Bitvector tokens +BITVECTOR_TOK : 'BitVec'; +CONCAT_TOK : 'concat'; +EXTRACT_TOK : 'extract'; +BVAND_TOK : 'bvand'; +BVOR_TOK : 'bvor'; +BVXOR_TOK : 'bvxor'; +BVNOT_TOK : 'bvnot'; +BVNAND_TOK : 'bvnand'; +BVNOR_TOK : 'bvnor'; +BVXNOR_TOK : 'bvxnor'; +BVCOMP_TOK : 'bvcomp'; +BVMUL_TOK : 'bvmul'; +BVADD_TOK : 'bvadd'; +BVSUB_TOK : 'bvsub'; +BVNEG_TOK : 'bvneg'; +BVUDIV_TOK : 'bvudiv'; +BVUREM_TOK : 'bvurem'; +BVSDIV_TOK : 'bvsdiv'; +BVSREM_TOK : 'bvsrem'; +BVSMOD_TOK : 'bvsmod'; +BVSHL_TOK : 'bvshl'; +BVLSHR_TOK : 'bvlshr'; +BVASHR_TOK : 'bvashr'; +BVULT_TOK : 'bvult'; +BVULE_TOK : 'bvule'; +BVUGT_TOK : 'bvugt'; +BVUGE_TOK : 'bvuge'; +BVSLT_TOK : 'bvslt'; +BVSLE_TOK : 'bvsle'; +BVSGT_TOK : 'bvsgt'; +BVSGE_TOK : 'bvsge'; +REPEAT_TOK : 'repeat'; +ZERO_EXTEND_TOK : 'zero_extend'; +SIGN_EXTEND_TOK : 'sign_extend'; +ROTATE_LEFT_TOK : 'rotate_left'; +ROTATE_RIGHT_TOK : 'rotate_right'; /** * Matches an identifier from the input. An identifier is a sequence of letters, diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index aeb425474..ba8fc4efd 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -6,21 +6,81 @@ theory ::CVC4::theory::bv::TheoryBV "theory_bv.h" -constant CONST_BITVECTOR \ +constant BITVECTOR_CONST \ ::CVC4::BitVector \ ::CVC4::BitVectorHashStrategy \ "util/bitvector.h" \ "a fixed-width bit-vector constant" operator BITVECTOR_CONCAT 2 "bit-vector concatenation" +operator BITVECTOR_AND 2 "bitwise and" +operator BITVECTOR_OR 2 "bitwise or" +operator BITVECTOR_XOR 2 "bitwise xor" +operator BITVECTOR_NOT 2 "bitwise not" +operator BITVECTOR_NAND 2 "bitwise nand" +operator BITVECTOR_NOR 2 "bitwise nor" +operator BITVECTOR_XNOR 2 "bitwise xnor" +operator BITVECTOR_COMP 2 "equality comparison (returns one bit)" +operator BITVECTOR_MULT 2 "bit-vector multiplication" +operator BITVECTOR_PLUS 2 "bit-vector addition" +operator BITVECTOR_SUB 2 "bit-vector subtraction" +operator BITVECTOR_NEG 1 "bit-vector unary negation" +operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)" +operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)" +operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division" +operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)" +operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)" +operator BITVECTOR_SHL 2 "bit-vector left shift" +operator BITVECTOR_LSHR 2 "bit-vector logical shift right" +operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right" +operator BITVECTOR_ULT 2 "bit-vector unsigned less than" +operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal" +operator BITVECTOR_UGT 2 "bit-vector unsigned greater than" +operator BITVECTOR_UGE 2 "bit-vector unsigned greater than or equal" +operator BITVECTOR_SLT 2 "bit-vector signed less than" +operator BITVECTOR_SLE 2 "bit-vector signed less than or equal" +operator BITVECTOR_SGT 2 "bit-vector signed greater than" +operator BITVECTOR_SGE 2 "signed greater than or equal" + 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" +constant BITVECTOR_REPEAT_OP \ + ::CVC4::BitVectorRepeat \ + "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRepeat >" \ + "util/bitvector.h" \ + "operator for the bit-vector repeat" + +constant BITVECTOR_ZERO_EXTEND_OP \ + ::CVC4::BitVectorZeroExtend \ + "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorZeroExtend >" \ + "util/bitvector.h" \ + "operator for the bit-vector zero-extend" + +constant BITVECTOR_SIGN_EXTEND_OP \ + ::CVC4::BitVectorSignExtend \ + "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSignExtend >" \ + "util/bitvector.h" \ + "operator for the bit-vector sign-extend" +constant BITVECTOR_ROTATE_LEFT_OP \ + ::CVC4::BitVectorRotateLeft \ + "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateLeft >" \ + "util/bitvector.h" \ + "operator for the bit-vector rotate left" - \ No newline at end of file +constant BITVECTOR_ROTATE_RIGHT_OP \ + ::CVC4::BitVectorRotateRight \ + "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateRight >" \ + "util/bitvector.h" \ + "operator for the bit-vector rotate right" + +parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract" +parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat" +parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend" +parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend" +parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left" +parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right" diff --git a/src/util/bitvector.h b/src/util/bitvector.h index e1c0131d9..1ab13230b 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -105,6 +105,9 @@ struct BitVectorExtract { /** The low bit of the range for this extract */ unsigned low; + BitVectorExtract(unsigned high, unsigned low) + : high(high), low(low) {} + bool operator == (const BitVectorExtract& extract) const { return high == extract.high && low == extract.low; } @@ -122,11 +125,51 @@ public: } }; -/** - * Hash function for the unsigned integers. - */ +struct BitVectorSize { + unsigned size; + BitVectorSize(unsigned size) + : size(size) {} + operator unsigned () const { return size; } +}; + +struct BitVectorRepeat { + unsigned repeatAmount; + BitVectorRepeat(unsigned repeatAmount) + : repeatAmount(repeatAmount) {} + operator unsigned () const { return repeatAmount; } +}; + +struct BitVectorZeroExtend { + unsigned zeroExtendAmount; + BitVectorZeroExtend(unsigned zeroExtendAmount) + : zeroExtendAmount(zeroExtendAmount) {} + operator unsigned () const { return zeroExtendAmount; } +}; + +struct BitVectorSignExtend { + unsigned signExtendAmount; + BitVectorSignExtend(unsigned signExtendAmount) + : signExtendAmount(signExtendAmount) {} + operator unsigned () const { return signExtendAmount; } +}; + +struct BitVectorRotateLeft { + unsigned rotateLeftAmount; + BitVectorRotateLeft(unsigned rotateLeftAmount) + : rotateLeftAmount(rotateLeftAmount) {} + operator unsigned () const { return rotateLeftAmount; } +}; + +struct BitVectorRotateRight { + unsigned rotateRightAmount; + BitVectorRotateRight(unsigned rotateRightAmount) + : rotateRightAmount(rotateRightAmount) {} + operator unsigned () const { return rotateRightAmount; } +}; + +template struct UnsignedHashStrategy { - static inline size_t hash(unsigned x) { + static inline size_t hash(const T& x) { return (size_t)x; } }; diff --git a/test/regress/regress0/bv/test00.smt b/test/regress/regress0/bv/test00.smt new file mode 100644 index 000000000..20fe6811f --- /dev/null +++ b/test/regress/regress0/bv/test00.smt @@ -0,0 +1,49 @@ +(benchmark umulov1bw016.smt +:source { +We verify the correctness of an unsigned multiplication +overflow detection unit, which is described in +"Combined Unsigned and Two's Complement Saturating Multipliers" +by M. Schulte et al. + +Bit-width: 4 + +Contributed by Robert Brummayer (robert.brummayer@gmail.com). +} +:status unsat +:category { industrial } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((v1 BitVec[4])) +:extrafuns ((v2 BitVec[4])) +:formula +(let (?e3 bv0[4]) +(let (?e4 (concat ?e3 v1)) +(let (?e5 (concat ?e3 v2)) +(let (?e6 (bvmul ?e4 ?e5)) +(let (?e7 (extract[7:4] ?e6)) +(let (?e8 (ite (= ?e7 ?e3) bv1[1] bv0[1])) + +(let (?e32 (extract[3:3] v2)) +(let (?e34 (extract[2:2] v2)) +(let (?e35 (bvand (bvnot ?e32) (bvnot ?e34))) +(let (?e36 (extract[1:1] v2)) +(let (?e37 (bvand ?e35 (bvnot ?e36))) +(let (?e38 (extract[1:1] v1)) + +(let (?e39 (bvand ?e38 ?e32)) +(let (?e40 (extract[2:2] v1)) +(let (?e41 (bvand ?e40 (bvnot ?e35))) +(let (?e42 (bvand (bvnot ?e39) (bvnot ?e41))) +(let (?e43 (extract[3:3] v1)) +(let (?e44 (bvand ?e43 (bvnot ?e37))) +(let (?e45 (bvand ?e42 (bvnot ?e44))) + +(let (?e82 bv0[1]) +(let (?e83 (concat ?e82 v1)) +(let (?e84 (concat ?e82 v2)) +(let (?e85 (bvmul ?e83 ?e84)) +(let (?e86 (extract[4:4] ?e85)) +(let (?e87 (bvand ?e45 (bvnot ?e86))) +(let (?e88 (ite (= (bvnot ?e8) (bvnot ?e87)) bv1[1] bv0[1])) +(not (= (bvnot ?e88) bv0[1])) +))))))))))))))))))))))))))) -- 2.30.2