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) override;
  37  private:
  38   static void toStreamLFSC(std::ostream& out, TheoryProof* tp,
  39                            const theory::eq::EqProof& pf,
  40                            const ProofLetMap& map);
  41   static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
  42                               const theory::eq::EqProof& pf,
  43                               unsigned tb, const ProofLetMap& map);
  44   // it is simply an equality engine proof
  45   std::shared_ptr<theory::eq::EqProof> d_proof;
  46 };
  47
  48 namespace theory {
  49 namespace arith {
  50 class TheoryArith;
  51 }
  52 }
  53
  54 typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
  55
  56
  57 class ArithProof : public TheoryProof {
  58 protected:
  59   // std::map<Expr, std::string> d_constRationalString; // all the variable/function declarations
  60
  61   //   TypeSet d_sorts;        // all the uninterpreted sorts in this theory
  62   ExprSet d_declarations; // all the variable/function declarations
  63
  64   bool d_realMode;
  65
  66 public:
  67   ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine);
  68
  69   virtual void registerTerm(Expr term);
  70 };
  71
  72 class LFSCArithProof : public ArithProof {
  73 public:
  74   LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine)
  75     : ArithProof(arith, proofEngine)
  76   {}
  77   virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
  78   virtual void printOwnedSort(Type type, std::ostream& os);
  79   virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
  80   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
  81   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
  82   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
  83   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
  84 };
  85
  86
  87 }/* CVC4 namespace */
  88
  89 #endif /* __CVC4__ARITH__PROOF_H */