1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
/********************* */
/*! \file cnf_proof.cpp
** \verbatim
** Original author: Liana Hadarean
** Major contributors: Morgan Deters
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "proof/cnf_proof.h"
#include "proof/theory_proof.h"
#include "proof/proof_manager.h"
#include "prop/sat_solver_types.h"
#include "prop/minisat/minisat.h"
#include "prop/cnf_stream.h"
using namespace CVC4::prop;
namespace CVC4 {
CnfProof::CnfProof(CnfStream* stream)
: d_cnfStream(stream)
, d_theoryProof(NULL)
{}
TheoryProof* CnfProof::getTheoryProof() {
Assert (d_theoryProof);
return d_theoryProof;
}
void CnfProof::setTheoryProof(TheoryProof* theory_proof) {
Assert (d_theoryProof == NULL);
d_theoryProof = theory_proof;
}
void CnfProof::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) {
for (unsigned i = 0; i < clause->size(); ++i) {
SatLiteral lit = clause->operator[](i);
addVariable(lit.getSatVariable());
}
if (kind == INPUT) {
d_inputClauses.insert(std::make_pair(id, clause));
return;
}
Assert (kind == THEORY_LEMMA);
d_theoryLemmas.insert(std::make_pair(id, clause));
}
void CnfProof::addVariable(prop::SatVariable var) {
d_propVars.insert(var);
Expr atom = getAtom(var);
getTheoryProof()->addAtom(atom);
}
Expr CnfProof::getAtom(prop::SatVariable var) {
prop::SatLiteral lit (var);
Expr atom = d_cnfStream->getNode(lit).toExpr();
return atom;
}
CnfProof::~CnfProof() {
for (IdToClause::iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) {
delete it->second;
}
for (IdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) {
delete it->second;
}
}
void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) {
for (VarSet::iterator it = d_propVars.begin();it != d_propVars.end(); ++it) {
Expr atom = getAtom(*it);
os << "(decl_atom ";
getTheoryProof()->printFormula(atom, os);
os << " (\\ " << ProofManager::printVarName(*it) << " (\\ " << ProofManager::printAtomName(*it) << "\n";
paren << ")))";
}
}
void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) {
printInputClauses(os, paren);
printTheoryLemmas(os, paren);
}
void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
os << " ;; Input Clauses \n";
for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) {
ClauseId id = it->first;
const prop::SatClause* clause = it->second;
os << "(satlem _ _ ";
std::ostringstream clause_paren;
printClause(*clause, os, clause_paren);
os << " (clausify_false trust)" << clause_paren.str();
os << "( \\ " << ProofManager::printInputClauseName(id) << "\n";
paren << "))";
}
}
void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) {
os << " ;; Theory Lemmas \n";
for (IdToClause::const_iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) {
ClauseId id = it->first;
const prop::SatClause* clause = it->second;
os << "(satlem _ _ ";
std::ostringstream clause_paren;
printClause(*clause, os, clause_paren);
os << " (clausify_false trust)" << clause_paren.str();
os << "( \\ " << ProofManager::printLemmaClauseName(id) <<"\n";
paren << "))";
}
}
void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren) {
for (unsigned i = 0; i < clause.size(); ++i) {
prop::SatLiteral lit = clause[i];
prop::SatVariable var = lit.getSatVariable();
if (lit.isNegated()) {
os << "(ast _ _ _ " << ProofManager::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " ";
paren << "))";
} else {
os << "(asf _ _ _ " << ProofManager::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " ";
paren << "))";
}
}
}
} /* CVC4 namespace */
|
