Timetabler
|
Class for time tabler. More...
#include <timetabler.h>
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 |
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.
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.
[in] | clauses | The clauses |
[in] | weight | The weight |
Definition at line 35 of file timetabler.cpp.
Referenced by ConstraintAdder::addSingleConstraint(), and Clauses::operator|().
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.
[in] | clauses | The clauses |
[in] | weight | The weight |
Definition at line 176 of file timetabler.cpp.
References Clauses::getClauses().
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.
[in] | clauseType | The clause type |
[in] | course | The corresponding course index (-1 for if there is no corresponding course) |
Definition at line 72 of file timetabler.cpp.
Referenced by ConstraintAdder::addSingleConstraint().
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.
[in] | index | The index of the custom constraint variable |
[in] | weight | The weight of the custom constraint |
Definition at line 105 of file timetabler.cpp.
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.
input | The input | |
[in] | weight | The weight |
Definition at line 147 of file timetabler.cpp.
Referenced by Clauses::operator|().
void Timetabler::addToFormula | ( | Lit | input, |
int | weight | ||
) |
Add single literal to the formula.
[in] | input | The input |
[in] | weight | The weight |
Definition at line 161 of file timetabler.cpp.
bool Timetabler::checkAllTrue | ( | const std::vector< Var > & | inputs | ) |
Checks if a given set of variables are true in the model returned by the solver.
[in] | inputs | The input variables |
Definition at line 207 of file timetabler.cpp.
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.
[in] | inputs | The input variables |
Definition at line 227 of file timetabler.cpp.
bool Timetabler::isVarTrue | ( | const Var & | v | ) |
Determines if a given variable is true in the model returned by the solver.
[in] | v | The variable to be checked |
Definition at line 247 of file timetabler.cpp.
Lit Timetabler::newLiteral | ( | bool | sign = false | ) |
Calls the formula to issue a new literal and returns it.
[in] | sign | The sign, whether the literal contains a sign with the variable |
Definition at line 276 of file timetabler.cpp.
Referenced by Clauses::operator|().
Var Timetabler::newVar | ( | ) |
Calls the formula to issue a new variable and returns it.
Definition at line 262 of file timetabler.cpp.
Referenced by Parser::addVars().
SolverStatus Timetabler::solve | ( | ) |
Calls the solver to solve for the constraints.
Definition at line 185 of file timetabler.cpp.
References HighLevelFailed, Solved, and Unsolved.
void Timetabler::writeOutput | ( | std::string | fileName | ) |
Writes the generated time table to a CSV file.
[in] | fileName | The file path of the output CSV file |
Definition at line 379 of file timetabler.cpp.
Data Timetabler::data |
Stores all the field and input data obtained by the parser
Definition at line 63 of file timetabler.h.
Referenced by ConstraintAdder::addConstraints(), ConstraintAdder::addSingleConstraint(), Parser::addVars(), ConstraintAdder::ConstraintAdder(), ConstraintEncoder::ConstraintEncoder(), Parser::parseInput(), and Parser::verify().