summaryrefslogtreecommitdiff
path: root/src/theory/bv/kinds
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/kinds')
-rw-r--r--src/theory/bv/kinds8
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index e7374284e..9f6c42aa6 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -4,7 +4,11 @@
# src/theory/builtin/kinds.
#
-theory ::CVC4::theory::bv::TheoryBV "theory_bv.h"
+theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h"
+
+properties finite check
+
+rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
constant BITVECTOR_TYPE \
::CVC4::BitVectorSize \
@@ -90,3 +94,5 @@ parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-
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"
+
+endtheory \ No newline at end of file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback