1 /*********************                                                        */
2 /*! \file proof_manager.h
3  ** \verbatim
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-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  ** \brief A manager for Proofs
13  **
14  ** A manager for Proofs.
15  **/
16 
17 #include "cvc4_private.h"
18 
19 #ifndef __CVC4__PROOF_MANAGER_H
20 #define __CVC4__PROOF_MANAGER_H
21 
22 #include <iosfwd>
23 #include <memory>
24 #include <unordered_map>
25 #include <unordered_set>
26 
27 #include "context/cdhashmap.h"
28 #include "context/cdhashset.h"
29 #include "expr/node.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"
37 #include "util/statistics_registry.h"
38 
39 namespace CVC4 {
40 
41 class SmtGlobals;
42 
43 // forward declarations
44 namespace Minisat {
45   class Solver;
46 }/* Minisat namespace */
47 
48 namespace BVMinisat {
49   class Solver;
50 }/* BVMinisat namespace */
51 
52 namespace prop {
53   class CnfStream;
54 }/* CVC4::prop namespace */
55 
56 class SmtEngine;
57 
58 const ClauseId ClauseIdEmpty(-1);
59 const ClauseId ClauseIdUndef(-2);
60 const ClauseId ClauseIdError(-3);
61 
62 template <class Solver> class TSatProof;
63 typedef TSatProof< CVC4::Minisat::Solver> CoreSatProof;
64 
65 class CnfProof;
66 class RewriterProof;
67 class TheoryProofEngine;
68 class TheoryProof;
69 class UFProof;
70 class ArithProof;
71 class ArrayProof;
72 
73 namespace proof {
74 class ResolutionBitVectorProof;
75 }
76 
77 template <class Solver> class LFSCSatProof;
78 typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof;
79 
80 class LFSCCnfProof;
81 class LFSCTheoryProofEngine;
82 class LFSCUFProof;
83 class LFSCRewriterProof;
84 
85 namespace prop {
86   typedef uint64_t SatVariable;
87   class SatLiteral;
88   typedef std::vector<SatLiteral> SatClause;
89 }/* CVC4::prop namespace */
90 
91 // different proof modes
92 enum ProofFormat {
93   LFSC,
94   NATIVE
95 };/* enum ProofFormat */
96 
97 std::string append(const std::string& str, uint64_t num);
98 
99 typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause;
100 typedef context::CDHashSet<Expr, ExprHashFunction> CDExprSet;
101 typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeToNodes;
102 typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction> CDNodeToNodes;
103 typedef std::unordered_set<ClauseId> IdHashSet;
104 
105 enum ProofRule {
106   RULE_GIVEN,       /* input assertion */
107   RULE_DERIVED,     /* a "macro" rule */
108   RULE_RECONSTRUCT, /* prove equivalence using another method */
109   RULE_TRUST,       /* trust without evidence (escape hatch until proofs are fully supported) */
110   RULE_INVALID,     /* assert-fail if this is ever needed in proof; use e.g. for split lemmas */
111   RULE_CONFLICT,    /* re-construct as a conflict */
112   RULE_TSEITIN,     /* Tseitin CNF transformation */
113   RULE_SPLIT,       /* A splitting lemma of the form a v ~ a*/
114 
115   RULE_ARRAYS_EXT,  /* arrays, extensional */
116   RULE_ARRAYS_ROW,  /* arrays, read-over-write */
117 };/* enum ProofRules */
118 
119 class RewriteLogEntry {
120 public:
RewriteLogEntry(unsigned ruleId,Node original,Node result)121   RewriteLogEntry(unsigned ruleId, Node original, Node result)
122     : d_ruleId(ruleId), d_original(original), d_result(result) {
123   }
124 
getRuleId()125   unsigned getRuleId() const {
126     return d_ruleId;
127   }
128 
getOriginal()129   Node getOriginal() const {
130     return d_original;
131   }
132 
getResult()133   Node getResult() const {
134     return d_result;
135   }
136 
137 private:
138   unsigned d_ruleId;
139   Node d_original;
140   Node d_result;
141 };
142 
143 class ProofManager {
144   context::Context* d_context;
145 
146   CoreSatProof*  d_satProof;
147   CnfProof*      d_cnfProof;
148   TheoryProofEngine* d_theoryProof;
149 
150   // information that will need to be shared across proofs
151   ExprSet    d_inputFormulas;
152   std::map<Expr, std::string> d_inputFormulaToName;
153   CDExprSet    d_inputCoreFormulas;
154   CDExprSet    d_outputCoreFormulas;
155 
156   SkolemizationManager d_skolemizationManager;
157 
158   int d_nextId;
159 
160   std::unique_ptr<Proof> d_fullProof;
161   ProofFormat d_format; // used for now only in debug builds
162 
163   CDNodeToNodes d_deps;
164 
165   std::set<Type> d_printedTypes;
166 
167   std::map<std::string, std::string> d_rewriteFilters;
168   std::map<Node, std::string> d_assertionFilters;
169 
170   std::vector<RewriteLogEntry> d_rewriteLog;
171 
172 protected:
173   LogicInfo d_logic;
174 
175 public:
176   ProofManager(context::Context* context, ProofFormat format = LFSC);
177   ~ProofManager();
178 
179   static ProofManager* currentPM();
180 
181   // initialization
182   void         initSatProof(Minisat::Solver* solver);
183   static void         initCnfProof(CVC4::prop::CnfStream* cnfStream,
184                                    context::Context* ctx);
185   static void         initTheoryProofEngine();
186 
187   // getting various proofs
188   static const Proof& getProof(SmtEngine* smt);
189   static CoreSatProof*  getSatProof();
190   static CnfProof*      getCnfProof();
191   static TheoryProofEngine* getTheoryProofEngine();
192   static TheoryProof* getTheoryProof( theory::TheoryId id );
193   static UFProof* getUfProof();
194   static proof::ResolutionBitVectorProof* getBitVectorProof();
195   static ArrayProof* getArrayProof();
196   static ArithProof* getArithProof();
197 
198   static SkolemizationManager *getSkolemizationManager();
199 
200   // iterators over data shared by proofs
201   typedef ExprSet::const_iterator assertions_iterator;
202 
203   // iterate over the assertions (these are arbitrary boolean formulas)
begin_assertions()204   assertions_iterator begin_assertions() const {
205     return d_inputFormulas.begin();
206   }
end_assertions()207   assertions_iterator end_assertions() const { return d_inputFormulas.end(); }
num_assertions()208   size_t num_assertions() const { return d_inputFormulas.size(); }
have_input_assertion(const Expr & assertion)209   bool have_input_assertion(const Expr& assertion) {
210     return d_inputFormulas.find(assertion) != d_inputFormulas.end();
211   }
212 
213   void ensureLiteral(Node node);
214 
215 //---from Morgan---
216   Node mkOp(TNode n);
217   Node lookupOp(TNode n) const;
218   bool hasOp(TNode n) const;
219 
220   std::map<Node, Node> d_ops;
221   std::map<Node, Node> d_bops;
222 //---end from Morgan---
223 
224 
225   // variable prefixes
226   static std::string getInputClauseName(ClauseId id, const std::string& prefix = "");
227   static std::string getLemmaClauseName(ClauseId id, const std::string& prefix = "");
228   static std::string getLemmaName(ClauseId id, const std::string& prefix = "");
229   static std::string getLearntClauseName(ClauseId id, const std::string& prefix = "");
230   static std::string getPreprocessedAssertionName(Node node, const std::string& prefix = "");
231   static std::string getAssertionName(Node node, const std::string& prefix = "");
232   static std::string getInputFormulaName(const Expr& expr);
233 
234   static std::string getVarName(prop::SatVariable var, const std::string& prefix = "");
235   static std::string getAtomName(prop::SatVariable var, const std::string& prefix = "");
236   static std::string getAtomName(TNode atom, const std::string& prefix = "");
237   static std::string getLitName(prop::SatLiteral lit, const std::string& prefix = "");
238   static std::string getLitName(TNode lit, const std::string& prefix = "");
239   static bool hasLitName(TNode lit);
240 
241   // for SMT variable names that have spaces and other things
242   static std::string sanitize(TNode var);
243 
244   // wrap term with (p_app ... ) if the term is printed as a boolean, and print
245   // used for "trust" assertions
246   static void printTrustedTerm(Node term,
247                                std::ostream& os,
248                                ProofLetMap& globalLetMap);
249 
250   /** Add proof assertion - unlike addCoreAssertion this is post definition expansion **/
251   void addAssertion(Expr formula);
252 
253   /** Public unsat core methods **/
254   void addCoreAssertion(Expr formula);
255 
256   void addDependence(TNode n, TNode dep);
257   void addUnsatCore(Expr formula);
258 
259   // trace dependences back to unsat core
260   void traceDeps(TNode n, ExprSet* coreAssertions);
261   void traceDeps(TNode n, CDExprSet* coreAssertions);
262   void traceUnsatCore();
263 
264   typedef CDExprSet::const_iterator output_core_iterator;
265 
begin_unsat_core()266   output_core_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); }
end_unsat_core()267   output_core_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
size_unsat_core()268   size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
269   std::vector<Expr> extractUnsatCore();
270 
271   bool unsatCoreAvailable() const;
272   void getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas);
273   Node getWeakestImplicantInUnsatCore(Node lemma);
274 
nextId()275   int nextId() { return d_nextId++; }
276 
277   void setLogic(const LogicInfo& logic);
getLogic()278   const std::string getLogic() const { return d_logic.getLogicString(); }
getLogicInfo()279   LogicInfo & getLogicInfo() { return d_logic; }
280 
281   void markPrinted(const Type& type);
282   bool wasPrinted(const Type& type) const;
283 
284   void addRewriteFilter(const std::string &original, const std::string &substitute);
285   void clearRewriteFilters();
286   bool haveRewriteFilter(TNode lit);
287 
288   void addAssertionFilter(const Node& node, const std::string& rewritten);
289 
290   static void registerRewrite(unsigned ruleId, Node original, Node result);
291   static void clearRewriteLog();
292 
293   std::vector<RewriteLogEntry> getRewriteLog();
294   void dumpRewriteLog() const;
295 
296   void printGlobalLetMap(std::set<Node>& atoms,
297                          ProofLetMap& letMap,
298                          std::ostream& out,
299                          std::ostringstream& paren);
300 
getProofProductionTime()301   TimerStat* getProofProductionTime() { return &d_stats.d_proofProductionTime; }
302 
303  private:
304   void constructSatProof();
305   std::set<Node> satClauseToNodeSet(prop::SatClause* clause);
306 
307   struct ProofManagerStatistics
308   {
309     ProofManagerStatistics();
310     ~ProofManagerStatistics();
311 
312     /**
313      * Time spent producing proofs (i.e. generating the proof from the logging
314      * information)
315      */
316     TimerStat d_proofProductionTime;
317   }; /* struct ProofManagerStatistics */
318 
319   ProofManagerStatistics d_stats;
320 
321 };/* class ProofManager */
322 
323 class LFSCProof : public Proof
324 {
325  public:
326   LFSCProof(SmtEngine* smtEngine,
327             CoreSatProof* sat,
328             LFSCCnfProof* cnf,
329             LFSCTheoryProofEngine* theory);
~LFSCProof()330   ~LFSCProof() override {}
331   void toStream(std::ostream& out) const override;
332   void toStream(std::ostream& out, const ProofLetMap& map) const override;
333 
334  private:
335   // FIXME: hack until we get preprocessing
336   void printPreprocessedAssertions(const NodeSet& assertions,
337                                    std::ostream& os,
338                                    std::ostream& paren,
339                                    ProofLetMap& globalLetMap) const;
340 
341   void checkUnrewrittenAssertion(const NodeSet& assertions) const;
342 
343   CoreSatProof* d_satProof;
344   LFSCCnfProof* d_cnfProof;
345   LFSCTheoryProofEngine* d_theoryProof;
346   SmtEngine* d_smtEngine;
347 }; /* class LFSCProof */
348 
349 std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k);
350 }/* CVC4 namespace */
351 
352 
353 
354 #endif /* __CVC4__PROOF_MANAGER_H */
355