StackProver Class Reference

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

#include <StackProver.hpp>

Public Member Functions
	StackProver ()
	You only need a basic constructor.
	StackProver (const StackProver &)=delete
	Don't try to copy this.
	StackProver (const StackProver &&)=delete
StackProver &	operator= (const StackProver &)=delete
StackProver &	operator= (const StackProver &&)=delete
std::tuple< VariableIndex *, FunctionIndex *, PredicateIndex *, TermIndex * >	get_indexes ()
	Straightforward get method.
string	get_status () const
	Straightforward get method.
void	set_timeout (chrono::steady_clock::time_point time)
	Set a timeout.
void	set_problem_path (fs::path &p)
	Set the path for the problem being solved. U.
void	set_num_preds (size_t)
	Set the number of predicates.
void	read_from_tptp_file (const string &, bool &, size_t &)
	Obviously, reads a problem from a TPTP file.
void	add_equality_axioms (Predicate *)
	After reading a problem in which = and/or != appears, add the axioms for equality.
void	deterministic_reorder (uint32_t n)
	Deterministically reorder the matrix n times.
void	show_matrix ()
	Show a nicely formatted matrix.
ProverOutcome	prove ()
	Here is where the magic happens.
void	show_matrix () const
void	show_path () const
void	show_stack ()
void	show_right_stack ()
void	show_term_index ()
void	show_statistics () const

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

Detailed Description

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

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

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

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

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_predicate

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

deterministic_reorder()

void StackProver::deterministic_reorder ( uint32_t  n )

inline

Deterministically reorder the matrix n times.

Parameters

n	Number of times to reorder.

prove()

ProverOutcome StackProver::prove

(

)

Here is where the magic happens.

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

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_name	Name of the file to use.
found_conjecture	Used to indicate whether a conjecture is found in the problem.
fof_size	Number of first-order formulas found.

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.

set_problem_path()

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

inline

Set the path for the problem being solved. U.

Used only to produce nice output.

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

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

---

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

• StackProver.hpp
• StackProver.cpp