src/proof/proof_manager.h

   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-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
  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 "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"
  37
  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 class BitVectorProof;
  73
  74 template <class Solver> class LFSCSatProof;
  75 typedef LFSCSatProof< CVC4::Minisat::Solver> LFSCCoreSatProof;
  76
  77 class LFSCCnfProof;
  78 class LFSCTheoryProofEngine;
  79 class LFSCUFProof;
  80 class LFSCBitVectorProof;
  81 class LFSCRewriterProof;
  82
  83 template <class Solver> class ProofProxy;
  84 typedef ProofProxy< CVC4::Minisat::Solver> CoreProofProxy;
  85 typedef ProofProxy< CVC4::BVMinisat::Solver> BVProofProxy;
  86
  87 namespace prop {
  88   typedef uint64_t SatVariable;
  89   class SatLiteral;
  90   typedef std::vector<SatLiteral> SatClause;
  91 }/* CVC4::prop namespace */
  92
  93 // different proof modes
  94 enum ProofFormat {
  95   LFSC,
  96   NATIVE
  97 };/* enum ProofFormat */
  98
  99 std::string append(const std::string& str, uint64_t num);
 100
 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;
 106
 107 enum ProofRule {
 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*/
 116
 117   RULE_ARRAYS_EXT,  /* arrays, extensional */
 118   RULE_ARRAYS_ROW,  /* arrays, read-over-write */
 119 };/* enum ProofRules */
 120
 121 class RewriteLogEntry {
 122 public:
 123   RewriteLogEntry(unsigned ruleId, Node original, Node result)
 124     : d_ruleId(ruleId), d_original(original), d_result(result) {
 125   }
 126
 127   unsigned getRuleId() const {
 128     return d_ruleId;
 129   }
 130
 131   Node getOriginal() const {
 132     return d_original;
 133   }
 134
 135   Node getResult() const {
 136     return d_result;
 137   }
 138
 139 private:
 140   unsigned d_ruleId;
 141   Node d_original;
 142   Node d_result;
 143 };
 144
 145 class ProofManager {
 146   context::Context* d_context;
 147
 148   CoreSatProof*  d_satProof;
 149   CnfProof*      d_cnfProof;
 150   TheoryProofEngine* d_theoryProof;
 151
 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;
 157
 158   SkolemizationManager d_skolemizationManager;
 159
 160   int d_nextId;
 161
 162   std::unique_ptr<Proof> d_fullProof;
 163   ProofFormat d_format; // used for now only in debug builds
 164
 165   CDNodeToNodes d_deps;
 166
 167   std::set<Type> d_printedTypes;
 168
 169   std::map<std::string, std::string> d_rewriteFilters;
 170   std::map<Node, std::string> d_assertionFilters;
 171
 172   std::vector<RewriteLogEntry> d_rewriteLog;
 173
 174 protected:
 175   LogicInfo d_logic;
 176
 177 public:
 178   ProofManager(context::Context* context, ProofFormat format = LFSC);
 179   ~ProofManager();
 180
 181   static ProofManager* currentPM();
 182
 183   // initialization
 184   void         initSatProof(Minisat::Solver* solver);
 185   static void         initCnfProof(CVC4::prop::CnfStream* cnfStream,
 186                                    context::Context* ctx);
 187   static void         initTheoryProofEngine();
 188
 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();
 199
 200   static SkolemizationManager *getSkolemizationManager();
 201
 202   // iterators over data shared by proofs
 203   typedef ExprSet::const_iterator assertions_iterator;
 204
 205   // iterate over the assertions (these are arbitrary boolean formulas)
 206   assertions_iterator begin_assertions() const {
 207     return d_inputFormulas.begin();
 208   }
 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();
 213   }
 214
 215   void ensureLiteral(Node node);
 216
 217 //---from Morgan---
 218   Node mkOp(TNode n);
 219   Node lookupOp(TNode n) const;
 220   bool hasOp(TNode n) const;
 221
 222   std::map<Node, Node> d_ops;
 223   std::map<Node, Node> d_bops;
 224 //---end from Morgan---
 225
 226
 227   // variable prefixes
 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);
 235
 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);
 242
 243   // for SMT variable names that have spaces and other things
 244   static std::string sanitize(TNode var);
 245
 246   /** Add proof assertion - unlike addCoreAssertion this is post definition expansion **/
 247   void addAssertion(Expr formula);
 248
 249   /** Public unsat core methods **/
 250   void addCoreAssertion(Expr formula);
 251
 252   void addDependence(TNode n, TNode dep);
 253   void addUnsatCore(Expr formula);
 254
 255   // trace dependences back to unsat core
 256   void traceDeps(TNode n, ExprSet* coreAssertions);
 257   void traceDeps(TNode n, CDExprSet* coreAssertions);
 258   void traceUnsatCore();
 259
 260   typedef CDExprSet::const_iterator output_core_iterator;
 261
 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();
 266
 267   bool unsatCoreAvailable() const;
 268   void getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas);
 269   Node getWeakestImplicantInUnsatCore(Node lemma);
 270
 271   int nextId() { return d_nextId++; }
 272
 273   void setLogic(const LogicInfo& logic);
 274   const std::string getLogic() const { return d_logic.getLogicString(); }
 275   LogicInfo & getLogicInfo() { return d_logic; }
 276
 277   void markPrinted(const Type& type);
 278   bool wasPrinted(const Type& type) const;
 279
 280   void addRewriteFilter(const std::string &original, const std::string &substitute);
 281   void clearRewriteFilters();
 282   bool haveRewriteFilter(TNode lit);
 283
 284   void addAssertionFilter(const Node& node, const std::string& rewritten);
 285
 286   static void registerRewrite(unsigned ruleId, Node original, Node result);
 287   static void clearRewriteLog();
 288
 289   std::vector<RewriteLogEntry> getRewriteLog();
 290   void dumpRewriteLog() const;
 291
 292   void printGlobalLetMap(std::set<Node>& atoms,
 293                          ProofLetMap& letMap,
 294                          std::ostream& out,
 295                          std::ostringstream& paren);
 296
 297 private:
 298   void constructSatProof();
 299   std::set<Node> satClauseToNodeSet(prop::SatClause* clause);
 300 };/* class ProofManager */
 301
 302 class LFSCProof : public Proof
 303 {
 304  public:
 305   LFSCProof(SmtEngine* smtEngine,
 306             LFSCCoreSatProof* sat,
 307             LFSCCnfProof* cnf,
 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;
 312
 313  private:
 314   // FIXME: hack until we get preprocessing
 315   void printPreprocessedAssertions(const NodeSet& assertions,
 316                                    std::ostream& os,
 317                                    std::ostream& paren,
 318                                    ProofLetMap& globalLetMap) const;
 319
 320   void checkUnrewrittenAssertion(const NodeSet& assertions) const;
 321
 322   LFSCCoreSatProof* d_satProof;
 323   LFSCCnfProof* d_cnfProof;
 324   LFSCTheoryProofEngine* d_theoryProof;
 325   SmtEngine* d_smtEngine;
 326 }; /* class LFSCProof */
 327
 328 std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k);
 329 }/* CVC4 namespace */
 330
 331
 332
 333 #endif /* __CVC4__PROOF_MANAGER_H */