Connect++ 0.7.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Private Attributes | Static 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.
 
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 random_reorder_literals ()
 Randomly reorder the literals in each clause in 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.
 
string proof_to_tptp ()
 Show the TPTP-formatted conversion to CNF.
 
string get_full_tptp_record ()
 Return everything that's been logged to far while constructing the TPTP-formatted output.
 
ProverOutcome prove ()
 Show a TPTP-formatted proof without the conversion info.
 
vector< pair< string, vector< size_t > > > get_internal_proof () const
 Get an internal representation of the proof stack.
 
void show_statistics () const
 Display counts of number of extensions tried and so on.
 
void show_full_statistics (size_t) const
 Display counts of number of extensions tried and so on, as well as numbers per second.
 
void show_matrix () const
 
void show_path () const
 
void show_stack ()
 
void show_right_stack ()
 
void show_term_index ()
 

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 axiom ()
 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.
 
ClauseCopyCache clause_cache
 Manages caching of copies of clauses from the matrix.
 
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 lemmas for the current node in the proof being constructed.
 
Unifier u
 We need a single Unifier to use throughout the process.
 
InferenceItem action
 Stores the next action from the current StackItem.
 
size_t si
 Index of 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.
 
string tptp_conversion_string
 TPTP-friendly description of the clause conversion.
 
TPTPRecords tptp_proof_output
 TPTP-friendly description of the entire proof, starting with the TPTP file details.
 
Stack stack
 Main stack: this is constructed by the search process and, if completed, represents a proof.
 
Stack 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 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.
 

Static Private Attributes

static uint32_t reductions_tried = 0
 We'll be keeping some simple statistics about the search process.
 
static uint32_t extensions_tried = 0
 We'll be keeping some simple statistics about the search process.
 
static uint32_t lemmata_tried = 0
 We'll be keeping some simple statistics about the search process.
 
static uint32_t right_branches_started = 0
 We'll be keeping some simple statistics about the search process.
 

Friends

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

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 77 of file StackProver.hpp.

Constructor & Destructor Documentation

◆ StackProver()

StackProver::StackProver ( )

You only need a basic constructor.

Definition at line 33 of file StackProver.cpp.

