blob: 4715b38f4e5d3e4305669dea47fe0cae961ea1f9 (
plain)
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
|
/********************* */
/*! \file drat_proof.h
** \verbatim
** Top contributors (to current version):
** Alex Ozdemir
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 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 DRAT Proof Format
**
** Declares C++ types that represent a DRAT proof.
** Defines serialization for these types.
**
** You can find an introduction to DRAT in the drat-trim paper:
** http://www.cs.utexas.edu/~marijn/publications/drat-trim.pdf
**
**/
#ifndef __CVC4__PROOF__DRAT__DRAT_PROOF_H
#define __CVC4__PROOF__DRAT__DRAT_PROOF_H
#include "cvc4_private.h"
#include "prop/sat_solver.h"
#include "prop/sat_solver_types.h"
namespace CVC4 {
namespace proof {
namespace drat {
using CVC4::prop::SatClause;
using CVC4::prop::SatLiteral;
using CVC4::prop::SatVariable;
class CVC4_PUBLIC InvalidDratProofException : public CVC4::Exception
{
public:
InvalidDratProofException() : Exception("Invalid DRAT Proof") {}
InvalidDratProofException(const std::string& msg) : Exception(msg) {}
InvalidDratProofException(const char* msg) : Exception(msg) {}
}; /* class InvalidDratProofException */
enum DratInstructionKind
{
ADDITION,
DELETION
};
struct DratInstruction
{
DratInstruction(DratInstructionKind kind, SatClause clause);
/**
* Write the DRAT instruction in textual format.
* The format is described in:
* http://www.cs.utexas.edu/~marijn/publications/drat-trim.pdf
*
* @param os the stream to write to
*/
void outputAsText(std::ostream& os) const;
DratInstructionKind d_kind;
SatClause d_clause;
};
class DratProof
{
public:
DratProof(const DratProof&) = default;
DratProof(DratProof&&) = default;
~DratProof() = default;
/**
* Parses a DRAT proof from the **binary format**.
* The format is described at:
* https://www.cs.utexas.edu/~marijn/drat-trim/#contact
*
* What do the standard authors mean by the format being "binary"?
* They just mean that proofs in this format should be understood as
* sequences of bytes, not sequences of ASCII/Unicode/your favorite character
* set characters.
*
* @param binaryProof a string containing the bytes of the binary proof.
* Even though the proof isn't text, it's safe to store it in a string
* because C++ strings don't make any gaurantees about the encoding of
* their contents. This makes them (effectively) just byte sequences.
*
* @return the parsed proof
*/
static DratProof fromBinary(const std::string& binaryProof);
/**
* @return The instructions in this proof
*/
const std::vector<DratInstruction>& getInstructions() const;
/**
* Write the DRAT proof in textual format.
* The format is described in:
* http://www.cs.utexas.edu/~marijn/publications/drat-trim.pdf
*
* @param os the stream to write to
*/
void outputAsText(std::ostream& os) const;
/**
* Write the DRAT proof as an LFSC value
* The format is from the LFSC signature drat.plf
*
* Reads the current `ProofManager` to determine what the variables should be
* named.
*
* @param os the stream to write to
* @param indentation the number of spaces to indent each proof instruction
*/
void outputAsLfsc(std::ostream& os, uint8_t indentation) const;
private:
/**
* Create an DRAT proof with no instructions.
*/
DratProof();
/**
* The instructions of the DRAT proof.
*/
std::vector<DratInstruction> d_instructions;
};
} // namespace drat
} // namespace proof
} // namespace CVC4
#endif // __CVC4__PROOF__DRAT__DRAT_PROOF_H
|
