1 /********************* */
2 /*! \file proof_manager.h
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Guy Katz, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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 A manager for Proofs
14 ** A manager for Proofs.
17 #include "cvc4_private.h"
19 #ifndef __CVC4__PROOF_MANAGER_H
20 #define __CVC4__PROOF_MANAGER_H
24 #include <unordered_map>
25 #include <unordered_set>
27 #include "expr/node.h"
28 #include "context/cdhashset.h"
29 #include "context/cdhashmap.h"
30 #include "proof/clause_id.h"
31 #include "proof/proof.h"
32 #include "proof/proof_utils.h"
33 #include "proof/skolemization_manager.h"
34 #include "theory/logic_info.h"
35 #include "theory/substitutions.h"
36 #include "util/proof.h"
43 // forward declarations
46 }/* Minisat namespace */
50 }/* BVMinisat namespace */
54 }/* CVC4::prop namespace */
58 const ClauseId
ClauseIdEmpty(-1);
59 const ClauseId
ClauseIdUndef(-2);
60 const ClauseId
ClauseIdError(-3);
62 template <class Solver
> class TSatProof
;
63 typedef TSatProof
< CVC4::Minisat::Solver
> CoreSatProof
;
67 class TheoryProofEngine
;
74 template <class Solver
> class LFSCSatProof
;
75 typedef LFSCSatProof
< CVC4::Minisat::Solver
> LFSCCoreSatProof
;
78 class LFSCTheoryProofEngine
;
80 class LFSCBitVectorProof
;
81 class LFSCRewriterProof
;
83 template <class Solver
> class ProofProxy
;
84 typedef ProofProxy
< CVC4::Minisat::Solver
> CoreProofProxy
;
85 typedef ProofProxy
< CVC4::BVMinisat::Solver
> BVProofProxy
;
88 typedef uint64_t SatVariable
;
90 typedef std::vector
<SatLiteral
> SatClause
;
91 }/* CVC4::prop namespace */
93 // different proof modes
97 };/* enum ProofFormat */
99 std::string
append(const std::string
& str
, uint64_t num
);
101 typedef std::unordered_map
<ClauseId
, prop::SatClause
*> IdToSatClause
;
102 typedef context::CDHashSet
<Expr
, ExprHashFunction
> CDExprSet
;
103 typedef std::unordered_map
<Node
, std::vector
<Node
>, NodeHashFunction
> NodeToNodes
;
104 typedef context::CDHashMap
<Node
, std::vector
<Node
>, NodeHashFunction
> CDNodeToNodes
;
105 typedef std::unordered_set
<ClauseId
> IdHashSet
;
108 RULE_GIVEN
, /* input assertion */
109 RULE_DERIVED
, /* a "macro" rule */
110 RULE_RECONSTRUCT
, /* prove equivalence using another method */
111 RULE_TRUST
, /* trust without evidence (escape hatch until proofs are fully supported) */
112 RULE_INVALID
, /* assert-fail if this is ever needed in proof; use e.g. for split lemmas */
113 RULE_CONFLICT
, /* re-construct as a conflict */
114 RULE_TSEITIN
, /* Tseitin CNF transformation */
115 RULE_SPLIT
, /* A splitting lemma of the form a v ~ a*/
117 RULE_ARRAYS_EXT
, /* arrays, extensional */
118 RULE_ARRAYS_ROW
, /* arrays, read-over-write */
119 };/* enum ProofRules */
121 class RewriteLogEntry
{
123 RewriteLogEntry(unsigned ruleId
, Node original
, Node result
)
124 : d_ruleId(ruleId
), d_original(original
), d_result(result
) {
127 unsigned getRuleId() const {
131 Node
getOriginal() const {
135 Node
getResult() const {
146 context::Context
* d_context
;
148 CoreSatProof
* d_satProof
;
149 CnfProof
* d_cnfProof
;
150 TheoryProofEngine
* d_theoryProof
;
152 // information that will need to be shared across proofs
153 ExprSet d_inputFormulas
;
154 std::map
<Expr
, std::string
> d_inputFormulaToName
;
155 CDExprSet d_inputCoreFormulas
;
156 CDExprSet d_outputCoreFormulas
;
158 SkolemizationManager d_skolemizationManager
;
162 std::unique_ptr
<Proof
> d_fullProof
;
163 ProofFormat d_format
; // used for now only in debug builds
165 CDNodeToNodes d_deps
;
167 std::set
<Type
> d_printedTypes
;
169 std::map
<std::string
, std::string
> d_rewriteFilters
;
170 std::map
<Node
, std::string
> d_assertionFilters
;
172 std::vector
<RewriteLogEntry
> d_rewriteLog
;
178 ProofManager(context::Context
* context
, ProofFormat format
= LFSC
);
181 static ProofManager
* currentPM();
184 void initSatProof(Minisat::Solver
* solver
);
185 static void initCnfProof(CVC4::prop::CnfStream
* cnfStream
,
186 context::Context
* ctx
);
187 static void initTheoryProofEngine();
189 // getting various proofs
190 static const Proof
& getProof(SmtEngine
* smt
);
191 static CoreSatProof
* getSatProof();
192 static CnfProof
* getCnfProof();
193 static TheoryProofEngine
* getTheoryProofEngine();
194 static TheoryProof
* getTheoryProof( theory::TheoryId id
);
195 static UFProof
* getUfProof();
196 static BitVectorProof
* getBitVectorProof();
197 static ArrayProof
* getArrayProof();
198 static ArithProof
* getArithProof();
200 static SkolemizationManager
*getSkolemizationManager();
202 // iterators over data shared by proofs
203 typedef ExprSet::const_iterator assertions_iterator
;
205 // iterate over the assertions (these are arbitrary boolean formulas)
206 assertions_iterator
begin_assertions() const {
207 return d_inputFormulas
.begin();
209 assertions_iterator
end_assertions() const { return d_inputFormulas
.end(); }
210 size_t num_assertions() const { return d_inputFormulas
.size(); }
211 bool have_input_assertion(const Expr
& assertion
) {
212 return d_inputFormulas
.find(assertion
) != d_inputFormulas
.end();
215 void ensureLiteral(Node node
);
219 Node
lookupOp(TNode n
) const;
220 bool hasOp(TNode n
) const;
222 std::map
<Node
, Node
> d_ops
;
223 std::map
<Node
, Node
> d_bops
;
224 //---end from Morgan---
228 static std::string
getInputClauseName(ClauseId id
, const std::string
& prefix
= "");
229 static std::string
getLemmaClauseName(ClauseId id
, const std::string
& prefix
= "");
230 static std::string
getLemmaName(ClauseId id
, const std::string
& prefix
= "");
231 static std::string
getLearntClauseName(ClauseId id
, const std::string
& prefix
= "");
232 static std::string
getPreprocessedAssertionName(Node node
, const std::string
& prefix
= "");
233 static std::string
getAssertionName(Node node
, const std::string
& prefix
= "");
234 static std::string
getInputFormulaName(const Expr
& expr
);
236 static std::string
getVarName(prop::SatVariable var
, const std::string
& prefix
= "");
237 static std::string
getAtomName(prop::SatVariable var
, const std::string
& prefix
= "");
238 static std::string
getAtomName(TNode atom
, const std::string
& prefix
= "");
239 static std::string
getLitName(prop::SatLiteral lit
, const std::string
& prefix
= "");
240 static std::string
getLitName(TNode lit
, const std::string
& prefix
= "");
241 static bool hasLitName(TNode lit
);
243 // for SMT variable names that have spaces and other things
244 static std::string
sanitize(TNode var
);
246 /** Add proof assertion - unlike addCoreAssertion this is post definition expansion **/
247 void addAssertion(Expr formula
);
249 /** Public unsat core methods **/
250 void addCoreAssertion(Expr formula
);
252 void addDependence(TNode n
, TNode dep
);
253 void addUnsatCore(Expr formula
);
255 // trace dependences back to unsat core
256 void traceDeps(TNode n
, ExprSet
* coreAssertions
);
257 void traceDeps(TNode n
, CDExprSet
* coreAssertions
);
258 void traceUnsatCore();
260 typedef CDExprSet::const_iterator output_core_iterator
;
262 output_core_iterator
begin_unsat_core() const { return d_outputCoreFormulas
.begin(); }
263 output_core_iterator
end_unsat_core() const { return d_outputCoreFormulas
.end(); }
264 size_t size_unsat_core() const { return d_outputCoreFormulas
.size(); }
265 std::vector
<Expr
> extractUnsatCore();
267 bool unsatCoreAvailable() const;
268 void getLemmasInUnsatCore(theory::TheoryId theory
, std::vector
<Node
> &lemmas
);
269 Node
getWeakestImplicantInUnsatCore(Node lemma
);
271 int nextId() { return d_nextId
++; }
273 void setLogic(const LogicInfo
& logic
);
274 const std::string
getLogic() const { return d_logic
.getLogicString(); }
275 LogicInfo
& getLogicInfo() { return d_logic
; }
277 void markPrinted(const Type
& type
);
278 bool wasPrinted(const Type
& type
) const;
280 void addRewriteFilter(const std::string
&original
, const std::string
&substitute
);
281 void clearRewriteFilters();
282 bool haveRewriteFilter(TNode lit
);
284 void addAssertionFilter(const Node
& node
, const std::string
& rewritten
);
286 static void registerRewrite(unsigned ruleId
, Node original
, Node result
);
287 static void clearRewriteLog();
289 std::vector
<RewriteLogEntry
> getRewriteLog();
290 void dumpRewriteLog() const;
292 void printGlobalLetMap(std::set
<Node
>& atoms
,
295 std::ostringstream
& paren
);
298 void constructSatProof();
299 std::set
<Node
> satClauseToNodeSet(prop::SatClause
* clause
);
300 };/* class ProofManager */
302 class LFSCProof
: public Proof
305 LFSCProof(SmtEngine
* smtEngine
,
306 LFSCCoreSatProof
* sat
,
308 LFSCTheoryProofEngine
* theory
);
309 ~LFSCProof() override
{}
310 void toStream(std::ostream
& out
) const override
;
311 void toStream(std::ostream
& out
, const ProofLetMap
& map
) const override
;
314 // FIXME: hack until we get preprocessing
315 void printPreprocessedAssertions(const NodeSet
& assertions
,
318 ProofLetMap
& globalLetMap
) const;
320 void checkUnrewrittenAssertion(const NodeSet
& assertions
) const;
322 LFSCCoreSatProof
* d_satProof
;
323 LFSCCnfProof
* d_cnfProof
;
324 LFSCTheoryProofEngine
* d_theoryProof
;
325 SmtEngine
* d_smtEngine
;
326 }; /* class LFSCProof */
328 std::ostream
& operator<<(std::ostream
& out
, CVC4::ProofRule k
);
329 }/* CVC4 namespace */
333 #endif /* __CVC4__PROOF_MANAGER_H */