Timetabler
|
Class for time tabler. More...
#include <time_tabler.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 | 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) |
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.
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 |
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 |
void Timetabler::addHighLevelConstraintClauses | ( | PredefinedClauses | clauseType | ) |
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 |
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 |
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 |
void Timetabler::addToFormula | ( | Lit | input, |
int | weight | ||
) |
Add single literal to the formula.
[in] | input | The input |
[in] | weight | The weight |
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 |
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 |
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 |
Var Timetabler::newVar | ( | ) |
Calls the formula to issue a new variable and returns it.
SolverStatus Timetabler::solve | ( | ) |
Calls the solver to solve for the constraints.
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 |
Data Timetabler::data |
Stores all the field and input data obtained by the parser