8e42d5cabae912eac7c1624a4db02ec48d350242
1 /********************* */
2 /*! \file bv_eager_solver.h
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Mathias Preiner, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Eager bit-blasting solver.
14 ** Eager bit-blasting solver.
17 #include "cvc4_private.h"
19 #ifndef CVC4__THEORY__BV__BV_EAGER_SOLVER_H
20 #define CVC4__THEORY__BV__BV_EAGER_SOLVER_H
22 #include <unordered_set>
25 #include "expr/node.h"
26 #include "proof/resolution_bitvector_proof.h"
27 #include "theory/bv/theory_bv.h"
28 #include "theory/theory_model.h"
34 class EagerBitblaster
;
40 class EagerBitblastSolver
{
42 EagerBitblastSolver(context::Context
* c
, theory::bv::TheoryBV
* bv
);
43 ~EagerBitblastSolver();
45 void assertFormula(TNode formula
);
50 bool collectModelInfo(theory::TheoryModel
* m
, bool fullModel
);
51 void setProofLog(proof::BitVectorProof
* bvp
);
54 context::CDHashSet
<Node
, NodeHashFunction
> d_assertionSet
;
55 context::CDHashSet
<Node
, NodeHashFunction
> d_assumptionSet
;
56 context::Context
* d_context
;
59 std::unique_ptr
<EagerBitblaster
> d_bitblaster
;
60 std::unique_ptr
<AigBitblaster
> d_aigBitblaster
;
64 proof::BitVectorProof
* d_bvp
;
65 }; // class EagerBitblastSolver
71 #endif // CVC4__THEORY__BV__BV_EAGER_SOLVER_H