Class for constraint encoder. More...

#include <constraint_encoder.h>

Public Member Functions
	ConstraintEncoder (Timetabler *)
	Constructs the ConstraintEncoder object. More...

Clauses	hasSameFieldTypeAndValue (int, int, FieldType)
	Gives Clauses that represent that a pair of courses have the same field value for a given FieldType. More...

Clauses	hasSameFieldTypeNotSameValue (int, int, FieldType)
	Gives Clauses that represent that a pair of courses do not have the same field value for a given FieldType. More...

Clauses	notIntersectingTime (int, int)
	Gives Clauses that represent that a pair of courses cannot have an intersecting schedule. More...

Clauses	notIntersectingTimeField (int, int, FieldType)
	Gives Clauses that represent that a pair of courses cannot have an intersecting value for a given FieldType, where the FieldType is of a time field, which is either a Segment or a Slot. More...

Clauses	hasExactlyOneFieldValueTrue (int, FieldType)
	Gives Clauses that represent that a Course can have exactly one field value of a given FieldType to be True. More...

Clauses	hasAtLeastOneFieldValueTrue (int, FieldType)
	Gives Clauses that represent that a Course can have at least one field value of a given FieldType to be True. More...

Clauses	hasAtMostOneFieldValueTrue (int, FieldType)
	Gives Clauses that represent that a Course can have at most one field value of a given FieldType to be True. More...

Clauses	hasCommonProgram (int, int)
	Gives Clauses that represent that a pair of courses are core for a given Program. More...

Clauses	hasNoCommonCoreProgram (int, int)
	Gives Clauses that represent that at least one out of a pair of courses is not core for a given Program. More...

Clauses	isMinorCourse (int)
	Gives Clauses that represent that a given Course is a minor Course. More...

Clauses	slotInMinorTime (int)
	Gives Clauses that represent that a given Course must have a minor Slot. More...

Clauses	isCoreCourse (int)
	Gives Clauses that represent that a Course is a core Course. More...

Clauses	isElectiveCourse (int)
	Gives Clauses that represent that a Course is an elective Course. More...

Clauses	courseInMorningTime (int)
	Gives Clauses that represent that a Course is scheduled in a morning Slot. More...

Clauses	programAtMostOneOfCoreOrElective (int)
	Gives Clauses that represent that for a Course, it can be a part of a Program as at most one out of core or elective. More...

Clauses	hasFieldTypeListedValues (int, FieldType, std::vector< int >)
	Gives Clauses that represent that a Course has a field value for a given FieldType out of a list of possible values. More...

Detailed Description

Class for constraint encoder.

This class is responsible for imposing constraints given a Course or a pair of Courses and a FieldType. The constraints are of a higher level than the operations of Clauses and of a lower level than the constraints defined in ConstraintAdder, which are the final constraints added to the solver. The class keeps a copy of the variables used for every 3-tuple of (Course, FieldType, field value) and a pointer to a Timetabler object to access the field data. Clauses for these constraints are created using the operations defined in Clauses.

Definition at line 26 of file constraint_encoder.h.

Constructor & Destructor Documentation

◆ ConstraintEncoder()

ConstraintEncoder::ConstraintEncoder ( Timetabler * timetabler )

Constructs the ConstraintEncoder object.

Parameters

timetabler The time tabler

Definition at line 19 of file constraint_encoder.cpp.

References Timetabler::data, Data::fieldValueVars, and timetabler.

Member Function Documentation

◆ courseInMorningTime()

Clauses ConstraintEncoder::courseInMorningTime ( int course )

Gives Clauses that represent that a Course is scheduled in a morning Slot.

Parameters

[in] course The course

Returns: A Clauses object representing the condition

Definition at line 365 of file constraint_encoder.cpp.

◆ hasAtLeastOneFieldValueTrue()

Clauses ConstraintEncoder::hasAtLeastOneFieldValueTrue	(	int	course,
		FieldType	fieldType
	)

Gives Clauses that represent that a Course can have at least one field value of a given FieldType to be True.

Parameters

[in]	course	The course
[in]	fieldType	The field type

Returns: A Clauses object representing the condition

Definition at line 215 of file constraint_encoder.cpp.

References CClause::createLitAndAdd().

◆ hasAtMostOneFieldValueTrue()

Clauses ConstraintEncoder::hasAtMostOneFieldValueTrue	(	int	course,
		FieldType	fieldType
	)

Gives Clauses that represent that a Course can have at most one field value of a given FieldType to be True.

The binomial encoding has been used to represent this constraint. A more efficient encoding, with auxiliary variables, has not been used because such an encoding would only be equisatisfiable. However, when using these clauses as an antecedent of an implication, we need that if the antecedent of the encoded clauses is False, the original set of clauses would also have been False, a property that equisatifiability does not guarantee.

Parameters

[in]	course	The course
[in]	fieldType	The field type

Returns: A Clauses object representing the condition

Definition at line 242 of file constraint_encoder.cpp.

References Clauses::addClauses().

◆ hasCommonProgram()

Clauses ConstraintEncoder::hasCommonProgram	(	int	course1,
		int	course2
	)

Gives Clauses that represent that a pair of courses are core for a given Program.

Parameters

[in]	course1	The course 1
[in]	course2	The course 2

Returns: A Clauses object representing the condition

Definition at line 90 of file constraint_encoder.cpp.

◆ hasExactlyOneFieldValueTrue()

Clauses ConstraintEncoder::hasExactlyOneFieldValueTrue	(	int	course,
		FieldType	fieldType
	)

Gives Clauses that represent that a Course can have exactly one field value of a given FieldType to be True.

This is helpful for defining constraints such as that that a given Course must have exactly one Instructor.

Parameters

[in]	course	The course
[in]	fieldType	The field type

Returns: A Clauses object representing the condition

Definition at line 199 of file constraint_encoder.cpp.

◆ hasFieldTypeListedValues()

Clauses ConstraintEncoder::hasFieldTypeListedValues	(	int	course,
		FieldType	fieldType,
		std::vector< int >	indexList
	)

Gives Clauses that represent that a Course has a field value for a given FieldType out of a list of possible values.

This is useful for encoding custom constraints.

Parameters

[in]	course	The course
[in]	fieldType	The field type
[in]	indexList	A vector of indices of the data corresponding to the FieldType for the allowed field values of the type.

Returns: A Clauses object representing the condition

Definition at line 410 of file constraint_encoder.cpp.

References CClause::createLitAndAdd().

◆ hasNoCommonCoreProgram()

Clauses ConstraintEncoder::hasNoCommonCoreProgram	(	int	course1,
		int	course2
	)

Gives Clauses that represent that at least one out of a pair of courses is not core for a given Program.

This is helpful to represent that two courses that are core for a Program cannot have an intersecting schedule.

Parameters

[in]	course1	The course 1
[in]	course2	The course 2

Returns: A Clauses object representing the condition

Definition at line 119 of file constraint_encoder.cpp.

◆ hasSameFieldTypeAndValue()

Clauses ConstraintEncoder::hasSameFieldTypeAndValue	(	int	course1,
		int	course2,
		FieldType	fieldType
	)

Gives Clauses that represent that a pair of courses have the same field value for a given FieldType.

For example, it can be used to represent that two courses have the same Slot. This is helpful for constructing constraints such as those enforcing that two courses have the same Slot.

Parameters

[in]	course1	The course 1
[in]	course2	The course 2
[in]	fieldType	The field type

Returns: A Clauses object representing the condition

Definition at line 38 of file constraint_encoder.cpp.

References CClause::createLitAndAdd().

◆ hasSameFieldTypeNotSameValue()

Clauses ConstraintEncoder::hasSameFieldTypeNotSameValue	(	int	course1,
		int	course2,
		FieldType	fieldType
	)

Gives Clauses that represent that a pair of courses do not have the same field value for a given FieldType.

For example, it can be used to represent that two courses do not have the same Instructor. This is helpful to define constraints such as that that an Instructor cannot have two courses at the same time.

Parameters

[in]	course1	The course 1
[in]	course2	The course 2
[in]	fieldType	The field type

Returns: A Clauses object representing the condition

Definition at line 68 of file constraint_encoder.cpp.

References Clauses::addClauses(), and CClause::addLits().

◆ isCoreCourse()

Clauses ConstraintEncoder::isCoreCourse ( int course )

Gives Clauses that represent that a Course is a core Course.

Parameters

[in] course The course

Returns: A Clauses object representing the condition

Definition at line 328 of file constraint_encoder.cpp.

◆ isElectiveCourse()

Clauses ConstraintEncoder::isElectiveCourse ( int course )

Gives Clauses that represent that a Course is an elective Course.

Parameters

[in] course The course

Returns: A Clauses object representing the condition

Definition at line 346 of file constraint_encoder.cpp.

◆ isMinorCourse()

Clauses ConstraintEncoder::isMinorCourse ( int course )

Gives Clauses that represent that a given Course is a minor Course.

Parameters

[in] course The course

Returns: A Clauses object representing the condition

Definition at line 296 of file constraint_encoder.cpp.

◆ notIntersectingTime()

Clauses ConstraintEncoder::notIntersectingTime	(	int	course1,
		int	course2
	)

Gives Clauses that represent that a pair of courses cannot have an intersecting schedule.

This describes that either the pair of courses have slots that do not intersect or that they have segments that do not intersect.

Parameters

[in]	course1	The course 1
[in]	course2	The course 2

Returns: A Clauses object representing the condition

Definition at line 144 of file constraint_encoder.cpp.

◆ notIntersectingTimeField()

Clauses ConstraintEncoder::notIntersectingTimeField	(	int	course1,
		int	course2,
		FieldType	fieldType
	)

Gives Clauses that represent that a pair of courses cannot have an intersecting value for a given FieldType, where the FieldType is of a time field, which is either a Segment or a Slot.

Parameters

[in]	course1	The course 1
[in]	course2	The course 2
[in]	fieldType	The field type

Returns: A Clauses object representing the condition

Definition at line 163 of file constraint_encoder.cpp.

◆ programAtMostOneOfCoreOrElective()

Clauses ConstraintEncoder::programAtMostOneOfCoreOrElective ( int course )

Gives Clauses that represent that for a Course, it can be a part of a Program as at most one out of core or elective.

Parameters

[in] course The course

Returns: A Clauses object representing the condition

Definition at line 385 of file constraint_encoder.cpp.

◆ slotInMinorTime()

Clauses ConstraintEncoder::slotInMinorTime ( int course )

Gives Clauses that represent that a given Course must have a minor Slot.

Parameters

[in] course The course

Returns: A Clauses object representing the condition

Definition at line 310 of file constraint_encoder.cpp.

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

/home/docs/checkouts/readthedocs.org/user_builds/timetabler/checkouts/docs2/include/constraint_encoder.h
/home/docs/checkouts/readthedocs.org/user_builds/timetabler/checkouts/docs2/src/constraint_encoder.cpp

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ ConstraintEncoder()

Member Function Documentation

◆ courseInMorningTime()

◆ hasAtLeastOneFieldValueTrue()

◆ hasAtMostOneFieldValueTrue()

◆ hasCommonProgram()

◆ hasExactlyOneFieldValueTrue()

◆ hasFieldTypeListedValues()

◆ hasNoCommonCoreProgram()

◆ hasSameFieldTypeAndValue()

◆ hasSameFieldTypeNotSameValue()

◆ isCoreCourse()

◆ isElectiveCourse()

◆ isMinorCourse()

◆ notIntersectingTime()

◆ notIntersectingTimeField()

◆ programAtMostOneOfCoreOrElective()

◆ slotInMinorTime()