diff options
author | Tim King <taking@cs.nyu.edu> | 2017-09-25 08:58:45 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-09-25 08:58:45 -0700 |
commit | c056e0711c6321b5d5b74e394cac3687dcade5b9 (patch) | |
tree | ef0dc24e067972f067d50717bfb6832fe0d77262 /src/theory/bv/bv_eager_solver.h | |
parent | e665b892db312e03ce9674b2a45aaca1b2dfd6ae (diff) |
Fixing CID 1362895: Initializing d_bvp to nullptr. (#1137)
* Fixing CID 1362895: Initializing d_bvp to nullptr. Miscellaneous cleanup.
Diffstat (limited to 'src/theory/bv/bv_eager_solver.h')
-rw-r--r-- | src/theory/bv/bv_eager_solver.h | 37 |
1 files changed, 19 insertions, 18 deletions
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index ec6cbad09..d259d49e6 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -22,8 +22,8 @@ #include <vector> #include "expr/node.h" -#include "theory/theory_model.h" #include "theory/bv/theory_bv.h" +#include "theory/theory_model.h" namespace CVC4 { namespace theory { @@ -36,31 +36,32 @@ class AigBitblaster; * BitblastSolver */ class EagerBitblastSolver { - typedef std::unordered_set<TNode, TNodeHashFunction> AssertionSet; - AssertionSet d_assertionSet; - /** Bitblasters */ - EagerBitblaster* d_bitblaster; - AigBitblaster* d_aigBitblaster; - bool d_useAig; - - TheoryBV* d_bv; - BitVectorProof * d_bvp; - -public: + public: EagerBitblastSolver(theory::bv::TheoryBV* bv); ~EagerBitblastSolver(); bool checkSat(); void assertFormula(TNode formula); // purely for debugging purposes - bool hasAssertions(const std::vector<TNode> &formulas); + bool hasAssertions(const std::vector<TNode>& formulas); void turnOffAig(); bool isInitialized(); void initialize(); void collectModelInfo(theory::TheoryModel* m, bool fullModel); - void setProofLog( BitVectorProof * bvp ); -}; + void setProofLog(BitVectorProof* bvp); + + private: + typedef std::unordered_set<TNode, TNodeHashFunction> AssertionSet; + AssertionSet d_assertionSet; + /** Bitblasters */ + EagerBitblaster* d_bitblaster; + AigBitblaster* d_aigBitblaster; + bool d_useAig; + + TheoryBV* d_bv; + BitVectorProof* d_bvp; +}; // class EagerBitblastSolver -} -} -} +} // namespace bv +} // namespace theory +} // namespace CVC4 |