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