summaryrefslogtreecommitdiff
path: root/libs
diff options
context:
space:
mode:
Diffstat (limited to 'libs')
-rw-r--r--libs/ezsat/ezsat.cc2
-rw-r--r--libs/ezsat/ezsat.h3
-rw-r--r--libs/ezsat/testbench.cc5
3 files changed, 0 insertions, 10 deletions
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 4ae5f4fd..f77a3b91 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -342,7 +342,6 @@ void ezSAT::clear()
cnfLiteralVariables.clear();
cnfExpressionVariables.clear();
cnfClauses.clear();
- cnfAssumptions.clear();
}
void ezSAT::freeze(int)
@@ -351,7 +350,6 @@ void ezSAT::freeze(int)
void ezSAT::assume(int id)
{
- cnfAssumptions.insert(id);
if (id < 0)
{
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 79100b87..8d340b3d 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -58,7 +58,6 @@ private:
int cnfVariableCount, cnfClausesCount;
std::vector<int> cnfLiteralVariables, cnfExpressionVariables;
std::vector<std::vector<int>> cnfClauses;
- std::set<int> cnfAssumptions;
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);
@@ -144,8 +143,6 @@ public:
virtual void freeze(int id);
void assume(int id);
int bind(int id);
-
- const std::set<int> &assumed() const { return cnfAssumptions; }
int bound(int id) const;
int numCnfVariables() const { return cnfVariableCount; }
diff --git a/libs/ezsat/testbench.cc b/libs/ezsat/testbench.cc
index cc0fe573..8283686e 100644
--- a/libs/ezsat/testbench.cc
+++ b/libs/ezsat/testbench.cc
@@ -38,11 +38,6 @@ struct xorshift128 {
bool test(ezSAT &sat, int assumption = 0)
{
- for (auto id : sat.assumed())
- printf("%s\n", sat.to_string(id).c_str());
- if (assumption)
- printf("%s\n", sat.to_string(assumption).c_str());
-
std::vector<int> modelExpressions;
std::vector<bool> modelValues;