src/proof/proof_manager.h

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