diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
| commit | f9a4fe48a4ec2355f8fec93d3f47242577df2511 (patch) | |
| tree | eb49b7760b16aa17666d59464c96979b445fbcc8 /src/theory/bv/kinds | |
| parent | eecc1e4f301711dbb2bf1508ea0ba6cd20acd593 (diff) | |
Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.
Diffstat (limited to 'src/theory/bv/kinds')
| -rw-r--r-- | src/theory/bv/kinds | 8 |
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 |