From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 1 Mar 2014 19:55:06 +0000 (+0100)
Subject: Removed ezSAT::assumed() API
X-Git-Tag: yosys-0.3.0~100
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=edc21460565ea75cff54cab69933da8c5e9db382;p=yosys.git

Removed ezSAT::assumed() API
---

diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 4ae5f4fda..f77a3b918 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 79100b876..8d340b3d6 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 cc0fe5734..8283686e3 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;