src/proof/cnf_proof.cpp

   1 /*********************                                                        */
   2 /*! \file cnf_proof.cpp
   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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "proof/cnf_proof.h"
  19 #include "proof/theory_proof.h"
  20 #include "proof/proof_manager.h"
  21 #include "prop/sat_solver_types.h"
  22 #include "prop/minisat/minisat.h"
  23 #include "prop/cnf_stream.h"
  24
  25 using namespace CVC4::prop;
  26
  27 namespace CVC4 {
  28
  29 CnfProof::CnfProof(CnfStream* stream)
  30   : d_cnfStream(stream)
  31 {}
  32
  33
  34 Expr CnfProof::getAtom(prop::SatVariable var) {
  35   prop::SatLiteral lit (var);
  36   Node node = d_cnfStream->getNode(lit);
  37   Expr atom = node.toExpr();
  38   return atom;
  39 }
  40
  41 CnfProof::~CnfProof() {
  42 }
  43
  44 LFSCCnfProof::iterator LFSCCnfProof::begin_atom_mapping() {
  45   return iterator(*this, ProofManager::currentPM()->begin_vars());
  46 }
  47
  48 LFSCCnfProof::iterator LFSCCnfProof::end_atom_mapping() {
  49   return iterator(*this, ProofManager::currentPM()->end_vars());
  50 }
  51
  52 void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) {
  53   ProofManager::var_iterator it = ProofManager::currentPM()->begin_vars();
  54   ProofManager::var_iterator end = ProofManager::currentPM()->end_vars();
  55
  56   for (;it != end;  ++it) {
  57     os << "(decl_atom ";
  58
  59     if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) {
  60       Expr atom = getAtom(*it);
  61       LFSCTheoryProof::printTerm(atom, os);
  62     } else {
  63       // print fake atoms for all other logics
  64       os << "true ";
  65     }
  66
  67     os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n";
  68     paren << ")))";
  69   }
  70 }
  71
  72 void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) {
  73   printInputClauses(os, paren);
  74   printTheoryLemmas(os, paren);
  75 }
  76
  77 void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
  78   os << " ;; Input Clauses \n";
  79   ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses();
  80   ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses();
  81
  82   for (; it != end; ++it) {
  83     ClauseId id = it->first;
  84     const prop::SatClause* clause = it->second;
  85     os << "(satlem _ _ ";
  86     std::ostringstream clause_paren;
  87     printClause(*clause, os, clause_paren);
  88     os << " (clausify_false trust)" << clause_paren.str();
  89     os << "( \\ " << ProofManager::getInputClauseName(id) << "\n";
  90     paren << "))";
  91   }
  92 }
  93
  94
  95 void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) {
  96   os << " ;; Theory Lemmas \n";
  97   ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas();
  98   ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas();
  99
 100   for (; it != end; ++it) {
 101     ClauseId id = it->first;
 102     const prop::SatClause* clause = it->second;
 103     os << "(satlem _ _ ";
 104     std::ostringstream clause_paren;
 105     printClause(*clause, os, clause_paren);
 106     os << " (clausify_false trust)" << clause_paren.str();
 107     os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n";
 108     paren << "))";
 109   }
 110 }
 111
 112 void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren) {
 113   for (unsigned i = 0; i < clause.size(); ++i) {
 114     prop::SatLiteral lit = clause[i];
 115     prop::SatVariable var = lit.getSatVariable();
 116     if (lit.isNegated()) {
 117       os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
 118       paren << "))";
 119     } else {
 120       os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
 121       paren << "))";
 122     }
 123   }
 124 }
 125
 126 } /* CVC4 namespace */