1 /********************* */
2 /*! \file clausal_bitvector_proof.h
4 ** Top contributors (to current version):
5 ** Alex Ozdemir, Mathias Preiner
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 Bitvector proof for clausal (DRAT/LRAT) formats
14 ** An internal string stream is hooked up to CryptoMiniSat, which spits out a
15 ** binary DRAT proof. Depending on which kind of proof we're going to turn
16 ** that into, we process it in different ways.
19 #include "cvc4_private.h"
21 #ifndef CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
22 #define CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
26 #include <unordered_map>
28 #include "expr/expr.h"
29 #include "proof/bitvector_proof.h"
30 #include "proof/drat/drat_proof.h"
31 #include "proof/lrat/lrat_proof.h"
32 #include "proof/theory_proof.h"
33 #include "prop/cnf_stream.h"
34 #include "prop/sat_solver_types.h"
35 #include "theory/bv/theory_bv.h"
36 #include "util/statistics_registry.h"
42 class ClausalBitVectorProof
: public BitVectorProof
45 ClausalBitVectorProof(theory::bv::TheoryBV
* bv
,
46 TheoryProofEngine
* proofEngine
);
48 ~ClausalBitVectorProof() = default;
50 void attachToSatSolver(prop::SatSolver
& sat_solver
) override
;
52 void initCnfProof(prop::CnfStream
* cnfStream
,
53 context::Context
* cnf
,
54 prop::SatVariable trueVar
,
55 prop::SatVariable falseVar
) override
;
57 std::ostream
& getDratOstream() { return d_binaryDratProof
; }
59 void registerUsedClause(ClauseId id
, prop::SatClause
& clause
);
61 void calculateAtomsInBitblastingProof() override
;
64 // A list of all clauses and their ids which are passed into the SAT solver
65 std::unordered_map
<ClauseId
, prop::SatClause
> d_clauses
{};
66 std::vector
<ClauseId
> d_originalClauseIndices
{};
67 // Stores the proof recieved from the SAT solver.
68 std::ostringstream d_binaryDratProof
{};
69 std::vector
<ClauseId
> d_coreClauseIndices
{};
71 struct DratTranslationStatistics
73 DratTranslationStatistics();
74 ~DratTranslationStatistics();
76 // Total time spent doing translation (optimized binary DRAT -> in memory
77 // target format including IO, postprocessing, etc.)
78 TimerStat d_totalTime
;
79 // Time that the external tool actually spent
83 DratTranslationStatistics d_dratTranslationStatistics
;
86 // Optimizes the DRAT proof stored in `d_binaryDratProof` and returns a list
87 // of clause actually needed to check that proof (a smaller UNSAT core)
88 void optimizeDratProof();
90 // Given reference to a SAT clause encoded as a vector of literals, puts the
91 // literals into a canonical order
92 static void canonicalizeClause(prop::SatClause
& clause
);
94 struct DratOptimizationStatistics
96 DratOptimizationStatistics();
97 ~DratOptimizationStatistics();
99 // Total time spent using drat-trim to optimize the DRAT proof/formula
100 // (including IO, etc.)
101 TimerStat d_totalTime
;
102 // Time that drat-trim actually spent optimizing the DRAT proof/formula
103 TimerStat d_toolTime
;
104 // Time that was spent matching clauses in drat-trim's output to clauses in
106 TimerStat d_clauseMatchingTime
;
107 // Bytes in binary DRAT proof before optimization
108 IntStat d_initialDratSize
;
109 // Bytes in binary DRAT proof after optimization
110 IntStat d_optimizedDratSize
;
111 // Bytes in textual DIMACS bitblasted formula before optimization
112 IntStat d_initialFormulaSize
;
113 // Bytes in textual DIMACS bitblasted formula after optimization
114 IntStat d_optimizedFormulaSize
;
117 DratOptimizationStatistics d_dratOptimizationStatistics
;
121 * A representation of a clausal proof of a bitvector problem's UNSAT nature
123 class LfscClausalBitVectorProof
: public ClausalBitVectorProof
126 LfscClausalBitVectorProof(theory::bv::TheoryBV
* bv
,
127 TheoryProofEngine
* proofEngine
)
128 : ClausalBitVectorProof(bv
, proofEngine
)
132 void printTheoryLemmaProof(std::vector
<Expr
>& lemma
,
135 const ProofLetMap
& map
) override
;
136 void printBBDeclarationAndCnf(std::ostream
& os
,
138 ProofLetMap
& letMap
) override
;
142 * A DRAT proof for a bit-vector problem
144 class LfscDratBitVectorProof
: public LfscClausalBitVectorProof
147 LfscDratBitVectorProof(theory::bv::TheoryBV
* bv
,
148 TheoryProofEngine
* proofEngine
)
149 : LfscClausalBitVectorProof(bv
, proofEngine
)
153 void printEmptyClauseProof(std::ostream
& os
, std::ostream
& paren
) override
;
157 * An LRAT proof for a bit-vector problem
159 class LfscLratBitVectorProof
: public LfscClausalBitVectorProof
162 LfscLratBitVectorProof(theory::bv::TheoryBV
* bv
,
163 TheoryProofEngine
* proofEngine
)
164 : LfscClausalBitVectorProof(bv
, proofEngine
)
168 void printEmptyClauseProof(std::ostream
& os
, std::ostream
& paren
) override
;
172 * An Extended Resolution proof for a bit-vector problem
174 class LfscErBitVectorProof
: public LfscClausalBitVectorProof
177 LfscErBitVectorProof(theory::bv::TheoryBV
* bv
, TheoryProofEngine
* proofEngine
)
178 : LfscClausalBitVectorProof(bv
, proofEngine
)
182 void printEmptyClauseProof(std::ostream
& os
, std::ostream
& paren
) override
;
189 #endif /* CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */