src/proof/proof_manager.h

   1 /*********************                                                        */
   2 /*! \file proof_manager.h
   3  ** \verbatim
   4  ** Original author: lianah
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief A manager for Proofs.
  15  **
  16  ** A manager for Proofs.
  17  **
  18  **
  19  **/
  20
  21 #ifndef __CVC4__PROOF_MANAGER_H
  22 #define __CVC4__PROOF_MANAGER_H
  23
  24 #include <iostream>
  25 #include "proof/proof.h"
  26
  27 // forward declarations
  28 namespace Minisat {
  29 class Solver;
  30 }
  31
  32 namespace CVC4 {
  33 namespace prop {
  34 class CnfStream;
  35 }
  36 class Proof;
  37 class SatProof;
  38 class CnfProof;
  39
  40 // different proof modes
  41 enum ProofFormat {
  42   LFSC,
  43   NATIVE
  44 };
  45
  46 class ProofManager {
  47   SatProof*   d_satProof;
  48   CnfProof*   d_cnfProof;
  49   ProofFormat d_format;
  50
  51   static ProofManager* proofManager;
  52   static bool isInitialized;
  53   ProofManager(ProofFormat format);
  54 public:
  55   static ProofManager* currentPM();
  56
  57   static void      initSatProof(Minisat::Solver* solver);
  58   static void      initCnfProof(CVC4::prop::CnfStream* cnfStream);
  59
  60   static Proof* getProof();
  61   static SatProof* getSatProof();
  62   static CnfProof* getCnfProof();
  63
  64 };
  65
  66 } /* CVC4 namespace*/
  67 #endif /* __CVC4__PROOF_MANAGER_H */