Connect++ 0.4.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Private Attributes | List of all members
ProofChecker Class Reference

#include <ProofChecker.hpp>

Collaboration diagram for ProofChecker:
Collaboration graph
[legend]

Public Member Functions

 ProofChecker (Matrix &, const ProofType &, VariableIndex *, TermIndex *)
 
pair< bool, string > check_proof_verbose ()
 Check the proof and produce a string with a detailed description.
 
bool check_proof ()
 Check the proof quietly.
 

Private Member Functions

bool C_i_ok (size_t) const
 Check index. Self-explanatory!
 
bool Lit_i_ok (size_t) const
 Check index. Self-explanatory!
 
bool P_i_ok (size_t) const
 Check index. Self-explanatory!
 
bool Lem_i_ok (size_t) const
 Check index. Self-explanatory!
 
string state_to_string () const
 Make a string containing the current state.
 

Private Attributes

VariableIndex * vi
 Needed as we need to generate things with new variables.
 
TermIndex * ti
 Needed as we need to generate things with new variables.
 
Matrix & matrix
 Reference to the problem matrix.
 
Clause C
 Part of the representation of the current state of the proof.
 
vector< Literal > P
 Part of the representation of the current state of the proof.
 
vector< Literal > Lem
 Part of the representation of the current state of the proof.
 
ProofType proof
 Straightforward internal representation of the proof.
 
Unifier u
 Needed to check some proof steps.
 
vector< RightStackItem > r_stack
 Collection of right-hand branches to complete.
 
size_t num_subs
 Use this to undo the substitutions when you've finished.
 

Detailed Description

This is an alternative to the Prolog proof checker. It uses the contents of stack and matrix to re-construct the proof, checking as it goes that the substitutions work. As an extra check, it re-does unifications rather than using anything stored.

Note: undoes its substitutions when it's finished.

Definition at line 70 of file ProofChecker.hpp.

Constructor & Destructor Documentation

◆ ProofChecker()

ProofChecker::ProofChecker ( Matrix & m,
const ProofType & p,
VariableIndex * _vi,
TermIndex * _ti )

Definition at line 28 of file ProofChecker.cpp.

32: vi(_vi)
33, ti(_ti)
34, matrix(m)
35, C()
36, P()
37, Lem()
38, proof(p)
39, u()
40, r_stack()
41, num_subs(0)
42{}
ProofChecker::proof
ProofType proof
Straightforward internal representation of the proof.
Definition ProofChecker.hpp:99
ProofChecker::vi
VariableIndex * vi
Needed as we need to generate things with new variables.
Definition ProofChecker.hpp:75
ProofChecker::P
vector< Literal > P
Part of the representation of the current state of the proof.
Definition ProofChecker.hpp:91
ProofChecker::ti
TermIndex * ti
Needed as we need to generate things with new variables.
Definition ProofChecker.hpp:79
ProofChecker::Lem
vector< Literal > Lem
Part of the representation of the current state of the proof.
Definition ProofChecker.hpp:95
ProofChecker::u
Unifier u
Needed to check some proof steps.
Definition ProofChecker.hpp:103
ProofChecker::matrix
Matrix & matrix
Reference to the problem matrix.
Definition ProofChecker.hpp:83
ProofChecker::C
Clause C
Part of the representation of the current state of the proof.
Definition ProofChecker.hpp:87
ProofChecker::r_stack
vector< RightStackItem > r_stack
Collection of right-hand branches to complete.
Definition ProofChecker.hpp:107
ProofChecker::num_subs
size_t num_subs
Use this to undo the substitutions when you've finished.
Definition ProofChecker.hpp:111

Member Function Documentation

◆ C_i_ok()

bool ProofChecker::C_i_ok ( size_t i) const
private

Check index. Self-explanatory!

Definition at line 44 of file ProofChecker.cpp.

44 {
45 return (i >= 0 && i < matrix.get_num_clauses());
46}
Matrix::get_num_clauses
ClauseNum get_num_clauses() const
Straightforward get method.
Definition Matrix.hpp:227

◆ check_proof()

bool ProofChecker::check_proof ( )

Check the proof quietly.

Definition at line 299 of file ProofChecker.cpp.

299 {
300 bool result = true;
301
302 for (size_t i = 0; i < proof.size(); i++) {
303
304 ProofLine line = proof[i];
305
306 if (line.first == "start") {
307 size_t C_i = line.second[0];
308 if (i != 0) {
309 result = false;
310 break;
311 }
312 if (!C_i_ok(C_i)) {
313 result = false;
314 break;
315 }
316 Clause start = matrix[C_i];
317 C = start.make_copy_with_new_vars(*vi, *ti);
318 }
319 else if (line.first == "left_branch") {
320 size_t Lit_i = line.second[0];
321 size_t newC_i = line.second[1];
322 size_t newLit_i = line.second[2];
323 size_t d = line.second[3];
324 if (!Lit_i_ok(Lit_i)) {
325 result = false;
326 break;
327 }
328 Literal Lit = C[Lit_i];
329 if (!C_i_ok(newC_i)) {
330 result = false;
331 break;
332 }
333 Clause newC = matrix[newC_i];
334 Clause newCcopy = newC.make_copy_with_new_vars(*vi, *ti);
335 if (newLit_i < 0 || newLit_i >= newC.size()) {
336 result = false;
337 break;
338 }
339 Literal newLit = newCcopy[newLit_i];
340 Literal newLitinv = newCcopy[newLit_i];
341 newLitinv.invert();
342 UnificationOutcome out = u(Lit, newLitinv);
343 if (out != UnificationOutcome::Succeed) {
344 result = false;
345 break;
346 }
347 num_subs++;
348
349 // Make the material for the right branch.
350 vector<Literal> rightP(P);
351 vector<Literal> rightLem(Lem);
352 rightLem.push_back(Lit);
353 Clause rightC(C);
354 rightC.drop_literal(Lit_i);
355 RightStackItem r_item;
356 r_item = std::make_tuple(rightC, rightP, rightLem, d);
357 r_stack.push_back(r_item);
358
359 // Make the material for the left branch.
360 newCcopy.drop_literal(newLit_i);
361 C = newCcopy;
362 P.push_back(Lit);
363 }
364 else if (line.first == "reduction") {
365 size_t Lit_i = line.second[0];
366 size_t P_i = line.second[1];
367 if (!Lit_i_ok(Lit_i)) {
368 result = false;
369 break;
370 }
371 if (!P_i_ok(P_i)) {
372 result = false;
373 break;
374 }
375 Literal l1 = C[Lit_i];
376 Literal l2inv = P[P_i];
377 l2inv.invert();
378 Literal l2 = P[P_i];
379 UnificationOutcome out = u(l1, l2inv);
380 if (out != UnificationOutcome::Succeed) {
381 result = false;
382 break;
383 }
384 num_subs++;
385 Lem.push_back(l1);
386 C.drop_literal(Lit_i);
387 }
388 else if (line.first == "lemmata") {
389 size_t Lit_i = line.second[0];
390 size_t Lem_i = line.second[1];
391 if (!Lit_i_ok(Lit_i)) {
392 result = false;
393 break;
394 }
395 if (!Lem_i_ok(Lem_i)) {
396 result = false;
397 break;
398 }
399 Literal l1 = C[Lit_i];
400 Literal l2 = Lem[Lem_i];
401 if (!l1.subbed_equal(&l2)) {
402 result = false;
403 break;
404 }
405 C.drop_literal(Lit_i);
406 }
407 else if (line.first == "right_branch") {
408 size_t new_d = line.second[0];
409 if (r_stack.empty()) {
410 result = false;
411 break;
412 }
413 if (C.size() != 0) {
414 result = false;
415 break;
416 }
417 RightStackItem r_item(r_stack.back());
418 r_stack.pop_back();
419 C = get<0>(r_item);
420 P = get<1>(r_item);
421 Lem = get<2>(r_item);
422 size_t d = get<3>(r_item);
423 if (d != new_d) {
424 result = false;
425 break;
426 }
427 }
428 else {
429 result = false;
430 break;
431 }
432 }
433 if (!C.empty()) {
434 result = false;
435 }
436 for (size_t i = 0; i < num_subs; i++) {
437 u.backtrack();
438 }
439 return result;
440}
Clause
Representation of clauses.
Definition Clause.hpp:52
Clause::empty
bool empty() const
Straightforward get method.
Definition Clause.hpp:82
Clause::make_copy_with_new_vars
Clause make_copy_with_new_vars(VariableIndex &, TermIndex &) const
Make a copy of an entire clause, introducing new variables.
Definition Clause.cpp:98
Clause::size
size_t size() const
Straightforward get method.
Definition Clause.hpp:78
Clause::drop_literal
void drop_literal(LitNum)
Get rid of the specified Literal.
Definition Clause.cpp:135
Literal
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Definition Literal.hpp:50
Literal::subbed_equal
bool subbed_equal(Literal *) const
Equality, taking account of substitutions.
Definition Literal.cpp:126
Literal::invert
void invert()
Basic manipulation - entirely self-explanatory.
Definition Literal.hpp:103
ProofChecker::P_i_ok
bool P_i_ok(size_t) const
Check index. Self-explanatory!
Definition ProofChecker.cpp:52
ProofChecker::C_i_ok
bool C_i_ok(size_t) const
Check index. Self-explanatory!
Definition ProofChecker.cpp:44
ProofChecker::Lem_i_ok
bool Lem_i_ok(size_t) const
Check index. Self-explanatory!
Definition ProofChecker.cpp:56
ProofChecker::Lit_i_ok
bool Lit_i_ok(size_t) const
Check index. Self-explanatory!
Definition ProofChecker.cpp:48
Unifier::backtrack
void backtrack()
Apply the backtracking process to the substitution that has been constructed.
Definition Unifier.cpp:134

