Timetabler
|
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 &) |
Clauses | operator & (const Clauses &) |
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. | |
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.
CClause::CClause | ( | const std::vector< Lit > & | lits | ) |
Constructs the CClause object.
[in] | lits | The literals in the clause |
Definition at line 16 of file cclause.cpp.
CClause::CClause | ( | const Lit & | lit | ) |
Constructs the CClause object.
[in] | lit | A literal, which creates a unit clause |
Definition at line 23 of file cclause.cpp.
CClause::CClause | ( | const Var & | var | ) |
Constructs the CClause object.
[in] | var | A variable, which is converted to a Lit with positive polarity and added to create a unit clause |
Definition at line 34 of file cclause.cpp.
void CClause::addLits | ( | const Lit & | lit1 | ) |
Adds a Lit, a literal, to the clause.
[in] | lit1 | The literal to be added |
Definition at line 251 of file cclause.cpp.
Referenced by ConstraintEncoder::hasSameFieldTypeNotSameValue(), operator|(), and Clauses::operator|().
void CClause::addLits | ( | const Lit & | lit1, |
const Lit & | lit2 | ||
) |
Adds two Lits to the clause.
[in] | lit1 | The first Lit |
[in] | lit2 | The second Lit |
Definition at line 259 of file cclause.cpp.
void CClause::addLits | ( | const Lit & | lit1, |
const Lit & | lit2, | ||
const Lit & | lit3 | ||
) |
Adds three Lits to the clause.
[in] | lit1 | The first Lit |
[in] | lit2 | The second Lit |
[in] | lit3 | The third Lit |
Definition at line 271 of file cclause.cpp.
void CClause::addLits | ( | const std::vector< Lit > & | otherLits | ) |
Adds a vector of Lits to the clause.
[in] | otherLits | The vector of Lits to be added |
Definition at line 282 of file cclause.cpp.
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.
[in] | var1 | The variable to be added |
Definition at line 213 of file cclause.cpp.
Referenced by ConstraintEncoder::hasAtLeastOneFieldValueTrue(), ConstraintEncoder::hasFieldTypeListedValues(), and ConstraintEncoder::hasSameFieldTypeAndValue().
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.
[in] | var1 | The first Var |
[in] | var2 | The second Var |
Definition at line 225 of file cclause.cpp.
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.
[in] | var1 | The first Var |
[in] | var2 | The second Var |
[in] | var3 | The third Var |
Definition at line 239 of file cclause.cpp.
std::vector< Lit > CClause::getLits | ( | ) | const |
Gets the literals in the clause.
Definition at line 291 of file cclause.cpp.
Referenced by operator|().
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.
other | The clause which is the consequent |
Definition at line 178 of file cclause.cpp.
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.
other | The Clauses which form the consequent |
Definition at line 200 of file cclause.cpp.
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.
other | The clause to disjunct with |
Definition at line 113 of file cclause.cpp.
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.
other | The Clauses to disjunct with |
Definition at line 160 of file cclause.cpp.
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.
Definition at line 53 of file cclause.cpp.
References Clauses::addClauses(), and Clauses::getClauses().