src/proof/arith_proof.h

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