Timetabler
Public Member Functions | Public Attributes | List of all members
Timetabler Class Reference

Class for time tabler. More...

#include <timetabler.h>

Collaboration diagram for Timetabler:
Collaboration graph
[legend]

Public Member Functions

 Timetabler ()
 Constructs the Timetabler object.
 
 ~Timetabler ()
 Destroys the object, and deletes the solver.
 
void addClauses (const std::vector< CClause > &, int)
 Adds clauses to the solver with specified weights. More...
 
void addClauses (const Clauses &, int)
 Adds clauses to the solver with specified weights. More...
 
bool checkAllTrue (const std::vector< Var > &)
 Checks if a given set of variables are true in the model returned by the solver. More...
 
bool checkAllTrue (const std::vector< std::vector< Var >> &)
 Checks if a given set of variables (in 2D vector) are true in the model returned by the solver. More...
 
bool isVarTrue (const Var &)
 Determines if a given variable is true in the model returned by the solver. More...
 
SolverStatus solve ()
 Calls the solver to solve for the constraints. More...
 
Var newVar ()
 Calls the formula to issue a new variable and returns it. More...
 
Lit newLiteral (bool sign=false)
 Calls the formula to issue a new literal and returns it. More...
 
void printResult (SolverStatus)
 Prints the result of the problem.
 
void displayTimeTable ()
 Displays the generated time table.
 
void displayUnsatisfiedOutputReasons ()
 Displays the reasons due to which the formula could not be satisfied, if applicable.
 
void addHighLevelClauses ()
 Adds unit soft clauses for the high level variables to the solver.
 
void addHighLevelConstraintClauses (PredefinedClauses, const int course)
 Adds high level clauses for predefined constraints. More...
 
void addHighLevelCustomConstraintClauses (int, int)
 Adds high level custom constraint clauses. More...
 
void writeOutput (std::string)
 Writes the generated time table to a CSV file. More...
 
void addExistingAssignments ()
 Adds unit clauses corresponding to existing assignments given in the input to the solver.
 
void addToFormula (vec< Lit > &, int)
 Add a given vec of literals with the given weight to the formula. More...
 
void addToFormula (Lit, int)
 Add single literal to the formula. More...
 
void displayChangesInGivenAssignment ()
 Displays the changes that have been made to the default assignment given by the user as input by the solver.
 

Public Attributes

Data data
 

Detailed Description

Class for time tabler.

This class is responsible for handling the solver. This accepts constraints, adds it to the MaxSATFormula, calls the solver, and interprets and displays the result. It is also responsible for writing the output to a CSV, and creating new literals or variables in the solver when requested and returning them.

Definition at line 44 of file timetabler.h.

Member Function Documentation

◆ addClauses() [1/2]

void Timetabler::addClauses ( const std::vector< CClause > &  clauses,
int  weight 
)

Adds clauses to the solver with specified weights.

A negative weight implies that the clauses are hard, and a zero weight implies that the clauses are not added to the solver.

Parameters
[in]clausesThe clauses
[in]weightThe weight

Definition at line 35 of file timetabler.cpp.

Referenced by ConstraintAdder::addSingleConstraint(), and Clauses::operator|().

◆ addClauses() [2/2]

void Timetabler::addClauses ( const Clauses clauses,
int  weight 
)

Adds clauses to the solver with specified weights.

A negative weight implies that the clauses are had, and a zero weight implies that the clauses are not added to the solver.

Parameters
[in]clausesThe clauses
[in]weightThe weight

Definition at line 176 of file timetabler.cpp.

References Clauses::getClauses().

◆ addHighLevelConstraintClauses()

void Timetabler::addHighLevelConstraintClauses ( PredefinedClauses  clauseType,
const int  course 
)

Adds high level clauses for predefined constraints.

For each predefined constraint C, a variable x is created, and a hard clause x->C is added to the solver. A unit clause with x is added as a soft clause with weight as specified for the constraint.

Parameters
[in]clauseTypeThe clause type
[in]courseThe corresponding course index (-1 for if there is no corresponding course)

Definition at line 72 of file timetabler.cpp.

Referenced by ConstraintAdder::addSingleConstraint().

◆ addHighLevelCustomConstraintClauses()

void Timetabler::addHighLevelCustomConstraintClauses ( int  index,
int  weight 
)

Adds high level custom constraint clauses.

For each custom constraint C, a variable x is created, and a hard clause x->C is added to the solver. A unit clause with x is added as a soft clause with weight as specified for the constraint.

Parameters
[in]indexThe index of the custom constraint variable
[in]weightThe weight of the custom constraint

Definition at line 105 of file timetabler.cpp.

◆ addToFormula() [1/2]

void Timetabler::addToFormula ( vec< Lit > &  input,
int  weight 
)

Add a given vec of literals with the given weight to the formula.

A negative weight implies that the clauses are had, and a zero weight implies that the clauses are not added to the solver.

Parameters
inputThe input
[in]weightThe weight

Definition at line 147 of file timetabler.cpp.

Referenced by Clauses::operator|().

◆ addToFormula() [2/2]

void Timetabler::addToFormula ( Lit  input,
int  weight 
)

Add single literal to the formula.

Parameters
[in]inputThe input
[in]weightThe weight

Definition at line 161 of file timetabler.cpp.

◆ checkAllTrue() [1/2]

bool Timetabler::checkAllTrue ( const std::vector< Var > &  inputs)

Checks if a given set of variables are true in the model returned by the solver.

Parameters
[in]inputsThe input variables
Returns
True, if all variables are True, False otherwise

Definition at line 207 of file timetabler.cpp.

◆ checkAllTrue() [2/2]

bool Timetabler::checkAllTrue ( const std::vector< std::vector< Var >> &  inputs)

Checks if a given set of variables (in 2D vector) are true in the model returned by the solver.

Parameters
[in]inputsThe input variables
Returns
True, if all variables are True, False otherwise

Definition at line 227 of file timetabler.cpp.

◆ isVarTrue()

bool Timetabler::isVarTrue ( const Var &  v)

Determines if a given variable is true in the model returned by the solver.

Parameters
[in]vThe variable to be checked
Returns
True if variable true, False otherwise

Definition at line 247 of file timetabler.cpp.

◆ newLiteral()

Lit Timetabler::newLiteral ( bool  sign = false)

Calls the formula to issue a new literal and returns it.

Parameters
[in]signThe sign, whether the literal contains a sign with the variable
Returns
The Lit corresponding to the new Var added to the formula

Definition at line 276 of file timetabler.cpp.

Referenced by Clauses::operator|().

◆ newVar()

Var Timetabler::newVar ( )

Calls the formula to issue a new variable and returns it.

Returns
The new Var added to the formula

Definition at line 262 of file timetabler.cpp.

Referenced by Parser::addVars().

◆ solve()

SolverStatus Timetabler::solve ( )

Calls the solver to solve for the constraints.

Returns
True, if all high level variables were satisfied, False otherwise

Definition at line 185 of file timetabler.cpp.

References HighLevelFailed, Solved, and Unsolved.

◆ writeOutput()

void Timetabler::writeOutput ( std::string  fileName)

Writes the generated time table to a CSV file.

Parameters
[in]fileNameThe file path of the output CSV file

Definition at line 379 of file timetabler.cpp.

Member Data Documentation

◆ data

Data Timetabler::data

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