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