1 /********************* */
2 /*! \file bv_solver_simple.h
4 ** Top contributors (to current version):
5 ** Mathias Preiner, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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 Simple bit-blast solver
14 ** Simple bit-blast solver that sends bit-blast lemmas directly to MiniSat.
17 #include "cvc4_private.h"
19 #ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
20 #define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
22 #include <unordered_map>
24 #include "theory/bv/bitblast/simple_bitblaster.h"
25 #include "theory/bv/bv_solver.h"
26 #include "theory/bv/proof_checker.h"
27 #include "theory/eager_proof_generator.h"
35 * Simple bit-blasting solver that sends bit-blasting lemmas directly to the
36 * internal MiniSat. It is also ablo to handle atoms of kind
37 * BITVECTOR_EAGER_ATOM.
39 * Sends lemmas atom <=> bb(atom) to MiniSat on preNotifyFact().
41 class BVSolverSimple
: public BVSolver
44 BVSolverSimple(TheoryState
* state
,
45 TheoryInferenceManager
& inferMgr
,
46 ProofNodeManager
* pnm
);
47 ~BVSolverSimple() = default;
49 void preRegisterTerm(TNode n
) override
{}
51 bool preNotifyFact(TNode atom
,
55 bool isInternal
) override
;
57 std::string
identify() const override
{ return "BVSolverSimple"; };
59 Theory::PPAssertStatus
ppAssert(
60 TrustNode in
, TrustSubstitutionMap
& outSubstitutions
) override
62 return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED
;
65 bool collectModelValues(TheoryModel
* m
,
66 const std::set
<Node
>& termSet
) override
;
70 * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the
73 void addBBLemma(TNode fact
);
75 /** Bit-blaster used to bit-blast atoms/terms. */
76 std::unique_ptr
<BBSimple
> d_bitblaster
;
78 /** Proof generator that manages proofs for lemmas generated by this class. */
79 std::unique_ptr
<EagerProofGenerator
> d_epg
;
81 BVProofRuleChecker d_bvProofChecker
;