diff options
Diffstat (limited to 'src/theory/bv/bv_eager_solver.h')
| -rw-r--r-- | src/theory/bv/bv_eager_solver.h | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 2754bdd3b..6a89a0f7c 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -2,7 +2,7 @@ /*! \file bv_eager_solver.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Andrew Reynolds + ** Liana Hadarean, Tim King, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -16,7 +16,8 @@ #include "cvc4_private.h" -#pragma once +#ifndef __CVC4__THEORY__BV__BV_EAGER_SOLVER_H +#define __CVC4__THEORY__BV__BV_EAGER_SOLVER_H #include <unordered_set> #include <vector> @@ -37,7 +38,7 @@ class AigBitblaster; */ class EagerBitblastSolver { public: - EagerBitblastSolver(theory::bv::TheoryBV* bv); + EagerBitblastSolver(context::Context* c, theory::bv::TheoryBV* bv); ~EagerBitblastSolver(); bool checkSat(); void assertFormula(TNode formula); @@ -51,11 +52,13 @@ class EagerBitblastSolver { void setProofLog(BitVectorProof* bvp); private: - typedef std::unordered_set<TNode, TNodeHashFunction> AssertionSet; - AssertionSet d_assertionSet; + context::CDHashSet<Node, NodeHashFunction> d_assertionSet; + context::CDHashSet<Node, NodeHashFunction> d_assumptionSet; + context::Context* d_context; + /** Bitblasters */ - EagerBitblaster* d_bitblaster; - AigBitblaster* d_aigBitblaster; + std::unique_ptr<EagerBitblaster> d_bitblaster; + std::unique_ptr<AigBitblaster> d_aigBitblaster; bool d_useAig; TheoryBV* d_bv; @@ -65,3 +68,5 @@ class EagerBitblastSolver { } // namespace bv } // namespace theory } // namespace CVC4 + +#endif // __CVC4__THEORY__BV__BV_EAGER_SOLVER_H |