src/proof/cnf_proof.h

   1 /*********************                                                        */
   2 /*! \file cnf_proof.h
   3  ** \verbatim
   4  ** Original author: Liana Hadarean
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief A manager for CnfProofs.
  13  **
  14  ** A manager for CnfProofs.
  15  **
  16  **
  17  **/
  18
  19 #ifndef __CVC4__CNF_PROOF_H
  20 #define __CVC4__CNF_PROOF_H
  21
  22 #include "cvc4_private.h"
  23 #include "util/proof.h"
  24 #include "proof/sat_proof.h"
  25
  26 #include <ext/hash_set>
  27 #include <ext/hash_map>
  28 #include <iostream>
  29
  30 namespace CVC4 {
  31 namespace prop {
  32   class CnfStream;
  33 }
  34
  35 class CnfProof;
  36
  37 class AtomIterator {
  38   CnfProof& d_cnf;
  39   ProofManager::var_iterator d_it;
  40
  41 public:
  42   AtomIterator(CnfProof& cnf, const ProofManager::var_iterator& it)
  43     : d_cnf(cnf), d_it(it)
  44   {}
  45   inline Expr operator*();
  46   AtomIterator& operator++() { ++d_it; return *this; }
  47   AtomIterator operator++(int) { AtomIterator x = *this; ++d_it; return x; }
  48   bool operator==(const AtomIterator& it) const { return &d_cnf == &it.d_cnf && d_it == it.d_it; }
  49   bool operator!=(const AtomIterator& it) const { return !(*this == it); }
  50 };/* class AtomIterator */
  51
  52 class CnfProof {
  53 protected:
  54   CVC4::prop::CnfStream* d_cnfStream;
  55   Expr getAtom(prop::SatVariable var);
  56   friend class AtomIterator;
  57 public:
  58   CnfProof(CVC4::prop::CnfStream* cnfStream);
  59
  60   typedef AtomIterator iterator;
  61   virtual iterator begin_atom_mapping() = 0;
  62   virtual iterator end_atom_mapping() = 0;
  63
  64   virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0;
  65   virtual void printClauses(std::ostream& os, std::ostream& paren) = 0;
  66   virtual ~CnfProof();
  67 };
  68
  69 class LFSCCnfProof : public CnfProof {
  70   void printInputClauses(std::ostream& os, std::ostream& paren);
  71   void printTheoryLemmas(std::ostream& os, std::ostream& paren);
  72   void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren);
  73
  74 public:
  75   LFSCCnfProof(CVC4::prop::CnfStream* cnfStream)
  76     : CnfProof(cnfStream)
  77   {}
  78
  79   virtual iterator begin_atom_mapping();
  80   virtual iterator end_atom_mapping();
  81
  82   virtual void printAtomMapping(std::ostream& os, std::ostream& paren);
  83   virtual void printClauses(std::ostream& os, std::ostream& paren);
  84 };
  85
  86 inline Expr AtomIterator::operator*() {
  87   return d_cnf.getAtom(*d_it);
  88 }
  89
  90 } /* CVC4 namespace */
  91
  92 #endif /* __CVC4__CNF_PROOF_H */