::CVC4::BitVector \
::CVC4::BitVectorHashFunction \
"util/bitvector.h" \
- "a fixed-width bit-vector constant"
+ "a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class"
enumerator BITVECTOR_TYPE \
"::CVC4::theory::bv::BitVectorEnumerator" \
"(*CVC4::theory::TypeEnumerator(%TYPE%))" \
"theory/type_enumerator.h"
-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 1 "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)"
-# total division kinds
-operator BITVECTOR_UDIV_TOTAL 2 "bit-vector total unsigned division, truncating towards 0 (undefined if divisor is 0)"
-operator BITVECTOR_UREM_TOTAL 2 "bit-vector total unsigned remainder from truncating division (undefined if divisor is 0)"
-
-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"
-
-operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting"
-operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bitblasting ackerman expansion of bvudiv"
-operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bitblasting ackerman expansion of bvurem"
+operator BITVECTOR_CONCAT 2: "concatenation of two or more bit-vectors"
+operator BITVECTOR_AND 2: "bitwise and of two or more bit-vectors"
+operator BITVECTOR_OR 2: "bitwise or of two or more bit-vectors"
+operator BITVECTOR_XOR 2: "bitwise xor of two or more bit-vectors"
+operator BITVECTOR_NOT 1 "bitwise not of a bit-vector"
+operator BITVECTOR_NAND 2 "bitwise nand of two bit-vectors"
+operator BITVECTOR_NOR 2 "bitwise nor of two bit-vectors"
+operator BITVECTOR_XNOR 2 "bitwise xnor of two bit-vectors"
+operator BITVECTOR_COMP 2 "equality comparison of two bit-vectors (returns one bit)"
+operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors"
+operator BITVECTOR_PLUS 2: "addition of two or more bit-vectors"
+operator BITVECTOR_SUB 2 "subtraction of two bit-vectors"
+operator BITVECTOR_NEG 1 "unary negation of a bit-vector"
+operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0)"
+operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0)"
+operator BITVECTOR_SDIV 2 "2's complement signed division"
+operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)"
+operator BITVECTOR_SMOD 2 "2's complement signed remainder (sign follows divisor)"
+# total division kinds
+operator BITVECTOR_UDIV_TOTAL 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)"
+operator BITVECTOR_UREM_TOTAL 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)"
+
+operator BITVECTOR_SHL 2 "bit-vector shift left (the two bit-vector parameters must have same width)"
+operator BITVECTOR_LSHR 2 "bit-vector logical shift right (the two bit-vector parameters must have same width)"
+operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)"
+operator BITVECTOR_ULT 2 "bit-vector unsigned less than (the two bit-vector parameters must have same width)"
+operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal (the two bit-vector parameters must have same width)"
+operator BITVECTOR_UGT 2 "bit-vector unsigned greater than (the two bit-vector parameters must have same width)"
+operator BITVECTOR_UGE 2 "bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width)"
+operator BITVECTOR_SLT 2 "bit-vector signed less than (the two bit-vector parameters must have same width)"
+operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vector parameters must have same width)"
+operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)"
+operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)"
+
+operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)"
+operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)"
+operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)"
constant BITVECTOR_BITOF_OP \
::CVC4::BitVectorBitOf \
::CVC4::BitVectorBitOfHashFunction \
"util/bitvector.h" \
- "operator for the bit-vector boolean bit extract"
+ "operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::BitVectorBitOf class"
constant BITVECTOR_EXTRACT_OP \
::CVC4::BitVectorExtract \
::CVC4::BitVectorExtractHashFunction \
"util/bitvector.h" \
- "operator for the bit-vector extract"
+ "operator for the bit-vector extract; payload is an instance of the CVC4::BitVectorExtract class"
constant BITVECTOR_REPEAT_OP \
::CVC4::BitVectorRepeat \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >" \
"util/bitvector.h" \
- "operator for the bit-vector repeat"
+ "operator for the bit-vector repeat; payload is an instance of the CVC4::BitVectorRepeat class"
constant BITVECTOR_ZERO_EXTEND_OP \
::CVC4::BitVectorZeroExtend \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >" \
"util/bitvector.h" \
- "operator for the bit-vector zero-extend"
+ "operator for the bit-vector zero-extend; payload is an instance of the CVC4::BitVectorZeroExtend class"
constant BITVECTOR_SIGN_EXTEND_OP \
::CVC4::BitVectorSignExtend \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >" \
"util/bitvector.h" \
- "operator for the bit-vector sign-extend"
+ "operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend class"
constant BITVECTOR_ROTATE_LEFT_OP \
::CVC4::BitVectorRotateLeft \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >" \
"util/bitvector.h" \
- "operator for the bit-vector rotate left"
+ "operator for the bit-vector rotate left; payload is an instance of the CVC4::BitVectorRotateLeft class"
constant BITVECTOR_ROTATE_RIGHT_OP \
::CVC4::BitVectorRotateRight \
"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >" \
"util/bitvector.h" \
- "operator for the bit-vector rotate right"
+ "operator for the bit-vector rotate right; payload is an instance of the CVC4::BitVectorRotateRight class"
-parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract"
-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"
+parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term"
+parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term"
+parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term"
+parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term"
+parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term"
+parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term"
+parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term"
constant INT_TO_BITVECTOR_OP \
::CVC4::IntToBitVector \
"::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >" \
"util/bitvector.h" \
- "operator for the integer conversion to bit-vector"
-parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector"
-operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer"
+ "operator for the integer conversion to bit-vector; payload is an instance of the CVC4::IntToBitVector class"
+parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term"
+operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer; parameter is a bit-vector"
typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule
typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompRule
+typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompTypeRule
typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule
typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule
-typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatRule
+typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatTypeRule
typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
** Major contributors: Liana Hadarean, Christopher L. Conway, Morgan Deters
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Bitvector theory.
+ ** \brief Bitvector theory typing rules
**
- ** Bitvector theory.
+ ** Bitvector theory typing rules.
**/
#include "cvc4_private.h"
}
return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize());
}
-};
-
+};/* class BitVectorConstantTypeRule */
class BitVectorBitOfTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw (TypeCheckingExceptionPrivate) {
-
+
if(check) {
BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>();
TypeNode t = n[0].getType(check);
-
+
if (!t.isBitVector()) {
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
}
throw TypeCheckingExceptionPrivate(n, "extract index is larger than the bitvector size");
}
}
- return nodeManager->booleanType();
+ return nodeManager->booleanType();
}
-};
-
+};/* class BitVectorBitOfTypeRule */
-class BitVectorCompRule {
+class BitVectorCompTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw (TypeCheckingExceptionPrivate, AssertionException) {
}
return nodeManager->mkBitVectorType(1);
}
-};
+};/* class BitVectorCompTypeRule */
class BitVectorFixedWidthTypeRule {
public:
}
return t;
}
-};
+};/* class BitVectorFixedWidthTypeRule */
class BitVectorPredicateTypeRule {
public:
}
return nodeManager->booleanType();
}
-};
+};/* class BitVectorPredicateTypeRule */
class BitVectorEagerAtomTypeRule {
public:
}
return nodeManager->booleanType();
}
-};
+};/* class BitVectorEagerAtomTypeRule */
class BitVectorAckermanizationUdivTypeRule {
public:
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
}
}
- return lhsType;
+ return lhsType;
}
-};
+};/* class BitVectorAckermanizationUdivTypeRule */
class BitVectorAckermanizationUremTypeRule {
public:
throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
}
}
- return lhsType;
+ return lhsType;
}
-};
-
+};/* class BitVectorAckermanizationUremTypeRule */
class BitVectorExtractTypeRule {
public:
}
return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1);
}
-};
+};/* class BitVectorExtractTypeRule */
class BitVectorExtractOpTypeRule {
public:
Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP);
return nodeManager->builtinOperatorType();
}
-};
+};/* class BitVectorExtractOpTypeRule */
-class BitVectorConcatRule {
+class BitVectorConcatTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw (TypeCheckingExceptionPrivate, AssertionException) {
}
return nodeManager->mkBitVectorType(size);
}
-};
+};/* class BitVectorConcatTypeRule */
class BitVectorRepeatTypeRule {
public:
unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
}
-};
+};/* class BitVectorRepeatTypeRule */
class BitVectorExtendTypeRule {
public:
(unsigned) n.getOperator().getConst<BitVectorZeroExtend>();
return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize());
}
-};
+};/* class BitVectorExtendTypeRule */
class BitVectorConversionTypeRule {
public:
InternalError("bv-conversion typerule invoked for non-bv-conversion kind");
}
-};
+};/* class BitVectorConversionTypeRule */
class CardinalityComputer {
public:
projects / cvc5.git / commitdiff