satoko SAT solver

docs/changelog.rst

@@ -10,6 +10,8 @@ v0.1 (not yet released)
     - GHack (`solver<solvers::ghack>`)
     - Glucose 4.1 (`solver<solvers::glucose_41>`)
     - ABC bsat2 (`solver<solvers::bsat2>`)
+    - ABC bmcg (`solver<solvers::bmcg>`)
+    - ABC satoko (`solver<solvers::satoko>`)
 * Types:
     - Wrapper for variables (`var_type`)
     - Wrapper for literals (`lit_type`)

include/bill/sat/solver.hpp

@@ -31,7 +31,9 @@
 #define ABC_USE_NAMESPACE pabc
 #define ABC_NAMESPACE pabc
 #define ABC_USE_NO_READLINE
+#define SATOKO_NAMESPACE satoko
 #include "sat_solvers/abc.hpp"
+#include "sat_solvers/satoko.hpp"
 #endif
 #pragma GCC diagnostic pop
 #endif
@@ -135,6 +137,7 @@ enum class solvers {
 	maple,
 	bsat2,
 	bmcg,
+	satoko,
 #endif
 	ghack,
 };
@@ -909,4 +912,159 @@ class solver<solvers::bmcg> {
 };
 #endif
 
+#if !defined(BILL_WINDOWS_PLATFORM)
+template<>
+class solver<solvers::satoko> {
+public:
+	using solver_type = satoko::satoko_t;
+
+#pragma region Constructors
+	solver()
+	{
+		solver_ = satoko::satoko_create();
+	}
+
+	~solver()
+	{
+		satoko::satoko_destroy(solver_);
+		solver_ = nullptr;
+	}
+
+	/* disallow copying */
+	solver(solver<solvers::satoko> const&) = delete;
+	solver<solvers::satoko>& operator=(const solver<solvers::satoko>&) = delete;
+#pragma endregion
+
+#pragma region Modifiers
+	void restart()
+	{
+		satoko::satoko_reset(solver_);
+		state_ = result::states::undefined;
+	}
+
+	var_type add_variable()
+	{
+		return satoko::satoko_add_variable(solver_, 0);
+	}
+
+	void add_variables(uint32_t num_variables = 1)
+	{
+		for (auto i = 0u; i < num_variables; ++i) {
+			satoko::satoko_add_variable(solver_, 0);
+		}
+	}
+
+	auto add_clause(std::vector<lit_type>::const_iterator it,
+	                std::vector<lit_type>::const_iterator ie)
+	{
+		auto counter = 0u;
+		while (it != ie) {
+			literals[counter++] = pabc::Abc_Var2Lit(it->variable(),
+			                                        it->is_complemented());
+			++it;
+		}
+		auto const result = satoko::satoko_add_clause(solver_, literals, counter);
+		state_ = result ? result::states::dirty : result::states::unsatisfiable;
+		return result;
+	}
+
+	auto add_clause(std::vector<lit_type> const& clause)
+	{
+		return add_clause(clause.begin(), clause.end());
+	}
+
+	auto add_clause(lit_type lit)
+	{
+		return add_clause(std::vector<lit_type>{lit});
+	}
+
+	result get_model() const
+	{
+		assert(state_ == result::states::satisfiable);
+		result::model_type model;
+		for (auto i = 0u; i < num_variables(); ++i) {
+			auto const value = satoko::satoko_read_cex_varvalue(solver_, i);
+			if (value == 1) {
+				model.emplace_back(lbool_type::true_);
+			} else {
+				model.emplace_back(lbool_type::false_);
+			}
+		}
+		return result(model);
+	}
+
+	result get_result() const
+	{
+		assert(state_ != result::states::dirty);
+		if (state_ == result::states::satisfiable) {
+			return get_model();
+		} else {
+			return result();
+		}
+	}
+
+	result::states solve(std::vector<lit_type> const& assumptions = {},
+	                     uint32_t conflict_limit = 0)
+	{
+		/* special case: empty solver state */
+		if (num_variables() == 0u)
+			return result::states::undefined;
+
+		int result;
+		if (assumptions.size() > 0u) {
+			/* solve with assumptions */
+			uint32_t counter = 0u;
+			auto it = assumptions.begin();
+			while (it != assumptions.end()) {
+				literals[counter++] = pabc::Abc_Var2Lit(it->variable(),
+				                                        it->is_complemented());
+				++it;
+			}
+			result = satoko::satoko_solve_assumptions_limit(solver_, literals, counter,
+			                                                conflict_limit);
+		} else {
+			/* solve without assumptions */
+			result = satoko::satoko_solve_assumptions_limit(solver_, 0, 0,
+			                                                conflict_limit);
+		}
+
+		if (result == satoko::SATOKO_SAT) {
+			state_ = result::states::satisfiable;
+		} else if (result == satoko::SATOKO_UNSAT) {
+			state_ = result::states::unsatisfiable;
+		} else {
+			state_ = result::states::undefined;
+		}
+
+		return state_;
+	}
+#pragma endregion
+
+#pragma region Properties
+	uint32_t num_variables() const
+	{
+		return satoko::satoko_varnum(solver_);
+	}
+
+	uint32_t num_clauses() const
+	{
+		return satoko::satoko_clausenum(solver_);
+	}
+#pragma endregion
+
+private:
+	/*! \brief Backend solver */
+	solver_type* solver_ = nullptr;
+
+	/*! \brief Current state of the solver */
+	result::states state_ = result::states::undefined;
+
+	/*! \brief Temporary storage for one clause */
+	pabc::lit literals[2048];
+
+	/*! \brief Count the number of variables */
+	uint32_t variable_counter_ = 0u;
+};
+#endif
+
 } // namespace bill