time_tabler.h

Go to the documentation of this file.

#ifndef TIME_TABLER_H
#define TIME_TABLER_H

#include <vector>
#include "MaxSATFormula.h"
#include "cclause.h"
#include "core/SolverTypes.h"
#include "data.h"
#include "mtl/Vec.h"
#include "tsolver.h"

using namespace NSPACE;

enum SolverStatus {
  Solved,
  HighLevelFailed,
  Unsolved
};

class Timetabler {
 private:
  TSolver *solver;
  MaxSATFormula *formula;
  std::vector<lbool> model;

 public:
  Data data;
  Timetabler();
  ~Timetabler();
  void addClauses(const std::vector<CClause> &, int);
  void addClauses(const Clauses &, int);
  bool checkAllTrue(const std::vector<Var> &);
  bool isVarTrue(const Var &);
  SolverStatus solve();
  Var newVar();
  Lit newLiteral(bool sign = false);
  void printResult(SolverStatus);
  void displayTimeTable();
  void displayUnsatisfiedOutputReasons();
  void addHighLevelClauses();
  void addHighLevelConstraintClauses(PredefinedClauses);
  void addHighLevelCustomConstraintClauses(int, int);
  void writeOutput(std::string);
  void addExistingAssignments();
  void addToFormula(vec<Lit> &, int);
  void addToFormula(Lit, int);
  void displayChangesInGivenAssignment();
};

#endif