diff options
| author | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
| commit | 5f072a19d299191dbedc4b69c8e0eda694cfa957 (patch) | |
| tree | 0ebfc27bd05d06b0cdb2fc0813b7d5649d36aee4 /src/theory/bv/kinds | |
| parent | db51926b5ce806754fc26c81b1b7d3e739fc4fc5 (diff) | |
Merging CAV14 paper bit-vector work.
Diffstat (limited to 'src/theory/bv/kinds')
| -rw-r--r-- | src/theory/bv/kinds | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index cf83150e1..4b2bba741 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -8,7 +8,7 @@ theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h" typechecker "theory/bv/theory_bv_type_rules.h" properties finite -properties check propagate presolve +properties check propagate presolve ppStaticLearn rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" @@ -70,6 +70,10 @@ 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" + constant BITVECTOR_BITOF_OP \ ::CVC4::BitVectorBitOf \ ::CVC4::BitVectorBitOfHashFunction \ @@ -167,6 +171,10 @@ typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule +typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule +typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule + typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule |