1 /********************* */ 2 /*! \file sat_proof.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Liana Hadarean, Tim King, Andres Noetzli 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 Resolution proof 13 ** 14 ** Resolution proof 15 **/ 16 17 #include "cvc4_private.h" 18 19 #ifndef __CVC4__SAT__PROOF_H 20 #define __CVC4__SAT__PROOF_H 21 22 #include <stdint.h> 23 24 #include <iosfwd> 25 #include <set> 26 #include <sstream> 27 #include <unordered_map> 28 #include <vector> 29 30 #include "context/cdhashmap.h" 31 #include "context/cdmaybe.h" 32 #include "expr/expr.h" 33 #include "proof/clause_id.h" 34 #include "proof/proof_manager.h" 35 #include "util/proof.h" 36 #include "util/statistics_registry.h" 37 38 // Forward declarations. 39 namespace CVC4 { 40 class CnfProof; 41 } /* namespace CVC4 */ 42 43 namespace CVC4 { 44 /** 45 * Helper debugging functions 46 */ 47 template <class Solver> 48 void printDebug(typename Solver::TLit l); 49 template <class Solver> 50 void printDebug(typename Solver::TClause& c); 51 52 enum ClauseKind { 53 INPUT, 54 THEORY_LEMMA, // we need to distinguish because we must reprove deleted 55 // theory lemmas 56 LEARNT 57 }; /* enum ClauseKind */ 58 59 template <class Solver> 60 struct ResStep { 61 typename Solver::TLit lit; 62 ClauseId id; 63 bool sign; ResStepResStep64 ResStep(typename Solver::TLit l, ClauseId i, bool s) 65 : lit(l), id(i), sign(s) {} 66 }; /* struct ResStep */ 67 68 template <class Solver> 69 class ResChain { 70 public: 71 typedef std::vector<ResStep<Solver> > ResSteps; 72 typedef std::set<typename Solver::TLit> LitSet; 73 74 ResChain(ClauseId start); 75 ~ResChain(); 76 77 void addStep(typename Solver::TLit, ClauseId, bool); redundantRemoved()78 bool redundantRemoved() { 79 return (d_redundantLits == NULL || d_redundantLits->empty()); 80 } 81 void addRedundantLit(typename Solver::TLit lit); 82 83 // accessor methods getStart()84 ClauseId getStart() const { return d_start; } getSteps()85 const ResSteps& getSteps() const { return d_steps; } getRedundant()86 LitSet* getRedundant() const { return d_redundantLits; } 87 88 private: 89 ClauseId d_start; 90 ResSteps d_steps; 91 LitSet* d_redundantLits; 92 }; /* class ResChain */ 93 94 template <class Solver> 95 class TSatProof { 96 protected: 97 typedef ResChain<Solver> ResolutionChain; 98 99 typedef std::set<typename Solver::TLit> LitSet; 100 typedef std::set<typename Solver::TVar> VarSet; 101 typedef std::unordered_map<ClauseId, typename Solver::TCRef> IdCRefMap; 102 typedef std::unordered_map<typename Solver::TCRef, ClauseId> ClauseIdMap; 103 typedef context::CDHashMap<ClauseId, typename Solver::TLit> IdUnitMap; 104 typedef context::CDHashMap<int, ClauseId> UnitIdMap; 105 typedef context::CDHashMap<ClauseId, ResolutionChain*> IdResMap; 106 typedef std::unordered_map<ClauseId, uint64_t> IdProofRuleMap; 107 typedef std::vector<ResolutionChain*> ResStack; 108 typedef std::set<ClauseId> IdSet; 109 typedef std::vector<typename Solver::TLit> LitVector; 110 typedef std::unordered_map<ClauseId, typename Solver::TClause&> 111 IdToMinisatClause; 112 typedef std::unordered_map<ClauseId, LitVector*> IdToConflicts; 113 114 public: 115 TSatProof(Solver* solver, context::Context* context, 116 const std::string& name, bool checkRes = false); 117 ~TSatProof(); 118 119 void startResChain(typename Solver::TLit start); 120 void startResChain(typename Solver::TCRef start); 121 void addResolutionStep(typename Solver::TLit lit, 122 typename Solver::TCRef clause, bool sign); 123 /** 124 * Pops the current resolution of the stack and stores it 125 * in the resolution map. Also registers the 'clause' parameter 126 * @param clause the clause the resolution is proving 127 */ 128 // void endResChain(typename Solver::TCRef clause); 129 void endResChain(typename Solver::TLit lit); 130 void endResChain(ClauseId id); 131 132 /** 133 * Pops the current resolution of the stack *without* storing it. 134 */ 135 void cancelResChain(); 136 137 /** 138 * Stores in the current derivation the redundant literals that were 139 * eliminated from the conflict clause during conflict clause minimization. 140 * @param lit the eliminated literal 141 */ 142 void storeLitRedundant(typename Solver::TLit lit); 143 144 /// update the CRef Id maps when Minisat does memory reallocation x 145 void updateCRef(typename Solver::TCRef old_ref, 146 typename Solver::TCRef new_ref); 147 void finishUpdateCRef(); 148 149 /** 150 * Constructs the empty clause resolution from the final conflict 151 * 152 * @param conflict 153 */ 154 void finalizeProof(typename Solver::TCRef conflict); 155 156 /// clause registration methods 157 158 ClauseId registerClause(const typename Solver::TCRef clause, ClauseKind kind); 159 ClauseId registerUnitClause(const typename Solver::TLit lit, ClauseKind kind); 160 void registerTrueLit(const typename Solver::TLit lit); 161 void registerFalseLit(const typename Solver::TLit lit); 162 163 ClauseId getTrueUnit() const; 164 ClauseId getFalseUnit() const; 165 166 void registerAssumption(const typename Solver::TVar var); 167 ClauseId registerAssumptionConflict(const typename Solver::TLitVec& confl); 168 169 ClauseId storeUnitConflict(typename Solver::TLit lit, ClauseKind kind); 170 171 /** 172 * Marks the deleted clauses as deleted. Note we may still use them in the 173 * final 174 * resolution. 175 * @param clause 176 */ 177 void markDeleted(typename Solver::TCRef clause); isDeleted(ClauseId id)178 bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); } 179 /** 180 * Constructs the resolution of ~q and resolves it with the current 181 * resolution thus eliminating q from the current clause 182 * @param q the literal to be resolved out 183 */ 184 void resolveOutUnit(typename Solver::TLit q); 185 /** 186 * Constructs the resolution of the literal lit. Called when a clause 187 * containing lit becomes satisfied and is removed. 188 * @param lit 189 */ 190 void storeUnitResolution(typename Solver::TLit lit); 191 192 /** 193 * Constructs the SAT proof for the given clause, 194 * by collecting the needed clauses in the d_seen 195 * data-structures, also notifying the proofmanager. 196 */ 197 void constructProof(ClauseId id); constructProof()198 void constructProof() { constructProof(d_emptyClauseId); } 199 void refreshProof(ClauseId id); refreshProof()200 void refreshProof() { refreshProof(d_emptyClauseId); } 201 bool proofConstructed() const; 202 void collectClauses(ClauseId id); 203 bool derivedEmptyClause() const; 204 prop::SatClause* buildClause(ClauseId id); 205 206 void collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas); 207 208 void storeClauseGlue(ClauseId clause, int glue); 209 210 bool isInputClause(ClauseId id) const; 211 bool isLemmaClause(ClauseId id) const; 212 bool isAssumptionConflict(ClauseId id) const; 213 214 bool hasResolutionChain(ClauseId id) const; 215 216 /** Returns the resolution chain associated with id. Assert fails if 217 * hasResolution(id) does not hold. */ 218 const ResolutionChain& getResolutionChain(ClauseId id) const; 219 getName()220 const std::string& getName() const { return d_name; } getEmptyClauseId()221 const ClauseId& getEmptyClauseId() const { return d_emptyClauseId; } getSeenLearnt()222 const IdSet& getSeenLearnt() const { return d_seenLearnt; } getAssumptionConflicts()223 const IdToConflicts& getAssumptionConflicts() const 224 { 225 return d_assumptionConflictsDebug; 226 } 227 228 private: 229 bool isUnit(ClauseId id) const; 230 typename Solver::TLit getUnit(ClauseId id) const; 231 232 bool isUnit(typename Solver::TLit lit) const; 233 ClauseId getUnitId(typename Solver::TLit lit) const; 234 235 void createLitSet(ClauseId id, LitSet& set); 236 237 /** 238 * Registers a ClauseId with a resolution chain res. 239 * Takes ownership of the memory associated with res. 240 */ 241 void registerResolution(ClauseId id, ResolutionChain* res); 242 243 244 bool hasClauseIdForCRef(typename Solver::TCRef clause) const; 245 ClauseId getClauseIdForCRef(typename Solver::TCRef clause) const; 246 247 bool hasClauseIdForLiteral(typename Solver::TLit lit) const; 248 ClauseId getClauseIdForLiteral(typename Solver::TLit lit) const; 249 250 bool hasClauseRef(ClauseId id) const; 251 typename Solver::TCRef getClauseRef(ClauseId id) const; 252 253 254 const typename Solver::TClause& getClause(typename Solver::TCRef ref) const; 255 256 void getLitVec(ClauseId id, LitVector& vec); 257 258 bool checkResolution(ClauseId id); 259 260 /** 261 * Constructs a resolution tree that proves lit 262 * and returns the ClauseId for the unit clause lit 263 * @param lit the literal we are proving 264 * 265 * @return 266 */ 267 ClauseId resolveUnit(typename Solver::TLit lit); 268 269 /** 270 * Does a depth first search on removed literals and adds the literals 271 * to be removed in the proper order to the stack. 272 * 273 * @param lit the literal we are recursing on 274 * @param removedSet the previously computed set of redundant literals 275 * @param removeStack the stack of literals in reverse order of resolution 276 */ 277 void removedDfs(typename Solver::TLit lit, LitSet* removedSet, 278 LitVector& removeStack, LitSet& inClause, LitSet& seen); 279 void removeRedundantFromRes(ResChain<Solver>* res, ClauseId id); 280 281 void print(ClauseId id) const; 282 void printRes(ClauseId id) const; 283 void printRes(const ResolutionChain& res) const; 284 285 std::unordered_map<ClauseId, int> d_glueMap; 286 struct Statistics { 287 IntStat d_numLearnedClauses; 288 IntStat d_numLearnedInProof; 289 IntStat d_numLemmasInProof; 290 AverageStat d_avgChainLength; 291 HistogramStat<uint64_t> d_resChainLengths; 292 HistogramStat<uint64_t> d_usedResChainLengths; 293 HistogramStat<uint64_t> d_clauseGlue; 294 HistogramStat<uint64_t> d_usedClauseGlue; 295 Statistics(const std::string& name); 296 ~Statistics(); 297 }; 298 299 std::string d_name; 300 301 const ClauseId d_emptyClauseId; 302 IdSet d_seenLearnt; 303 IdToConflicts d_assumptionConflictsDebug; 304 305 // Internal data. 306 Solver* d_solver; 307 context::Context* d_context; 308 309 // clauses 310 IdCRefMap d_idClause; 311 ClauseIdMap d_clauseId; 312 IdUnitMap d_idUnit; 313 UnitIdMap d_unitId; 314 IdHashSet d_deleted; 315 IdToSatClause d_deletedTheoryLemmas; 316 317 IdHashSet d_inputClauses; 318 IdHashSet d_lemmaClauses; 319 VarSet d_assumptions; // assumption literals for bv solver 320 IdHashSet d_assumptionConflicts; // assumption conflicts not actually added 321 // to SAT solver 322 323 // Resolutions. 324 325 /** 326 * Map from ClauseId to resolution chain corresponding proving the 327 * clause corresponding to the ClauseId. d_resolutionChains owns the 328 * memory of the ResChain* it contains. 329 */ 330 IdResMap d_resolutionChains; 331 332 /* 333 * Stack containting current ResChain* we are working on. d_resStack 334 * owns the memory for the ResChain* it contains. Invariant: no 335 * ResChain* pointer can be both in d_resStack and 336 * d_resolutionChains. Memory ownership is transfered from 337 * d_resStack to d_resolutionChains via registerResolution. 338 */ 339 ResStack d_resStack; 340 bool d_checkRes; 341 342 const ClauseId d_nullId; 343 344 // temporary map for updating CRefs 345 ClauseIdMap d_temp_clauseId; 346 IdCRefMap d_temp_idClause; 347 348 // unit conflict 349 context::CDMaybe<ClauseId> d_unitConflictId; 350 351 ClauseId d_trueLit; 352 ClauseId d_falseLit; 353 354 IdToSatClause d_seenInputs; 355 IdToSatClause d_seenLemmas; 356 357 bool d_satProofConstructed; 358 Statistics d_statistics; 359 }; /* class TSatProof */ 360 361 template <class Solver> 362 prop::SatLiteral toSatLiteral(typename Solver::TLit lit); 363 364 /** 365 * Convert from minisat clause to SatClause 366 * 367 * @param minisat_cl 368 * @param sat_cl 369 */ 370 template <class Solver> 371 void toSatClause(const typename Solver::TClause& minisat_cl, 372 prop::SatClause& sat_cl); 373 374 } /* CVC4 namespace */ 375 376 #endif /* __CVC4__SAT__PROOF_H */ 377