34: num_preds(0)
35, var_index()
36, fun_index()
37, term_index()
38, pred_index()
39, sub_stack()
40, results()
41, matrix()
42, clause_cache()
43, path()
44, new_C()
45, lemmata()
46, u()
47, action(InferenceItemType::Start)
48, si(0)
49, current_depth_limit(0)
50, current_depth(1)
51, depth_limit_reached(false)
52, status()
53, tptp_conversion_string()
54, stack()
55, right_branch_stack()
56, backtrack(false)
57, proof_printer(&stack)
58, problem_path()
59, output_interval(params::output_frequency)
60, proof_count(0)
61, use_timeout(false)
62, end_time()
63, show(params::verbosity)
64, cnf_only(false)
65, conjecture_true(false)
66, conjecture_false(false)
67, conjecture_missing(false)
68, negated_conjecture_removed(false)
69, fof_has_axioms(false)
70, simplified_fof_has_axioms(false)
71, tptp_proof_output()
72{}
StackProver::depth_limit_reached
bool depth_limit_reached
Self-explanatary.
Definition StackProver.hpp:170
StackProver::status
string status
Problem status, if found in input file.
Definition StackProver.hpp:174
StackProver::results
vector< StartClauseStatus > results
This is populated by the StackProver::set_up_start_clauses method.
Definition StackProver.hpp:119
StackProver::negated_conjecture_removed
bool negated_conjecture_removed
Keep track of whether the parser simplified the conjecture away.
Definition StackProver.hpp:346
StackProver::stack
Stack stack
Main stack: this is constructed by the search process and, if completed, represents a proof.
Definition StackProver.hpp:188
StackProver::clause_cache
ClauseCopyCache clause_cache
Manages caching of copies of clauses from the matrix.
Definition StackProver.hpp:128
StackProver::current_depth_limit
uint32_t current_depth_limit
Self-explanatary.
Definition StackProver.hpp:162
StackProver::tptp_proof_output
TPTPRecords tptp_proof_output
TPTP-friendly description of the entire proof, starting with the TPTP file details.
Definition StackProver.hpp:183
StackProver::action
InferenceItem action
Stores the next action from the current StackItem.
Definition StackProver.hpp:154
StackProver::num_preds
size_t num_preds
How many prdicates does the problem of interest have?
Definition StackProver.hpp:83
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:351
StackProver::matrix
Matrix matrix
A copy of the matrix you're working with.
Definition StackProver.hpp:123
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:103
StackProver::proof_printer
ProofPrinter proof_printer
You need one of these to print LaTeX output or any kind of proof certificate.
Definition StackProver.hpp:203
StackProver::cnf_only
bool cnf_only
Keep track of whether there were any FOF formulas in the problem file.
Definition StackProver.hpp:330
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:134
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:93
StackProver::lemmata
Lemmata lemmata
At any point in the search process this is a copy of the list of lemmas for the current node in the p...
Definition StackProver.hpp:146
StackProver::current_depth
uint32_t current_depth
Self-explanatary.
Definition StackProver.hpp:166
StackProver::tptp_conversion_string
string tptp_conversion_string
TPTP-friendly description of the clause conversion.
Definition StackProver.hpp:178
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:356
StackProver::conjecture_missing
bool conjecture_missing
Keep track of whether the parser found a conjecture in the problem file.
Definition StackProver.hpp:342
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:98
StackProver::proof_count
uint32_t proof_count
If we're searching for multiple proofs, keep count of which one this is.
Definition StackProver.hpp:239
StackProver::conjecture_false
bool conjecture_false
Keep track of whether the parser found the conjecture to be false.
Definition StackProver.hpp:338
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:88
StackProver::si
size_t si
Index of the current StackItem.
Definition StackProver.hpp:158
StackProver::conjecture_true
bool conjecture_true
Keep track of whether the parser found the conjecture to be true.
Definition StackProver.hpp:334
StackProver::backtrack
bool backtrack
Are we moving up or down the stack?
Definition StackProver.hpp:198
StackProver::end_time
chrono::steady_clock::time_point end_time
When do we stop because of a timeout?
Definition StackProver.hpp:247
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:140
StackProver::problem_path
fs::path problem_path
Path for the problem of interest.
Definition StackProver.hpp:207
StackProver::use_timeout
bool use_timeout
Are we using a timeout?
Definition StackProver.hpp:243
StackProver::right_branch_stack
Stack 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:194
StackProver::sub_stack
SubstitutionStack sub_stack
There is a separate stack to make application and removal of substitutions straightforward.
Definition StackProver.hpp:108
StackProver::show
verbose_print::VPrint show
Set up printing according to verbosity.
Definition StackProver.hpp:251
StackProver::u
Unifier u
We need a single Unifier to use throughout the process.
Definition StackProver.hpp:150
StackProver::output_interval
Interval output_interval
How often do you output updates about progress?
Definition StackProver.hpp:211

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 129 of file StackProver.cpp.

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

◆ axiom()

bool StackProver::axiom ( )
private

Test to see if you're at an axiom.

Definition at line 332 of file StackProver.cpp.

332 {
333 return stack[si].c.empty();
334}
Stack::empty
bool empty() const
Exact analogue of the same function for vector<>.
Definition Stack.hpp:88

◆ 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 542 of file StackProver.cpp.

542 {
543 backtrack = true;
544 stack.pop_back();
545 si--;
546 current_depth = stack[si].depth;
547}
Stack::pop_back
void pop_back()
Exact analogue of the same function for vector<>. BUT - importantly - avoid calling the StackItem des...
Definition Stack.hpp:116

◆ 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 433 of file StackProver.hpp.

433 {
434 matrix.deterministic_reorder(n);
435 }
Matrix::deterministic_reorder
void deterministic_reorder(size_t)
Deterministic reorder of the clauses.
Definition Matrix.cpp:139

◆ extend_with_action()

void StackProver::extend_with_action ( )
private

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

Definition at line 336 of file StackProver.cpp.

336 {
337 /*
338 * Add a new StackItem using the next action from the list stored
339 * in the StackItem currently in play. If necessary, also
340 * add something to right_branch_stack. Populate the new list of
341 * actions and update si.
342 */
343 current_depth++;
344 /*
345 * Why are the scope rules for switch so odd???
346 */
347 Clause old_C;
348 Lemmata old_Lem;
349 Literal neg_lit;
350 UnificationOutcome outcome;
351 Substitution sig;
352 Literal ext_L;
353 switch (action.T) {
354 //----------------------------------------------------------------------
355 //----------------------------------------------------------------------
356 //----------------------------------------------------------------------
357 // Lemmas.
358 //----------------------------------------------------------------------
359 //----------------------------------------------------------------------
360 //----------------------------------------------------------------------
361 case InferenceItemType::Lemma:
362 lemmata_tried++;
363 /*
364 * If you are restricting backtracking for lemmas then
365 * at this point you can remove all alternatives.
366 */
367 if (params::limit_bt_lemmas)
368 stack[si].restrict_backtrack();
369 /*
370 * Work out the new state.
371 */
372 new_C = stack[si].c;
373 new_C.drop_literal(action.Lindex);
374 path = stack[si].p;
375 lemmata = stack[si].l;
376 /*
377 * Extend the stack.
378 */
379 stack.emplace_back(StackItemType::Lemmata, new_C, path,
380 lemmata, current_depth);
381 stack.back().set_this_action(action);
382 break;
383 //----------------------------------------------------------------------
384 //----------------------------------------------------------------------
385 //----------------------------------------------------------------------
386 // Reduction.
387 //----------------------------------------------------------------------
388 //----------------------------------------------------------------------
389 //----------------------------------------------------------------------
390 case InferenceItemType::Reduction:
391 reductions_tried++;
392 /*
393 * If you are restricting backtracking for reductions then
394 * at this point you can remove all alternatives.
395 */
396 if (params::limit_bt_reductions)
397 stack[si].restrict_backtrack();
398 /*
399 * Reductions have a substitution, so apply it and remember
400 * in case you need to undo it later.
401 */
402 action.sigma.apply();
403 sub_stack.push_all(action.sigma);
404 /*
405 * Work out the new state.
406 */
407 new_C = stack[si].c;
408 new_C.drop_literal(action.Lindex);
409 path = stack[si].p;
410 lemmata = stack[si].l;
411 lemmata.push_back(action.L);
412 /*
413 * Extend the stack.
414 */
415 stack.emplace_back(StackItemType::Reduction, new_C, path,
416 lemmata, action.sigma, current_depth);
417 stack.back().set_this_action(action);
418 break;
419 //----------------------------------------------------------------------
420 //----------------------------------------------------------------------
421 //----------------------------------------------------------------------
422 // Extension.
423 //----------------------------------------------------------------------
424 //----------------------------------------------------------------------
425 //----------------------------------------------------------------------
426 case InferenceItemType::Extension:
427 extensions_tried++;
428 /*
429 * You're going to generate new variables, so remember where to
430 * backtrack to.
431 */
432 //var_index.add_backtrack_point();
433 /*
434 * This is an Extension, so you're going to add something to
435 * right_branch_stack.
436 */
437 path = stack[si].p;
438 old_C = stack[si].c;
439 old_C.drop_literal(action.Lindex);
440 old_Lem = stack[si].l;
441 old_Lem.push_back(action.L);
442 /*
443 * DON'T do populate_stack_item here! That can wait until you actually
444 * use the right branch. In fact it *has* to wait because we might
445 * apply substitutions that affect it.
446 */
447 right_branch_stack.emplace_back(StackItemType::RightBranch, old_C,
448 path, old_Lem, current_depth);
449 /*
450 * The right branch needs to know where to restrict backtracking.
451 */
452 right_branch_stack.back().set_bt_restriction_index(stack.size() - 1);
453 /*
454 * Now you can deal with the left branch.
455 */
456
457 //matrix.get_literal_clause_pair(action.index_in_LC_index, action.index_to_LC, ext_L, new_C);
458 //new_C.make_copy_with_new_vars(ext_L, new_C, var_index, term_index);
459
460 clause_cache.make_copy_with_new_variables(action.C_2, new_C, matrix, var_index, term_index);
461 ext_L = new_C[action.Lprime];
462 new_C.drop_literal(action.Lprime);
463 /*
464 * Extensions have a substitution, so apply it and remember
465 * in case you need to undo it later.
466 */
467 neg_lit = action.L;
468 neg_lit.invert();
469 outcome = u(neg_lit, ext_L);
470 sig = u.get_substitution();
471 u.backtrack();
472 sig.apply();
473 sub_stack.push_all(sig);
474 /*
475 * Work out the new state.
476 */
477 path.push(action.L);
478 lemmata = stack[si].l;
479 /*
480 * Extend the stack.
481 */
482 stack.emplace_back(StackItemType::LeftBranch, new_C, path,
483 lemmata, sig, current_depth);
484 stack.back().set_this_action(action);
485 break;
486 default:
487 cerr << "PANIC!!! You should only have a lemmata, reduction or an extension here!"
488 << endl;
489 break;
490 }
491 /*
492 * Finally, move si on and work out the next bunch of possible actions.
493 */
494 si++;
495 populate_stack_item();
496}
ClauseCopyCache::make_copy_with_new_variables
void make_copy_with_new_variables(size_t, Clause &, const Matrix &, VariableIndex &, TermIndex &)
If there is a copy cached, replace the parameter with it. Otherwise, use the parameter to actually ma...
Definition ClauseCopyCache.cpp:46
Clause::drop_literal
void drop_literal(LitNum)
Get rid of the specified Literal.
Definition Clause.cpp:168
Lemmata
Representation of the lemma list.
Definition Lemmata.hpp:49
Lemmata::push_back
void push_back(const Literal &)
Self-explanatory.
Definition Lemmata.cpp:28
Stack::emplace_back
void emplace_back(StackItemType sit, const Clause &_c, const SimplePath &_p, const Lemmata &_l, uint32_t _d)
(Almost!) exact analogue of the same function for vector<>.
Definition Stack.hpp:132
Stack::size
size_t size() const
Exact analogue of the same function for vector<>.
Definition Stack.hpp:94
Stack::back
StackItem & back()
Exact analogue of the same function for vector<>.
Definition Stack.hpp:109
StackProver::lemmata_tried
static uint32_t lemmata_tried
We'll be keeping some simple statistics about the search process.
Definition StackProver.hpp:229
StackProver::populate_stack_item
void populate_stack_item()
Fill the vector of possible actions with everything available.
Definition StackProver.cpp:314
StackProver::extensions_tried
static uint32_t extensions_tried
We'll be keeping some simple statistics about the search process.
Definition StackProver.hpp:224
StackProver::reductions_tried
static uint32_t reductions_tried
We'll be keeping some simple statistics about the search process.
Definition StackProver.hpp:219
Substitution
General representation of a substitution.
Definition Substitution.hpp:57
Substitution::apply
void apply() const
Apply a substitution everywhere.
Definition Substitution.cpp:85
SubstitutionStack::push_all
void push_all(Substitution &)
Take all the substitutions provided and add the corresponding variables to the stack.
Definition SubstitutionStack.cpp:28
Unifier::backtrack
void backtrack()
Apply the backtracking process to the substitution that has been constructed.
Definition Unifier.cpp:195
Unifier::get_substitution
Substitution get_substitution() const
Trivial get methods for the result.
Definition Unifier.hpp:122
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. This may or may not be reusable,...
Definition InferenceItem.hpp:89
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::set_bt_restriction_index
void set_bt_restriction_index(size_t i)
Basic set method.
Definition StackItem.hpp:195
StackItem::set_this_action
void set_this_action(const InferenceItem &inf_i)
Basic set method.
Definition StackItem.hpp:189

◆ get_full_tptp_record()

string StackProver::get_full_tptp_record ( )
inline

Return everything that's been logged to far while constructing the TPTP-formatted output.

Definition at line 526 of file StackProver.hpp.

526 {
527 return tptp_proof_output.to_tptp_string_all();
528 }
TPTPRecords::to_tptp_string_all
string to_tptp_string_all()
Format everything, including every step whether used or not.
Definition TPTPRecords.cpp:243

◆ get_indexes()

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

Straightforward get method.

Definition at line 372 of file StackProver.hpp.

372 {
373 auto result = std::make_tuple(&var_index, &fun_index, &pred_index, &term_index);
374 return result;
375 }

◆ 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 1252 of file StackProver.cpp.

1252 {
1253 return proof_printer.make_internal();
1254}
ProofPrinter::make_internal
vector< pair< string, vector< size_t > > > make_internal() const
Make a simple data structure representing the proof stack.
Definition ProofPrinter.cpp:365

◆ get_matrix()

Matrix & StackProver::get_matrix ( )
inline

Get a reference to the matrix.

Definition at line 459 of file StackProver.hpp.

459 {
460 return matrix;
461 };

◆ get_status()

string StackProver::get_status ( ) const
inline

Straightforward get method.

Definition at line 379 of file StackProver.hpp.

379{ return status; }

◆ go()

ProverResult StackProver::go ( )
private

This runs the proof search from a given Start Move.

Definition at line 649 of file StackProver.cpp.

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

◆ left_extension_backtrack()

void StackProver::left_extension_backtrack ( )
private

One of several different kinds of backtracking.

Definition at line 558 of file StackProver.cpp.

558 {
559 /*
560 * You're backtracking through a left branch, so you
561 * need to remember to get rid of the corresponding
562 * right branch as well.
563 */
564 right_branch_stack.pop_back();
565 //var_index.backtrack();
566 clause_cache.backtrack();
567 sub_stack.backtrack();
568 backtrack_once();
569}
ClauseCopyCache::backtrack
void backtrack()
Backtracking is just looking at the last copy supplied and undoing that action.
Definition ClauseCopyCache.cpp:61
StackProver::backtrack_once
void backtrack_once()
Basic, single step backtrack on the stack.
Definition StackProver.cpp:542
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

◆ lemmata_backtrack()

void StackProver::lemmata_backtrack ( )
private

One of several different kinds of backtracking.

Definition at line 554 of file StackProver.cpp.

554 {
555 backtrack_once();
556}

◆ populate_stack_item()

void StackProver::populate_stack_item ( )
private

Fill the vector of possible actions with everything available.

Definition at line 314 of file StackProver.cpp.

314 {
315 /*
316 * Don't waste your time if the regularity test applies.
317 */
318 if (params::use_regularity_test && !path.test_for_regularity(new_C))
319 return;
320 /*
321 * Don't try to populate axioms.
322 */
323 if (new_C.size() == 0) {
324 return;
325 }
326 /*
327 * Extensions, reductions and lemmas.
328 */
329 stack[si].initialize(matrix);
330}
Clause::size
size_t size() const
Straightforward get method.
Definition Clause.hpp:78

◆ problem_has_false_conjecture()

bool StackProver::problem_has_false_conjecture ( ) const
inline

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

Definition at line 480 of file StackProver.hpp.

480 {
481 return conjecture_false;
482 }

◆ 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 502 of file StackProver.hpp.

502 {
503 return fof_has_axioms;
504 }

◆ 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 488 of file StackProver.hpp.

488 {
489 return conjecture_missing;
490 }

◆ 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 495 of file StackProver.hpp.

495 {
496 return negated_conjecture_removed;
497 }

◆ problem_has_true_conjecture()

bool StackProver::problem_has_true_conjecture ( ) const
inline

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

Definition at line 473 of file StackProver.hpp.

473 {
474 return conjecture_true;
475 }

◆ problem_is_cnf_only()

bool StackProver::problem_is_cnf_only ( ) const
inline

Find out whether the problem is CNF only.

Definition at line 466 of file StackProver.hpp.

466 {
467 return cnf_only;
468 }

◆ 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 498 of file StackProver.cpp.

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

◆ proof_to_tptp()

string StackProver::proof_to_tptp ( )

Show the TPTP-formatted conversion to CNF.

Show the entire proof in TPTP format.

Definition at line 1256 of file StackProver.cpp.

1256 {
1257 pair<string, unordered_set<string>> proof(proof_printer.make_tptp(&matrix, &var_index, &term_index));
1258 string result(tptp_proof_output.to_tptp_string(proof.second));
1259 result += proof.first;
1260 return result;
1261}
ProofPrinter::make_tptp
pair< string, unordered_set< string > > make_tptp(Matrix *, VariableIndex *, TermIndex *)
Show the proof in a TPTP-friendly format.
Definition ProofPrinter.cpp:357
TPTPRecords::to_tptp_string
string to_tptp_string(const unordered_set< string > &)
Format everything.
Definition TPTPRecords.cpp:226

◆ prove()

ProverOutcome StackProver::prove ( )

Show a TPTP-formatted proof without the conversion info.

Here is where the magic happens.

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

Make sure you deal with reordering.

Definition at line 1037 of file StackProver.cpp.

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

◆ random_reorder()

void StackProver::random_reorder ( )
inline

Randomly reorder the matrix.

Definition at line 439 of file StackProver.hpp.

439 {
440 matrix.random_reorder();
441 }
Matrix::random_reorder
void random_reorder()
Randomly reorder the matrix.
Definition Matrix.cpp:173

◆ random_reorder_literals()

void StackProver::random_reorder_literals ( )
inline

Randomly reorder the literals in each clause in the matrix.

Definition at line 446 of file StackProver.hpp.

446 {
447 matrix.random_reorder_literals();
448 }
Matrix::random_reorder_literals
void random_reorder_literals()
Randomly reorder the literals in each clause in the matrix.
Definition Matrix.cpp:203

◆ 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 80 of file StackProver.cpp.

82 {
83 TPTPParser parser(&var_index, &fun_index, &term_index, &pred_index, &matrix, &tptp_proof_output);
84 parser.parse_tptp_from_file(file_name);
85 status = parser.get_problem_status();
86 bool equality = parser.equality_used();
87 found_conjecture = parser.conjecture_present();
88 fof_size = parser.number_of_fof_formulas();
89 Predicate* equals_predicate = parser.get_equals_predicate();
90 cnf_only = parser.problem_is_cnf_only();
91 conjecture_true = parser.fof_conjecture_is_true();
92 conjecture_false = parser.fof_conjecture_is_false();
93 conjecture_missing = parser.fof_conjecture_is_missing();
94 negated_conjecture_removed = parser.fof_negated_conjecture_removed();
95 fof_has_axioms = parser.fof_has_axioms();
96 simplified_fof_has_axioms = parser.simplified_fof_has_axioms();
97 //tptp_conversion_string = parser.get_tptp_conversion_string();
98 parser.clear();
99 num_preds = pred_index.get_num_preds();
100 /*
101 * num_preds for Matrix is set by parser.
102 */
103 path.set_num_preds(num_preds);
104
105 if (params::show_clauses) {
106 std::exit(EXIT_SUCCESS);
107 }
108
109 if (status != string("") && params::first_parse) {
110 show(1, string("Problem status found: "));
111 show(1, status, true);
112 }
113 if (equality && params::add_equality_axioms) {
114 if (params::first_parse) {
115 show(1, string("Problem involves equality: adding axioms for =."), true);
116 params::first_parse = false;
117 }
118 add_equality_axioms(equals_predicate);
119 if (params::equality_axioms_at_start) {
120 matrix.move_equals_to_start();
121 }
122 }
123 /*
124 * Any further variables will be anonymous.
125 */
126 var_index.set_all_names_added();
127 }
Matrix::move_equals_to_start
void move_equals_to_start()
Self-explanatory.
Definition Matrix.cpp:222
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:129
TPTPParser
Wrap up everything the TPTP parser needs to do inside a single class.
Definition TPTPParser.hpp:661
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:66

◆ reduction_backtrack()

void StackProver::reduction_backtrack ( )
private

One of several different kinds of backtracking.

Definition at line 549 of file StackProver.cpp.

549 {
550 sub_stack.backtrack();
551 backtrack_once();
552}

◆ reset_for_start()

void StackProver::reset_for_start ( )
inlineprivate

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

Definition at line 316 of file StackProver.hpp.

316 {
317 depth_limit_reached = false;
318 si = 0;
319 backtrack = false;
320 path.clear();
321 stack.clear();
322 lemmata.clear();
323 right_branch_stack.clear();
324 sub_stack.clear();
325 }
Lemmata::clear
void clear()
Self-explanatory.
Definition Lemmata.hpp:74
Stack::clear
void clear()
Exact analogue of the same function for vector<>.
Definition Stack.hpp:82
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!

Definition at line 587 of file StackProver.cpp.

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

◆ 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 74 of file StackProver.cpp.

74 {
75 num_preds = n;
76 matrix.set_num_preds(n);
77 path.set_num_preds(n);
78}
Matrix::set_num_preds
void set_num_preds(size_t)
Make an empty index.
Definition Matrix.cpp:46

◆ set_problem_path()

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

Set the path for the problem being solved.

Used only to produce nice output.

Definition at line 400 of file StackProver.hpp.

400{ 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 391 of file StackProver.hpp.

391 {
392 use_timeout = true;
393 end_time = time;
394 }

◆ 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 910 of file StackProver.cpp.

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

◆ show_full_statistics()

void StackProver::show_full_statistics ( size_t ms) const

Display counts of number of extensions tried and so on, as well as numbers per second.

Definition at line 1291 of file StackProver.cpp.

1291 {
1292 size_t total = reductions_tried + extensions_tried + lemmata_tried + right_branches_started;
1293 double s = static_cast<double>(ms) / 1000.0;
1294 double ext_rate = (static_cast<double>(extensions_tried) / s);
1295 double red_rate = (static_cast<double>(reductions_tried) / s);
1296 double lem_rate = (static_cast<double>(lemmata_tried) / s);
1297 double right_rate = (static_cast<double>(right_branches_started) / s);
1298 double total_rate = (static_cast<double>(total) / s);
1299 cout << "Reductions: " << setw(15) << reductions_tried << " (" << static_cast<size_t>(red_rate) << "/s)" << endl;
1300 cout << "Extensions: " << setw(15) << extensions_tried << " (" << static_cast<size_t>(ext_rate) << "/s)" << endl;
1301 cout << "Lemmas: " << setw(15) << lemmata_tried << " (" << static_cast<size_t>(lem_rate) << "/s)" << endl;
1302 cout << "Right branches: " << setw(15) << right_branches_started << " (" << static_cast<size_t>(right_rate) << "/s)" << endl;
1303 cout << "Total: " << setw(15) << total << " (" << static_cast<size_t>(total_rate) << "/s)" << endl;
1304}

◆ show_matrix() [1/2]

void StackProver::show_matrix ( )
inline

Show a nicely formatted matrix.

Definition at line 452 of file StackProver.hpp.

452 {
453 cout << "Matrix:" << endl;
454 cout << matrix.to_string() << endl;
455 }
Matrix::to_string
string to_string() const
Make a string representation.
Definition Matrix.cpp:252

◆ show_matrix() [2/2]

void StackProver::show_matrix ( ) const
inline

Definition at line 561 of file StackProver.hpp.

561{ cout << matrix << endl; }

◆ show_path()

void StackProver::show_path ( ) const
inline

Definition at line 562 of file StackProver.hpp.

562{ cout << path << endl; }

◆ show_right_stack()

void StackProver::show_right_stack ( )

Definition at line 1271 of file StackProver.cpp.

1271 {
1272 cout << "--------------------------------------------------------" << endl;
1273 cout << "Right Stack:" << endl;
1274 cout << "--------------------------------------------------------" << endl;
1275 cout << right_branch_stack << endl;
1276 cout << "--------------------------------------------------------" << endl;
1277}

◆ show_stack()

void StackProver::show_stack ( )

Definition at line 1263 of file StackProver.cpp.

1263 {
1264 cout << "--------------------------------------------------------" << endl;
1265 cout << "Stack:" << endl;
1266 cout << "--------------------------------------------------------" << endl;
1267 cout << stack << endl;
1268 cout << "--------------------------------------------------------" << endl;
1269}

◆ show_statistics()

void StackProver::show_statistics ( ) const

Display counts of number of extensions tried and so on.

Definition at line 1279 of file StackProver.cpp.

1279 {
1280 verbose_print::VPrint show(params::verbosity);
1281 show(1, string("Reductions: "));
1282 show(1, std::to_string(reductions_tried));
1283 show(1, string(" Extensions: "));
1284 show(1, std::to_string(extensions_tried));
1285 show(1, string(" Lemmata: "));
1286 show(1, std::to_string(lemmata_tried));
1287 show(1, string(" Right branches: "));
1288 show(1, std::to_string(right_branches_started), true);
1289}
verbose_print::VPrint
Definition vic_strings.hpp:240

◆ show_term_index()

void StackProver::show_term_index ( )
inline

Definition at line 565 of file StackProver.hpp.

565{ cout << term_index << endl; }

◆ 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 509 of file StackProver.hpp.

509 {
510 return simplified_fof_has_axioms;
511 }

Friends And Related Symbol Documentation

◆ operator<<

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

Definition at line 1306 of file StackProver.cpp.

1306 {
1307 out << "Current state of the RecursiveProver object" << endl;
1308 out << "-------------------------------------------" << endl << endl;
1309 out << p.var_index << endl;
1310 out << p.fun_index << endl;
1311 out << p.term_index << endl;
1312 out << p.path << endl;
1313 out << p.matrix << endl;
1314 return out;
1315}

Member Data Documentation

◆ action

InferenceItem StackProver::action
private

Stores the next action from the current StackItem.

Definition at line 154 of file StackProver.hpp.

◆ backtrack

bool StackProver::backtrack
private

Are we moving up or down the stack?

Definition at line 198 of file StackProver.hpp.

◆ clause_cache

ClauseCopyCache StackProver::clause_cache
private

Manages caching of copies of clauses from the matrix.

Definition at line 128 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 330 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 338 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 342 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 334 of file StackProver.hpp.

◆ current_depth

uint32_t StackProver::current_depth
private

Self-explanatary.

Definition at line 166 of file StackProver.hpp.

◆ current_depth_limit

uint32_t StackProver::current_depth_limit
private

Self-explanatary.

Definition at line 162 of file StackProver.hpp.

◆ depth_limit_reached

bool StackProver::depth_limit_reached
private

Self-explanatary.

Definition at line 170 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 247 of file StackProver.hpp.

◆ extensions_tried

uint32_t StackProver::extensions_tried = 0
staticprivate

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

Definition at line 224 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 351 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 93 of file StackProver.hpp.

◆ lemmata

Lemmata StackProver::lemmata
private

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

Definition at line 146 of file StackProver.hpp.

◆ lemmata_tried

uint32_t StackProver::lemmata_tried = 0
staticprivate

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

Definition at line 229 of file StackProver.hpp.

◆ matrix

Matrix StackProver::matrix
private

A copy of the matrix you're working with.

Definition at line 123 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 346 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 140 of file StackProver.hpp.

◆ num_preds

size_t StackProver::num_preds
private

How many prdicates does the problem of interest have?

Definition at line 83 of file StackProver.hpp.

◆ output_interval

Interval StackProver::output_interval
private

How often do you output updates about progress?

Definition at line 211 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 134 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 103 of file StackProver.hpp.

◆ problem_path

fs::path StackProver::problem_path
private

Path for the problem of interest.

Definition at line 207 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 239 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 203 of file StackProver.hpp.

◆ reductions_tried

uint32_t StackProver::reductions_tried = 0
staticprivate

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 219 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 119 of file StackProver.hpp.

◆ right_branch_stack

Stack 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 194 of file StackProver.hpp.

◆ right_branches_started

uint32_t StackProver::right_branches_started = 0
staticprivate

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

Definition at line 234 of file StackProver.hpp.

◆ show

verbose_print::VPrint StackProver::show
private

Set up printing according to verbosity.

Definition at line 251 of file StackProver.hpp.

◆ si

size_t StackProver::si
private

Index of the current StackItem.

Definition at line 158 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 356 of file StackProver.hpp.

◆ stack

Stack StackProver::stack
private

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

Definition at line 188 of file StackProver.hpp.

◆ status

string StackProver::status
private

Problem status, if found in input file.

Definition at line 174 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 108 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 98 of file StackProver.hpp.

◆ tptp_conversion_string

string StackProver::tptp_conversion_string
private

TPTP-friendly description of the clause conversion.

Definition at line 178 of file StackProver.hpp.

◆ tptp_proof_output

TPTPRecords StackProver::tptp_proof_output
private

TPTP-friendly description of the entire proof, starting with the TPTP file details.

Definition at line 183 of file StackProver.hpp.

◆ u

Unifier StackProver::u
private

We need a single Unifier to use throughout the process.

Definition at line 150 of file StackProver.hpp.

◆ use_timeout

bool StackProver::use_timeout
private

Are we using a timeout?

Definition at line 243 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 88 of file StackProver.hpp.

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