1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mathias Preiner, Haniel Barbosa, Andrew Reynolds
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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.
11 * ****************************************************************************
13 * Bit-blast solver that sends bit-blast lemmas directly to the internal
17 #include "cvc5_private.h"
19 #ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H
20 #define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H
22 #include "smt/env_obj.h"
23 #include "theory/bv/bitblast/proof_bitblaster.h"
24 #include "theory/bv/bv_solver.h"
25 #include "theory/bv/proof_checker.h"
32 * Bit-blasting solver that sends bit-blasting lemmas directly to the
33 * internal MiniSat. It is also ablo to handle atoms of kind
34 * BITVECTOR_EAGER_ATOM.
36 * Sends lemmas atom <=> bb(atom) to MiniSat on preNotifyFact().
38 class BVSolverBitblastInternal
: public BVSolver
41 BVSolverBitblastInternal(Env
& env
,
43 TheoryInferenceManager
& inferMgr
,
44 ProofNodeManager
* pnm
);
45 ~BVSolverBitblastInternal() = default;
47 bool needsEqualityEngine(EeSetupInfo
& esi
) override
{ return true; }
49 void preRegisterTerm(TNode n
) override
{}
51 bool preNotifyFact(TNode atom
,
55 bool isInternal
) override
;
57 TrustNode
explain(TNode n
) override
;
59 std::string
identify() const override
{ return "BVSolverBitblastInternal"; };
61 bool collectModelValues(TheoryModel
* m
,
62 const std::set
<Node
>& termSet
) override
;
64 Node
getValue(TNode node
, bool initialize
) override
;
66 /** get the proof checker of this theory */
67 BVProofRuleChecker
* getProofChecker();
71 * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the
74 void addBBLemma(TNode fact
);
76 /** Proof node manager. */
77 ProofNodeManager
* d_pnm
;
78 /** Bit-blaster used to bit-blast atoms/terms. */
79 std::unique_ptr
<BBProof
> d_bitblaster
;
80 /** Proof rule checker */
81 BVProofRuleChecker d_checker
;