7 #include "MaxSATFormula.h" 9 #include "core/SolverTypes.h" 53 MaxSATFormula *formula;
57 std::vector<lbool> model;
66 void addClauses(
const std::vector<CClause> &,
int);
67 void addClauses(
const Clauses &,
int);
68 bool checkAllTrue(
const std::vector<Var> &);
69 bool checkAllTrue(
const std::vector<std::vector<Var>> &);
70 bool isVarTrue(
const Var &);
73 Lit newLiteral(
bool sign =
false);
75 void displayTimeTable();
76 void displayUnsatisfiedOutputReasons();
77 void addHighLevelClauses();
79 void addHighLevelCustomConstraintClauses(
int,
int);
80 void writeOutput(std::string);
81 void addExistingAssignments();
82 void addToFormula(vec<Lit> &,
int);
83 void addToFormula(Lit,
int);
84 void displayChangesInGivenAssignment();
PredefinedClauses
Enum that represents all the predefined constraints.
Class for representing a set of clauses.