src/proof/lemma_proof.h

   1 /*********************                                                        */
   2 /*! \file lemma_proof.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Guy Katz
   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  ** A class for recoding the steps required in order to prove a theory lemma.
  13
  14 **/
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef __CVC4__LEMMA_PROOF_H
  19 #define __CVC4__LEMMA_PROOF_H
  20
  21 #include "expr/expr.h"
  22 #include "proof/clause_id.h"
  23 #include "prop/sat_solver_types.h"
  24 #include "util/proof.h"
  25 #include "expr/node.h"
  26
  27 namespace CVC4 {
  28
  29 class LemmaProofRecipe {
  30 public:
  31   class ProofStep {
  32   public:
  33     ProofStep(theory::TheoryId theory, Node literalToProve);
  34     theory::TheoryId getTheory() const;
  35     Node getLiteral() const;
  36     void addAssertion(const Node& assertion);
  37     std::set<Node> getAssertions() const;
  38
  39   private:
  40     theory::TheoryId d_theory;
  41     Node d_literalToProve;
  42     std::set<Node> d_assertions;
  43   };
  44
  45   //* The lemma assertions and owner */
  46   void addBaseAssertion(Node baseAssertion);
  47   std::set<Node> getBaseAssertions() const;
  48   theory::TheoryId getTheory() const;
  49
  50   //* Rewrite rules */
  51   typedef std::map<Node, Node>::const_iterator RewriteIterator;
  52   RewriteIterator rewriteBegin() const;
  53   RewriteIterator rewriteEnd() const;
  54
  55   void addRewriteRule(Node assertion, Node explanation);
  56   bool wasRewritten(Node assertion) const;
  57   Node getExplanation(Node assertion) const;
  58
  59   //* Original lemma */
  60   void setOriginalLemma(Node lemma);
  61   Node getOriginalLemma() const;
  62
  63   //* Proof Steps */
  64   void addStep(ProofStep& proofStep);
  65   const ProofStep* getStep(unsigned index) const;
  66   ProofStep* getStep(unsigned index);
  67   unsigned getNumSteps() const;
  68   std::set<Node> getMissingAssertionsForStep(unsigned index) const;
  69   bool simpleLemma() const;
  70   bool compositeLemma() const;
  71
  72   void dump(const char *tag) const;
  73   bool operator<(const LemmaProofRecipe& other) const;
  74
  75 private:
  76   //* The list of assertions for this lemma */
  77   std::set<Node> d_baseAssertions;
  78
  79   //* The various steps needed to derive the empty clause */
  80   std::list<ProofStep> d_proofSteps;
  81
  82   //* A map from assertions to their rewritten explanations (toAssert --> toExplain) */
  83   std::map<Node, Node> d_assertionToExplanation;
  84
  85   //* The original lemma, as asserted by the owner theory solver */
  86   Node d_originalLemma;
  87 };
  88
  89 } /* CVC4 namespace */
  90
  91 #endif /* __CVC4__LEMMA_PROOF_H */