constraint_encoder.cpp

#include "constraint_encoder.h"

#include <cassert>
#include <iostream>
#include <vector>
#include "cclause.h"
#include "clauses.h"
#include "core/SolverTypes.h"
#include "global.h"
#include "timetabler.h"

using namespace NSPACE;

ConstraintEncoder::ConstraintEncoder(Timetabler *timetabler) {
  this->timetabler = timetabler;
  this->vars = timetabler->data.fieldValueVars;
}

Clauses ConstraintEncoder::hasSameFieldTypeAndValue(int course1, int course2,
                                                    FieldType fieldType) {
  Clauses result;
  for (unsigned i = 0; i < vars[course1][fieldType].size(); i++) {
    CClause field1, field2;
    field1.createLitAndAdd(vars[course1][fieldType][i]);
    field2.createLitAndAdd(vars[course2][fieldType][i]);
    Clauses conjunction(field1 & field2);
    if (i == 0)
      result = conjunction;
    else
      result = result | conjunction;
  }
  return result;
}

Clauses ConstraintEncoder::hasSameFieldTypeNotSameValue(int course1,
                                                        int course2,
                                                        FieldType fieldType) {
  Clauses result;
  for (unsigned i = 0; i < vars[course1][fieldType].size(); i++) {
    CClause resultClause;
    resultClause.addLits(~mkLit(vars[course1][fieldType][i], false));
    resultClause.addLits(~mkLit(vars[course2][fieldType][i], false));
    result.addClauses(resultClause);
  }
  return result;
}

Clauses ConstraintEncoder::hasCommonProgram(int course1, int course2) {
  Clauses result;
  for (unsigned i = 0; i < vars[course1][FieldType::program].size(); i++) {
    if (timetabler->data.programs[i].isCoreProgram()) {
      CClause field1, field2;
      field1.createLitAndAdd(vars[course1][FieldType::program][i]);
      field2.createLitAndAdd(vars[course2][FieldType::program][i]);
      Clauses conjunction(field1 & field2);
      if (i == 0)
        result = conjunction;
      else
        result = result | conjunction;
    }
  }
  return result;
}

Clauses ConstraintEncoder::hasNoCommonCoreProgram(int course1, int course2) {
  Clauses result;
  for (unsigned i = 0; i < vars[course1][FieldType::program].size(); i++) {
    if (timetabler->data.programs[i].isCoreProgram()) {
      CClause resultClause;
      resultClause.addLits(~mkLit(vars[course1][FieldType::program][i], false));
      resultClause.addLits(~mkLit(vars[course2][FieldType::program][i], false));
      result.addClauses(resultClause);
    }
  }
  return result;
}

Clauses ConstraintEncoder::notIntersectingTime(int course1, int course2) {
  Clauses notSegmentIntersecting =
      Clauses(notIntersectingTimeField(course1, course2, FieldType::segment));
  Clauses notSlotIntersecting =
      Clauses(notIntersectingTimeField(course1, course2, FieldType::slot));
  return (notSegmentIntersecting | notSlotIntersecting);
}

Clauses ConstraintEncoder::notIntersectingTimeField(int course1, int course2,
                                                    FieldType fieldType) {
  assert(fieldType == FieldType::segment || fieldType == FieldType::slot);
  assert(vars[course1][fieldType].size() == vars[course2][fieldType].size());
  assert(course1 != course2);
  Clauses result;
  for (unsigned i = 0; i < vars[course1][fieldType].size(); i++) {
    Clauses hasFieldValue1(vars[course1][fieldType][i]);
    Clauses notIntersecting1;
    for (unsigned j = 0; j < vars[course1][fieldType].size(); j++) {
      if ((fieldType == FieldType::segment &&
           timetabler->data.segments[i].isIntersecting(
               timetabler->data.segments[j])) ||
          (fieldType == FieldType::slot &&
           timetabler->data.slots[i].isIntersecting(
               timetabler->data.slots[j]))) {
        notIntersecting1.addClauses(~Clauses(vars[course2][fieldType][j]));
      }
    }
    result.addClauses(hasFieldValue1 >> notIntersecting1);
  }
  return result;
}

Clauses ConstraintEncoder::hasExactlyOneFieldValueTrue(int course,
                                                       FieldType fieldType) {
  Clauses atLeastOne = Clauses(hasAtLeastOneFieldValueTrue(course, fieldType));
  Clauses atMostOne = Clauses(hasAtMostOneFieldValueTrue(course, fieldType));
  return (atLeastOne & atMostOne);
}

Clauses ConstraintEncoder::hasAtLeastOneFieldValueTrue(int course,
                                                       FieldType fieldType) {
  std::vector<Var> varsToUse = getAllowedVars(course, fieldType);
  CClause resultClause;
  for (unsigned i = 0; i < varsToUse.size(); i++) {
    resultClause.createLitAndAdd(varsToUse[i]);
  }
  Clauses result(resultClause);
  return result;
}

Clauses ConstraintEncoder::hasAtMostOneFieldValueTrue(int course,
                                                      FieldType fieldType) {
  std::vector<Var> varsToUse = getAllowedVars(course, fieldType);
  Clauses result;
  for (unsigned i = 0; i < vars[course][fieldType].size(); i++) {
    for (unsigned j = i + 1; j < vars[course][fieldType].size(); j++) {
      Clauses first(vars[course][fieldType][i]);
      Clauses second(vars[course][fieldType][j]);
      Clauses negSecond = ~second;
      result.addClauses(~first | negSecond);
    }
  }
  return result;
}

std::vector<Var> ConstraintEncoder::getAllowedVars(int course,
                                                   FieldType fieldType) {
  std::vector<Var> varsToUse;
  varsToUse.clear();
  if (fieldType != FieldType::classroom) {
    varsToUse = vars[course][fieldType];
  } else {
    for (unsigned i = 0; i < vars[course][fieldType].size(); i++) {
      if (timetabler->data.courses[course].getClassSize() <=
          timetabler->data.classrooms[i].getSize()) {
        varsToUse.push_back(vars[course][fieldType][i]);
      }
    }
  }
  return varsToUse;
}

Clauses ConstraintEncoder::isMinorCourse(int course) {
  Clauses result(vars[course][FieldType::isMinor]
                     [static_cast<unsigned>(MinorType::isMinorCourse)]);
  return result;
}

Clauses ConstraintEncoder::slotInMinorTime(int course) {
  CClause resultClause;
  for (unsigned i = 0; i < vars[course][FieldType::slot].size(); i++) {
    if (timetabler->data.slots[i].isMinorSlot()) {
      resultClause.createLitAndAdd(vars[course][FieldType::slot][i]);
    }
  }
  Clauses result(resultClause);
  return result;
}

Clauses ConstraintEncoder::isCoreCourse(int course) {
  CClause resultClause;
  for (unsigned i = 0; i < vars[course][FieldType::program].size(); i++) {
    if (timetabler->data.programs[i].isCoreProgram()) {
      resultClause.createLitAndAdd(vars[course][FieldType::program][i]);
    }
  }
  Clauses result(resultClause);
  return result;
}

Clauses ConstraintEncoder::isElectiveCourse(int course) {
  CClause resultClause;
  for (unsigned i = 0; i < vars[course][FieldType::program].size(); i++) {
    if (!(timetabler->data.programs[i].isCoreProgram())) {
      resultClause.createLitAndAdd(vars[course][FieldType::program][i]);
    }
  }
  Clauses result(resultClause);
  return result;
}

Clauses ConstraintEncoder::courseInMorningTime(int course) {
  CClause resultClause;
  for (unsigned i = 0; i < vars[course][FieldType::slot].size(); i++) {
    if (timetabler->data.slots[i].isMorningSlot()) {
      resultClause.createLitAndAdd(vars[course][FieldType::slot][i]);
    }
  }
  Clauses result(resultClause);
  return result;
}

Clauses ConstraintEncoder::programAtMostOneOfCoreOrElective(int course) {
  Clauses result;
  for (unsigned i = 0; i < vars[course][FieldType::program].size(); i += 2) {
    CClause resultClause;
    resultClause.addLits(~mkLit(vars[course][FieldType::program][i], false));
    resultClause.addLits(
        ~mkLit(vars[course][FieldType::program][i + 1], false));
    result.addClauses(resultClause);
  }
  return result;
}

Clauses ConstraintEncoder::hasFieldTypeListedValues(
    int course, FieldType fieldType, std::vector<int> indexList) {
  CClause resultClause;
  for (unsigned i = 0; i < indexList.size(); i++) {
    resultClause.createLitAndAdd(vars[course][fieldType][indexList[i]]);
  }
  Clauses result(resultClause);
  return result;
}