Removed ezSAT::assumed() API

diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 4ae5f4fdad99df329098807a5c8221fbfc874058..f77a3b9188176f5be6b97c06f100033466f345d9 100644 (file)
--- 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 79100b876df0b8b8df34a6094c6ae039250fd73e..8d340b3d6bd98531b1be349aad6d918eeb4abad6 100644 (file)
--- 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 cc0fe5734063f09573c28c1c796dc4ea931e5b8c..8283686e3bc36c3c3156425505ddc3ebcba89e74 100644 (file)
--- 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;