7 #include "core/SolverTypes.h" 22 this->encoder = encoder;
43 for (
unsigned i = 0; i < courses.size(); i++) {
44 for (
unsigned j = i + 1; j < courses.size(); j++) {
50 encoder->hasSameFieldTypeNotSameValue(i, j, fieldType);
51 Clauses consequent = encoder->notIntersectingTime(i, j);
67 Clauses ConstraintAdder::instructorSingleCourseAtATime() {
68 return fieldSingleValueAtATime(FieldType::instructor);
80 Clauses ConstraintAdder::classroomSingleCourseAtATime() {
81 return fieldSingleValueAtATime(FieldType::classroom);
93 Clauses ConstraintAdder::programSingleCoreCourseAtATime() {
97 for (
unsigned i = 0; i < courses.size(); i++) {
98 for (
unsigned j = i + 1; j < courses.size(); j++) {
103 Clauses antecedent = encoder->hasNoCommonCoreProgram(i, j);
104 Clauses consequent = encoder->notIntersectingTime(i, j);
119 std::vector<Clauses> ConstraintAdder::minorInMinorTime() {
121 std::vector<Clauses> result(courses.size());
122 for (
unsigned i = 0; i < courses.size(); i++) {
128 Clauses antecedent = encoder->isMinorCourse(i);
129 Clauses consequent = encoder->slotInMinorTime(i);
130 result[i].
addClauses(antecedent >> consequent);
131 result[i].addClauses(consequent >> antecedent);
150 std::vector<Clauses> ConstraintAdder::exactlyOneFieldValuePerCourse(
153 std::vector<Clauses> result(courses.size());
154 for (
unsigned i = 0; i < courses.size(); i++) {
158 encoder->hasExactlyOneFieldValueTrue(i, fieldType);
163 result[i].addClauses(cclause >> exactlyOneFieldValue);
207 addSingleConstraint(PredefinedClauses::instructorSingleCourseAtATime,
208 instructorSingleCourseAtATime(), -1);
209 addSingleConstraint(PredefinedClauses::classroomSingleCourseAtATime,
210 classroomSingleCourseAtATime(), -1);
211 addSingleConstraint(PredefinedClauses::programSingleCoreCourseAtATime,
212 programSingleCoreCourseAtATime(), -1);
214 auto clauses = minorInMinorTime();
215 for (
unsigned i = 0; i < clauses.size(); i++) {
216 addSingleConstraint(PredefinedClauses::minorInMinorTime, clauses[i], i);
219 clauses = programAtMostOneOfCoreOrElective();
220 for (
unsigned i = 0; i < clauses.size(); i++) {
221 addSingleConstraint(PredefinedClauses::programAtMostOneOfCoreOrElective,
225 clauses = exactlyOneFieldValuePerCourse(FieldType::slot);
226 for (
unsigned i = 0; i < clauses.size(); i++) {
227 addSingleConstraint(PredefinedClauses::exactlyOneSlotPerCourse, clauses[i],
231 clauses = exactlyOneFieldValuePerCourse(FieldType::classroom);
232 for (
unsigned i = 0; i < clauses.size(); i++) {
233 addSingleConstraint(PredefinedClauses::exactlyOneClassroomPerCourse,
237 clauses = exactlyOneFieldValuePerCourse(FieldType::instructor);
238 for (
unsigned i = 0; i < clauses.size(); i++) {
239 addSingleConstraint(PredefinedClauses::exactlyOneInstructorPerCourse,
243 clauses = exactlyOneFieldValuePerCourse(FieldType::isMinor);
244 for (
unsigned i = 0; i < clauses.size(); i++) {
245 addSingleConstraint(PredefinedClauses::exactlyOneIsMinorPerCourse,
249 clauses = exactlyOneFieldValuePerCourse(FieldType::segment);
250 for (
unsigned i = 0; i < clauses.size(); i++) {
251 addSingleConstraint(PredefinedClauses::exactlyOneSegmentPerCourse,
255 clauses = coreInMorningTime();
256 for (
unsigned i = 0; i < clauses.size(); i++) {
257 addSingleConstraint(PredefinedClauses::coreInMorningTime, clauses[i], i);
260 clauses = electiveInNonMorningTime();
261 for (
unsigned i = 0; i < clauses.size(); i++) {
262 addSingleConstraint(PredefinedClauses::electiveInNonMorningTime, clauses[i],
278 std::vector<Clauses> ConstraintAdder::coreInMorningTime() {
280 std::vector<Clauses> result(courses.size());
281 for (
unsigned i = 0; i < courses.size(); i++) {
283 Clauses coreCourse = encoder->isCoreCourse(i);
284 Clauses morningTime = encoder->courseInMorningTime(i);
285 result[i].
addClauses(coreCourse >> morningTime);
297 std::vector<Clauses> ConstraintAdder::electiveInNonMorningTime() {
299 std::vector<Clauses> result(courses.size());
300 for (
unsigned i = 0; i < courses.size(); i++) {
302 Clauses coreCourse = encoder->isElectiveCourse(i);
303 Clauses morningTime = encoder->courseInMorningTime(i);
304 result[i].
addClauses(coreCourse >> (~morningTime));
318 std::vector<Clauses> ConstraintAdder::programAtMostOneOfCoreOrElective() {
320 std::vector<Clauses> result(courses.size());
321 for (
unsigned i = 0; i < courses.size(); i++) {
323 result[i].addClauses(encoder->programAtMostOneOfCoreOrElective(i));
void addConstraints()
Adds all the constraints with their respective weights using the Timetabler object to the solver...
std::vector< int > predefinedClausesWeights
Class for representing a clause.
std::vector< std::vector< Var > > predefinedConstraintVars
PredefinedClauses
Enum that represents all the predefined constraints.
Class for constraint encoder.
FieldType
Enum that represents all the field types.
void addSingleConstraint(PredefinedClauses, const Clauses &, const int course)
Adds a single predefined constraint to the solver.
void addClauses(const CClause &)
Adds a CClause to the set of clauses.
std::vector< Course > courses
void clear()
Clears the Clauses object by removing all the clauses.
std::vector< std::vector< Var > > highLevelVars
Class for representing a set of clauses.
ConstraintAdder(ConstraintEncoder *, Timetabler *)
Constructs the ConstraintAdder object.