Class for representing a clause. More...

#include <cclause.h>

Public Member Functions
	CClause (const std::vector< Lit > &)
	Constructs the CClause object. More...

	CClause (const Lit &)
	Constructs the CClause object. More...

	CClause (const Var &)
	Constructs the CClause object. More...

	CClause ()
	Constructs the CClause object, as an empty clause.

std::vector< CClause >	operator~ ()
	Defines the operator to negate the clause in this object. More...

std::vector< CClause >	operator& (const CClause &)
	Defines the operator to perform conjunction of two clauses. More...

Clauses	operator& (const Clauses &)
	Defines the operator to perform the conjunction of a clause with a set of clauses. More...

CClause	operator\| (const CClause &)
	Defines the operator to perform a disjunction of two clauses. More...

Clauses	operator\| (const Clauses &)
	Defines the operator to perform a disjunction between a clause and a set of Clauses. More...

std::vector< CClause >	operator>> (const CClause &)
	Defines the operator to perform an implication with another clause. More...

Clauses	operator>> (const Clauses &)
	Defines the operator to perform an implication with a set of Clauses. More...

void	createLitAndAdd (const Var &)
	Creates a Lit, a literal, given a variable, a Var, and adds it to the clause. More...

void	createLitAndAdd (const Var &, const Var &)
	Creates Lits given two Vars and adds them to the clause. More...

void	createLitAndAdd (const Var &, const Var &, const Var &)
	Creates Lits given three Vars and adds them to the clause. More...

void	addLits (const Lit &)
	Adds a Lit, a literal, to the clause. More...

void	addLits (const Lit &, const Lit &)
	Adds two Lits to the clause. More...

void	addLits (const Lit &, const Lit &, const Lit &)
	Adds three Lits to the clause. More...

void	addLits (const std::vector< Lit > &)
	Adds a vector of Lits to the clause. More...

std::vector< Lit >	getLits () const
	Gets the literals in the clause. More...

void	clear ()
	Clears the clause by removing all the literals.

void	printClause ()
	Displays the clause.

Detailed Description

Class for representing a clause.

A clause is represented as a vector of Lits. This class defines operators for operations between clauses, such as AND, OR, NOT, and IMPLIES, and functions to add literals and work with them in the clause. After each operation, the clause is maintained in the CNF form.

Constructor & Destructor Documentation

CClause::CClause ( const std::vector< Lit > & lits )

Constructs the CClause object.

Parameters

[in] lits The literals in the clause

CClause::CClause ( const Lit & lit )

Constructs the CClause object.

Parameters

[in] lit A literal, which creates a unit clause

CClause::CClause ( const Var & var )

Constructs the CClause object.

Parameters

[in] var A variable, which is converted to a Lit with positive polarity and added to create a unit clause

Member Function Documentation

void CClause::addLits ( const Lit & lit1 )

Adds a Lit, a literal, to the clause.

Parameters

[in] lit1 The literal to be added

void CClause::addLits	(	const Lit &	lit1,
		const Lit &	lit2
	)

Adds two Lits to the clause.

Parameters

[in]	lit1	The first Lit
[in]	lit2	The second Lit

void CClause::addLits	(	const Lit &	lit1,
		const Lit &	lit2,
		const Lit &	lit3
	)

Adds three Lits to the clause.

Parameters

[in]	lit1	The first Lit
[in]	lit2	The second Lit
[in]	lit3	The third Lit

void CClause::addLits ( const std::vector< Lit > & otherLits )

Adds a vector of Lits to the clause.

Parameters

[in] otherLits The vector of Lits to be added

void CClause::createLitAndAdd ( const Var & var1 )

Creates a Lit, a literal, given a variable, a Var, and adds it to the clause.

The literal is created with positive polarity.

Parameters

[in] var1 The variable to be added

void CClause::createLitAndAdd	(	const Var &	var1,
		const Var &	var2
	)

Creates Lits given two Vars and adds them to the clause.

The literals are created with positive polarity.

Parameters

[in]	var1	The first Var
[in]	var2	The second Var

void CClause::createLitAndAdd	(	const Var &	var1,
		const Var &	var2,
		const Var &	var3
	)

Creates Lits given three Vars and adds them to the clause.

The literals are created with positive polarity.

Parameters

[in]	var1	The first Var
[in]	var2	The second Var
[in]	var3	The third Var

std::vector< Lit > CClause::getLits ( ) const

Gets the literals in the clause.

Returns: The literals in the clause

std::vector< CClause > CClause::operator& ( const CClause & other )

Defines the operator to perform conjunction of two clauses.

The conjunction of clause (a1 OR a2) and (b1 OR b2) is given by ((a1 OR a2) AND (b1 OR b2)). This function simply returns a vector with both clauses appended to it.

Parameters

other The clause to conjunct with

Returns: The vector with the clauses as the result of performing the AND operation

Clauses CClause::operator& ( const Clauses & other )

Defines the operator to perform the conjunction of a clause with a set of clauses.

Given a clause and a set of clauses, the conjunction is simply appending all the clauses together. This does that and returns a Clauses object with all the clauses.

Parameters

other The set of clauses to conjunct with.

Returns: A Clauses object with the result of performing the AND operation

std::vector< CClause > CClause::operator>> ( const CClause & other )

Defines the operator to perform an implication with another clause.

Given this clause (a1 OR a2) and another clause (b1 OR b2), this defines ((a1 OR a2) -> (b1 OR b2)). This is done using the fact that (p->q) is equivalent to (~p OR q). This clause acts as the antecedent, and the argument as the consequent. The result is converted to CNF form and returned.

Parameters

other The clause which is the consequent

Returns: A vector of clauses as a result of the implication

Clauses CClause::operator>> ( const Clauses & other )

Defines the operator to perform an implication with a set of Clauses.

Given this clause p and a set of Clauses q, this computes and returns (p->q) in CNF form.

Parameters

other The Clauses which form the consequent

Returns: A Clauses object as a result of the implication

CClause CClause::operator| ( const CClause & other )

Defines the operator to perform a disjunction of two clauses.

The disjunction of clause (a1 OR a2) and (b1 OR b2) is given by (a1 OR a2 OR b1 OR b2). This is achieved by appending the literals of the two clauses and returning the resultant clause. Extra checks are added to avoid repeating literals.

Parameters

other The clause to disjunct with

Returns: The clause with the result on performing the OR operation

Clauses CClause::operator| ( const Clauses & other )

Defines the operator to perform a disjunction between a clause and a set of Clauses.

The working is described in the operator defined for OR between two Clauses objects. This function converts the current clause to a Clauses object and performs the operation.

Parameters

other The Clauses to disjunct with

Returns: A Clauses with the result of performing the AND operation

std::vector< CClause > CClause::operator~ ( )

Defines the operator to negate the clause in this object.

The negation of a clause (a1 OR a2 OR a3) is given by (~a1 AND ~a2 AND ~a3). Thus, the result is a set of clauses, and hence, this function returns this as a vector of CClause.

Returns: The negation of the clause

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

/home/docs/checkouts/readthedocs.org/user_builds/timetabler/checkouts/stable/include/cclause.h
/home/docs/checkouts/readthedocs.org/user_builds/timetabler/checkouts/stable/src/cclause.cpp

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation