3 files changed, 46 insertions, 1 deletions
diff --git a/kernel/register.cc b/kernel/register.cc
index cdba4c36f..af1cb77b5 100644
--- a/kernel/register.cc
+++ b/kernel/register.cc
@@ -18,6 +18,8 @@
  */
 
 #include "kernel/yosys.h"
+#include "kernel/satgen.h"
+
 #include <string.h>
 #include <stdlib.h>
 #include <stdio.h>
@@ -691,6 +693,18 @@ struct EchoPass : public Pass {
 		log("echo %s\n", echo_mode ? "on" : "off");
 	}
 } EchoPass;
+
+SatSolver *yosys_satsolver_list;
+SatSolver *yosys_satsolver;
+
+struct MinisatSatSolver : public SatSolver {
+	MinisatSatSolver() : SatSolver("minisat") {
+		yosys_satsolver = this;
+	}
+	virtual ezSAT *create() YS_OVERRIDE {
+		return new ezMiniSAT();
+	}
+} MinisatSatSolver;
  
 YOSYS_NAMESPACE_END
 
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 2f5efe674..093d248d4 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -29,7 +29,37 @@
 
 YOSYS_NAMESPACE_BEGIN
 
-typedef ezMiniSAT ezDefaultSAT;
+// defined in kernel/register.cc
+extern struct SatSolver *yosys_satsolver_list;
+extern struct SatSolver *yosys_satsolver;
+
+struct SatSolver
+{
+	string name;
+	SatSolver *next;
+	virtual ezSAT *create() = 0;
+
+	SatSolver(string name) : name(name) {
+		next = yosys_satsolver_list;
+		yosys_satsolver_list = this;
+	}
+
+	virtual ~SatSolver() {
+		auto p = &yosys_satsolver_list;
+		while (*p) {
+			if (*p == this)
+				*p = next;
+			else
+				p = &(*p)->next;
+		}
+		if (yosys_satsolver == this)
+			yosys_satsolver = yosys_satsolver_list;
+	}
+};
+
+struct ezSatPtr : public std::unique_ptr<ezSAT> {
+	ezSatPtr() : unique_ptr<ezSAT>(yosys_satsolver->create()) { }
+};
 
 struct SatGen
 {
diff --git a/kernel/yosys.h b/kernel/yosys.h
index 47275ecd4..467d2074f 100644
--- a/kernel/yosys.h
+++ b/kernel/yosys.h
@@ -49,6 +49,7 @@
 #include <unordered_set>
 #include <initializer_list>
 #include <stdexcept>
+#include <memory>
 
 #include <sstream>
 #include <fstream>