25#include "StackProver.hpp"
41, action(InferenceItemType::Start)
43, current_depth_limit(0)
45, depth_limit_reached(false)
50, proof_printer(&stack)
52, output_interval(
params::output_frequency)
56, right_branches_started(0)
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)
77 bool& found_conjecture,
100 if (params::show_clauses) {
101 std::exit(EXIT_SUCCESS);
104 if (
status !=
string(
"")) {
105 show(1,
string(
"Problem status found: "));
108 if (equality && params::add_equality_axioms) {
109 show(1,
string(
"Problem involves equality: adding axioms for =."),
true);
111 if (params::equality_axioms_at_start) {
120 if (params::generate_Prolog_proof && params::build_proof) {
137 uint32_t max_arity = max_fun_arity;
138 if (max_pred_arity > max_arity)
139 max_arity = max_pred_arity;
144 string xvar(
"__eqx_");
145 string yvar(
"__eqy_");
146 for (
size_t i = 0; i < max_arity; i++) {
158 bool pol = !params::positive_representation;
159 uint32_t n_added = 0;
164 ref.push_back(xs[0]);
165 ref.push_back(xs[0]);
166 Literal reflexive(equals_predicate, ref, 2, pol);
180 Literal sym1(equals_predicate, xy, 2, !pol);
181 Literal sym2(equals_predicate, yx, 2, pol);
196 Literal tr1(equals_predicate, xy, 2, !pol);
197 Literal tr2(equals_predicate, yz, 2, !pol);
198 Literal tr3(equals_predicate, xz, 2, pol);
215 for (
size_t i = 0; i < ar; i++) {
216 x1xn.push_back(xs[i]);
217 y1yn.push_back(ys[i]);
219 xiyi.push_back(xs[i]);
220 xiyi.push_back(ys[i]);
221 Literal eq_lit(equals_predicate, xiyi, 2, !pol);
227 Literal f_lit(equals_predicate, t, 2, pol);
239 if (ar > 0 && p != equals_predicate) {
243 for (
size_t i = 0; i < ar; i++) {
244 x1xn.push_back(xs[i]);
245 y1yn.push_back(ys[i]);
247 xiyi.push_back(xs[i]);
248 xiyi.push_back(ys[i]);
249 Literal eq_lit(equals_predicate, xiyi, 2, !pol);
252 Literal p_lit1(p, x1xn, ar, !pol);
253 Literal p_lit2(p, y1yn, ar, pol);
264 if (!params::no_distinct_objects && min_arity == 0) {
265 vector<Term*> all_distinct_constants;
266 vector<Term*> empty_args;
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] ==
'\"');
278 (params::all_distinct_objects || is_quoted)) {
280 all_distinct_constants.push_back(t);
283 size_t s = all_distinct_constants.size();
285 for (
size_t i = s - 1; i > 0; i--) {
286 for (
size_t j = 0; j < i; j++) {
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);
321 if (params::limit_extensions)
328 if (params::limit_reductions)
335 if (params::use_lemmata) {
336 if (params::limit_lemmata)
379 case InferenceItemType::Lemma:
385 if (params::limit_bt_lemmas)
408 case InferenceItemType::Reduction:
414 if (params::limit_bt_reductions)
444 case InferenceItemType::Extension:
495 cerr <<
"PANIC!!! You should only have a lemmata, reduction or an extension here!"
545 if (params::limit_bt_extensions) {
604 if (!params::limit_bt_extensions ||
605 ((params::limit_bt_extensions || params::limit_bt_all) &&
606 !params::limit_bt_extensions_left_tree)) {
612 stack.back().clear();
633 if (params::limit_bt_extensions_left_tree) {
635 size_t current_index =
stack.size() - 1;
636 while (current_index > target_index) {
638 case StackItemType::Lemmata:
640 case StackItemType::Reduction:
643 case StackItemType::LeftBranch:
647 case StackItemType::RightBranch:
650 cerr <<
"Something is VERY WRONG!" << endl;
677 return ProverResult::TimeOut;
682 cout << cursor_symbols::Cursor::to_column(1);
686 cout <<
" Stack size: " <<
stack.size();
704 case StackItemType::Start:
707 return ProverResult::OptionsExhausted;
718 case StackItemType::Lemmata:
730 return ProverResult::Valid;
776 case StackItemType::Reduction:
786 return ProverResult::Valid;
833 case StackItemType::LeftBranch:
867 case StackItemType::RightBranch:
874 return ProverResult::Valid;
897 cerr <<
"Something is VERY WRONG!" << endl;
901 return ProverResult::Error;
924 if (params::all_start) {
925 for (
size_t i = 0; i < m_size; i++) {
926 results.push_back(StartClauseStatus::Start);
930 bool first_clause_included =
false;
937 if (params::all_pos_neg_start && !params::conjecture_start) {
938 for (
size_t i = 0; i < m_size; i++) {
946 (!(params::restrict_start && first_clause_included))
948 results.push_back(StartClauseStatus::Start);
949 first_clause_included =
true;
952 results.push_back(StartClauseStatus::NoStart);
959 else if (!params::all_pos_neg_start && params::conjecture_start) {
960 for (
size_t i = 0; i < m_size; i++) {
963 (!(params::restrict_start && first_clause_included))) {
964 results.push_back(StartClauseStatus::Start);
965 first_clause_included =
true;
968 results.push_back(StartClauseStatus::NoStart);
979 for (
size_t i = 0; i < m_size; i++) {
988 !(params::restrict_start && first_clause_included)) {
989 results.push_back(StartClauseStatus::Start);
990 first_clause_included =
true;
993 results.push_back(StartClauseStatus::NoStart);
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;
1016 for (
size_t i = 0; i < m_size; i++) {
1022 !(params::restrict_start && first_clause_included)) {
1023 results.push_back(StartClauseStatus::Start);
1024 first_clause_included =
true;
1027 results.push_back(StartClauseStatus::NoStart);
1045 if (!start_clause.first) {
1046 return ProverOutcome::False;
1057 bool switched_to_complete =
false;
1066 && !switched_to_complete) {
1074 switched_to_complete =
true;
1077 show(1, cs(
"Switching to complete search.").orange(),
true);
1080 show(1,
string(
"SEARCH TO DEPTH: "));
1086 size_t start_clause_index = 0;
1091 if (
results[start_clause_index] == StartClauseStatus::NoStart
1092 ||
results[start_clause_index] == StartClauseStatus::False) {
1093 start_clause_index++;
1115 show(1,
string(
"START from clause "));
1116 show(1, std::to_string(start_clause_index + 1));
1117 show(1,
string(
" of "));
1119 show(2,
string(
": "));
1128 stack.push_back(start_item);
1139 ProverResult result =
go();
1145 case ProverResult::Valid:
1147 if (params::build_proof) {
1148 if (params::generate_LaTeX_proof) {
1153 if (params::generate_Prolog_proof) {
1154 fs::path prolog_path = params::Prolog_proof_path;
1158 show(1,
string(
": Found proof number "));
1160 return ProverOutcome::Valid;
1162 case ProverResult::Error:
1163 return ProverOutcome::Error;
1165 case ProverResult::TimeOut:
1166 return ProverOutcome::TimeOut;
1168 case ProverResult::OptionsExhausted:
1174 show(1,
string(
": Depth limited"),
true);
1182 results[start_clause_index] = StartClauseStatus::False;
1183 show(1,
string(
": False"),
true);
1186 start_clause_index++;
1189 return ProverOutcome::Error;
1205 bool all_false =
true;
1206 for (StartClauseStatus& outcome :
results) {
1207 if (outcome == StartClauseStatus::Start) {
1213 return ProverOutcome::False;
1218 return ProverOutcome::PathLenLimit;
1225void StackProver::show_stack() {
1226 cout <<
"--------------------------------------------------------" << endl;
1227 cout <<
"Stack:" << endl;
1228 cout <<
"--------------------------------------------------------" << endl;
1229 for (
auto s :
stack) {
1232 cout <<
"--------------------------------------------------------" << endl;
1235void StackProver::show_right_stack() {
1236 cout <<
"--------------------------------------------------------" << endl;
1237 cout <<
"Right Stack:" << endl;
1238 cout <<
"--------------------------------------------------------" << endl;
1242 cout <<
"--------------------------------------------------------" << endl;
1245void StackProver::show_statistics()
const {
1247 show(1,
string(
"Reductions: "));
1249 show(1,
string(
" Extensions: "));
1251 show(1,
string(
" Lemmata: "));
1253 show(1,
string(
" Right branches: "));
1257ostream& operator<<(ostream& out,
const StackProver& p) {
1258 out <<
"Current state of the RecursiveProver object" << endl;
1259 out <<
"-------------------------------------------" << endl << endl;
1263 out << p.
path << endl;
Representation of clauses.
bool empty() const
Straightforward get method.
Clause make_copy_with_new_vars(VariableIndex &, TermIndex &) const
Make a copy of an entire clause, introducing new variables.
void add_lit(const Literal &)
Add a literal, making sure you don't duplicate.
size_t size() const
Straightforward get method.
string to_string(bool=false) const
Convert to a string.
void drop_literal(LitNum)
Get rid of the specified Literal.
Basic representation of functions.
Arity get_arity() const
Most basic access function.
string get_name() const
Most basic access function.
Arity find_minimum_arity() const
Find the smallest arity appearing for any Function in the index.
size_t get_size() const
Self-explanatory.
Arity find_maximum_arity() const
Find the largest arity appearing for any Function in the index.
Representation of the lemma list.
void find_initial_lemmata(vector< InferenceItem > &, Clause &)
Find all lemmata that are applicable, but only for the initial Literal in a Clause.
void find_all_lemmata(vector< InferenceItem > &, Clause &)
Find all lemmata that are applicable, given a Clause.
void push_back(const Literal &)
Self-explanatory.
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
void move_equals_to_start()
Self-explanatory.
ClauseNum get_num_clauses() const
Straightforward get method.
string make_LaTeX(bool=false) const
Make a usable LaTeX representation.
void add_clause(Clause &, string="")
Add a Clause to the Matrix and update the index accordingly.
bool is_negative(size_t i) const
Is a particular Clause negative?.
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.
void find_all_extensions(Unifier &, vector< InferenceItem > &, Clause &, VariableIndex &, TermIndex &)
Find all possible extensions given a Clause, considering all Literals in the Clause.
bool is_conjecture(size_t i) const
Is a particular Clause a conjecture?
void write_to_prolog_file(const path &) const
Write to a file that can be read by Prolog.
void set_num_equals(uint32_t n)
Straightforward set method.
bool is_positive(size_t i) const
Is a particular Clause positive?.
void set_num_preds(size_t)
Make an empty index.
pair< bool, size_t > find_start() const
Use a simple heuristic to find a good start clause.
Basic representation of predicates: here just names, ids and arities.
Arity get_arity() const
Basic get method.
size_t get_num_preds() const
Basic get method.
Arity find_maximum_arity() const
Find the largest arity appearing in the index.
void make_Prolog(const path &)
Convert to a form suitable for use by the Prolog proof checker and write to a file.
void make_LaTeX(const path &, const path &, const string &)
Convert to LaTeX and store in the specified file.
vector< pair< string, vector< size_t > > > make_internal() const
Make a simple data structure representing the proof stack.
uint32_t length() const
Straightforward get method.
void push(const Literal &)
Add a new Literal to the Path.
void set_num_preds(size_t num_predicates)
Set method for num_predicates.
bool test_for_regularity(Clause &) const
Regularity test.
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...
void find_all_reductions(Unifier &, vector< InferenceItem > &, Clause &)
Given a Clause, find all possible reductions given the current Path.
Prover using a pair of stacks to conduct the proof search.
void set_num_preds(size_t)
Set the number of predicates.
bool depth_limit_reached
Self-explanatary.
void process_axiom_forward()
Start a right branch to continue from an axiom.
string status
Problem status, if found in input file.
void read_from_tptp_file(const string &, bool &, size_t &)
Obviously, reads a problem from a TPTP file.
vector< StartClauseStatus > results
This is populated by the StackProver::set_up_start_clauses method.
bool negated_conjecture_removed
Keep track of whether the parser simplified the conjecture away.
uint32_t lemmata_tried
We'll be keeping some simple statistics about the search process.
void lemmata_backtrack()
One of several different kinds of backtracking.
void reset_for_start()
Reset everything so that you can start from a specified start clause.
uint32_t current_depth_limit
Self-explanatary.
InferenceItem action
Stores the next action from the current StackItem.
void set_up_start_clauses()
The start clauses to use depend on the settings, and the settings can change.
size_t num_preds
How many prdicates does the problem of interest have?
bool fof_has_axioms
Keep track of whether the parser found that it's an FOF problem with axioms before simplification.
vector< StackItem > stack
Main stack: this is constructed by the search process and, if completed, represents a proof.
ProverResult go()
This runs the proof search from a given Start Move.
Matrix matrix
A copy of the matrix you're working with.
PredicateIndex pred_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
vector< StackItem > right_branch_stack
We build the proof by trying the left branches of extensions first: this stack keeps track of the rig...
ProofPrinter proof_printer
You need one of these to print LaTeX output or any kind of proof certificate.
void extend_with_action()
Take a single inference (action) and update the stacks accordingly.
bool cnf_only
Keep track of whether there were any FOF formulas in the problem file.
SimplePath path
At any point in the search process this is a copy of the path for the current node in the proof being...
FunctionIndex fun_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
void populate_stack_item()
Fill the vector of possible actions with everything available.
Lemmata lemmata
At any point in the search process this is a copy of the list of lemmata for the current node in the ...
uint32_t extensions_tried
We'll be keeping some simple statistics about the search process.
uint32_t current_depth
Self-explanatary.
void add_equality_axioms(Predicate *)
After reading a problem in which = and/or != appears, add the axioms for equality.
bool simplified_fof_has_axioms
Keep track of whether the parser found that it's an FOF problem with axioms after simplification.
bool conjecture_missing
Keep track of whether the parser found a conjecture in the problem file.
TermIndex term_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
uint32_t proof_count
If we're searching for multiple proofs, keep count of which one this is.
bool conjecture_false
Keep track of whether the parser found the conjecture to be false.
VariableIndex var_index
This class needs one of each kind of index to keep track of Variables, Terms etc.
void backtrack_once()
Basic, single step backtrack on the stack.
bool depth_limited()
Test for the depth limit.
bool conjecture_true
Keep track of whether the parser found the conjecture to be true.
void left_extension_backtrack()
One of several different kinds of backtracking.
uint32_t right_branches_started
We'll be keeping some simple statistics about the search process.
bool backtrack
Are we moving up or down the stack?
chrono::steady_clock::time_point end_time
When do we stop because of a timeout?
vector< pair< string, vector< size_t > > > get_internal_proof() const
Get an internal representation of the proof stack.
StackItem * si
Pointer to the current StackItem.
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...
void right_extension_backtrack()
One of several different kinds of backtracking.
fs::path problem_path
Path for the problem of interest.
StackProver()
You only need a basic constructor.
bool use_timeout
Are we using a timeout?
void reduction_backtrack()
One of several different kinds of backtracking.
uint32_t reductions_tried
We'll be keeping some simple statistics about the search process.
SubstitutionStack sub_stack
There is a separate stack to make application and removal of substitutions straightforward.
verbose_print::VPrint show
Set up printing according to verbosity.
Unifier u
We need a single Unifier to use throught the process.
bool axiom() const
Test to see if you're at an axiom.
ProverOutcome prove()
Here is where the magic happens.
Interval output_interval
How often do you output updates about progress?
void apply() const
Apply a substitution everywhere.
void backtrack()
Remove variables from the stack, and remove substitutions as you go, as far back as the most recent b...
void push_all(Substitution &)
Take all the substitutions provided and add the corresponding variables to the stack.
Wrap up everything the TPTP parser needs to do inside a single class.
bool simplified_fof_has_axioms() const
Where there any axioms for an FOF problem after simplification?
string get_problem_status()
The parse tries to identify the problem status.
void clear()
Clear everything associated with the TPTP parser.
bool parse_tptp_from_file(const string &)
Main method to parse from a TPTP file to the data structures needed by the prover.
bool fof_conjecture_is_missing() const
Was there a conjecture clause in the problem file?
bool equality_used()
Did equality turn up anywhere in the parse?
bool conjecture_present() const
Did a conjecture turn up anywhere in the parse?
bool fof_has_axioms() const
Where there any axioms for an FOF problem before simplification?
bool fof_conjecture_is_false() const
Self-explanatory.
bool fof_conjecture_is_true() const
Self-explanatory.
Predicate * get_equals_predicate() const
If equality turned up anywhere in the parse it will have been turned into an actual Predicate,...
bool problem_is_cnf_only() const
Self-explanatory.
size_t number_of_fof_formulas() const
How many first-order formulas turned up in the parse?
bool fof_negated_conjecture_removed() const
Was there a conjecture clause that got simplified away?
General representation of terms.
Term * add_function_term(Function *, const vector< Term * > &)
Self-explanatory: add a Term containing a function to the index.
Term * add_variable_term(Variable *)
Self-explanatory: add a Term containing a variable to the index.
Basic representation of variables.
Variable * add_named_var(const string &)
Add a variable with the specified name to the index.
void set_all_names_added()
Call this to indicate that only anonymous variables can now be created.
void backtrack()
Backtrack to the last marker.
void add_backtrack_point()
Add a backtrack point.
Simple addition of colour to strings and ostreams.
static string erase_line(uint8_t n)
void nl(uint8_t, uint8_t=1)
Full representation of inferences, beyond just the name.
LitNum Lindex
The index of the literal within the clause being used.
LitNum Lprime
The index of the literal in C_2 being used.
Substitution sigma
A copy of the substitution that makes the rule applicable.
Literal L
The Literal that is used to make the inference.
ClauseNum C_2
For extensions, the number of the clause for which a fresh copy is being made.
InferenceItemType T
What kind of inference is this?
Stack items: each contains its own stack of possible next inferences.
void restrict_backtrack()
Adjust the collection of actions to limit backtracking.
SimplePath p
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the path.
vector< InferenceItem > actions
Actions available to try.
uint32_t depth
How deep in the proof tree are we?
size_t bt_restriction_index
Pointer that allows a right branch to know where to delete alternatives for restricted backtracking.
void set_this_action(const InferenceItem &inf_i)
Basic set method.
Lemmata l
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the lemmata.
Clause c
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the clause.
StackItemType item_type
What type of StackItem is this?
Structure containing all the command line and other options.
static void set_complete_parameters()
Change the parameters to make the search complete.
static bool no_start_options()
Self-explanatory.
static void correct_missing_start_options()
Self-explanatory.
static bool search_is_complete()
Self-explanatory.