1 /********************* */
2 /*! \file theory_proof.h
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Guy Katz, Yoni Zohar
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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 ** [[ Add lengthier description here ]]
14 ** \todo document this file
18 #include "cvc4_private.h"
20 #ifndef __CVC4__THEORY_PROOF_H
21 #define __CVC4__THEORY_PROOF_H
24 #include <unordered_map>
25 #include <unordered_set>
27 #include "expr/expr.h"
28 #include "proof/clause_id.h"
29 #include "proof/proof_utils.h"
30 #include "prop/sat_solver_types.h"
31 #include "theory/uf/equality_engine.h"
32 #include "util/proof.h"
37 } /* namespace CVC4::theory */
39 typedef std::unordered_map
< ClauseId
, prop::SatClause
* > IdToSatClause
;
43 typedef std::unordered_set
<Expr
, ExprHashFunction
> ExprSet
;
44 typedef std::map
<theory::TheoryId
, TheoryProof
* > TheoryProofTable
;
46 typedef std::set
<theory::TheoryId
> TheoryIdSet
;
47 typedef std::map
<Expr
, TheoryIdSet
> ExprToTheoryIds
;
49 class TheoryProofEngine
{
51 ExprSet d_registrationCache
;
52 TheoryProofTable d_theoryProofTable
;
53 ExprToTheoryIds d_exprToTheoryIds
;
56 * Returns whether the theory is currently supported in proof
59 bool supportedTheory(theory::TheoryId id
);
63 virtual ~TheoryProofEngine();
66 * Print the theory term (could be an atom) by delegating to the proper theory.
71 virtual void printLetTerm(Expr term
, std::ostream
& os
) = 0;
72 virtual void printBoundTerm(Expr term
, std::ostream
& os
,
73 const ProofLetMap
& map
) = 0;
76 * Print the proof representation of the given sort.
80 virtual void printSort(Type type
, std::ostream
& os
) = 0;
83 * Go over the assertions and register all terms with the theories.
86 * @param paren closing parenthesis
88 virtual void registerTermsFromAssertions() = 0;
91 * Print the theory assertions (arbitrary formulas over
95 * @param paren closing parenthesis
97 virtual void printAssertions(std::ostream
& os
, std::ostream
& paren
) = 0;
99 * Print variable declarations that need to appear within the proof,
100 * e.g. skolemized variables.
103 * @param paren closing parenthesis
105 virtual void printDeferredDeclarations(std::ostream
& os
, std::ostream
& paren
) = 0;
108 * Print aliasing declarations.
111 * @param paren closing parenthesis
113 virtual void printAliasingDeclarations(std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
&globalLetMap
) = 0;
116 * Print proofs of all the theory lemmas (must prove
117 * actual clause used in resolution proof).
122 virtual void printTheoryLemmas(const IdToSatClause
& lemmas
, std::ostream
& os
,
123 std::ostream
& paren
, ProofLetMap
& map
) = 0;
126 * Register theory atom (ensures all terms and atoms are declared).
130 void registerTerm(Expr atom
);
133 * Ensures that a theory proof class for the given theory is created.
134 * This method can be invoked regardless of whether the "proof" option
139 void registerTheory(theory::Theory
* theory
);
141 * Additional configuration of the theory proof class for the given theory.
142 * This method should only be invoked when the "proof" option has been set.
146 void finishRegisterTheory(theory::Theory
* theory
);
148 theory::TheoryId
getTheoryForLemma(const prop::SatClause
* clause
);
149 TheoryProof
* getTheoryProof(theory::TheoryId id
);
151 void markTermForFutureRegistration(Expr term
, theory::TheoryId id
);
153 void printConstantDisequalityProof(std::ostream
& os
, Expr c1
, Expr c2
, const ProofLetMap
&globalLetMap
);
155 virtual void printTheoryTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
) = 0;
157 bool printsAsBool(const Node
&n
);
160 class LFSCTheoryProofEngine
: public TheoryProofEngine
{
161 void bind(Expr term
, ProofLetMap
& map
, Bindings
& let_order
);
163 LFSCTheoryProofEngine()
164 : TheoryProofEngine() {}
166 void printTheoryTerm(Expr term
,
168 const ProofLetMap
& map
) override
;
170 void registerTermsFromAssertions() override
;
171 void printSortDeclarations(std::ostream
& os
, std::ostream
& paren
);
172 void printTermDeclarations(std::ostream
& os
, std::ostream
& paren
);
173 void printCoreTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
);
174 void printLetTerm(Expr term
, std::ostream
& os
) override
;
175 void printBoundTerm(Expr term
,
177 const ProofLetMap
& map
) override
;
178 void printAssertions(std::ostream
& os
, std::ostream
& paren
) override
;
179 void printLemmaRewrites(NodePairSet
& rewrites
,
181 std::ostream
& paren
);
182 void printDeferredDeclarations(std::ostream
& os
,
183 std::ostream
& paren
) override
;
184 void printAliasingDeclarations(std::ostream
& os
,
186 const ProofLetMap
& globalLetMap
) override
;
187 void printTheoryLemmas(const IdToSatClause
& lemmas
,
190 ProofLetMap
& map
) override
;
191 void printSort(Type type
, std::ostream
& os
) override
;
193 void performExtraRegistrations();
195 void finalizeBvConflicts(const IdToSatClause
& lemmas
, std::ostream
& os
);
198 static void dumpTheoryLemmas(const IdToSatClause
& lemmas
);
200 // TODO: this function should be moved into the BV prover.
202 std::map
<Node
, std::string
> d_assertionToRewrite
;
207 // Pointer to the theory for this proof
208 theory::Theory
* d_theory
;
209 TheoryProofEngine
* d_proofEngine
;
210 virtual theory::TheoryId
getTheoryId() = 0;
213 TheoryProof(theory::Theory
* th
, TheoryProofEngine
* proofEngine
)
215 , d_proofEngine(proofEngine
)
217 virtual ~TheoryProof() {};
219 * Print a term belonging some theory, not necessarily this one.
221 * @param term expresion representing term
222 * @param os output stream
224 void printTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
) {
225 d_proofEngine
->printBoundTerm(term
, os
, map
);
228 * Print a term belonging to THIS theory.
230 * @param term expression representing term
231 * @param os output stream
233 virtual void printOwnedTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
) = 0;
235 * Print the proof representation of the given type that belongs to some theory.
240 void printSort(Type type
, std::ostream
& os
) {
241 d_proofEngine
->printSort(type
, os
);
244 // congrence matching term helper
245 bool match(TNode n1
, TNode n2
);
248 * Helper function for ProofUF::toStreamRecLFSC and
249 * ProofArray::toStreamRecLFSC
251 * - pf: equality engine proof
252 * - map: A map for the let-expressions in the proof
253 * - subTrans: main transitivity proof part
254 * - pPrettyPrinter: optional pretty printer for sub-proofs
256 * - the index of the contradicting node in pf.
259 const theory::eq::EqProof
& pf
,
260 const ProofLetMap
& map
,
261 std::shared_ptr
<theory::eq::EqProof
> subTrans
,
262 theory::eq::EqProof::PrettyPrinter
* pPrettyPrinter
= nullptr);
265 * Helper function for ProofUF::toStreamRecLFSC and
266 * ProofArray::toStreamRecLFSC
268 * - evenLengthSequence: true iff the length of the sequence
269 * of the identical equalities is even.
270 * - sequenceOver: have we reached the last equality of this sequence?
271 * - pf: equality engine proof
272 * - map: A map for the let-expressions in the proof
273 * - subproofStr: current stringstream content
274 * - outStream: output stream to which the proof is printed
275 * - n: transitivity sub-proof
276 * - nodeAfterEqualitySequence: The node after the identical sequence.
278 * A pair of nodes, that are the updated nodes n and nodeAfterEqualitySequence
281 std::pair
<Node
, Node
> identicalEqualitiesPrinterHelper(
282 bool evenLengthSequence
,
284 const theory::eq::EqProof
& pf
,
285 const ProofLetMap
& map
,
286 const std::string subproofStr
,
287 std::stringstream
* outStream
,
289 Node nodeAfterEqualitySequence
);
292 * Print the proof representation of the given type that belongs to THIS theory.
297 virtual void printOwnedSort(Type type
, std::ostream
& os
) = 0;
299 * Print a proof for the theory lemmas. Must prove
300 * clause representing lemmas to be used in resolution proof.
302 * @param os output stream
304 virtual void printTheoryLemmaProof(std::vector
<Expr
>& lemma
,
307 const ProofLetMap
& map
);
309 * Print the sorts declarations for this theory.
314 virtual void printSortDeclarations(std::ostream
& os
, std::ostream
& paren
) = 0;
316 * Print the term declarations for this theory.
321 virtual void printTermDeclarations(std::ostream
& os
, std::ostream
& paren
) = 0;
323 * Print any deferred variable/sorts declarations for this theory
324 * (those that need to appear inside the actual proof).
329 virtual void printDeferredDeclarations(std::ostream
& os
, std::ostream
& paren
) = 0;
331 * Print any aliasing declarations.
336 virtual void printAliasingDeclarations(std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
&globalLetMap
) = 0;
338 * Register a term of this theory that appears in the proof.
342 virtual void registerTerm(Expr term
) = 0;
344 * Print a proof for the disequality of two constants that belong to this theory.
348 virtual void printConstantDisequalityProof(std::ostream
& os
, Expr c1
, Expr c2
, const ProofLetMap
&globalLetMap
);
350 * Print a proof for the equivalence of n1 and n2.
354 virtual void printRewriteProof(std::ostream
& os
, const Node
&n1
, const Node
&n2
);
356 // Return true if node prints as bool, false if it prints as a formula.
357 virtual bool printsAsBool(const Node
&n
) {
358 // Most nodes print as formulas, so this is the default.
363 class BooleanProof
: public TheoryProof
{
365 ExprSet d_declarations
; // all the boolean variables
366 theory::TheoryId
getTheoryId() override
;
369 BooleanProof(TheoryProofEngine
* proofEngine
);
371 void registerTerm(Expr term
) override
;
374 class LFSCBooleanProof
: public BooleanProof
{
376 LFSCBooleanProof(TheoryProofEngine
* proofEngine
)
377 : BooleanProof(proofEngine
)
379 void printOwnedTerm(Expr term
,
381 const ProofLetMap
& map
) override
;
382 void printOwnedSort(Type type
, std::ostream
& os
) override
;
383 void printTheoryLemmaProof(std::vector
<Expr
>& lemma
,
386 const ProofLetMap
& map
) override
;
387 void printSortDeclarations(std::ostream
& os
, std::ostream
& paren
) override
;
388 void printTermDeclarations(std::ostream
& os
, std::ostream
& paren
) override
;
389 void printDeferredDeclarations(std::ostream
& os
,
390 std::ostream
& paren
) override
;
391 void printAliasingDeclarations(std::ostream
& os
,
393 const ProofLetMap
& globalLetMap
) override
;
395 bool printsAsBool(const Node
& n
) override
;
396 void printConstantDisequalityProof(std::ostream
& os
,
399 const ProofLetMap
& globalLetMap
) override
;
402 } /* CVC4 namespace */
404 #endif /* __CVC4__THEORY_PROOF_H */