diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/kinds | 8 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 4 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 14 |
3 files changed, 22 insertions, 4 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 381e90d47..d10e32ee0 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -6,7 +6,8 @@ theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h" -properties finite check propagate +properties finite +properties check propagate rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" @@ -15,6 +16,9 @@ constant BITVECTOR_TYPE \ "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \ "util/bitvector.h" \ "bit-vector type" +cardinality BITVECTOR_TYPE \ + "::CVC4::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \ + "theory/bv/theory_bv_type_rules.h" constant CONST_BITVECTOR \ ::CVC4::BitVector \ @@ -95,4 +99,4 @@ parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign- 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 +endtheory diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index d65f0388b..748352321 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -113,11 +113,11 @@ public: void preRegisterTerm(TNode n); - void registerTerm(TNode n) { } + //void registerTerm(TNode n) { } void check(Effort e); - void presolve() { } + //void presolve() { } void propagate(Effort e) { } diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index a27fd351c..613df47f3 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -189,6 +189,20 @@ public: } }; +class CardinalityComputer { +public: + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::BITVECTOR_TYPE); + + unsigned size = type.getConst<BitVectorSize>(); + if(size == 0) { + return 0; + } + Integer i = Integer(2).pow(size); + return i; + } +};/* class CardinalityComputer */ + }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |