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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
/********************* */
/*! \file er_proof.h
** \verbatim
** Top contributors (to current version):
** Alex Ozdemir
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief ER Proof Format
**
** Declares C++ types that represent an ER/TRACECHECK proof.
** Defines serialization for these types.
**
** You can find details about the way ER is encoded in the TRACECHECK
** format at these locations:
** https://github.com/benjaminkiesl/drat2er
** http://www.cs.utexas.edu/users/marijn/publications/ijcar18.pdf
**
**/
#include "cvc4_private.h"
#ifndef __CVC4__PROOF__ER__ER_PROOF_H
#define __CVC4__PROOF__ER__ER_PROOF_H
#include <memory>
#include <vector>
#include "proof/clause_id.h"
#include "prop/sat_solver_types.h"
namespace CVC4 {
namespace proof {
namespace er {
using ClauseUseRecord = std::vector<std::pair<ClauseId, prop::SatClause>>;
/**
* A definition of the form:
* newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n)
*/
struct ErDefinition
{
ErDefinition(prop::SatVariable newVariable,
prop::SatLiteral oldLiteral,
std::vector<prop::SatLiteral>&& otherLiterals)
: d_newVariable(newVariable),
d_oldLiteral(oldLiteral),
d_otherLiterals(otherLiterals)
{
}
// newVar
prop::SatVariable d_newVariable;
// p
prop::SatLiteral d_oldLiteral;
// A list of the x_i's
std::vector<prop::SatLiteral> d_otherLiterals;
};
// For representing a clause's index within a TRACECHECK proof.
using TraceCheckIdx = size_t;
/**
* A single line in a TRACECHECK proof.
*
* Consists of the index of a new clause, the literals of that clause, and the
* indices for preceding clauses which can be combined in a resolution chain to
* produce this new clause.
*/
struct TraceCheckLine
{
TraceCheckLine(TraceCheckIdx idx,
std::vector<prop::SatLiteral>&& clause,
std::vector<TraceCheckIdx>&& chain)
: d_idx(idx), d_clause(clause), d_chain(chain)
{
}
// The index of the new clause
TraceCheckIdx d_idx;
// The new clause
std::vector<prop::SatLiteral> d_clause;
/**
* Indices of clauses which must be resolved to produce this new clause.
* While the TRACECHECK format does not specify the order, we require them to
* be in resolution-order.
*/
std::vector<TraceCheckIdx> d_chain;
};
/**
* A TRACECHECK proof -- just a list of lines
*/
struct TraceCheckProof
{
static TraceCheckProof fromText(std::istream& in);
TraceCheckProof() : d_lines() {}
// The lines of this proof.
std::vector<TraceCheckLine> d_lines;
};
/**
* An extended resolution proof.
* It supports resolution, along with extensions of the form
*
* newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n)
*/
class ErProof
{
public:
/**
* Construct an ER proof from a DRAT proof, using drat2er
*
* @param usedClauses The CNF formula that we're deriving bottom from.
* @param dratBinary The DRAT proof from the SAT solver, as a binary stream.
*/
static ErProof fromBinaryDratProof(const ClauseUseRecord& usedClauses,
const std::string& dratBinary);
/**
* Construct an ER proof from a TRACECHECK ER proof
*
* This basically just identifies groups of lines which correspond to
* definitions, and extracts them.
*
* @param usedClauses The CNF formula that we're deriving bottom from.
* @param tracecheck The TRACECHECK proof, as a stream.
*/
ErProof(const ClauseUseRecord& usedClauses, TraceCheckProof&& tracecheck);
/**
* Write the ER proof as an LFSC value of type (holds cln).
* The format is from the LFSC signature er.plf
*
* Reads the current `ProofManager` to determine what the variables should be
* named.
*
* @param os the stream to write to
*/
void outputAsLfsc(std::ostream& os) const;
const std::vector<ClauseId>& getInputClauseIds() const
{
return d_inputClauseIds;
}
const std::vector<ErDefinition>& getDefinitions() const
{
return d_definitions;
}
const TraceCheckProof& getTraceCheckProof() const { return d_tracecheck; }
private:
/**
* Creates an empty ErProof.
*/
ErProof() : d_inputClauseIds(), d_definitions(), d_tracecheck() {}
/**
* Computes the pivots on the basis of which an in-order resolution chain is
* resolved.
*
* c0 c1
* \ / Clauses c_i being resolved in a chain around
* v1 c2 pivots v_i.
* \ /
* v2 c3
* \ /
* v3 c4
* \ /
* v4
*
*
* @param chain the chain, of N clause indices
*
* @return a list of N - 1 variables, the list ( v_i ) from i = 1 to N - 1
*/
std::vector<prop::SatLiteral> computePivotsForChain(
const std::vector<TraceCheckIdx>& chain) const;
/**
* Write the LFSC identifier for the proof of a clause
*
* @param o where to write to
* @param i the TRACECHECK index for the clause whose proof identifier to
* print
*/
void writeIdForClauseProof(std::ostream& o, TraceCheckIdx i) const;
// A list of the Ids for the input clauses, in order.
std::vector<ClauseId> d_inputClauseIds;
// A list of new variable definitions, in order.
std::vector<ErDefinition> d_definitions;
// The underlying TRACECHECK proof.
TraceCheckProof d_tracecheck;
};
} // namespace er
} // namespace proof
} // namespace CVC4
#endif // __CVC4__PROOF__ER__ER_PROOF_H
|
