riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Removed ezSAT::assumed() API

This commit is contained in:
Clifford Wolf 2014-03-01 20:55:06 +01:00
parent e3debea4e6
commit edc2146056
3 changed files with 0 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/ezsat/ezsat.cc
View File

@ -342,7 +342,6 @@ void ezSAT::clear()
cnfLiteralVariables.clear(); cnfLiteralVariables.clear();
cnfExpressionVariables.clear(); cnfExpressionVariables.clear();
cnfClauses.clear(); cnfClauses.clear();
cnfAssumptions.clear();
} }
void ezSAT::freeze(int) void ezSAT::freeze(int)
@ -351,7 +350,6 @@ void ezSAT::freeze(int)
void ezSAT::assume(int id) void ezSAT::assume(int id)
{ {
cnfAssumptions.insert(id);
if (id < 0) if (id < 0)
{ {

3
libs/ezsat/ezsat.h
View File

@ -58,7 +58,6 @@ private:
int cnfVariableCount, cnfClausesCount; int cnfVariableCount, cnfClausesCount;
std::vector<int> cnfLiteralVariables, cnfExpressionVariables; std::vector<int> cnfLiteralVariables, cnfExpressionVariables;
std::vector<std::vector<int>> cnfClauses; 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);
void add_clause(const std::vector<int> &args, bool argsPolarity, int a = 0, int b = 0, int c = 0); 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); virtual void freeze(int id);
void assume(int id); void assume(int id);
int bind(int id); int bind(int id);
const std::set<int> &assumed() const { return cnfAssumptions; }
int bound(int id) const; int bound(int id) const;
int numCnfVariables() const { return cnfVariableCount; } int numCnfVariables() const { return cnfVariableCount; }

5
libs/ezsat/testbench.cc
View File

@ -38,11 +38,6 @@ struct xorshift128 {
bool test(ezSAT &sat, int assumption = 0) 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<int> modelExpressions;
std::vector<bool> modelValues; std::vector<bool> modelValues;