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

Prover using a pair of stacks to conduct the proof search. More...

#include <StackProver.hpp>

Collaboration diagram for StackProver:
Collaboration graph
[legend]

Public Member Functions

 StackProver ()
 You only need a basic constructor.
 
 StackProver (const StackProver &)=delete
 Don't try to copy this.
 
 StackProver (const StackProver &&)=delete
 
StackProver & operator= (const StackProver &)=delete
 
StackProver & operator= (const StackProver &&)=delete
 
std::tuple< VariableIndex *, FunctionIndex *, PredicateIndex *, TermIndex * > get_indexes ()
 Straightforward get method.
 
string get_status () const
 Straightforward get method.
 
void set_timeout (chrono::steady_clock::time_point time)
 Set a timeout.
 
void set_problem_path (fs::path &p)
 Set the path for the problem being solved. U.
 
void set_num_preds (size_t)
 Set the number of predicates.
 
void read_from_tptp_file (const string &, bool &, size_t &)
 Obviously, reads a problem from a TPTP file.
 
void add_equality_axioms (Predicate *)
 After reading a problem in which = and/or != appears, add the axioms for equality.
 
void deterministic_reorder (uint32_t n)
 Deterministically reorder the matrix n times.
 
void random_reorder ()
 Randomly reorder the matrix.
 
void show_matrix ()
 Show a nicely formatted matrix.
 
Matrix & get_matrix ()
 Get a reference to the matrix.
 
bool problem_is_cnf_only () const
 Find out whether the problem is CNF only.
 
bool problem_has_true_conjecture () const
 Find out whether the problem's conjecture
is $true.
 
bool problem_has_false_conjecture () const
 Find out whether the problem's conjecture
is $false.
 
bool problem_has_missing_conjecture () const
 Find out whether the problem's conjecture
is missing, in the sense that it didn't appear in the input file.
 
bool problem_has_negated_conjecture_removed () const
 Find out whether the problem's
negated conjecture was simplified out.
 
bool problem_has_fof_axioms () const
 Find out from the parser whether the problem had axioms before simplification.
 
bool simplified_problem_has_fof_axioms () const
 Find out from the parser whether the problem had axioms after simplification.
 
void show_tptp_proof ()
 Show a Prolog-formatted proof.
 
ProverOutcome prove ()
 Here is where the magic happens.
 
vector< pair< string, vector< size_t > > > get_internal_proof () const
 Get an internal representation of the proof stack.
 
void show_matrix () const
 
void show_path () const
 
void show_stack ()
 
void show_right_stack ()
 
void show_term_index ()
 
void show_statistics () const
 

Private Member Functions

ProverResult go ()
 This runs the proof search from a given Start Move.
 
void populate_stack_item ()
 Fill the vector of possible actions with everything available.
 
void extend_with_action ()
 Take a single inference (action) and update the stacks accordingly.
 
bool depth_limited ()
 Test for the depth limit.
 
bool axiom () const
 Test to see if you're at an axiom.
 
void process_axiom_forward ()
 Start a right branch to continue from an axiom.
 
void backtrack_once ()
 Basic, single step backtrack on the stack.
 
void reduction_backtrack ()
 One of several different kinds of backtracking.
 
void lemmata_backtrack ()
 One of several different kinds of backtracking.
 
void left_extension_backtrack ()
 One of several different kinds of backtracking.
 
void right_extension_backtrack ()
 One of several different kinds of backtracking.
 
void set_up_start_clauses ()
 The start clauses to use depend on the settings, and the settings can change.
 
void reset_for_start ()
 Reset everything so that you can start from a specified start clause.
 

Private Attributes

size_t num_preds
 How many prdicates does the problem of interest have?
 
VariableIndex var_index
 This class needs one of each kind of index to keep track of Variables, Terms etc.
 
FunctionIndex fun_index
 This class needs one of each kind of index to keep track of Variables, Terms etc.
 
TermIndex term_index
 This class needs one of each kind of index to keep track of Variables, Terms etc.
 
PredicateIndex pred_index
 This class needs one of each kind of index to keep track of Variables, Terms etc.
 
SubstitutionStack sub_stack
 There is a separate stack to make application and removal of substitutions straightforward.
 
vector< StartClauseStatus > results
 This is populated by the StackProver::set_up_start_clauses method.
 
Matrix matrix
 A copy of the matrix you're working with.
 
SimplePath path
 At any point in the search process this is a copy of the path for the current node in the proof being constructed.
 
Clause new_C
 At any point in the search process this is a copy of the clause for the current node in the proof being constructed.
 
Lemmata lemmata
 At any point in the search process this is a copy of the list of lemmata for the current node in the proof being constructed.
 
Unifier u
 We need a single Unifier to use throught the process.
 
InferenceItem action
 Stores the next action from the current StackItem.
 
StackItem * si
 Pointer to the current StackItem.
 
uint32_t current_depth_limit
 Self-explanatary.
 
uint32_t current_depth
 Self-explanatary.
 
bool depth_limit_reached
 Self-explanatary.
 
string status
 Problem status, if found in input file.
 
vector< StackItem > stack
 Main stack: this is constructed by the search process and, if completed, represents a proof.
 
vector< StackItem > right_branch_stack
 We build the proof by trying the left branches of extensions first: this stack keeps track of the right branches that we need to come back to.
 
bool backtrack
 Are we moving up or down the stack?
 
ProofPrinter proof_printer
 You need one of these to print LaTeX output or any kind of proof certificate.
 
fs::path problem_path
 Path for the problem of interest.
 
Interval output_interval
 How often do you output updates about progress?
 
uint32_t reductions_tried
 We'll be keeping some simple statistics about the search process.
 
uint32_t extensions_tried
 We'll be keeping some simple statistics about the search process.
 
uint32_t lemmata_tried
 We'll be keeping some simple statistics about the search process.
 
uint32_t right_branches_started
 We'll be keeping some simple statistics about the search process.
 
uint32_t proof_count
 If we're searching for multiple proofs, keep count
of which one this is.
 
bool use_timeout
 Are we using a timeout?
 
chrono::steady_clock::time_point end_time
 When do we stop because of a timeout?
 
verbose_print::VPrint show
 Set up printing according to verbosity.
 
bool cnf_only
 Keep track of whether there were any FOF formulas in the problem file.
 
bool conjecture_true
 Keep track of whether the parser found the conjecture to be true.
 
bool conjecture_false
 Keep track of whether the parser found the conjecture to be false.
 
bool conjecture_missing
 Keep track of whether the parser found a conjecture in the problem file.
 
bool negated_conjecture_removed
 Keep track of whether the parser simplified the conjecture away.
 
bool fof_has_axioms
 Keep track of whether the parser found that it's an FOF problem with axioms before simplification.
 
bool simplified_fof_has_axioms
 Keep track of whether the parser found that it's an FOF problem with axioms after simplification.
 

Friends

ostream & operator<< (ostream &, const StackProver &)
 

Detailed Description

Prover using a pair of stacks to conduct the proof search.

This version is a straightforward translation of the proof method to search for a tree with all its leaves being axioms. However, by not using recursion we retain the ability to fully control backtracking and therefore, amongst other things, find all possible proofs.

This is really the main class for Connect++, and everything else essentially exists to support it. There's a lot going on here so hang on to your hat!

This is also one of only a small number of places where you'll need to modify stuff to incorporate machine learning. The main advice is simple: take notice of the comments that point out where to do this, and be very careful to leave the general stack manipulation code alone unless you really know what you're doing, because that stuff is quite easy to break.

Definition at line 74 of file StackProver.hpp.

Constructor & Destructor Documentation

◆ StackProver()

StackProver::StackProver ( )

You only need a basic constructor.

Definition at line 28 of file StackProver.cpp.

29: num_preds(0)
30, var_index()
31, fun_index()
32, term_index()
33, pred_index()
34, sub_stack()
35, results()
36, matrix()
37, path()
38, new_C()
39, lemmata()
40, u()
41, action(InferenceItemType::Start)
42, si(nullptr)
43, current_depth_limit(0)
44, current_depth(1)
45, depth_limit_reached(false)
46, status()
47, stack()
48, right_branch_stack()
49, backtrack(false)
50, proof_printer(&stack)
51, problem_path()
52, output_interval(params::output_frequency)
53, reductions_tried(0)
54, extensions_tried(0)
55, lemmata_tried(0)
56, right_branches_started(0)
57, proof_count(0)
58, use_timeout(false)
59, end_time()
60, show(params::verbosity)
61, cnf_only(false)
62, conjecture_true(false)
63, conjecture_false(false)
64, conjecture_missing(false)
65, negated_conjecture_removed(false)
66, fof_has_axioms(false)
67, simplified_fof_has_axioms(false)
68{}
StackProver::depth_limit_reached
bool depth_limit_reached
Self-explanatary.
Definition StackProver.hpp:168
StackProver::status
string status
Problem status, if found in input file.
Definition StackProver.hpp:172
StackProver::results
vector< StartClauseStatus > results
This is populated by the StackProver::set_up_start_clauses method.
Definition StackProver.hpp:116
StackProver::negated_conjecture_removed
bool negated_conjecture_removed
Keep track of whether the parser simplified the conjecture away.
Definition StackProver.hpp:339
StackProver::lemmata_tried
uint32_t lemmata_tried
We'll be keeping some simple statistics about the search process.
Definition StackProver.hpp:218
StackProver::current_depth_limit
uint32_t current_depth_limit
Self-explanatary.
Definition StackProver.hpp:160
StackProver::action
InferenceItem action
Stores the next action from the current StackItem.
Definition StackProver.hpp:146
StackProver::num_preds
size_t num_preds
How many prdicates does the problem of interest have?
Definition StackProver.hpp:80
StackProver::fof_has_axioms
bool fof_has_axioms
Keep track of whether the parser found that it's an FOF problem with axioms before simplification.
Definition StackProver.hpp:344
StackProver::stack
vector< StackItem > stack
Main stack: this is constructed by the search process and, if completed, represents a proof.
Definition StackProver.hpp:177
StackProver::matrix
Matrix matrix
A copy of the matrix you're working with.
Definition StackProver.hpp:120
StackProver::pred_index
PredicateIndex pred_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
Definition StackProver.hpp:100
StackProver::right_branch_stack
vector< StackItem > right_branch_stack
We build the proof by trying the left branches of extensions first: this stack keeps track of the rig...
Definition StackProver.hpp:183
StackProver::proof_printer
ProofPrinter proof_printer
You need one of these to print LaTeX output or any kind of proof certificate.
Definition StackProver.hpp:192
StackProver::cnf_only
bool cnf_only
Keep track of whether there were any FOF formulas in the problem file.
Definition StackProver.hpp:323
StackProver::path
SimplePath path
At any point in the search process this is a copy of the path for the current node in the proof being...
Definition StackProver.hpp:126
StackProver::fun_index
FunctionIndex fun_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
Definition StackProver.hpp:90
StackProver::lemmata
Lemmata lemmata
At any point in the search process this is a copy of the list of lemmata for the current node in the ...
Definition StackProver.hpp:138
StackProver::extensions_tried
uint32_t extensions_tried
We'll be keeping some simple statistics about the search process.
Definition StackProver.hpp:213
StackProver::current_depth
uint32_t current_depth
Self-explanatary.
Definition StackProver.hpp:164
StackProver::simplified_fof_has_axioms
bool simplified_fof_has_axioms
Keep track of whether the parser found that it's an FOF problem with axioms after simplification.
Definition StackProver.hpp:349
StackProver::conjecture_missing
bool conjecture_missing
Keep track of whether the parser found a conjecture in the problem file.
Definition StackProver.hpp:335
StackProver::term_index
TermIndex term_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
Definition StackProver.hpp:95
StackProver::proof_count
uint32_t proof_count
If we're searching for multiple proofs, keep count of which one this is.
Definition StackProver.hpp:228
StackProver::conjecture_false
bool conjecture_false
Keep track of whether the parser found the conjecture to be false.
Definition StackProver.hpp:331
StackProver::var_index
VariableIndex var_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
Definition StackProver.hpp:85
StackProver::conjecture_true
bool conjecture_true
Keep track of whether the parser found the conjecture to be true.
Definition StackProver.hpp:327
StackProver::right_branches_started
uint32_t right_branches_started
We'll be keeping some simple statistics about the search process.
Definition StackProver.hpp:223
StackProver::backtrack
bool backtrack
Are we moving up or down the stack?
Definition StackProver.hpp:187
StackProver::end_time
chrono::steady_clock::time_point end_time
When do we stop because of a timeout?
Definition StackProver.hpp:236
StackProver::si
StackItem * si
Pointer to the current StackItem.
Definition StackProver.hpp:156
StackProver::new_C
Clause new_C
At any point in the search process this is a copy of the clause for the current node in the proof bei...
Definition StackProver.hpp:132
StackProver::problem_path
fs::path problem_path
Path for the problem of interest.
Definition StackProver.hpp:196
StackProver::use_timeout
bool use_timeout
Are we using a timeout?
Definition StackProver.hpp:232
StackProver::reductions_tried
uint32_t reductions_tried
We'll be keeping some simple statistics about the search process.
Definition StackProver.hpp:208
StackProver::sub_stack
SubstitutionStack sub_stack
There is a separate stack to make application and removal of substitutions straightforward.
Definition StackProver.hpp:105
StackProver::show
verbose_print::VPrint show
Set up printing according to verbosity.
Definition StackProver.hpp:240
StackProver::u
Unifier u
We need a single Unifier to use throught the process.
Definition StackProver.hpp:142
StackProver::output_interval
Interval output_interval
How often do you output updates about progress?
Definition StackProver.hpp:200

Member Function Documentation

◆ add_equality_axioms()

void StackProver::add_equality_axioms ( Predicate *  equals_predicate)

After reading a problem in which = and/or != appears, add the axioms for equality.

Parameters
equals_predicatePointer to a Predicate representing equals. This will have been obtained as an output from parsing the input file.

Definition at line 125 of file StackProver.cpp.

125 {
126 /*
127 * Equality axioms as described in Handbook of Automated
128 * Reasoning, Volume 1, page 615.
129 */
130 Arity max_fun_arity = fun_index.find_maximum_arity();
131 Arity max_pred_arity = pred_index.find_maximum_arity();
132 /*
133 * You need at least three variables to describe these, and
134 * twice as many as the arity of the biggest predicate or
135 * function.
136 */
137 uint32_t max_arity = max_fun_arity;
138 if (max_pred_arity > max_arity)
139 max_arity = max_pred_arity;
140 if (max_arity < 3)
141 max_arity = 3;
142 vector<Term*> xs;
143 vector<Term*> ys;
144 string xvar("__eqx_");
145 string yvar("__eqy_");
146 for (size_t i = 0; i < max_arity; i++) {
147 Variable* xvarp = var_index.add_named_var(xvar + std::to_string(i));
148 Variable* yvarp = var_index.add_named_var(yvar + std::to_string(i));
149 xs.push_back(term_index.add_variable_term(xvarp));
150 ys.push_back(term_index.add_variable_term(yvarp));
151 }
152 /*
153 * How you construct these depends on which representation you're using.
154 * It's easy enough to show that the difference is only a case
155 * of swapping negations. See for example "Equality Preprocessing in
156 * Connection Calculi", Oliver and Otten.
157 */
158 bool pol = !params::positive_representation;
159 uint32_t n_added = 0;
160 /*
161 * Axiom for reflexivity.
162 */
163 vector<Term*> ref;
164 ref.push_back(xs[0]);
165 ref.push_back(xs[0]);
166 Literal reflexive(equals_predicate, ref, 2, pol);
167 Clause ref_c;
168 ref_c.add_lit(reflexive);
169 matrix.add_clause(ref_c, "equality");
170 n_added++;
171 /*
172 * Axiom for symmetry.
173 */
174 vector<Term*> xy;
175 xy.push_back(xs[0]);
176 xy.push_back(xs[1]);
177 vector<Term*> yx;
178 yx.push_back(xs[1]);
179 yx.push_back(xs[0]);
180 Literal sym1(equals_predicate, xy, 2, !pol);
181 Literal sym2(equals_predicate, yx, 2, pol);
182 Clause sym_c;
183 sym_c.add_lit(sym1);
184 sym_c.add_lit(sym2);
185 matrix.add_clause(sym_c, "equality");
186 n_added++;
187 /*
188 * Axiom for transitivity.
189 */
190 vector<Term*> yz;
191 yz.push_back(xs[1]);
192 yz.push_back(xs[2]);
193 vector<Term*> xz;
194 xz.push_back(xs[0]);
195 xz.push_back(xs[2]);
196 Literal tr1(equals_predicate, xy, 2, !pol);
197 Literal tr2(equals_predicate, yz, 2, !pol);
198 Literal tr3(equals_predicate, xz, 2, pol);
199 Clause tr_c;
200 tr_c.add_lit(tr1);
201 tr_c.add_lit(tr2);
202 tr_c.add_lit(tr3);
203 matrix.add_clause(tr_c, "equality");
204 n_added++;
205 /*
206 * Function substitution.
207 */
208 for (size_t j = 0; j < fun_index.get_size(); j++) {
209 Function* p = fun_index[j];
210 Arity ar = p->get_arity();
211 if (ar > 0) {
212 Clause c;
213 vector<Term*> x1xn;
214 vector<Term*> y1yn;
215 for (size_t i = 0; i < ar; i++) {
216 x1xn.push_back(xs[i]);
217 y1yn.push_back(ys[i]);
218 vector<Term*> xiyi;
219 xiyi.push_back(xs[i]);
220 xiyi.push_back(ys[i]);
221 Literal eq_lit(equals_predicate, xiyi, 2, !pol);
222 c.add_lit(eq_lit);
223 }
224 vector<Term*> t;
225 t.push_back(term_index.add_function_term(p, x1xn));
226 t.push_back(term_index.add_function_term(p, y1yn));
227 Literal f_lit(equals_predicate, t, 2, pol);
228 c.add_lit(f_lit);
229 matrix.add_clause(c, "equality");
230 n_added++;
231 }
232 }
233 /*
234 * Predicate substitution.
235 */
236 for (size_t j = 0; j < pred_index.get_num_preds(); j++) {
237 Predicate* p = pred_index[j];
238 Arity ar = p->get_arity();
239 if (ar > 0 && p != equals_predicate) {
240 Clause c;
241 vector<Term*> x1xn;
242 vector<Term*> y1yn;
243 for (size_t i = 0; i < ar; i++) {
244 x1xn.push_back(xs[i]);
245 y1yn.push_back(ys[i]);
246 vector<Term*> xiyi;
247 xiyi.push_back(xs[i]);
248 xiyi.push_back(ys[i]);
249 Literal eq_lit(equals_predicate, xiyi, 2, !pol);
250 c.add_lit(eq_lit);
251 }
252 Literal p_lit1(p, x1xn, ar, !pol);
253 Literal p_lit2(p, y1yn, ar, pol);
254 c.add_lit(p_lit1);
255 c.add_lit(p_lit2);
256 matrix.add_clause(c, "equality");
257 n_added++;
258 }
259 }
260 /*
261 * Distinct objects
262 */
263 Arity min_arity = fun_index.find_minimum_arity();
264 if (!params::no_distinct_objects && min_arity == 0) {
265 vector<Term*> all_distinct_constants;
266 vector<Term*> empty_args;
267 for (size_t i = 0; i < fun_index.get_size(); i++) {
268 Function* p = fun_index[i];
269 Arity ar = p->get_arity();
270 // Remember, you don't want to do this for Skolem constants.
271 string name = p->get_name();
272 string prefix = name.string::substr(0,params::unique_skolem_prefix.length());
273 bool is_skolem = (params::unique_skolem_prefix.string::compare(0, string::npos, prefix) == 0) &&
274 (params::unique_skolem_prefix.length() < name.length());
275 bool is_quoted = (name[0] == '\"' && name[name.size() - 1] == '\"');
276 if (ar == 0 &&
277 !is_skolem &&
278 (params::all_distinct_objects || is_quoted)) {
279 Term* t = term_index.add_function_term(p, empty_args);
280 all_distinct_constants.push_back(t);
281 }
282 }
283 size_t s = all_distinct_constants.size();
284 if (s > 1) {
285 for (size_t i = s - 1; i > 0; i--) {
286 for (size_t j = 0; j < i; j++) {
287 Clause c;
288 vector<Term*> args;
289 args.push_back(all_distinct_constants[i]);
290 args.push_back(all_distinct_constants[j]);
291 Literal eq_lit(equals_predicate, args, 2, !pol);
292 c.add_lit(eq_lit);
293 matrix.add_clause(c, "distinct_objects");
294 n_added++;
295 }
296 }
297 }
298 }
299 matrix.set_num_equals(n_added);
300}
Clause
Representation of clauses.
Definition Clause.hpp:52
Clause::add_lit
void add_lit(const Literal &)
Add a literal, making sure you don't duplicate.
Definition Clause.cpp:87
Function
Basic representation of functions.
Definition Function.hpp:54
Function::get_arity
Arity get_arity() const
Most basic access function.
Definition Function.hpp:89
Function::get_name
string get_name() const
Most basic access function.
Definition Function.hpp:85
FunctionIndex::find_minimum_arity
Arity find_minimum_arity() const
Find the smallest arity appearing for any Function in the index.
Definition FunctionIndex.cpp:81
FunctionIndex::get_size
size_t get_size() const
Self-explanatory.
Definition FunctionIndex.hpp:96
FunctionIndex::find_maximum_arity
Arity find_maximum_arity() const
Find the largest arity appearing for any Function in the index.
Definition FunctionIndex.cpp:71
Literal
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Definition Literal.hpp:50
Matrix::add_clause
void add_clause(Clause &, string="")
Add a Clause to the Matrix and update the index accordingly.
Definition Matrix.cpp:91
Matrix::set_num_equals
void set_num_equals(uint32_t n)
Straightforward set method.
Definition Matrix.hpp:223
Predicate
Basic representation of predicates: here just names, ids and arities.
Definition Predicate.hpp:51
Predicate::get_arity
Arity get_arity() const
Basic get method.
Definition Predicate.hpp:90
PredicateIndex::get_num_preds
size_t get_num_preds() const
Basic get method.
Definition PredicateIndex.hpp:92
PredicateIndex::find_maximum_arity
Arity find_maximum_arity() const
Find the largest arity appearing in the index.
Definition PredicateIndex.cpp:66
Term
General representation of terms.
Definition Term.hpp:62
TermIndex::add_function_term
Term * add_function_term(Function *, const vector< Term * > &)
Self-explanatory: add a Term containing a function to the index.
Definition TermIndex.cpp:73
TermIndex::add_variable_term
Term * add_variable_term(Variable *)
Self-explanatory: add a Term containing a variable to the index.
Definition TermIndex.cpp:56
Variable
Basic representation of variables.
Definition Variable.hpp:58
VariableIndex::add_named_var
Variable * add_named_var(const string &)
Add a variable with the specified name to the index.
Definition VariableIndex.cpp:44

◆ axiom()

bool StackProver::axiom ( ) const
private

Test to see if you're at an axiom.

Definition at line 352 of file StackProver.cpp.

352 {
353 return si->c.empty();
354}
Clause::empty
bool empty() const
Straightforward get method.
Definition Clause.hpp:82
StackItem::c
Clause c
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the clause.
Definition StackItem.hpp:60

◆ backtrack_once()

void StackProver::backtrack_once ( )
private

Basic, single step backtrack on the stack.

Careful though: you need to treat the depth of the tree correctly if you want to keep track of it.

Definition at line 550 of file StackProver.cpp.

550 {
551 backtrack = true;
552 stack.pop_back();
553 si = &stack.back();
554 current_depth = si->depth;
555}
StackItem::depth
uint32_t depth
How deep in the proof tree are we?
Definition StackItem.hpp:88

◆ depth_limited()

bool StackProver::depth_limited ( )
private

Test for the depth limit.

Definition at line 343 of file StackProver.cpp.

343 {
344 bool result = ((params::limit_by_tree_depth && (current_depth == current_depth_limit))
345 ||
346 (!params::limit_by_tree_depth && (si->p.length() == current_depth_limit)));
347 if (result)
348 depth_limit_reached = true;
349 return result;
350}
SimplePath::length
uint32_t length() const
Straightforward get method.
Definition SimplePath.hpp:93
StackItem::p
SimplePath p
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the path.
Definition StackItem.hpp:65

◆ deterministic_reorder()

void StackProver::deterministic_reorder ( uint32_t  n)
inline

Deterministically reorder the matrix n times.

Parameters
nNumber of times to reorder.

Definition at line 426 of file StackProver.hpp.

426 {
427 matrix.deterministic_reorder(n);
428 }
Matrix::deterministic_reorder
void deterministic_reorder(size_t)
Deterministic reorder of the clauses.
Definition Matrix.cpp:105

◆ extend_with_action()

void StackProver::extend_with_action ( )
private

Take a single inference (action) and update the stacks accordingly.

Definition at line 356 of file StackProver.cpp.

356 {
357 /*
358 * Add a new StackItem using the next action from the list stored
359 * in the StackItem currently in play. If necessary, also
360 * add something to right_branch_stack. Populate the new list of
361 * actions and update si.
362 */
363 action = si->actions.back();
364 si->actions.pop_back();
365 current_depth++;
366 /*
367 * Why are the scope rules for switch so odd???
368 */
369 Clause old_C;
370 Lemmata old_Lem;
371 switch (action.T) {
372 //----------------------------------------------------------------------
373 //----------------------------------------------------------------------
374 //----------------------------------------------------------------------
375 // Lemmata.
376 //----------------------------------------------------------------------
377 //----------------------------------------------------------------------
378 //----------------------------------------------------------------------
379 case InferenceItemType::Lemma:
380 lemmata_tried++;
381 /*
382 * If you are restricting backtracking for lemmata then
383 * at this point you can remove all alternatives.
384 */
385 if (params::limit_bt_lemmas)
386 si->restrict_backtrack();
387 /*
388 * Work out the new state.
389 */
390 new_C = si->c;
391 new_C.drop_literal(action.Lindex);
392 path = si->p;
393 lemmata = si->l;
394 /*
395 * Extend the stack.
396 */
397 stack.push_back(StackItem(StackItemType::Lemmata, new_C, path,
398 lemmata, current_depth));
399 stack.back().set_this_action(action);
400 break;
401 //----------------------------------------------------------------------
402 //----------------------------------------------------------------------
403 //----------------------------------------------------------------------
404 // Reduction.
405 //----------------------------------------------------------------------
406 //----------------------------------------------------------------------
407 //----------------------------------------------------------------------
408 case InferenceItemType::Reduction:
409 reductions_tried++;
410 /*
411 * If you are restricting backtracking for reductions then
412 * at this point you can remove all alternatives.
413 */
414 if (params::limit_bt_reductions)
415 si->restrict_backtrack();
416 /*
417 * Reductions have a substitution, so apply it and remember
418 * in case you need to undo it later.
419 */
420 action.sigma.apply();
421 sub_stack.push_all(action.sigma);
422 /*
423 * Work out the new state.
424 */
425 new_C = si->c;
426 new_C.drop_literal(action.Lindex);
427 path = si->p;
428 lemmata = si->l;
429 lemmata.push_back(action.L);
430 /*
431 * Extend the stack.
432 */
433 stack.push_back(StackItem(StackItemType::Reduction, new_C, path,
434 lemmata, action.sigma, current_depth));
435 stack.back().set_this_action(action);
436 break;
437 //----------------------------------------------------------------------
438 //----------------------------------------------------------------------
439 //----------------------------------------------------------------------
440 // Extension.
441 //----------------------------------------------------------------------
442 //----------------------------------------------------------------------
443 //----------------------------------------------------------------------
444 case InferenceItemType::Extension:
445 extensions_tried++;
446 /*
447 * You're going to generate new variables, so remember where to
448 * backtrack to.
449 */
450 var_index.add_backtrack_point();
451 /*
452 * This is an Extension, so you're going to add something to
453 * right_branch_stack.
454 */
455 path = si->p;
456 old_C = si->c;
457 old_C.drop_literal(action.Lindex);
458 old_Lem = si->l;
459 old_Lem.push_back(action.L);
460 /*
461 * DON'T do populate_stack_item here! That can wait until you actually
462 * use the right branch. In fact it *has* to wait because we might
463 * apply substitutions that affect it.
464 */
465 right_branch_stack.push_back(StackItem(StackItemType::RightBranch, old_C,
466 path, old_Lem, current_depth));
467 /*
468 * The right branch needs to know where to restrict backtracking.
469 */
470 right_branch_stack.back().set_bt_restriction_index(stack.size() - 1);
471 /*
472 * Now you can deal with the left branch.
473 */
474 new_C = matrix[action.C_2].make_copy_with_new_vars(var_index, term_index);
475 /*
476 * Extensions have a substitution, so apply it and remember
477 * in case you need to undo it later.
478 */
479 action.sigma.apply();
480 sub_stack.push_all(action.sigma);
481 /*
482 * Work out the new state.
483 */
484 new_C.drop_literal(action.Lprime);
485 path.push(action.L);
486 lemmata = si->l;
487 /*
488 * Extend the stack.
489 */
490 stack.push_back(StackItem(StackItemType::LeftBranch, new_C, path,
491 lemmata, action.sigma, current_depth));
492 stack.back().set_this_action(action);
493 break;
494 default:
495 cerr << "PANIC!!! You should only have a lemmata, reduction or an extension here!"
496 << endl;
497 break;
498 }
499 /*
500 * Finally, move si on and work out the next bunch of possible actions.
501 */
502 si = &stack.back();
503 populate_stack_item();
504}
Clause::drop_literal
void drop_literal(LitNum)
Get rid of the specified Literal.
Definition Clause.cpp:135
Lemmata
Representation of the lemma list.
Definition Lemmata.hpp:49
Lemmata::push_back
void push_back(const Literal &)
Self-explanatory.
Definition Lemmata.cpp:28
SimplePath::push
void push(const Literal &)
Add a new Literal to the Path.
Definition SimplePath.cpp:39
StackProver::populate_stack_item
void populate_stack_item()
Fill the vector of possible actions with everything available.
Definition StackProver.cpp:302
Substitution::apply
void apply() const
Apply a substitution everywhere.
Definition Substitution.cpp:56
SubstitutionStack::push_all
void push_all(Substitution &)
Take all the substitutions provided and add the corresponding variables to the stack.
Definition SubstitutionStack.cpp:28
VariableIndex::add_backtrack_point
void add_backtrack_point()
Add a backtrack point.
Definition VariableIndex.cpp:125
InferenceItem::Lindex
LitNum Lindex
The index of the literal within the clause being used.
Definition InferenceItem.hpp:73
InferenceItem::Lprime
LitNum Lprime
The index of the literal in C_2 being used.
Definition InferenceItem.hpp:82
InferenceItem::sigma
Substitution sigma
A copy of the substitution that makes the rule applicable.
Definition InferenceItem.hpp:87
InferenceItem::L
Literal L
The Literal that is used to make the inference.
Definition InferenceItem.hpp:69
InferenceItem::C_2
ClauseNum C_2
For extensions, the number of the clause for which a fresh copy is being made.
Definition InferenceItem.hpp:78
InferenceItem::T
InferenceItemType T
What kind of inference is this?
Definition InferenceItem.hpp:65
StackItem
Stack items: each contains its own stack of possible next inferences.
Definition StackItem.hpp:51
StackItem::restrict_backtrack
void restrict_backtrack()
Adjust the collection of actions to limit backtracking.
Definition StackItem.cpp:51
StackItem::actions
vector< InferenceItem > actions
Actions available to try.
Definition StackItem.hpp:84
StackItem::l
Lemmata l
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the lemmata.
Definition StackItem.hpp:70

◆ get_indexes()

std::tuple< VariableIndex *, FunctionIndex *, PredicateIndex *, TermIndex * > StackProver::get_indexes ( )
inline

Straightforward get method.

Definition at line 365 of file StackProver.hpp.

365 {
366 auto result = std::make_tuple(&var_index, &fun_index, &pred_index, &term_index);
367 return result;
368 }

◆ get_internal_proof()

vector< pair< string, vector< size_t > > > StackProver::get_internal_proof ( ) const

Get an internal representation of the proof stack.

Definition at line 1221 of file StackProver.cpp.

1221 {
1222 return proof_printer.make_internal();
1223}
ProofPrinter::make_internal
vector< pair< string, vector< size_t > > > make_internal() const
Make a simple data structure representing the proof stack.
Definition ProofPrinter.cpp:360

◆ get_matrix()

Matrix & StackProver::get_matrix ( )
inline

Get a reference to the matrix.

Definition at line 445 of file StackProver.hpp.

445 {
446 return matrix;
447 };

◆ get_status()

string StackProver::get_status ( ) const
inline

Straightforward get method.

Definition at line 372 of file StackProver.hpp.

372{ return status; }

◆ go()

ProverResult StackProver::go ( )
private

This runs the proof search from a given Start Move.

Definition at line 659 of file StackProver.cpp.

659 {
660 /*
661 * Having set up a single entry on the stack, containing a start
662 * state, search for a proof.
663 *
664 * Either you return by ending at the start state with nothing left
665 * to try, by finding a proof, by depth limiting or by timing out.
666 *
667 * The backtrack variable is important here - when true you are
668 * (surprise surprise) backtracking. So mostly each case in the
669 * following switch is divided according to whether you're going
670 * forward or backtracking.
671 */
672 while(true) {
673 /*
674 * Test for and deal with a timeout.
675 */
676 if (use_timeout && chrono::steady_clock::now() > end_time)
677 return ProverResult::TimeOut;
678 /*
679 * Say what's going on.
680 */
681 if (output_interval.tick() && params::verbosity >= 2) {
682 cout << cursor_symbols::Cursor::to_column(1);
683 cout << cursor_symbols::Cursor::erase_line(2);
684 cout << "Reductions: " << reductions_tried << " Extensions: " << extensions_tried;
685 cout << " Lemmata: " << lemmata_tried << " Right branches: " << right_branches_started;
686 cout << " Stack size: " << stack.size();
687 cout.flush();
688 }
689 /*
690 * si must point to the back of the stack at this point.
691 *
692 * Remember that extend_with_action will deal with this for you.
693 */
694 switch (si->item_type) {
695 //----------------------------------------------------------------
696 //----------------------------------------------------------------
697 //----------------------------------------------------------------
698 // Deal with the start state. Essentially straightforward. Just
699 // deal with a completed search, otherwise work out the
700 // possibly actions and get on with it.
701 //----------------------------------------------------------------
702 //----------------------------------------------------------------
703 //----------------------------------------------------------------
704 case StackItemType::Start:
705 backtrack = false;
706 if (si->actions.empty())
707 return ProverResult::OptionsExhausted;
708 else
709 extend_with_action();
710 break;
711 //----------------------------------------------------------------
712 //----------------------------------------------------------------
713 //----------------------------------------------------------------
714 // Lemmata. Again, mostly straightforward.
715 //----------------------------------------------------------------
716 //----------------------------------------------------------------
717 //----------------------------------------------------------------
718 case StackItemType::Lemmata:
719 /*
720 * Operation is essentially similar to the reduction case.
721 *
722 * First deal with moving forward.
723 */
724 if (!backtrack) {
725 if (axiom()) {
726 /*
727 * Either you've found a proof or you try a right branch.
728 */
729 if (right_branch_stack.empty())
730 return ProverResult::Valid;
731 else
732 process_axiom_forward();
733 }
734 /*
735 * Backtrack because of depth limiting.
736 */
737 else if (depth_limited())
738 lemmata_backtrack();
739 /*
740 * Backtrack because there's nothing left to try.
741 */
742 else if (si->actions.empty())
743 lemmata_backtrack();
744 /*
745 * There must be something left to try, so try it.
746 */
747 else
748 extend_with_action();
749 }
750 /*
751 * We are moving down the stack.
752 */
753 else {
754 /*
755 * If you're backtracking then you need to jump over axioms.
756 */
757 if (axiom())
758 lemmata_backtrack();
759 /*
760 * If you're not at an axiom then you can start going forward
761 * again.
762 */
763 else
764 backtrack = false;
765 }
766 break;
767 //----------------------------------------------------------------
768 //----------------------------------------------------------------
769 //----------------------------------------------------------------
770 // Reduction. Almost identical to Lemmata, but note the
771 // slightly different backtracking requirement to take account
772 // of undoing the substitution.
773 //----------------------------------------------------------------
774 //----------------------------------------------------------------
775 //----------------------------------------------------------------
776 case StackItemType::Reduction:
777 /*
778 * We are moving up the stack.
779 */
780 if (!backtrack) {
781 if (axiom()) {
782 /*
783 * Either you've found a proof or you try a right branch.
784 */
785 if (right_branch_stack.empty())
786 return ProverResult::Valid;
787 else
788 process_axiom_forward();
789 }
790 /*
791 * Backtrack because of depth limiting.
792 */
793 else if (depth_limited())
794 reduction_backtrack();
795 /*
796 * Backtrack because there's nothing left to try.
797 */
798 else if (si->actions.empty())
799 reduction_backtrack();
800 /*
801 * There must be something left to try, so try it.
802 */
803 else
804 extend_with_action();
805 }
806 /*
807 * We are moving down the stack.
808 */
809 else {
810 /*
811 * If you're backtracking then you need to jump over axioms.
812 */
813 if (axiom())
814 reduction_backtrack();
815 /*
816 * If you're not at an axiom then you can start going forward
817 * again.
818 */
819 else
820 backtrack = false;
821 }
822 break;
823 //----------------------------------------------------------------
824 //----------------------------------------------------------------
825 //----------------------------------------------------------------
826 // Left branch of Extension. Mostly similar to the Reduction
827 // and Lemmata cases, but the backtrack is again different to
828 // take care of the new variables, the substitution, and the
829 // right_branch_stack.
830 //----------------------------------------------------------------
831 //----------------------------------------------------------------
832 //----------------------------------------------------------------
833 case StackItemType::LeftBranch:
834 /*
835 * Operation is essentially similar to the Reduction and
836 * Lemmata cases. See those for corresponding comments.
837 */
838 if (!backtrack) {
839 if (axiom())
840 process_axiom_forward();
841 else if (depth_limited())
842 left_extension_backtrack();
843 else if (si->actions.empty())
844 left_extension_backtrack();
845 else
846 extend_with_action();
847 }
848 /*
849 * We are moving down the stack.
850 */
851 else {
852 if (axiom())
853 left_extension_backtrack();
854 else
855 backtrack = false;
856 }
857 break;
858 //----------------------------------------------------------------
859 //----------------------------------------------------------------
860 //----------------------------------------------------------------
861 // Right branch of Extension. Mostly similar to the Reduction
862 // and Lemmata cases, but the backtrack is now much more
863 // delicate. See the documentation for right_extension_backtrack.
864 //----------------------------------------------------------------
865 //----------------------------------------------------------------
866 //----------------------------------------------------------------
867 case StackItemType::RightBranch:
868 /*
869 * Operation is essentially similar to the reduction case.
870 */
871 if (!backtrack) {
872 if (axiom()) {
873 if (right_branch_stack.empty())
874 return ProverResult::Valid;
875 else
876 process_axiom_forward();
877 }
878 else if (depth_limited())
879 right_extension_backtrack();
880 else if (si->actions.empty())
881 right_extension_backtrack();
882 else
883 extend_with_action();
884 }
885 /*
886 * We are moving down the stack.
887 */
888 else {
889 if (axiom())
890 right_extension_backtrack();
891 else
892 backtrack = false;
893 }
894 break;
895 //----------------------------------------------------------------
896 default:
897 cerr << "Something is VERY WRONG!" << endl;
898 break;
899 }
900 }
901 return ProverResult::Error;
902}
Interval::tick
bool tick()
Definition Interval.hpp:54
StackProver::process_axiom_forward
void process_axiom_forward()
Start a right branch to continue from an axiom.
Definition StackProver.cpp:506
StackProver::lemmata_backtrack
void lemmata_backtrack()
One of several different kinds of backtracking.
Definition StackProver.cpp:562
StackProver::extend_with_action
void extend_with_action()
Take a single inference (action) and update the stacks accordingly.
Definition StackProver.cpp:356
StackProver::depth_limited
bool depth_limited()
Test for the depth limit.
Definition StackProver.cpp:343
StackProver::left_extension_backtrack
void left_extension_backtrack()
One of several different kinds of backtracking.
Definition StackProver.cpp:566
StackProver::right_extension_backtrack
void right_extension_backtrack()
One of several different kinds of backtracking.
Definition StackProver.cpp:597
StackProver::reduction_backtrack
void reduction_backtrack()
One of several different kinds of backtracking.
Definition StackProver.cpp:557
StackProver::axiom
bool axiom() const
Test to see if you're at an axiom.
Definition StackProver.cpp:352
cursor_symbols::Cursor::erase_line
static string erase_line(uint8_t n)
Definition cursor.hpp:157
StackItem::item_type
StackItemType item_type
What type of StackItem is this?
Definition StackItem.hpp:55

◆ left_extension_backtrack()

void StackProver::left_extension_backtrack ( )
private

One of several different kinds of backtracking.

Definition at line 566 of file StackProver.cpp.

566 {
567 /*
568 * You're backtracking through a left branch, so you
569 * need to remember to get rid of the corresponding
570 * right branch as well.
571 */
572 right_branch_stack.pop_back();
573 var_index.backtrack();
574 sub_stack.backtrack();
575 backtrack_once();
576}
StackProver::backtrack_once
void backtrack_once()
Basic, single step backtrack on the stack.
Definition StackProver.cpp:550
SubstitutionStack::backtrack
void backtrack()
Remove variables from the stack, and remove substitutions as you go, as far back as the most recent b...
Definition SubstitutionStack.cpp:36
VariableIndex::backtrack
void backtrack()
Backtrack to the last marker.
Definition VariableIndex.cpp:134

◆ lemmata_backtrack()

void StackProver::lemmata_backtrack ( )
private

One of several different kinds of backtracking.

Definition at line 562 of file StackProver.cpp.

562 {
563 backtrack_once();
564}

◆ populate_stack_item()

void StackProver::populate_stack_item ( )
private

Fill the vector of possible actions with everything available.

Definition at line 302 of file StackProver.cpp.

302 {
303 /*
304 * Don't waste your time if the regularity test applies.
305 */
306 if (params::use_regularity_test && !path.test_for_regularity(new_C))
307 return;
308 /*
309 * Don't try to populate axioms.
310 */
311 if (new_C.size() == 0) {
312 return;
313 }
314 /*
315 * NOTE: As these are being stacked, lemmata are actually tried
316 * first.
317 */
318 /*
319 * Extensions
320 */
321 if (params::limit_extensions)
322 matrix.find_limited_extensions(u, si->actions, new_C, var_index, term_index);
323 else
324 matrix.find_all_extensions(u, si->actions, new_C, var_index, term_index);
325 /*
326 * Reductions
327 */
328 if (params::limit_reductions)
329 path.find_limited_reductions(u, si->actions, new_C);
330 else
331 path.find_all_reductions(u, si->actions, new_C);
332 /*
333 * Lemmata
334 */
335 if (params::use_lemmata) {
336 if (params::limit_lemmata)
337 lemmata.find_initial_lemmata(si->actions, new_C);
338 else
339 lemmata.find_all_lemmata(si->actions, new_C);
340 }
341}
Clause::size
size_t size() const
Straightforward get method.
Definition Clause.hpp:78
Lemmata::find_initial_lemmata
void find_initial_lemmata(vector< InferenceItem > &, Clause &)
Find all lemmata that are applicable, but only for the initial Literal in a Clause.
Definition Lemmata.cpp:33
Lemmata::find_all_lemmata
void find_all_lemmata(vector< InferenceItem > &, Clause &)
Find all lemmata that are applicable, given a Clause.
Definition Lemmata.cpp:56
Matrix::find_limited_extensions
void find_limited_extensions(Unifier &, vector< InferenceItem > &, Clause &, VariableIndex &, TermIndex &)
Find all possible extensions given a Clause, but only consider the first Literal in the Clause.
Definition Matrix.cpp:212
Matrix::find_all_extensions
void find_all_extensions(Unifier &, vector< InferenceItem > &, Clause &, VariableIndex &, TermIndex &)
Find all possible extensions given a Clause, considering all Literals in the Clause.
Definition Matrix.cpp:222
SimplePath::test_for_regularity
bool test_for_regularity(Clause &) const
Regularity test.
Definition SimplePath.cpp:64
SimplePath::find_limited_reductions
void find_limited_reductions(Unifier &, vector< InferenceItem > &, Clause &)
Given a Clause, find all possible reductions given the current Path, but only for the first Literal i...
Definition SimplePath.cpp:102
SimplePath::find_all_reductions
void find_all_reductions(Unifier &, vector< InferenceItem > &, Clause &)
Given a Clause, find all possible reductions given the current Path.
Definition SimplePath.cpp:115

◆ problem_has_false_conjecture()

bool StackProver::problem_has_false_conjecture ( ) const
inline

Find out whether the problem's conjecture
is $false.

Definition at line 466 of file StackProver.hpp.

466 {
467 return conjecture_false;
468 }

◆ problem_has_fof_axioms()

bool StackProver::problem_has_fof_axioms ( ) const
inline

Find out from the parser whether the problem had axioms before simplification.

Definition at line 488 of file StackProver.hpp.

488 {
489 return fof_has_axioms;
490 }

◆ problem_has_missing_conjecture()

bool StackProver::problem_has_missing_conjecture ( ) const
inline

Find out whether the problem's conjecture
is missing, in the sense that it didn't appear in the input file.

Definition at line 474 of file StackProver.hpp.

474 {
475 return conjecture_missing;
476 }

◆ problem_has_negated_conjecture_removed()

bool StackProver::problem_has_negated_conjecture_removed ( ) const
inline

Find out whether the problem's
negated conjecture was simplified out.

Definition at line 481 of file StackProver.hpp.

481 {
482 return negated_conjecture_removed;
483 }

◆ problem_has_true_conjecture()

bool StackProver::problem_has_true_conjecture ( ) const
inline

Find out whether the problem's conjecture
is $true.

Definition at line 459 of file StackProver.hpp.

459 {
460 return conjecture_true;
461 }

◆ problem_is_cnf_only()

bool StackProver::problem_is_cnf_only ( ) const
inline

Find out whether the problem is CNF only.

Definition at line 452 of file StackProver.hpp.

452 {
453 return cnf_only;
454 }

◆ process_axiom_forward()

void StackProver::process_axiom_forward ( )
private

Start a right branch to continue from an axiom.

You do this by taking the next available thing from the stack of right branches.

Definition at line 506 of file StackProver.cpp.

506 {
507 /*
508 * When you're moving forward in the search and you hit an axiom,
509 * you need to see whether there are right branches still needing
510 * to be dealt with.
511 *
512 * Note that an empty right_branch_stack - meaning that you've
513 * found a proof - is dealt with by go().
514 *
515 * this_action does not get populated for the new StackItem in
516 * this case.
517 */
518 right_branches_started++;
519 /*
520 * Move the next right branch to the stack.
521 */
522 stack.push_back(right_branch_stack.back());
523 right_branch_stack.pop_back();
524 /*
525 * Reset si.
526 */
527 si = &stack.back();
528 /*
529 * Set up the new state.
530 */
531 new_C = si->c;
532 path = si->p;
533 lemmata = si->l;
534 current_depth = si->depth;
535 /*
536 * We deliberately delayed doing this, so do it now. (See
537 * documentation for StackProver::extend_with_action.)
538 */
539 populate_stack_item();
540 /*
541 * At this point you are starting a right branch, so
542 * if you are restricting backtracking you remove all
543 * alternatives from the relevant point in the stack.
544 */
545 if (params::limit_bt_extensions) {
546 stack[si->bt_restriction_index].restrict_backtrack();
547 }
548}
StackItem::bt_restriction_index
size_t bt_restriction_index
Pointer that allows a right branch to know where to delete alternatives for restricted backtracking.
Definition StackItem.hpp:101

◆ prove()

ProverOutcome StackProver::prove ( )

Here is where the magic happens.

You should only need to load the problem and call this method.

Definition at line 1039 of file StackProver.cpp.

1039 {
1040 pair<bool, size_t> start_clause = matrix.find_start();
1041 /*
1042 * If the initial clauses don't have a positive and a negative
1043 * clause then the problem is trivial.
1044 */
1045 if (!start_clause.first) {
1046 return ProverOutcome::False;
1047 }
1048 /*
1049 * Deal with the possible ways to set up start clause(s) according to
1050 * the options. Keep track of which start clauses are in use, and if
1051 * necessary what outcomes for them have been seen so far.
1052 */
1053 set_up_start_clauses();
1054 /*
1055 * Main loop for iterative deepening search.
1056 */
1057 bool switched_to_complete = false;
1058 for (current_depth_limit = params::start_depth;
1059 current_depth_limit <= params::depth_limit;
1060 current_depth_limit += params::depth_increment) {
1061 /*
1062 * See if the parameters dictate that it's time to convert to
1063 * a complete search.
1064 */
1065 if (current_depth_limit >= params::switch_to_complete
1066 && !switched_to_complete) {
1067 params::set_complete_parameters();
1068 /*
1069 * You may have changed some parameters, so make sure all relevant
1070 * start clauses now get tried.
1071 */
1072 set_up_start_clauses();
1073 current_depth_limit = params::start_depth;
1074 switched_to_complete = true;
1075 colour_string::ColourString cs(params::use_colours);
1076 show.nl(1);
1077 show(1, cs("Switching to complete search.").orange(), true);
1078 }
1079 show.nl(1);
1080 show(1, string("SEARCH TO DEPTH: "));
1081 show(1, std::to_string(current_depth_limit), true);
1082 /*
1083 * Generate each possible start move, and try to prove from
1084 * it.
1085 */
1086 size_t start_clause_index = 0;
1087 for (const Clause& C : matrix) {
1088 /*
1089 * Find the next start clause.
1090 */
1091 if (results[start_clause_index] == StartClauseStatus::NoStart
1092 || results[start_clause_index] == StartClauseStatus::False) {
1093 start_clause_index++;
1094 continue;
1095 }
1096 /*
1097 * Reset everything to use the current start clause.
1098 *
1099 * TODO: this is slightly messy at present because
1100 * the var_index doesn't necessarily get reset in the
1101 * most efficient way possible if a previous schedule
1102 * attempt timed out. (You'd need to go back down
1103 * the stack and backtrack it as necessary.) This is
1104 * of course irrelevant
1105 * because it just means you might not get full re-use of
1106 * new variable names, but all the same it would be nice
1107 * to fix.
1108 */
1109 var_index.add_backtrack_point();
1110 new_C = C.make_copy_with_new_vars(var_index, term_index);
1111 reset_for_start();
1112 /*
1113 * Say what's going on.
1114 */
1115 show(1, string("START from clause "));
1116 show(1, std::to_string(start_clause_index + 1));
1117 show(1, string(" of "));
1118 show(1, std::to_string(matrix.get_num_clauses()));
1119 show(2, string(": "));
1120 show(2, new_C.to_string(), true);
1121 cout.flush();
1122 /*
1123 * Set up the initial stack item containing the start clause, and
1124 * populate it.
1125 */
1126 StackItem start_item(StackItemType::Start, new_C, path, lemmata, 1);
1127 start_item.set_this_action(InferenceItem(InferenceItemType::Start, start_clause_index));
1128 stack.push_back(start_item);
1129 si = &stack.back();
1130 populate_stack_item();
1131 /*
1132 * Start with depth 1, as this makes sense when reading output if you're
1133 * using depth of recursion or path length.
1134 */
1135 current_depth = 1;
1136 /*
1137 * Liftoff!!!
1138 */
1139 ProverResult result = go();
1140 /*
1141 * Dealing with the outcome takes some care and depends on
1142 * the parameters being used.
1143 */
1144 switch (result) {
1145 case ProverResult::Valid:
1146 proof_count++;
1147 if (params::build_proof) {
1148 if (params::generate_LaTeX_proof) {
1149 proof_printer.make_LaTeX(params::LaTeX_proof_path,
1150 problem_path,
1151 matrix.make_LaTeX());
1152 }
1153 if (params::generate_Prolog_proof) {
1154 fs::path prolog_path = params::Prolog_proof_path;
1155 proof_printer.make_Prolog(prolog_path);
1156 }
1157 }
1158 show(1, string(": Found proof number "));
1159 show(1, std::to_string(proof_count), true);
1160 return ProverOutcome::Valid;
1161 break;
1162 case ProverResult::Error:
1163 return ProverOutcome::Error;
1164 break;
1165 case ProverResult::TimeOut:
1166 return ProverOutcome::TimeOut;
1167 break;
1168 case ProverResult::OptionsExhausted:
1169 /*
1170 * If you ran out of options because you reached the depth
1171 * limit then you still need to continue.
1172 */
1173 if (depth_limit_reached) {
1174 show(1, string(": Depth limited"), true);
1175 }
1176 /*
1177 * If you ran out of options without reaching the depth limit, then
1178 * what you do depends on whether or not the search is complete.
1179 */
1180 else {
1181 if (params::search_is_complete()) {
1182 results[start_clause_index] = StartClauseStatus::False;
1183 show(1, string(": False"), true);
1184 }
1185 }
1186 start_clause_index++;
1187 break;
1188 default:
1189 return ProverOutcome::Error;
1190 break;
1191 }
1192 /*
1193 * This is necessary. Yes, I've checked. Think about it: you need
1194 * one extra backtrack to undo the new variables generated when you
1195 * make a start clause.
1196 */
1197 var_index.backtrack();
1198 }
1199 /*
1200 * Loop for start moves ends here.
1201 *
1202 * If everything was False then the theorem is False, otherwise
1203 * at least one attempt was depth-limited.
1204 */
1205 bool all_false = true;
1206 for (StartClauseStatus& outcome : results) {
1207 if (outcome == StartClauseStatus::Start) {
1208 all_false = false;
1209 break;
1210 }
1211 }
1212 if (all_false)
1213 return ProverOutcome::False;
1214 }
1215 /*
1216 * Iterative deepening loop ends here.
1217 */
1218 return ProverOutcome::PathLenLimit;
1219}
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::to_string
string to_string(bool=false) const
Convert to a string.
Definition Clause.cpp:202
Matrix::get_num_clauses
ClauseNum get_num_clauses() const
Straightforward get method.
Definition Matrix.hpp:191
Matrix::make_LaTeX
string make_LaTeX(bool=false) const
Make a usable LaTeX representation.
Definition Matrix.cpp:257
Matrix::find_start
pair< bool, size_t > find_start() const
Use a simple heuristic to find a good start clause.
Definition Matrix.cpp:51
ProofPrinter::make_Prolog
void make_Prolog(const path &)
Convert to a form suitable for use by the Prolog proof checker and write to a file.
Definition ProofPrinter.cpp:189
ProofPrinter::make_LaTeX
void make_LaTeX(const path &, const path &, const string &)
Convert to LaTeX and store in the specified file.
Definition ProofPrinter.cpp:116
StackProver::reset_for_start
void reset_for_start()
Reset everything so that you can start from a specified start clause.
Definition StackProver.hpp:309
StackProver::set_up_start_clauses
void set_up_start_clauses()
The start clauses to use depend on the settings, and the settings can change.
Definition StackProver.cpp:912
StackProver::go
ProverResult go()
This runs the proof search from a given Start Move.
Definition StackProver.cpp:659
colour_string::ColourString
Simple addition of colour to strings and ostreams.
Definition vic_strings.hpp:118
verbose_print::VPrint::nl
void nl(uint8_t, uint8_t=1)
Definition vic_strings.cpp:140
InferenceItem
Full representation of inferences, beyond just the name.
Definition InferenceItem.hpp:61
params::set_complete_parameters
static void set_complete_parameters()
Change the parameters to make the search complete.
Definition Parameters.cpp:180
params::search_is_complete
static bool search_is_complete()
Self-explanatory.
Definition Parameters.cpp:192

◆ random_reorder()

void StackProver::random_reorder ( )
inline

Randomly reorder the matrix.

Definition at line 432 of file StackProver.hpp.

432 {
433 matrix.random_reorder();
434 }
Matrix::random_reorder
void random_reorder()
Randomly reorder the matrix.
Definition Matrix.cpp:136

◆ read_from_tptp_file()

void StackProver::read_from_tptp_file ( const string &  file_name,
bool &  found_conjecture,
size_t &  fof_size 
)

Obviously, reads a problem from a TPTP file.

Does pretty much all of the setup required.

Parameters
file_nameName of the file to use.
found_conjectureUsed to indicate whether a conjecture is found in the problem.
fof_sizeNumber of first-order formulas found.

Definition at line 76 of file StackProver.cpp.

78 {
79 TPTPParser parser(&var_index, &fun_index, &term_index, &pred_index, &matrix);
80 parser.parse_tptp_from_file(file_name);
81 status = parser.get_problem_status();
82 bool equality = parser.equality_used();
83 found_conjecture = parser.conjecture_present();
84 fof_size = parser.number_of_fof_formulas();
85 Predicate* equals_predicate = parser.get_equals_predicate();
86 cnf_only = parser.problem_is_cnf_only();
87 conjecture_true = parser.fof_conjecture_is_true();
88 conjecture_false = parser.fof_conjecture_is_false();
89 conjecture_missing = parser.fof_conjecture_is_missing();
90 negated_conjecture_removed = parser.fof_negated_conjecture_removed();
91 fof_has_axioms = parser.fof_has_axioms();
92 simplified_fof_has_axioms = parser.simplified_fof_has_axioms();
93 parser.clear();
94 num_preds = pred_index.get_num_preds();
95 /*
96 * num_preds for Matrix is set by parser.
97 */
98 path.set_num_preds(num_preds);
99
100 if (params::show_clauses) {
101 std::exit(EXIT_SUCCESS);
102 }
103
104 if (status != string("")) {
105 show(1, string("Problem status found: "));
106 show(1, status, true);
107 }
108 if (equality && params::add_equality_axioms) {
109 show(1, string("Problem involves equality: adding axioms for =."), true);
110 add_equality_axioms(equals_predicate);
111 if (params::equality_axioms_at_start) {
112 matrix.move_equals_to_start();
113 }
114 }
115 /*
116 * Any further variables will be anonymous.
117 */
118 var_index.set_all_names_added();
119
120 if (params::generate_Prolog_proof && params::build_proof) {
121 matrix.write_to_prolog_file(params::Prolog_matrix_path);
122 }
123 }
Matrix::move_equals_to_start
void move_equals_to_start()
Self-explanatory.
Definition Matrix.cpp:167
Matrix::write_to_prolog_file
void write_to_prolog_file(const path &) const
Write to a file that can be read by Prolog.
Definition Matrix.cpp:270
SimplePath::set_num_preds
void set_num_preds(size_t num_predicates)
Set method for num_predicates.
Definition SimplePath.hpp:101
StackProver::add_equality_axioms
void add_equality_axioms(Predicate *)
After reading a problem in which = and/or != appears, add the axioms for equality.
Definition StackProver.cpp:125
TPTPParser
Wrap up everything the TPTP parser needs to do inside a single class.
Definition TPTPParser.hpp:658
VariableIndex::set_all_names_added
void set_all_names_added()
Call this to indicate that only anonymous variables can now be created.
Definition VariableIndex.cpp:63

◆ reduction_backtrack()

void StackProver::reduction_backtrack ( )
private

One of several different kinds of backtracking.

Definition at line 557 of file StackProver.cpp.

557 {
558 sub_stack.backtrack();
559 backtrack_once();
560}

◆ reset_for_start()

void StackProver::reset_for_start ( )
inlineprivate

Reset everything so that you can start from a specified start clause.

Definition at line 309 of file StackProver.hpp.

309 {
310 depth_limit_reached = false;
311 si = nullptr;
312 backtrack = false;
313 path.clear();
314 stack.clear();
315 lemmata.clear();
316 right_branch_stack.clear();
317 sub_stack.clear();
318 }
Lemmata::clear
void clear()
Self-explanatory.
Definition Lemmata.hpp:70
SimplePath::clear
void clear()
evert to the empty state without changing num_preds.
Definition SimplePath.cpp:34
SubstitutionStack::clear
void clear()
Reset everything.
Definition SubstitutionStack.hpp:91

◆ right_extension_backtrack()

void StackProver::right_extension_backtrack ( )
private

One of several different kinds of backtracking.

Here be DRAGONS.

Care needed here. If the state is a right branch, then it may or may not have to go back on right_branch_stack as you may or may not need to try it again, depending on the settings.

If you get this wrong you get a REALLY evil bug, because with the standard restricted backtracking you put it back on the stack when it's not needed. You then end up with extra things in the proof certificate which invalidate it, even though you can take them out and possibly get something valid.

Guess how I know this!

TODO: when I implement params::hard_prune it needs to be considered here.

Definition at line 597 of file StackProver.cpp.

597 {
598 /*
599 * If you're not limiting backtracking for extensions, or
600 * you *are*, but you're still exploring left trees, then this
601 * is straightforward: just put the item back on right_branch_stack
602 * so that it gets explored again later.
603 */
604 if (!params::limit_bt_extensions ||
605 ((params::limit_bt_extensions || params::limit_bt_all) &&
606 !params::limit_bt_extensions_left_tree)) {
607 /*
608 * Why is this necessary? After we backtrack we may make different
609 * substitutions, so in revisiting the right branch different
610 * possibilties may apply, so we re-compute them later.
611 */
612 stack.back().clear();
613 right_branch_stack.push_back(stack.back());
614 backtrack_once();
615 return;
616 }
617 /*
618 * We know we are limiting backtracking for extensions, and we
619 * are not exploring the left tree.
620 *
621 * Care is needed if you're not backtracking within the left
622 * part of the tree. You need to move back down the stack,
623 * deleting everything while also making sure that sub_stack
624 * and var_index are correctly maintained. Also, you don't
625 * want to return anything to right_branch_stack.
626 *
627 * This goes back to where the relevant literal was selected.
628 * Thus if you are not limiting the possibilities to only those
629 * for the first literal, it's open to the backtracking
630 * restriction to leave other possibilites to be tried, and
631 * they get picked up from this point.
632 */
633 if (params::limit_bt_extensions_left_tree) {
634 size_t target_index = si->bt_restriction_index;
635 size_t current_index = stack.size() - 1;
636 while (current_index > target_index) {
637 switch (si->item_type) {
638 case StackItemType::Lemmata:
639 break;
640 case StackItemType::Reduction:
641 sub_stack.backtrack();
642 break;
643 case StackItemType::LeftBranch:
644 var_index.backtrack();
645 sub_stack.backtrack();
646 break;
647 case StackItemType::RightBranch:
648 break;
649 default:
650 cerr << "Something is VERY WRONG!" << endl;
651 break;
652 }
653 backtrack_once();
654 current_index--;
655 }
656 }
657}

◆ set_num_preds()

void StackProver::set_num_preds ( size_t  n)

Set the number of predicates.

But don't! You should never need to do this.

Definition at line 70 of file StackProver.cpp.

70 {
71 num_preds = n;
72 matrix.set_num_preds(n);
73 path.set_num_preds(n);
74}
Matrix::set_num_preds
void set_num_preds(size_t)
Make an empty index.
Definition Matrix.cpp:42

◆ set_problem_path()

void StackProver::set_problem_path ( fs::path &  p)
inline

Set the path for the problem being solved. U.

Used only to produce nice output.

Definition at line 393 of file StackProver.hpp.

393{ problem_path = p; }

◆ set_timeout()

void StackProver::set_timeout ( chrono::steady_clock::time_point  time)
inline

Set a timeout.

A StackProver is always constructed to have no timeout. This sets a timeout to use in seconds. The parameters are separate from the params::???? values as the latter apply globally whereas these allow for schedules to be constructed.

Parameters
timethe time to stop: you will need to know about the standard library!

Definition at line 384 of file StackProver.hpp.

384 {
385 use_timeout = true;
386 end_time = time;
387 }

◆ set_up_start_clauses()

void StackProver::set_up_start_clauses ( )
private

The start clauses to use depend on the settings, and the settings can change.

Definition at line 912 of file StackProver.cpp.

912 {
913 results.clear();
914 size_t m_size = matrix.get_num_clauses();
915 /*
916 * Make sure noone has messed up and not set any start
917 * clause optionss.
918 */
919 if (params::no_start_options())
920 params::correct_missing_start_options();
921 /*
922 * The allstart option overides everything else so this is easy.
923 */
924 if (params::all_start) {
925 for (size_t i = 0; i < m_size; i++) {
926 results.push_back(StartClauseStatus::Start);
927 }
928 return;
929 }
930 bool first_clause_included = false;
931 /*
932 * params::all_pos_neg_start indicates use of positive
933 * or negative start clauses according to the representation.
934 * When you don't also have conjecture_start, either include
935 * all, or just the first possibility found.
936 */
937 if (params::all_pos_neg_start && !params::conjecture_start) {
938 for (size_t i = 0; i < m_size; i++) {
939 if (
940 (
941 (params::positive_representation && matrix.is_positive(i))
942 ||
943 (!params::positive_representation && matrix.is_negative(i))
944 )
945 &&
946 (!(params::restrict_start && first_clause_included))
947 ) {
948 results.push_back(StartClauseStatus::Start);
949 first_clause_included = true;
950 }
951 else {
952 results.push_back(StartClauseStatus::NoStart);
953 }
954 }
955 }
956 /*
957 * Similar case if you have conjecture_start but not all_pos_neg_start.
958 */
959 else if (!params::all_pos_neg_start && params::conjecture_start) {
960 for (size_t i = 0; i < m_size; i++) {
961 if (matrix.is_conjecture(i)
962 &&
963 (!(params::restrict_start && first_clause_included))) {
964 results.push_back(StartClauseStatus::Start);
965 first_clause_included = true;
966 }
967 else {
968 results.push_back(StartClauseStatus::NoStart);
969 }
970 }
971 }
972 /*
973 * The tricky case is when you want to combine pos/neg clauses,
974 * conjecture clauses, and restriction in some other way.
975 *
976 * Assume here that you have all_pos_neg_start and conjecture_start.
977 */
978 else {
979 for (size_t i = 0; i < m_size; i++) {
980 if (matrix.is_conjecture(i)
981 &&
982 (
983 (params::positive_representation && matrix.is_positive(i))
984 ||
985 (!params::positive_representation && matrix.is_negative(i))
986 )
987 &&
988 !(params::restrict_start && first_clause_included)) {
989 results.push_back(StartClauseStatus::Start);
990 first_clause_included = true;
991 }
992 else {
993 results.push_back(StartClauseStatus::NoStart);
994 }
995 }
996 }
997 /*
998 * There's a rare possibility that---because either there was no
999 * (negated) conjecture clause in the problem, or they were
1000 * simplified out---at this point no start clause has been
1001 * selected. If that's the case, either use all positive/negative
1002 * clauses or just the first, according to the parameters set.
1003 *
1004 * Note: this must choose at least one start clause because problems
1005 * without a positive and negative clause have already been solved.
1006 */
1007 if (!first_clause_included) {
1008 if (params::verbosity > 2) {
1009 cout << "Note: you're asking for a conjecture to start, but there are none!" << endl;
1010 cout << " depending on the other parameter settings, we will use one or " << endl;
1011 cout << " all of the negative clauses." << endl;
1012 }
1013 // Don't forget this! If you get here you have a whole bunch of
1014 // NoStart in results!
1015 results.clear();
1016 for (size_t i = 0; i < m_size; i++) {
1017 if ((
1018 (params::positive_representation && matrix.is_positive(i))
1019 ||
1020 (!params::positive_representation && matrix.is_negative(i))
1021 ) &&
1022 !(params::restrict_start && first_clause_included)) {
1023 results.push_back(StartClauseStatus::Start);
1024 first_clause_included = true;
1025 }
1026 else {
1027 results.push_back(StartClauseStatus::NoStart);
1028 }
1029 }
1030 }
1031}
Matrix::is_negative
bool is_negative(size_t i) const
Is a particular Clause negative?.
Definition Matrix.hpp:211
Matrix::is_conjecture
bool is_conjecture(size_t i) const
Is a particular Clause a conjecture?
Definition Matrix.cpp:46
Matrix::is_positive
bool is_positive(size_t i) const
Is a particular Clause positive?.
Definition Matrix.hpp:205
params::no_start_options
static bool no_start_options()
Self-explanatory.
Definition Parameters.cpp:212
params::correct_missing_start_options
static void correct_missing_start_options()
Self-explanatory.
Definition Parameters.cpp:219

◆ show_matrix() [1/2]

void StackProver::show_matrix ( )
inline

Show a nicely formatted matrix.

Definition at line 438 of file StackProver.hpp.

438 {
439 cout << "Matrix:" << endl;
440 cout << matrix.to_string() << endl;
441 }
Matrix::to_string
string to_string() const
Make a string representation.
Definition Matrix.cpp:234

◆ show_matrix() [2/2]

void StackProver::show_matrix ( ) const
inline

Definition at line 522 of file StackProver.hpp.

522{ cout << matrix << endl; }

◆ show_path()

void StackProver::show_path ( ) const
inline

Definition at line 523 of file StackProver.hpp.

523{ cout << path << endl; }

◆ show_right_stack()

void StackProver::show_right_stack ( )

Definition at line 1235 of file StackProver.cpp.

1235 {
1236 cout << "--------------------------------------------------------" << endl;
1237 cout << "Right Stack:" << endl;
1238 cout << "--------------------------------------------------------" << endl;
1239 for (auto s : right_branch_stack) {
1240 cout << s << endl;
1241 }
1242 cout << "--------------------------------------------------------" << endl;
1243}

◆ show_stack()

void StackProver::show_stack ( )

Definition at line 1225 of file StackProver.cpp.

1225 {
1226 cout << "--------------------------------------------------------" << endl;
1227 cout << "Stack:" << endl;
1228 cout << "--------------------------------------------------------" << endl;
1229 for (auto s : stack) {
1230 cout << s << endl;
1231 }
1232 cout << "--------------------------------------------------------" << endl;
1233}

◆ show_statistics()

void StackProver::show_statistics ( ) const

Definition at line 1245 of file StackProver.cpp.

1245 {
1246 verbose_print::VPrint show(params::verbosity);
1247 show(1, string("Reductions: "));
1248 show(1, std::to_string(reductions_tried));
1249 show(1, string(" Extensions: "));
1250 show(1, std::to_string(extensions_tried));
1251 show(1, string(" Lemmata: "));
1252 show(1, std::to_string(lemmata_tried));
1253 show(1, string(" Right branches: "));
1254 show(1, std::to_string(right_branches_started), true);
1255}
verbose_print::VPrint
Definition vic_strings.hpp:238

◆ show_term_index()

void StackProver::show_term_index ( )
inline

Definition at line 526 of file StackProver.hpp.

526{ cout << term_index << endl; }

◆ show_tptp_proof()

void StackProver::show_tptp_proof ( )
inline

Show a Prolog-formatted proof.

Definition at line 501 of file StackProver.hpp.

501 {
502 cout << endl << "% Problem matrix:" << endl;
503 matrix.show_tptp();
504 cout << endl << "% Proof stack:" << endl;
505 proof_printer.show_tptp();
506 }
Matrix::show_tptp
void show_tptp() const
Output in TPTP compatible format.
Definition Matrix.cpp:287
ProofPrinter::show_tptp
void show_tptp()
Show the proof in a TPTP-friendly format.
Definition ProofPrinter.cpp:303

◆ simplified_problem_has_fof_axioms()

bool StackProver::simplified_problem_has_fof_axioms ( ) const
inline

Find out from the parser whether the problem had axioms after simplification.

Definition at line 495 of file StackProver.hpp.

495 {
496 return simplified_fof_has_axioms;
497 }

Friends And Related Symbol Documentation

◆ operator<<

ostream & operator<< ( ostream &  out,
const StackProver &  p 
)
friend

Definition at line 1257 of file StackProver.cpp.

1257 {
1258 out << "Current state of the RecursiveProver object" << endl;
1259 out << "-------------------------------------------" << endl << endl;
1260 out << p.var_index << endl;
1261 out << p.fun_index << endl;
1262 out << p.term_index << endl;
1263 out << p.path << endl;
1264 out << p.matrix << endl;
1265 return out;
1266}

Member Data Documentation

◆ action

InferenceItem StackProver::action
private

Stores the next action from the current StackItem.

Definition at line 146 of file StackProver.hpp.

◆ backtrack

bool StackProver::backtrack
private

Are we moving up or down the stack?

Definition at line 187 of file StackProver.hpp.

◆ cnf_only

bool StackProver::cnf_only
private

Keep track of whether there were any FOF formulas in the problem file.

Definition at line 323 of file StackProver.hpp.

◆ conjecture_false

bool StackProver::conjecture_false
private

Keep track of whether the parser found the conjecture to be false.

Definition at line 331 of file StackProver.hpp.

◆ conjecture_missing

bool StackProver::conjecture_missing
private

Keep track of whether the parser found a conjecture in the problem file.

Definition at line 335 of file StackProver.hpp.

◆ conjecture_true

bool StackProver::conjecture_true
private

Keep track of whether the parser found the conjecture to be true.

Definition at line 327 of file StackProver.hpp.

◆ current_depth

uint32_t StackProver::current_depth
private

Self-explanatary.

Definition at line 164 of file StackProver.hpp.

◆ current_depth_limit

uint32_t StackProver::current_depth_limit
private

Self-explanatary.

Definition at line 160 of file StackProver.hpp.

◆ depth_limit_reached

bool StackProver::depth_limit_reached
private

Self-explanatary.

Definition at line 168 of file StackProver.hpp.

◆ end_time

chrono::steady_clock::time_point StackProver::end_time
private

When do we stop because of a timeout?

Definition at line 236 of file StackProver.hpp.

◆ extensions_tried

uint32_t StackProver::extensions_tried
private

We'll be keeping some simple statistics about the search process.

Definition at line 213 of file StackProver.hpp.

◆ fof_has_axioms

bool StackProver::fof_has_axioms
private

Keep track of whether the parser found that it's an FOF problem with axioms before simplification.

Definition at line 344 of file StackProver.hpp.

◆ fun_index

FunctionIndex StackProver::fun_index
private

This class needs one of each kind of index to keep track of Variables, Terms etc.

Definition at line 90 of file StackProver.hpp.

◆ lemmata

Lemmata StackProver::lemmata
private

At any point in the search process this is a copy of the list of lemmata for the current node in the proof being constructed.

Definition at line 138 of file StackProver.hpp.

◆ lemmata_tried

uint32_t StackProver::lemmata_tried
private

We'll be keeping some simple statistics about the search process.

Definition at line 218 of file StackProver.hpp.

◆ matrix

Matrix StackProver::matrix
private

A copy of the matrix you're working with.

Definition at line 120 of file StackProver.hpp.

◆ negated_conjecture_removed

bool StackProver::negated_conjecture_removed
private

Keep track of whether the parser simplified the conjecture away.

Definition at line 339 of file StackProver.hpp.

◆ new_C

Clause StackProver::new_C
private

At any point in the search process this is a copy of the clause for the current node in the proof being constructed.

Definition at line 132 of file StackProver.hpp.

◆ num_preds

size_t StackProver::num_preds
private

How many prdicates does the problem of interest have?

Definition at line 80 of file StackProver.hpp.

◆ output_interval

Interval StackProver::output_interval
private

How often do you output updates about progress?

Definition at line 200 of file StackProver.hpp.

◆ path

SimplePath StackProver::path
private

At any point in the search process this is a copy of the path for the current node in the proof being constructed.

Definition at line 126 of file StackProver.hpp.

◆ pred_index

PredicateIndex StackProver::pred_index
private

This class needs one of each kind of index to keep track of Variables, Terms etc.

Definition at line 100 of file StackProver.hpp.

◆ problem_path

fs::path StackProver::problem_path
private

Path for the problem of interest.

Definition at line 196 of file StackProver.hpp.

◆ proof_count

uint32_t StackProver::proof_count
private

If we're searching for multiple proofs, keep count
of which one this is.

Definition at line 228 of file StackProver.hpp.

◆ proof_printer

ProofPrinter StackProver::proof_printer
private

You need one of these to print LaTeX output or any kind of proof certificate.

Definition at line 192 of file StackProver.hpp.

◆ reductions_tried

uint32_t StackProver::reductions_tried
private

We'll be keeping some simple statistics about the search process.

Note that at present these statistics include everything tried over all steps in a schedule.

Definition at line 208 of file StackProver.hpp.

◆ results

vector<StartClauseStatus> StackProver::results
private

This is populated by the StackProver::set_up_start_clauses method.

That method looks at the settings for start clauses and tries to achieve them all in a sensible way. Initially this indicates which clauses to use to start, but then stores the results obtained after trying each possibility.

Definition at line 116 of file StackProver.hpp.

◆ right_branch_stack

vector<StackItem> StackProver::right_branch_stack
private

We build the proof by trying the left branches of extensions first: this stack keeps track of the right branches that we need to come back to.

Definition at line 183 of file StackProver.hpp.

◆ right_branches_started

uint32_t StackProver::right_branches_started
private

We'll be keeping some simple statistics about the search process.

Definition at line 223 of file StackProver.hpp.

◆ show

verbose_print::VPrint StackProver::show
private

Set up printing according to verbosity.

Definition at line 240 of file StackProver.hpp.

◆ si

StackItem* StackProver::si
private

Pointer to the current StackItem.

Be very careful with this. At present its use is fine because I don't think that the stack gets modified while the pointer is in use. BUT it may be a good future modification to make this an index rather than a pointer in case we run into trouble with the vector class moving things in memory.

Definition at line 156 of file StackProver.hpp.

◆ simplified_fof_has_axioms

bool StackProver::simplified_fof_has_axioms
private

Keep track of whether the parser found that it's an FOF problem with axioms after simplification.

Definition at line 349 of file StackProver.hpp.

◆ stack

vector<StackItem> StackProver::stack
private

Main stack: this is constructed by the search process and, if completed, represents a proof.

Definition at line 177 of file StackProver.hpp.

◆ status

string StackProver::status
private

Problem status, if found in input file.

Definition at line 172 of file StackProver.hpp.

◆ sub_stack

SubstitutionStack StackProver::sub_stack
private

There is a separate stack to make application and removal of substitutions straightforward.

Definition at line 105 of file StackProver.hpp.

◆ term_index

TermIndex StackProver::term_index
private

This class needs one of each kind of index to keep track of Variables, Terms etc.

Definition at line 95 of file StackProver.hpp.

◆ u

Unifier StackProver::u
private

We need a single Unifier to use throught the process.

Definition at line 142 of file StackProver.hpp.

◆ use_timeout

bool StackProver::use_timeout
private

Are we using a timeout?

Definition at line 232 of file StackProver.hpp.

◆ var_index

VariableIndex StackProver::var_index
private

This class needs one of each kind of index to keep track of Variables, Terms etc.

Definition at line 85 of file StackProver.hpp.

The documentation for this class was generated from the following files:
Generated by doxygen 1.9.7