diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
commit | 7aa55e0d38e73a02b11ad0c5a60196b610674050 (patch) | |
tree | c59def0ed00dcde29a5a6498cf74ac87dc3a2a6f /src/util/bitvector.h | |
parent | d8da6a3644d1cdbe62d44a8eb80068da4d1d2855 (diff) |
Refactored CnfStream to work with the bv theory Bitblaster:
* separated SatSolverInput interface class into two classes:
- TheoryProxy for the sat solver to communicate with the theories
- SatSolverInterface abstract class to communicate with the sat solver
* instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
* added abstract classes for DPLLSatSolver and BVSatSolver different interfaces
Replaced TheoryBV with bitblasting implementation:
* all operators bitblasted
* only operator elimination rewrite rules so far
Diffstat (limited to 'src/util/bitvector.h')
-rw-r--r-- | src/util/bitvector.h | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h index d7f0e13a5..8adb466cf 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -203,6 +203,33 @@ public: } };/* class BitVectorExtractHashStrategy */ + +/** + * The structure representing the extraction of one Boolean bit. + */ +struct CVC4_PUBLIC BitVectorBitOf { + /** The index of the bit */ + unsigned bitIndex; + BitVectorBitOf(unsigned i) + : bitIndex(i) {} + + bool operator == (const BitVectorBitOf& other) const { + return bitIndex == other.bitIndex; + } +};/* struct BitVectorBitOf */ + +/** + * Hash function for the BitVectorBitOf objects. + */ +class CVC4_PUBLIC BitVectorBitOfHashStrategy { +public: + static size_t hash(const BitVectorBitOf& b) { + return b.bitIndex; + } +};/* class BitVectorBitOfHashStrategy */ + + + struct CVC4_PUBLIC BitVectorSize { unsigned size; BitVectorSize(unsigned size) @@ -262,6 +289,13 @@ inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) { return os << "[" << bv.high << ":" << bv.low << "]"; } +inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) CVC4_PUBLIC; +inline std::ostream& operator <<(std::ostream& os, const BitVectorBitOf& bv) { + return os << "[" << bv.bitIndex << "]"; +} + + + }/* CVC4 namespace */ #endif /* __CVC4__BITVECTOR_H */ |