src/proof/theory_proof.h

   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-2018 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:
 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:
 213   TheoryProof(theory::Theory* th, TheoryProofEngine* proofEngine)
 214     : d_theory(th)
 215     , d_proofEngine(proofEngine)
 216   {}
 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    */
 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    */
 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.
 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:
 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 */