src/proof/uf_proof.h

   1 /*********************                                                        */
   2 /*! \file uf_proof.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Mathias Preiner, Tim King
   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  ** \brief UF proof
  13  **
  14  ** UF proof
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__UF__PROOF_H
  20 #define __CVC4__UF__PROOF_H
  21
  22 #include <memory>
  23 #include <unordered_set>
  24
  25 #include "expr/expr.h"
  26 #include "proof/theory_proof.h"
  27 #include "theory/uf/equality_engine.h"
  28 #include "util/proof.h"
  29
  30 namespace CVC4 {
  31
  32 // proof object outputted by TheoryUF
  33 class ProofUF : public Proof
  34 {
  35  public:
  36   ProofUF(std::shared_ptr<theory::eq::EqProof> pf) : d_proof(pf) {}
  37   void toStream(std::ostream& out) const override;
  38   void toStream(std::ostream& out, const ProofLetMap& map) const override;
  39
  40  private:
  41   static void toStreamLFSC(std::ostream& out, TheoryProof* tp,
  42                            const theory::eq::EqProof& pf,
  43                            const ProofLetMap& map);
  44   static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
  45                               const theory::eq::EqProof& pf, unsigned tb,
  46                               const ProofLetMap& map);
  47
  48   // it is simply an equality engine proof
  49   std::shared_ptr<theory::eq::EqProof> d_proof;
  50 };
  51
  52 namespace theory {
  53 namespace uf {
  54 class TheoryUF;
  55 }
  56 }
  57
  58 typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
  59
  60
  61 class UFProof : public TheoryProof {
  62 protected:
  63   TypeSet d_sorts;        // all the uninterpreted sorts in this theory
  64   ExprSet d_declarations; // all the variable/function declarations
  65   theory::TheoryId getTheoryId() override;
  66
  67  public:
  68   UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine);
  69
  70   void registerTerm(Expr term) override;
  71 };
  72
  73 class LFSCUFProof : public UFProof {
  74 public:
  75   LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine)
  76     : UFProof(uf, proofEngine)
  77   {}
  78   void printOwnedTerm(Expr term,
  79                       std::ostream& os,
  80                       const ProofLetMap& map) override;
  81   void printOwnedSort(Type type, std::ostream& os) override;
  82   void printTheoryLemmaProof(std::vector<Expr>& lemma,
  83                              std::ostream& os,
  84                              std::ostream& paren,
  85                              const ProofLetMap& map) override;
  86   void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
  87   void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
  88   void printDeferredDeclarations(std::ostream& os,
  89                                  std::ostream& paren) override;
  90   void printAliasingDeclarations(std::ostream& os,
  91                                  std::ostream& paren,
  92                                  const ProofLetMap& globalLetMap) override;
  93
  94   bool printsAsBool(const Node& n) override;
  95
  96   void printConstantDisequalityProof(std::ostream& os,
  97                                      Expr c1,
  98                                      Expr c2,
  99                                      const ProofLetMap& globalLetMap) override;
 100 };
 101
 102
 103 }/* CVC4 namespace */
 104
 105 #endif /* __CVC4__UF__PROOF_H */