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
}
inline TypeNode NodeManager::bitVectorType(unsigned size) {
- return TypeNode(mkTypeConst<unsigned>(kind::BITVECTOR_TYPE));
+ return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
}
/** Make a function type from domain to range. */
/** Is this a bit-vector type of size <code>size</code> */
bool TypeNode::isBitVector(unsigned size) const {
- return getKind() == kind::BITVECTOR_TYPE && getConst<unsigned>() == size;
+ return getKind() == kind::BITVECTOR_TYPE && getConst<BitVectorSize>() == size;
}
/** Get the size of this bit-vector type */
unsigned TypeNode::getBitVectorSize() const {
Assert(isBitVector());
- return getConst<unsigned>();
+ return getConst<BitVectorSize>();
}
/** 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 */
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;
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);
}
| 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
| 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. */
;
*/
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))); }
;
/**
}
: functionName[name,CHECK_DECLARED]
{ PARSER_STATE->checkFunction(name);
- fun = PARSER_STATE->getVariable(name); }
+ fun = PARSER_STATE->getVariable(name); }
;
/**
}
: sortName[name,CHECK_NONE]
{ $t = PARSER_STATE->getSort(name); }
+ | BITVECTOR_TOK '[' NUMERAL_TOK ']' {
+ $t = EXPR_MANAGER->bitVectorType(AntlrInput::tokenToUnsigned($NUMERAL_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,
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"
/** 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;
}
}
};
-/**
- * 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 <typename T>
struct UnsignedHashStrategy {
- static inline size_t hash(unsigned x) {
+ static inline size_t hash(const T& x) {
return (size_t)x;
}
};
--- /dev/null
+(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]))
+)))))))))))))))))))))))))))
projects / cvc5.git / commitdiff