Matrix Class Reference

Representation of the Matrix within a proof. More...

#include <Matrix.hpp>

Public Member Functions
	Matrix ()
	Use this constructor if you really want an empty Matrix.
	Matrix (size_t)
	Use this constructor when you know how many predicates there are.
	Matrix (const Matrix &)=delete
	You're never going to need to copy a Matrix.
	Matrix (const Matrix &&)=delete
Matrix &	operator= (const Matrix &)=delete
Matrix &	operator= (const Matrix &&)=delete
ClauseNum	get_num_clauses () const
	Straightforward get method.
const Clause &	operator[] (size_t i) const
	Straightforward get method.
bool	is_positive (size_t i) const
	Is a particular Clause positive?.
bool	is_negative (size_t i) const
	Is a particular Clause negative?.
bool	is_conjecture (size_t i) const
	Is a particular Clause a conjecture?
void	set_num_equals (uint32_t n)
	Straightforward set method.
pair< bool, size_t >	find_start () const
	Use a simple heuristic to find a good start clause.
void	set_num_preds (size_t)
	Make an empty index.
void	add_clause (Clause &, string="")
	Add a Clause to the Matrix and update the index accordingly.
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.
void	deterministic_reorder (size_t)
	Deterministic reorder of the clauses.
void	move_equals_to_start ()
	Self-explanatory.
vector< Clause >::const_iterator	cbegin () const
vector< Clause >::const_iterator	cend () const
vector< Clause >::iterator	begin ()
vector< Clause >::iterator	end ()
string	to_string () const
	Make a string representation.
string	make_LaTeX (bool=false) const
	Make a usable LaTeX representation.
void	write_to_prolog_file (const path &) const
	Write to a file that can be read by Prolog.

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

Detailed Description

Representation of the Matrix within a proof.

The Matrix itself never actually changes. However we do want to be able to look things up quickly when finding possible extension steps, so we build an index to help with that.

This class is also the natural place to implement the finding of all extensions, and the start clause heuristics.

Constructor & Destructor Documentation

Matrix() [1/2]

Matrix::Matrix

(

size_t

num_predicates

)

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

Parameters

num_predicates

Number of predicates.

Matrix() [2/2]

Matrix::Matrix ( const Matrix &  )

delete

You're never going to need to copy a Matrix.

Let the compiler be your friend.

Member Function Documentation

add_clause()

void Matrix::add_clause	(	Clause &	clause,
		string	role = ""
	)

Add a Clause to the Matrix and update the index accordingly.

Optionally add a clause role.

Parameters

clause	Reference to the Clause.
role	A string denoting the role of the clause.

deterministic_reorder()

void Matrix::deterministic_reorder

(

size_t

n

)

Deterministic reorder of the clauses.

Call the reorder algorithm the specified number of times. This assumes you have stored a copy of the original clauses.

Parameters

n	Number of times to call the reorder algorithm

Only store a copy of the clauses the first time you do this.

find_all_extensions()

void Matrix::find_all_extensions	(	Unifier &	u,
		vector< InferenceItem > &	result,
		Clause &	c,
		VariableIndex &	var_index,
		TermIndex &	term_index
	)

Find all possible extensions given a Clause, considering all Literals in the Clause.

See the documentation for find_extensions, which does all the heavy lifting.

Parameters

u	A reference to a Unifier function object.
result	A reference to a vector of InferenceItems. Start with this empty.
c	The Clause of interest.
var_index	A reference to the VariableIndex.
term_index	A reference to the TermIndex.

find_limited_extensions()

void Matrix::find_limited_extensions	(	Unifier &	u,
		vector< InferenceItem > &	result,
		Clause &	c,
		VariableIndex &	var_index,
		TermIndex &	term_index
	)

Find all possible extensions given a Clause, but only consider the first Literal in the Clause.

See the documentation for find_extensions, which does all the heavy lifting.

Parameters

u	A reference to a Unifier function object.
result	A reference to a vector of InferenceItems. Start with this empty.
c	The Clause of interest.
var_index	A reference to the VariableIndex.
term_index	A reference to the TermIndex.

find_start()

pair< bool, size_t > Matrix::find_start

(

)

const

Use a simple heuristic to find a good start clause.

Find a start clause that is positive/negative according to the –negative flag, and if possible also a conjecture clause. Also, indicate if there is no positive/negative clause, which means the problem is trivial.

is_conjecture()

bool Matrix::is_conjecture

(

size_t

i

)

const

Is a particular Clause a conjecture?

Parameters

i	Index of Clause to check.

is_negative()

bool Matrix::is_negative ( size_t  i ) const

inline

Is a particular Clause negative?.

Parameters

i	Index of Clause to check.

is_positive()

bool Matrix::is_positive ( size_t  i ) const

inline

Is a particular Clause positive?.

Parameters

i	Index of Clause to check.

make_LaTeX()

string Matrix::make_LaTeX

(

bool

subbed = false

)

const

Make a usable LaTeX representation.

Parameters

subbed

Implement substitutions if true.

move_equals_to_start()

void Matrix::move_equals_to_start

(

)

Self-explanatory.

BUT only do this to the matrix built at the start of the process, as it assumes the equality axioms are at the end of the matrix.

operator[]()

const Clause & Matrix::operator[] ( size_t  i ) const

inline

Straightforward get method.

Beware - the parameter is not checked, so behave!

Parameters

i	Index of item to get.

set_num_equals()

void Matrix::set_num_equals ( uint32_t  n )

inline

Straightforward set method.

Parameters

n	Number of equality axioms.

write_to_prolog_file()

void Matrix::write_to_prolog_file

(

const path &

path_to_file

)

const

Write to a file that can be read by Prolog.

This is for proof checking.

Parameters

path_to_file

Reference to path object.

---

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

• Matrix.hpp
• Matrix.cpp