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

Made MiniSat solver backend configurable in ezminisat.h

This commit is contained in:
Clifford Wolf 2014-02-22 01:29:02 +01:00
parent 8b508dc90b
commit 1ec01d8c63
2 changed files with 10 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
libs/ezsat/ezminisat.cc
View File

@ -29,6 +29,7 @@
#include <cinttypes>
#include <minisat/core/Solver.h>
#include <minisat/simp/SimpSolver.h>
ezMiniSAT::ezMiniSAT() : minisatSolver(NULL)
{
@ -90,8 +91,10 @@ contradiction:
for (auto id : modelExpressions)
modelIdx.push_back(bind(id));
if (minisatSolver == NULL)
minisatSolver = new Minisat::Solver;
if (minisatSolver == NULL) {
minisatSolver = new EZMINISAT_SOLVER;
minisatSolver->verbosity = EZMINISAT_VERBOSITY;
}
std::vector<std::vector<int>> cnf;
consumeCnf(cnf);

6
libs/ezsat/ezminisat.h
View File

@ -20,6 +20,9 @@
#ifndef EZMINISAT_H
#define EZMINISAT_H
#define EZMINISAT_SOLVER Minisat::Solver
#define EZMINISAT_VERBOSITY 0
#include "ezsat.h"
#include <time.h>
@ -28,12 +31,13 @@
// don't force ezSAT users to use minisat headers..
namespace Minisat {
class Solver;
class SimpSolver;
}
class ezMiniSAT : public ezSAT
{
private:
Minisat::Solver *minisatSolver;
EZMINISAT_SOLVER *minisatSolver;
std::vector<int> minisatVars;
bool foundContradiction;