Clause Class Reference

Representation of clauses. More...

#include <Clause.hpp>

Public Member Functions
	Clause (const vector< Literal > &new_lits)
	Construction is just taking a new vector of Literals.
size_t	size () const
	Straightforward get method.
bool	empty () const
	Straightforward get method.
void	clear ()
	Straightforward reset method.
bool	is_positive () const
	A clause is positive if it has no negated literals.
bool	is_negative () const
	A clause is negative if it has only negated literals.
void	remove_duplicates ()
	Get rid of identical literals.
bool	has_complementary_literals () const
	Check whether the clause contains complementary literals.
void	add_lit (const Literal &)
	Add a literal, making sure you don't duplicate.
void	drop_literal (LitNum)
	Get rid of the specified Literal.
Literal	extract_literal (LitNum)
	Get rid of and return the specified Literal.
Literal &	operator[] (size_t)
	Direct read of the specified Literal.
Clause	make_copy_with_new_vars (VariableIndex &, TermIndex &) const
	Make a copy of an entire clause, introducing new variables.
SimplificationResult	simplify ()
	Simplify a clause by dealing with $true, $false, complementary literals, and duplicates.
string	to_string (bool=false) const
	Convert to a string.
string	to_prolog_string () const
	Convert to a string that can be read by Prolog.
string	make_LaTeX (bool=false) const
	Convert the clause to a LaTeX representation.
vector< Literal >::const_iterator	cbegin () const
vector< Literal >::const_iterator	cend () const
vector< Literal >::iterator	begin ()
vector< Literal >::iterator	end ()

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

Detailed Description

Representation of clauses.

Essentially straightforward as they are just vectors of Literals. Other classes do all the heavy lifting.

Constructor & Destructor Documentation

Clause()

Clause::Clause ( const vector< Literal > &  new_lits )

inline

Construction is just taking a new vector of Literals.

Parameters

new_lits

Reference to new vector of Literals.

Member Function Documentation

add_lit()

void Clause::add_lit

(

const Literal &

l

)

Add a literal, making sure you don't duplicate.

Yes, yes a set<> would be a good idea, but vectors are easy, nicer if you want indexes amd nicer for the cache.

Parameters

l	Reference to Literal to add

drop_literal()

void Clause::drop_literal

(

LitNum

l

)

Get rid of the specified Literal.

Parameters

l	Index of literal to remove.

extract_literal()

Literal Clause::extract_literal

(

LitNum

l

)

Get rid of and return the specified Literal.

Parameters

l	Index of literal to remove.

has_complementary_literals()

bool Clause::has_complementary_literals

(

)

const

Check whether the clause contains complementary literals.

This does not take account of substitutions as it is mainly used for simplification before any substitutions happen.

make_copy_with_new_vars()

Clause Clause::make_copy_with_new_vars	(	VariableIndex &	vi,
		TermIndex &	ti
	)		const

Make a copy of an entire clause, introducing new variables.

Straightforward because the heavy lifting is done elsewhere.

Parameters

vi	Reference to the VariableIndex
ti	Reference to the TermIndex

make_LaTeX()

string Clause::make_LaTeX

(

bool

subbed = false

)

const

Convert the clause to a LaTeX representation.

Assumes you are in Math Mode.

Parameters

subbed

implement substitution if true.

operator[]()

Literal & Clause::operator[]

(

size_t

i

)

Direct read of the specified Literal.

There is no check on whether you've given a sensible index, so behave yourself!

Parameters

i	Index of required Literal

remove_duplicates()

void Clause::remove_duplicates

(

)

Get rid of identical literals.

This does not take account of substitutions as it is mainly used for simplification before any substitutions happen.

to_prolog_string()

string Clause::to_prolog_string

(

)

const

Convert to a string that can be read by Prolog.

Does not apply substitutions.

to_string()

string Clause::to_string

(

bool

subbed = false

)

const

Convert to a string.

Parameters

subbed

Implement substitutions if true.

---

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

• Clause.hpp
• Clause.cpp