SimplePath Class Reference

Simple representation of the path within a proof tree. More...

#include <SimplePath.hpp>

Public Member Functions
	SimplePath ()
	You should () usually never need a more compilcated constructor.
	SimplePath (uint32_t)
	Use this constructor if you know how many predicates there are.
uint32_t	length () const
	Straightforward get method.
void	clear ()
	evert to the empty state without changing num_preds.
void	set_num_preds (size_t num_predicates)
	Set method for num_predicates.
void	push (const Literal &)
	Add a new Literal to the Path.
Literal	back () const
	Get the last Literal in the Path. Non-destructive.
void	pop ()
	Remove the last item from the Path.
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 in the Clause.
void	find_all_reductions (Unifier &, vector< InferenceItem > &, Clause &)
	Given a Clause, find all possible reductions given the current Path.
void	show_path_only (ostream &)
	Show just the path.
string	to_string (bool=false) const
	Convert the path to a string.
string	make_LaTeX (bool=false) const
	Convert the Path only to a LaTeX representation.
vector< Literal >::const_iterator	cbegin () const
	Iterators just traverse the path vector.
vector< Literal >::const_iterator	cend () const
vector< Literal >::iterator	begin ()
vector< Literal >::iterator	end ()

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

Detailed Description

Simple representation of the path within a proof tree.

While the Path class (not part of the source distribution) keeps a separate vector of literals for each possible predicate/negation c ombination so it's fast to get the potential literals for reductions, this does not. The reason is that this one needs to be copied to support full backtracking, and I haven't yet looked at optimising to see what the trade-off is between finding reductions fast, and making copies of the path_index.

This class is also a natural location for any methods used to find reductions, and a natural location for the test_for_regularity method.

Constructor & Destructor Documentation

SimplePath()

SimplePath::SimplePath

(

uint32_t

num_predicates

)

Use this constructor if you know how many predicates there are.

Parameters

num_predicates

Number of predicates.

Member Function Documentation

find_all_reductions()

void SimplePath::find_all_reductions	(	Unifier &	u,
		vector< InferenceItem > &	result,
		Clause &	c
	)

Given a Clause, find all possible reductions given the current Path.

See also the documentation for find_reductions.

Parameters

u	A reference to a Unifier function object.
result	A reference to a vector of InferenceItems. Start with this empty.
c	A Clause that you want the reductions for.

find_limited_reductions()

void SimplePath::find_limited_reductions	(	Unifier &	u,
		vector< InferenceItem > &	result,
		Clause &	c
	)

Given a Clause, find all possible reductions given the current Path, but only for the first Literal in the Clause.

See also the documentation for find_reductions.

Parameters

u	A reference to a Unifier function object.
result	A reference to a vector of InferenceItems. Start with this empty.
c	A Clause that you want the reductions for.

make_LaTeX()

string SimplePath::make_LaTeX

(

bool

subbed = false

)

const

Convert the Path only to a LaTeX representation.

Parameters

subbed

Implement substitutions if true.

push()

void SimplePath::push

(

const Literal &

lit

)

Add a new Literal to the Path.

Parameters

lit	Reference to Literal to add.

show_path_only()

void SimplePath::show_path_only

(

ostream &

out

)

Show just the path.

Use this if you don't need to see the index and other information.

This method is slightly out of place here as it's mainly for compatability with the Path class, that is not currently part of the distribution, You can probably safely ignore it.

Parameters

out	Reference to an ostream.

test_for_regularity()

bool SimplePath::test_for_regularity

(

Clause &

c

)

const

Regularity test.

Taking substitutions into account, test whether any literal in the clause appears in the path.

Parameters

c	Reference to Clause to use.

to_string()

string SimplePath::to_string

(

bool

subbed = false

)

const

Convert the path to a string.

Parameters

subbed

Implement substitution if true.

---

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

• SimplePath.hpp
• SimplePath.cpp