summaryrefslogtreecommitdiff
path: root/libs/ezsat/ezsat.h
diff options
context:
space:
mode:
Diffstat (limited to 'libs/ezsat/ezsat.h')
-rw-r--r--libs/ezsat/ezsat.h19
1 files changed, 18 insertions, 1 deletions
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 85240556..83e1b23c 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -48,6 +48,11 @@ public:
static const int FALSE;
private:
+ bool flag_keep_cnf;
+ bool flag_non_incremental;
+
+ bool non_incremental_solve_used_up;
+
std::map<std::string, int> literalsCache;
std::vector<std::string> literals;
@@ -57,7 +62,7 @@ private:
bool cnfConsumed;
int cnfVariableCount, cnfClausesCount;
std::vector<int> cnfLiteralVariables, cnfExpressionVariables;
- std::vector<std::vector<int>> cnfClauses;
+ std::vector<std::vector<int>> cnfClauses, cnfClausesBackup;
void add_clause(const std::vector<int> &args);
void add_clause(const std::vector<int> &args, bool argsPolarity, int a = 0, int b = 0, int c = 0);
@@ -67,6 +72,9 @@ private:
int bind_cnf_and(const std::vector<int> &args);
int bind_cnf_or(const std::vector<int> &args);
+protected:
+ void preSolverCallback();
+
public:
int solverTimeout;
bool solverTimoutStatus;
@@ -74,6 +82,12 @@ public:
ezSAT();
virtual ~ezSAT();
+ void keep_cnf() { flag_keep_cnf = true; }
+ void non_incremental() { flag_non_incremental = true; }
+
+ bool mode_keep_cnf() const { return flag_keep_cnf; }
+ bool mode_non_incremental() const { return flag_non_incremental; }
+
// manage expressions
int value(bool val);
@@ -155,6 +169,9 @@ public:
void consumeCnf();
void consumeCnf(std::vector<std::vector<int>> &cnf);
+ // use this function to get the full CNF in keep_cnf mode
+ void getFullCnf(std::vector<std::vector<int>> &full_cnf) const;
+
std::string cnfLiteralInfo(int idx) const;
// simple helpers for build expressions easily