◆ check_proof_verbose()

pair< bool, string > ProofChecker::check_proof_verbose ( )

Check the proof and produce a string with a detailed description.

Definition at line 79 of file ProofChecker.cpp.

79 {
80 bool result = true;
81 string out_string;
82
83 for (size_t i = 0; i < proof.size(); i++) {
84 out_string += "** Proof step: ";
85 out_string += std::to_string(i) += " *************************************************\n";
86
87 ProofLine line = proof[i];
88
89 if (line.first == "start") {
90 out_string += "Found a Start step with C = ";
91 size_t C_i = line.second[0];
92 out_string += std::to_string(C_i) += ".\n";
93 if (i != 0) {
94 out_string += "Error: you can only use the Start rule as step 1 of a proof.\n";
95 result = false;
96 break;
97 }
98 if (!C_i_ok(C_i)) {
99 out_string += "Error: the start clause index is out of range.\n";
100 result = false;
101 break;
102 }
103 Clause start = matrix[C_i];
104 out_string += "C = ";
105 out_string += start.to_string() += "\n";
106 C = start.make_copy_with_new_vars(*vi, *ti);
107 out_string += "Starting from state (with new variables):\n";
108 out_string += state_to_string();
109 }
110 else if (line.first == "left_branch") {
111 size_t Lit_i = line.second[0];
112 size_t newC_i = line.second[1];
113 size_t newLit_i = line.second[2];
114 size_t d = line.second[3];
115 out_string += "Found an Extension step (left) with: L = ";
116 out_string += std::to_string(Lit_i) += ", C' = ";
117 out_string += std::to_string(newC_i) += ", L' = ";
118 out_string += std::to_string(newLit_i) += ", depth = ";
119 out_string += std::to_string(d) += ".\n";
120 if (!Lit_i_ok(Lit_i)) {
121 out_string += "Error: the clause literal index is out of range.\n";
122 result = false;
123 break;
124 }
125 Literal Lit = C[Lit_i];
126 out_string += "L = ";
127 out_string += Lit.to_string() += "\nL = ";
128 out_string += Lit.to_string(true) += " substituted.\n";
129 if (!C_i_ok(newC_i)) {
130 out_string += "Error: the new clause index is out of range.\n";
131 result = false;
132 break;
133 }
134 Clause newC = matrix[newC_i];
135 out_string += "C' = ";
136 out_string += newC.to_string() += "\n";
137 Clause newCcopy = newC.make_copy_with_new_vars(*vi, *ti);
138 out_string += "C' = ";
139 out_string += newCcopy.to_string() += " with new variables.\n";
140 if (newLit_i < 0 || newLit_i >= newC.size()) {
141 out_string += "Error: the new literal index is out of range.\n";
142 result = false;
143 break;
144 }
145 Literal newLit = newCcopy[newLit_i];
146 Literal newLitinv = newCcopy[newLit_i];
147 newLitinv.invert();
148 out_string += "~L' = ";
149 out_string += newLitinv.to_string() += " and has new variables.\n";
150 UnificationOutcome out = u(Lit, newLitinv);
151 if (out != UnificationOutcome::Succeed) {
152 out_string += "Error: these literals can not be unified.\n";
153 result = false;
154 break;
155 }
156 num_subs++;
157 out_string += "Literals L and ~L' are unified by: ";
158 out_string += u.to_string() += "\n";
159
160 // Make the material for the right branch.
161 vector<Literal> rightP(P);
162 vector<Literal> rightLem(Lem);
163 rightLem.push_back(Lit);
164 Clause rightC(C);
165 rightC.drop_literal(Lit_i);
166 RightStackItem r_item;
167 r_item = std::make_tuple(rightC, rightP, rightLem, d);
168 r_stack.push_back(r_item);
169
170 // Make the material for the left branch.
171 newCcopy.drop_literal(newLit_i);
172 C = newCcopy;
173 P.push_back(Lit);
174 out_string += "Continuing with:\n";
175 out_string += state_to_string();
176 }
177 else if (line.first == "reduction") {
178 size_t Lit_i = line.second[0];
179 size_t P_i = line.second[1];
180 out_string += "Found a Reduction step with L = ";
181 out_string += std::to_string(Lit_i) += " and L' = ";
182 out_string += std::to_string(P_i) += ".\n";
183 if (!Lit_i_ok(Lit_i)) {
184 out_string += "Error: the clause literal index is out of range.\n";
185 result = false;
186 break;
187 }
188 if (!P_i_ok(P_i)) {
189 out_string += "Error: the path literal index is out of range.\n";
190 result = false;
191 break;
192 }
193 out_string += "L = ";
194 Literal l1 = C[Lit_i];
195 out_string += l1.to_string() += "\nL = ";
196 out_string += l1.to_string(true) += " substituted.\n";
197 out_string += "~L' = ";
198 Literal l2inv = P[P_i];
199 l2inv.invert();
200 Literal l2 = P[P_i];
201 out_string += l2inv.to_string() += "\n~L' = ";
202 out_string += l2inv.to_string(true) += " substituted.\n";
203 UnificationOutcome out = u(l1, l2inv);
204 if (out != UnificationOutcome::Succeed) {
205 out_string += "Error: these literals can not be unified.\n";
206 result = false;
207 break;
208 }
209 num_subs++;
210 out_string += "Literals L and ~L' are unified by: ";
211 out_string += u.to_string() += "\n";
212 Lem.push_back(l1);
213 C.drop_literal(Lit_i);
214 out_string += "Continuing with:\n";
215 out_string += state_to_string();
216 }
217 else if (line.first == "lemmata") {
218 size_t Lit_i = line.second[0];
219 size_t Lem_i = line.second[1];
220 out_string += "Found a Lemma step with L = ";
221 out_string += std::to_string(Lit_i) += " and L' = ";
222 out_string += std::to_string(Lem_i) += ".\n";
223 if (!Lit_i_ok(Lit_i)) {
224 out_string += "Error: the clause literal index is out of range.\n";
225 result = false;
226 break;
227 }
228 if (!Lem_i_ok(Lem_i)) {
229 out_string += "Error: the lemma literal index is out of range.\n";
230 result = false;
231 break;
232 }
233 out_string += "L = ";
234 Literal l1 = C[Lit_i];
235 out_string += l1.to_string() += "\nL = ";
236 out_string += l1.to_string(true) += " substituted.\n";
237 out_string += "L' = ";
238 Literal l2 = Lem[Lem_i];
239 out_string += l2.to_string() += "\nL' = ";
240 out_string += l2.to_string(true) += " substituted.\n";
241 if (!l1.subbed_equal(&l2)) {
242 out_string += "Error: these literals are not equal with the current substitution.\n";
243 result = false;
244 break;
245 }
246 out_string += "Literals L and L' are equal with the current substitution.\n";
247 C.drop_literal(Lit_i);
248 out_string += "Continuing with:\n";
249 out_string += state_to_string();
250 }
251 else if (line.first == "right_branch") {
252 size_t new_d = line.second[0];
253 out_string += "Found a right branch step with depth ";
254 out_string += std::to_string(new_d) += ".\n";
255 if (r_stack.empty()) {
256 out_string += "Error: the right stack is empty.\n";
257 result = false;
258 break;
259 }
260 if (C.size() != 0) {
261 out_string += "Error: this should be an axiom but C is not empty.\n";
262 result = false;
263 break;
264 }
265 out_string += "We have an Axiom!\n";
266 RightStackItem r_item(r_stack.back());
267 r_stack.pop_back();
268 C = get<0>(r_item);
269 P = get<1>(r_item);
270 Lem = get<2>(r_item);
271 size_t d = get<3>(r_item);
272 if (d != new_d) {
273 out_string += "Error: the depths don't match.\n";
274 result = false;
275 break;
276 }
277 out_string += "Continuing with:\n";
278 out_string += state_to_string();
279 }
280 else {
281 out_string += "The proof is badly-formed.\n";
282 result = false;
283 break;
284 }
285 }
286 if (!C.empty()) {
287 out_string += "Error: you haven't ended with an Axiom.\n";
288 result = false;
289 }
290 if (result) {
291 out_string += "SUCCESS! The proof is good.\n";
292 }
293 for (size_t i = 0; i < num_subs; i++) {
294 u.backtrack();
295 }
296 return pair<bool, string>(result, out_string);
297}
Clause::to_string
string to_string(bool=false) const
Convert to a string.
Definition Clause.cpp:202
Literal::to_string
string to_string(bool=false) const
Full conversion of Literal to string.
Definition Literal.cpp:150
ProofChecker::state_to_string
string state_to_string() const
Make a string containing the current state.
Definition ProofChecker.cpp:60
Unifier::to_string
string to_string(bool subbed=false) const
Make a nice string representation.
Definition Unifier.hpp:164

◆ Lem_i_ok()

bool ProofChecker::Lem_i_ok ( size_t i) const
private

Check index. Self-explanatory!

Definition at line 56 of file ProofChecker.cpp.

56 {
57 return (i >= 0 && i < Lem.size());
58}

◆ Lit_i_ok()

bool ProofChecker::Lit_i_ok ( size_t i) const
private

Check index. Self-explanatory!

Definition at line 48 of file ProofChecker.cpp.

48 {
49 return (i >= 0 && i < C.size());
50}

◆ P_i_ok()

bool ProofChecker::P_i_ok ( size_t i) const
private

Check index. Self-explanatory!

Definition at line 52 of file ProofChecker.cpp.

52 {
53 return (i >= 0 && i < P.size());
54}

◆ state_to_string()

string ProofChecker::state_to_string ( ) const
private

Make a string containing the current state.

Definition at line 60 of file ProofChecker.cpp.

60 {
61 string s("C = ");
62 s += C.to_string() += "\nC = ";
63 s += C.to_string(true) += " substituted.\n\nP = { ";
64 for (const Literal& l : P)
65 s += l.to_string() += " ";
66 s += " }\nP = { ";
67 for (const Literal& l : P)
68 s += l.to_string(true) += " ";
69 s += " } substituted.\n\nL = { ";
70 for (const Literal& l : Lem)
71 s += l.to_string() += " ";
72 s += " }\nL = { ";
73 for (const Literal& l : Lem)
74 s += l.to_string(true) += " ";
75 s += " } substituted.\n\n";
76 return s;
77}

Member Data Documentation

◆ C

Clause ProofChecker::C
private

Part of the representation of the current state of the proof.

Definition at line 87 of file ProofChecker.hpp.

◆ Lem

vector<Literal> ProofChecker::Lem
private

Part of the representation of the current state of the proof.

Definition at line 95 of file ProofChecker.hpp.

◆ matrix

Matrix& ProofChecker::matrix
private

Reference to the problem matrix.

Definition at line 83 of file ProofChecker.hpp.

◆ num_subs

size_t ProofChecker::num_subs
private

Use this to undo the substitutions when you've finished.

Definition at line 111 of file ProofChecker.hpp.

◆ P

vector<Literal> ProofChecker::P
private

Part of the representation of the current state of the proof.

Definition at line 91 of file ProofChecker.hpp.

◆ proof

ProofType ProofChecker::proof
private

Straightforward internal representation of the proof.

Definition at line 99 of file ProofChecker.hpp.

◆ r_stack

vector<RightStackItem> ProofChecker::r_stack
private

Collection of right-hand branches to complete.

Definition at line 107 of file ProofChecker.hpp.

◆ ti

TermIndex* ProofChecker::ti
private

Needed as we need to generate things with new variables.

Definition at line 79 of file ProofChecker.hpp.

◆ u

Unifier ProofChecker::u
private

Needed to check some proof steps.

Definition at line 103 of file ProofChecker.hpp.

◆ vi

VariableIndex* ProofChecker::vi
private

Needed as we need to generate things with new variables.

Definition at line 75 of file ProofChecker.hpp.

The documentation for this class was generated from the following files: