1 /*********************                                                        */
2 /*! \file theory_proof.h
3  ** \verbatim
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-2019 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
11  **
12  ** [[ Add lengthier description here ]]
13 
14  ** \todo document this file
15 
16 **/
17 
18 #include "cvc4_private.h"
19 
20 #ifndef __CVC4__THEORY_PROOF_H
21 #define __CVC4__THEORY_PROOF_H
22 
23 #include <iosfwd>
24 #include <unordered_map>
25 #include <unordered_set>
26 
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"
33 namespace CVC4 {
34 
35 namespace theory {
36 class Theory;
37 } /* namespace CVC4::theory */
38 
39 typedef std::unordered_map < ClauseId, prop::SatClause* > IdToSatClause;
40 
41 class TheoryProof;
42 
43 typedef std::unordered_set<Expr, ExprHashFunction > ExprSet;
44 typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable;
45 
46 typedef std::set<theory::TheoryId> TheoryIdSet;
47 typedef std::map<Expr, TheoryIdSet> ExprToTheoryIds;
48 
49 class TheoryProofEngine {
50 protected:
51   ExprSet d_registrationCache;
52   TheoryProofTable d_theoryProofTable;
53   ExprToTheoryIds d_exprToTheoryIds;
54 
55   /**
56    * Returns whether the theory is currently supported in proof
57    * production mode.
58    */
59   bool supportedTheory(theory::TheoryId id);
60 public:
61 
62   TheoryProofEngine();
63   virtual ~TheoryProofEngine();
64 
65   /**
66    * Print the theory term (could be an atom) by delegating to the proper theory.
67    *
68    * @param term
69    * @param os
70    */
71   virtual void printLetTerm(Expr term, std::ostream& os) = 0;
72   virtual void printBoundTerm(Expr term, std::ostream& os,
73                               const ProofLetMap& map) = 0;
74 
75   /**
76    * Print the proof representation of the given sort.
77    *
78    * @param os
79    */
80   virtual void printSort(Type type, std::ostream& os) = 0;
81 
82   /**
83    * Go over the assertions and register all terms with the theories.
84    *
85    * @param os
86    * @param paren closing parenthesis
87    */
88   virtual void registerTermsFromAssertions() = 0;
89 
90   /**
91    * Print the theory assertions (arbitrary formulas over
92    * theory atoms)
93    *
94    * @param os
95    * @param paren closing parenthesis
96    */
97   virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0;
98   /**
99    * Print variable declarations that need to appear within the proof,
100    * e.g. skolemized variables.
101    *
102    * @param os
103    * @param paren closing parenthesis
104    */
105   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
106 
107   /**
108    * Print aliasing declarations.
109    *
110    * @param os
111    * @param paren closing parenthesis
112    */
113   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) = 0;
114 
115   /**
116    * Print proofs of all the theory lemmas (must prove
117    * actual clause used in resolution proof).
118    *
119    * @param os
120    * @param paren
121    */
122   virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os,
123                                  std::ostream& paren, ProofLetMap& map) = 0;
124 
125   /**
126    * Register theory atom (ensures all terms and atoms are declared).
127    *
128    * @param atom
129    */
130   void registerTerm(Expr atom);
131 
132   /**
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
135    * has been set.
136    *
137    * @param theory
138    */
139   void registerTheory(theory::Theory* theory);
140   /**
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.
143    *
144    * @param theory
145    */
146   void finishRegisterTheory(theory::Theory* theory);
147 
148   theory::TheoryId getTheoryForLemma(const prop::SatClause* clause);
149   TheoryProof* getTheoryProof(theory::TheoryId id);
150 
151   void markTermForFutureRegistration(Expr term, theory::TheoryId id);
152 
153   void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
154 
155   virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
156 
157   bool printsAsBool(const Node &n);
158 };
159 
160 class LFSCTheoryProofEngine : public TheoryProofEngine {
161   void bind(Expr term, ProofLetMap& map, Bindings& let_order);
162 public:
LFSCTheoryProofEngine()163   LFSCTheoryProofEngine()
164     : TheoryProofEngine() {}
165 
166   void printTheoryTerm(Expr term,
167                        std::ostream& os,
168                        const ProofLetMap& map) override;
169 
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,
176                       std::ostream& os,
177                       const ProofLetMap& map) override;
178   void printAssertions(std::ostream& os, std::ostream& paren) override;
179   void printLemmaRewrites(NodePairSet& rewrites,
180                           std::ostream& os,
181                           std::ostream& paren);
182   void printDeferredDeclarations(std::ostream& os,
183                                  std::ostream& paren) override;
184   void printAliasingDeclarations(std::ostream& os,
185                                  std::ostream& paren,
186                                  const ProofLetMap& globalLetMap) override;
187   void printTheoryLemmas(const IdToSatClause& lemmas,
188                          std::ostream& os,
189                          std::ostream& paren,
190                          ProofLetMap& map) override;
191   void printSort(Type type, std::ostream& os) override;
192 
193   void performExtraRegistrations();
194 
195   void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os);
196 
197 private:
198   static void dumpTheoryLemmas(const IdToSatClause& lemmas);
199 
200   // TODO: this function should be moved into the BV prover.
201 
202   std::map<Node, std::string> d_assertionToRewrite;
203 };
204 
205 class TheoryProof {
206 protected:
207   // Pointer to the theory for this proof
208   theory::Theory* d_theory;
209   TheoryProofEngine* d_proofEngine;
210   virtual theory::TheoryId getTheoryId() = 0;
211 
212  public:
TheoryProof(theory::Theory * th,TheoryProofEngine * proofEngine)213   TheoryProof(theory::Theory* th, TheoryProofEngine* proofEngine)
214     : d_theory(th)
215     , d_proofEngine(proofEngine)
216   {}
~TheoryProof()217   virtual ~TheoryProof() {};
218   /**
219    * Print a term belonging some theory, not necessarily this one.
220    *
221    * @param term expresion representing term
222    * @param os output stream
223    */
printTerm(Expr term,std::ostream & os,const ProofLetMap & map)224   void printTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
225     d_proofEngine->printBoundTerm(term, os, map);
226   }
227   /**
228    * Print a term belonging to THIS theory.
229    *
230    * @param term expression representing term
231    * @param os output stream
232    */
233   virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
234   /**
235    * Print the proof representation of the given type that belongs to some theory.
236    *
237    * @param type
238    * @param os
239    */
printSort(Type type,std::ostream & os)240   void printSort(Type type, std::ostream& os) {
241     d_proofEngine->printSort(type, os);
242   }
243 
244   // congrence matching term helper
245   bool match(TNode n1, TNode n2);
246 
247   /**
248    * Helper function for ProofUF::toStreamRecLFSC and
249    * ProofArray::toStreamRecLFSC
250    * Inputs:
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
255    * returns:
256    *    - the index of the contradicting node in pf.
257    *    */
258   int assertAndPrint(
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);
263 
264   /**
265    * Helper function for ProofUF::toStreamRecLFSC and
266    * ProofArray::toStreamRecLFSC
267    * Inputs:
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.
277    * Returns:
278    *    A pair of nodes, that are the updated nodes n and nodeAfterEqualitySequence
279    *
280    */
281   std::pair<Node, Node> identicalEqualitiesPrinterHelper(
282       bool evenLengthSequence,
283       bool sequenceOver,
284       const theory::eq::EqProof& pf,
285       const ProofLetMap& map,
286       const std::string subproofStr,
287       std::stringstream* outStream,
288       Node n,
289       Node nodeAfterEqualitySequence);
290 
291   /**
292    * Print the proof representation of the given type that belongs to THIS theory.
293    *
294    * @param type
295    * @param os
296    */
297   virtual void printOwnedSort(Type type, std::ostream& os) = 0;
298   /**
299    * Print a proof for the theory lemmas. Must prove
300    * clause representing lemmas to be used in resolution proof.
301    *
302    * @param os output stream
303    */
304   virtual void printTheoryLemmaProof(std::vector<Expr>& lemma,
305                                      std::ostream& os,
306                                      std::ostream& paren,
307                                      const ProofLetMap& map);
308   /**
309    * Print the sorts declarations for this theory.
310    *
311    * @param os
312    * @param paren
313    */
314   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0;
315   /**
316    * Print the term declarations for this theory.
317    *
318    * @param os
319    * @param paren
320    */
321   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0;
322   /**
323    * Print any deferred variable/sorts declarations for this theory
324    * (those that need to appear inside the actual proof).
325    *
326    * @param os
327    * @param paren
328    */
329   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
330   /**
331    * Print any aliasing declarations.
332    *
333    * @param os
334    * @param paren
335    */
336   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) = 0;
337   /**
338    * Register a term of this theory that appears in the proof.
339    *
340    * @param term
341    */
342   virtual void registerTerm(Expr term) = 0;
343   /**
344    * Print a proof for the disequality of two constants that belong to this theory.
345    *
346    * @param term
347    */
348   virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
349   /**
350    * Print a proof for the equivalence of n1 and n2.
351    *
352    * @param term
353    */
354   virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
355 
356   // Return true if node prints as bool, false if it prints as a formula.
printsAsBool(const Node & n)357   virtual bool printsAsBool(const Node &n) {
358     // Most nodes print as formulas, so this is the default.
359     return false;
360   }
361 };
362 
363 class BooleanProof : public TheoryProof {
364 protected:
365   ExprSet d_declarations; // all the boolean variables
366   theory::TheoryId getTheoryId() override;
367 
368  public:
369   BooleanProof(TheoryProofEngine* proofEngine);
370 
371   void registerTerm(Expr term) override;
372 };
373 
374 class LFSCBooleanProof : public BooleanProof {
375 public:
LFSCBooleanProof(TheoryProofEngine * proofEngine)376   LFSCBooleanProof(TheoryProofEngine* proofEngine)
377     : BooleanProof(proofEngine)
378   {}
379   void printOwnedTerm(Expr term,
380                       std::ostream& os,
381                       const ProofLetMap& map) override;
382   void printOwnedSort(Type type, std::ostream& os) override;
383   void printTheoryLemmaProof(std::vector<Expr>& lemma,
384                              std::ostream& os,
385                              std::ostream& paren,
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,
392                                  std::ostream& paren,
393                                  const ProofLetMap& globalLetMap) override;
394 
395   bool printsAsBool(const Node& n) override;
396   void printConstantDisequalityProof(std::ostream& os,
397                                      Expr c1,
398                                      Expr c2,
399                                      const ProofLetMap& globalLetMap) override;
400 };
401 
402 } /* CVC4 namespace */
403 
404 #endif /* __CVC4__THEORY_PROOF_H */
405