time_tabler.h

Go to the documentation of this file.

#ifndef TIME_TABLER_H
#define TIME_TABLER_H

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

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