Merge pull request #35 from mdeters/bv-kinds

Bit-vector kinds documentation

2 files changed, 81 insertions, 84 deletions

diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 4b2bba741..b4ecc1d3d 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -25,7 +25,7 @@ constant CONST_BITVECTOR \
     ::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" \
@@ -36,101 +36,101 @@ well-founded BITVECTOR_TYPE \
     "(*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
 
@@ -142,7 +142,7 @@ typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 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
@@ -178,7 +178,7 @@ typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanization
 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
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index c1829ce69..d7e22c32c 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -5,13 +5,13 @@
  ** 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"
@@ -36,18 +36,17 @@ public:
     }
     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");
       }
@@ -55,12 +54,11 @@ public:
         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) {
@@ -73,7 +71,7 @@ public:
     }
     return nodeManager->mkBitVectorType(1);
   }
-};
+};/* class BitVectorCompTypeRule */
 
 class BitVectorFixedWidthTypeRule {
 public:
@@ -94,7 +92,7 @@ public:
     }
     return t;
   }
-};
+};/* class BitVectorFixedWidthTypeRule */
 
 class BitVectorPredicateTypeRule {
 public:
@@ -112,7 +110,7 @@ public:
     }
     return nodeManager->booleanType();
   }
-};
+};/* class BitVectorPredicateTypeRule */
 
 class BitVectorEagerAtomTypeRule {
 public:
@@ -126,7 +124,7 @@ public:
     }
     return nodeManager->booleanType();
   }
-};
+};/* class BitVectorEagerAtomTypeRule */
 
 class BitVectorAckermanizationUdivTypeRule {
 public:
@@ -138,9 +136,9 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
       }
     }
-    return lhsType; 
+    return lhsType;
   }
-};
+};/* class BitVectorAckermanizationUdivTypeRule */
 
 class BitVectorAckermanizationUremTypeRule {
 public:
@@ -152,10 +150,9 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term");
       }
     }
-    return lhsType; 
+    return lhsType;
   }
-};
-
+};/* class BitVectorAckermanizationUremTypeRule */
 
 class BitVectorExtractTypeRule {
 public:
@@ -181,7 +178,7 @@ public:
     }
     return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1);
   }
-};
+};/* class BitVectorExtractTypeRule */
 
 class BitVectorExtractOpTypeRule {
 public:
@@ -190,9 +187,9 @@ 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) {
@@ -211,7 +208,7 @@ public:
     }
     return nodeManager->mkBitVectorType(size);
   }
-};
+};/* class BitVectorConcatTypeRule */
 
 class BitVectorRepeatTypeRule {
 public:
@@ -227,7 +224,7 @@ public:
     unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>();
     return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize());
   }
-};
+};/* class BitVectorRepeatTypeRule */
 
 class BitVectorExtendTypeRule {
 public:
@@ -245,7 +242,7 @@ public:
         (unsigned) n.getOperator().getConst<BitVectorZeroExtend>();
     return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize());
   }
-};
+};/* class BitVectorExtendTypeRule */
 
 class BitVectorConversionTypeRule {
 public:
@@ -268,7 +265,7 @@ public:
 
     InternalError("bv-conversion typerule invoked for non-bv-conversion kind");
   }
-};
+};/* class BitVectorConversionTypeRule */
 
 class CardinalityComputer {
 public: