time_tabler.h

Go to the documentation of this file.

#ifndef TIME_TABLER_H
#define TIME_TABLER_H

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

using namespace Minisat;

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);
    void printResult(SolverStatus);
    void displayTimeTable();
    void displayUnsatisfiedOutputReasons();
    void addHighLevelClauses();
    void writeOutput(std::string);
    void addExistingAssignments();
    void addToFormula(vec<Lit> &, int);
    void displayChangesInGivenAssignment();
};

#endif