Add basic python sat interface

Cargo.toml

@@ -1,6 +1,5 @@
 [workspace]
 members = ["crates/*"]
-exclude = ["crates/pyndakaas"]
 resolver = "2"
 
 [workspace.package]

crates/pindakaas-derive/src/lib.rs

@@ -427,6 +427,280 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 	.into()
 }
 
+#[derive(FromDeriveInput)]
+#[darling(attributes(python_clause_database))]
+struct PythonClauseDatabaseOpts {
+	/// The struct field which implements ClauseDatabase and ClauseDatabaseTools
+	#[darling(default)]
+	db: Option<Ident>,
+}
+
+#[derive(FromDeriveInput)]
+#[darling(attributes(python_clause_database_tools))]
+// TODO not sure how to avoid duplication
+struct PythonClauseDatabaseToolsOpts {
+	/// The struct field which implements ClauseDatabase and ClauseDatabaseTools
+	#[darling(default)]
+	db: Option<Ident>,
+	// /// Whether to derive the ConditionalDatabase
+	// #[darling(default)]
+	// conditions: Option<bool>,
+}
+
+#[proc_macro_derive(PythonClauseDatabase, attributes(python_clause_database))]
+pub fn python_clause_database_derive(input: TokenStream) -> TokenStream {
+	let input = parse_macro_input!(input);
+	let opts = PythonClauseDatabaseOpts::from_derive_input(&input).expect("Invalid options");
+	// TODO actually, I want to make this non-optional but I can't get an Ident for tuple struct field access
+	let db = match opts.db {
+		Some(x) => quote! {  self.#x },
+		None => quote! { self.0 },
+	};
+	let DeriveInput { ident, .. } = input;
+
+	quote! {
+	#[pymethods]
+	impl #ident {
+		fn add_clause(&mut self, clause: Vec<Lit>) -> Result {
+			::pindakaas::ClauseDatabase::add_clause_from_slice(
+				&mut #db,
+				&clause.into_iter().map(|l| l.0).collect_vec(),
+			)
+			.map_err(|_| Unsatisfiable)
+		}
+
+	fn add_variables(&mut self, len: usize) -> VarRange {
+			VarRange(
+			::pindakaas::ClauseDatabase::new_var_range(
+							&mut #db,
+							len
+							))
+
+								// TODO not sure if we can make a generator here, but perhaps that's
+								// the proper translation to python
+				// Lit(
+				// ::pindakaas::ClauseDatabaseTools::new_vars(
+				// 				&mut self.0
+				// 			).into())
+	}
+		}
+		}
+	.into()
+}
+
+#[proc_macro_derive(PythonClauseDatabaseTools, attributes(python_clause_database_tools))]
+pub fn python_clause_database_tools_derive(input: TokenStream) -> TokenStream {
+	let input = parse_macro_input!(input);
+
+	let opts = PythonClauseDatabaseToolsOpts::from_derive_input(&input).expect("Invalid options");
+	let db = match opts.db {
+		Some(x) => quote! {  self.#x },
+		None => quote! { self.0 },
+	};
+	let DeriveInput { ident, .. } = input;
+
+	/*
+	let conditional_database = if opts.conditions.unwrap_or(true) {
+		let conditional_database_ident = format_ident!("Conditional{}", ident);
+		quote! {
+
+					#[pymethods]
+					impl #ident {
+
+
+				fn with_conditions(slf: PyRefMut<'_, Self>, conditions: Vec<Lit>) -> #conditional_database_ident {
+					// TODO can't really use this, because can't keep impl ClauseDatabase as struct field ?
+					// let c_db = ::pindakaas::ClauseDatabaseTools::with_conditions(
+					// 	&mut self.0,
+					// 	conditions.into_iter().map(|l| l.into()).collect(),
+					// );
+					Python::with_gil(move |py| {
+						#conditional_database_ident(
+							slf.into_py_any(py).unwrap().extract(py).unwrap(),
+							conditions,
+						)
+					})
+				}
+
+					}
+
+			// #[pyclass(extends = ClauseDatabase)] // TODO can't quite get this to work
+				// #[new]
+				// fn new(db: Py<#ident>, conditions: Vec<Lit>) -> (Self, ClauseDatabase) {
+				// 	(Self(db, conditions), ClauseDatabase::new())
+				// }
+			// TODO this approach works but now we don't get Cnf's methods in ConditionalCnf
+			#[pyclass]
+						// #[derive(PythonClauseDatabaseTools)]
+						// #[python_clause_database_tools(conditions = false)]
+			struct #conditional_database_ident(Py<#ident>, Vec<Lit>);
+
+			#[pymethods]
+			impl #conditional_database_ident {
+
+				fn __enter__(slf: Py<Self>) -> Py<Self> {
+					slf
+				}
+
+				fn __exit__(&mut self, _exc_type: PyObject, _exc_value: PyObject, _traceback: PyObject) {}
+
+				fn add_clause_from_slice(&mut self, clause: Vec<Lit>) -> Result {
+					Python::with_gil(move |py| {
+						self.0.borrow_mut(py).add_clause_from_slice(
+							self.1
+								.clone()
+								.into_iter()
+								.chain(clause.into_iter())
+								.collect(),
+						)
+					})
+				}
+
+				fn new_var_range(&mut self, len: usize) -> VarRange {
+					Python::with_gil(move |py| self.0.borrow_mut(py).new_var_range(len))
+				}
+
+							// TODO unfortunately, I can't derive ClauseDatabaseTools for Conditional*
+							// b/c it has a Py<ClauseDatabase>, but we
+														// only have to duplicate the methods once
+								fn add_clause(&mut self, clause: Vec<Lit>) -> Result {
+									self.add_clause_from_slice(clause)
+								}
+
+		fn add_variable(&mut self) -> Lit {
+					Python::with_gil(move |py| {
+						self.0.borrow_mut(py).add_variable()
+					})
+				}
+
+
+		fn add_variables(&mut self, len: usize) -> VarRange {
+					Python::with_gil(move |py| {
+						self.0.borrow_mut(py).add_variables(len)
+					})
+		}
+
+		#[pyo3(signature=(literals, /, coefficients = None, comparator = Some(Comparator::GreaterEq), k = Some(1)))]
+		fn add_linear(
+			&mut self,
+			literals: Vec<Lit>,
+			coefficients: Option<Vec<Coeff>>,
+			comparator: Option<Comparator>,
+			k: Option<Coeff>,
+		) -> Result {
+					Python::with_gil(move |py| {
+						self.0.borrow_mut(py).extract().0.with_conditions(self.1).add_linear(literals, coefficients, comparator, k)
+					})
+
+				}
+						}
+				}
+	} else {
+		quote! {()}
+	};
+		*/
+
+	quote! {
+		#[pymethods]
+		impl #ident {
+
+                    // TODO not entirely sure if this shouldn't also go to ClauseDatabase
+		fn add_variable(&mut self) -> Lit {
+				Lit(
+				::pindakaas::ClauseDatabaseTools::new_var(
+								&mut #db
+							).into())
+		}
+
+        ///// TODO not sure if this one should be in ClauseDatabase or ClauseDatabaseTools
+		///
+		/// Encode a linear constraint over Boolean literals
+		/// The default arguments encode a clause: all coefficients are one, comparator is >=, and k = 1.
+		/// Currently, the encoding is fixed as `adder` for PB and Cardinality constraints, and `PairWise` for AMOs/ALOs
+		#[pyo3(signature=(literals, /, coefficients = None, comparator = Some(Comparator::GreaterEq), k = Some(1), conditions = vec![]))]
+		fn add_linear(
+			&mut self,
+			literals: Vec<Lit>,
+			coefficients: Option<Vec<Coeff>>,
+			// TODO I'm not sure if adding Option is the best way to allow None to return default
+			comparator: Option<Comparator>,
+			k: Option<Coeff>,
+                        conditions: Vec<Lit>,
+		) -> Result {
+			let coefficients = coefficients.unwrap_or(literals.iter().map(|_| 1).collect());
+			assert_eq!(
+				coefficients.len(),
+				literals.len(),
+				"Literals and coefficients should have the same length"
+			);
+			let enc: LinearEncoder = LinearEncoder::default();
+                        let mut db = ::pindakaas::ClauseDatabaseTools::with_conditions(&mut #db, conditions.into_iter().map(|l| l.into()).collect());
+			Ok(enc.encode(
+				&mut db,
+				&BoolLinear::new(
+					BoolLinExp::from_slices(
+						&coefficients,
+						&literals.into_iter().map(|l| l.0).collect_vec(),
+					),
+					comparator.unwrap_or_default().into(),
+					k.unwrap_or(1),
+				),
+			)?)
+		}
+		}
+
+
+
+// #conditional_database
+			}
+	.into()
+}
+
+#[derive(FromDeriveInput)]
+#[darling(attributes(python_solver))]
+struct PythonSolverOpts {
+	/// The `slv` struct field which implements Solver
+	slv: Ident,
+}
+
+#[proc_macro_derive(PythonSolver, attributes(python_solver))]
+pub fn python_solver_derive(input: TokenStream) -> TokenStream {
+	let input = parse_macro_input!(input);
+	let slv = PythonSolverOpts::from_derive_input(&input)
+		.expect("Invalid options")
+		.slv;
+	let slv = quote! { self.#slv };
+	let DeriveInput { ident, .. } = input;
+
+	quote! {
+		#[pymethods]
+		impl #ident {
+
+	#[new]
+	fn new() -> Self {
+		Self::default()
+	}
+
+		fn solve(&mut self, vars: Vec<Lit>) -> Option<bool> {
+			match #slv.solve() {
+				::pindakaas::solver::SolveResult::Satisfied(sol) => {
+					self.solution = Some(MapSol::new(vars, &sol));
+					Some(true)
+				}
+				::pindakaas::solver::SolveResult::Unsatisfiable(_) => Some(false),
+				::pindakaas::solver::SolveResult::Unknown => None,
+			}
+		}
+
+		fn value(&self, lit: Lit) -> Option<bool> {
+			self.solution.as_ref().map(|sol| sol.value(lit.into()))
+		}
+
+	}
+	}
+	.into()
+}
+
 fn default_true() -> bool {
 	true
 }

crates/pindakaas/src/bool_linear.rs

@@ -1271,6 +1271,22 @@ impl BoolLinExp {
 	}
 }
 
+impl Add for Lit {
+	type Output = BoolLinExp;
+
+	fn add(self, rhs: Self) -> Self::Output {
+		BoolLinExp::from_terms(&[(self, 1), (rhs, 1)])
+	}
+}
+
+impl Mul<Lit> for Coeff {
+	type Output = BoolLinExp;
+
+	fn mul(self, rhs: Lit) -> Self::Output {
+		BoolLinExp::from_terms(&[(rhs, self)])
+	}
+}
+
 impl Add<(Lit, Coeff)> for BoolLinExp {
 	type Output = BoolLinExp;
 
@@ -1300,7 +1316,7 @@ impl<'a> Add<IntEncoding<'a>> for BoolLinExp {
 
 impl AddAssign<(Lit, Coeff)> for BoolLinExp {
 	fn add_assign(&mut self, rhs: (Lit, Coeff)) {
-		self.terms.push_front(rhs);
+		self.terms.push_back(rhs);
 		self.num_free += 1;
 	}
 }
@@ -1326,7 +1342,9 @@ impl AddAssign<BoolLinExp> for BoolLinExp {
 		debug_assert!(rh_terms.len() == rhs.num_free);
 		self.terms
 			.extend(rh_terms.into_iter().map(|(l, c)| (l, c * rhs.mult)));
-		self.terms.rotate_right(rhs.num_free);
+		// TODO [?] It's probably important, but I don't understand how the purpose of this
+		// rotate. But it changes the order when adding BoolLinExps
+		// self.terms.rotate_right(rhs.num_free);
 		self.num_free += rhs.num_free;
 		self.constraints.extend(rhs.constraints);
 	}
@@ -1914,6 +1932,20 @@ impl LinMarker for TotalizerEncoder {}
 
 #[cfg(test)]
 mod tests {
+
+	#[test]
+	fn test_interface() {
+		let (a, b) = Cnf::default().new_lits();
+		assert_eq!(a + b, BoolLinExp::from_terms(&[(a, 1), (b, 1)]));
+		assert_eq!((2 * a), BoolLinExp::from_terms(&[(a, 2)]));
+		assert_eq!((2 * a) + (3 * b), BoolLinExp::from_terms(&[(a, 2), (b, 3)]));
+		// TODO impl PartialEq properly for tests with mult
+		// assert_eq!(
+		// 	((2 * a) + (3 * b)) * 3,
+		// 	BoolLinExp::from_terms(&[(a, 2), (b, 3)])
+		// );
+	}
+
 	macro_rules! linear_test_suite {
 		($module:ident, $encoder:expr) => {
 			mod $module {
@@ -2904,6 +2936,15 @@ mod tests {
 		assert_checker(&db, &con);
 	}
 
+	impl PartialEq for BoolLinExp {
+		fn eq(&self, other: &Self) -> bool {
+			if self.mult != 1 {
+				unimplemented!("PartialEq only implemented for mult = 1");
+			}
+			self.add == other.add && self.terms().zip(other.terms()).all(|(a, b)| a == b)
+		}
+	}
+
 	impl PartialEq for BoolLinVariant {
 		fn eq(&self, other: &Self) -> bool {
 			let liteq =

crates/pindakaas/src/lib.rs

@@ -34,6 +34,7 @@ use std::{
 };
 
 use itertools::{traits::HomogeneousTuple, Itertools};
+use rustc_hash::FxHashMap;
 
 pub use crate::helpers::AsDynClauseDatabase;
 use crate::{helpers::subscript_number, propositional_logic::Formula, solver::VarFactory};
@@ -294,6 +295,58 @@ pub trait Valuation {
 	fn value(&self, lit: Lit) -> bool;
 }
 
+#[derive(Debug, Default, Clone, PartialEq, Eq)]
+// #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
+pub struct MapSol(pub(crate) FxHashMap<Var, bool>);
+
+impl MapSol {
+	pub fn new<V, I, F>(vars: I, sol: &F) -> Self
+	where
+		V: Into<Lit>,
+		I: IntoIterator<Item = V> + Clone,
+		F: Valuation + ?Sized,
+	{
+		Self(
+			vars.into_iter()
+				.map(|v| v.into())
+				.map(|v| (v.clone().var(), sol.value(v)))
+				.collect(),
+		)
+	}
+	pub fn iter(&self) -> impl Iterator<Item = Lit> + use<'_> {
+		self.0
+			.iter()
+			.map(|(&v, &b)| if b { Lit::from(v) } else { !Lit::from(v) })
+	}
+}
+
+impl Valuation for MapSol {
+	fn value(&self, lit: Lit) -> bool {
+		if let Some(&a) = self.0.get(&lit.var()) {
+			if lit.is_negated() {
+				!a
+			} else {
+				a
+			}
+		} else {
+			panic!("Literal {lit} was not assigned")
+		}
+	}
+}
+
+impl Display for MapSol {
+	fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+		write!(
+			f,
+			"{}",
+			self.iter()
+				.sorted_by_key(|lit| lit.var())
+				.map(|lit| format!("{}", lit))
+				.join(", ")
+		)
+	}
+}
+
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
 /// A cononical implementation of a Boolean decision variable, independent of
 /// negation.

crates/pindakaas/src/solver.rs

@@ -69,10 +69,11 @@ pub trait SolveAssuming: Solver {
 	) -> SolveResult<impl Valuation + '_, impl FailedAssumtions + '_>;
 }
 
-#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
+#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq, Default)]
 pub enum SolveResult<Sol: Valuation, Fail = ()> {
 	Satisfied(Sol),
 	Unsatisfiable(Fail),
+	#[default]
 	Unknown,
 }
 
@@ -201,10 +202,7 @@ impl VarFactory {
 			panic!("unable to create more than `Var::MAX_VARS` variables")
 		};
 		match size {
-			0 => VarRange::new(
-				Var(NonZeroI32::new(2).unwrap()),
-				Var(NonZeroI32::new(1).unwrap()),
-			),
+			0 => VarRange::empty(),
 			1 => {
 				self.next_var = start.next_var();
 				VarRange::new(start, start)

crates/pyndakaas/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "pyndakaas"
-description = "Python interface for to the pindakaas crate"
+description = "Python interface for Pindakaas"
 
 authors.workspace = true
 version.workspace = true
@@ -17,11 +17,17 @@ crate-type = ["cdylib"]
 doc = false
 
 [dependencies]
-pindakaas = { path = "../pindakaas" }
-pyo3 = { version = "0.22", features = ["extension-module"] }
+itertools = "0.14.0"
+pindakaas = { path = "../pindakaas", features= ["cadical", "kissat"] }
+pyo3 = {version = "0.23", features = ["multiple-pymethods"]}
+pindakaas-derive = { path = "../pindakaas-derive"}
+
+[features]
+extension-module = ["pyo3/extension-module"]
 
 [build-dependencies]
 pyo3-build-config = "0.22"
 
+
 [lints]
 workspace = true

crates/pyndakaas/README.md

@@ -0,0 +1,12 @@
+# Pyndakaas: python interface for pindakaas
+
+## To build and install locally
+
+Create and activate virtual enviroment, install dependencies, and run example with maturin
+
+```
+python -m venv venv
+source ./venv/bin/activate
+pip install .
+./example.py
+```

crates/pyndakaas/example.py

@@ -0,0 +1,77 @@
+#!/usr/bin/env python3
+import pindakaas as pk
+
+def main():
+    cnf = pk.Cnf()
+    a = cnf.add_variable()
+    b,c = cnf.add_variables(2)
+    cnf.add_clause([~a,b]) # ~a \/ b
+    cnf.add_clause([(~b).var(),c]) # b \/ c
+    # Not allowed: cnf.add_clause([-1,-2]) # `TypeError: argument 'clause': 'int' object cannot be converted to 'Lit'`
+
+    # TODO unfortunately, doesn't quite work.
+    # with cnf.with_conditions([a,b]) as ccnf:
+    #     ccnf.add_clause([c]) # (-1 /\ -2) -> 3
+    #     cnf.add_linear([a,b,c], coefficients=[2,3,5], comparator=pk.Comparator.LessEq, k=6)
+    #     print(f"CCNF {ccnf}") # TODO not sure why still available but ok
+    #     print(f"CNF {cnf}")
+    # exit(0)
+
+    try:
+        cnf.add_clause([])
+    except pk.Unsatisfiable as e:
+        print(f"Caught Unsatisfiable exception: {e} of type {type(e)}")
+
+    # 2*a + 3*b + 5*c <= 6
+    cnf.add_linear([a,b,c], coefficients=[2,3,5], comparator=pk.Comparator.LessEq, k=6)
+    p = cnf.add_variable()
+    cnf.add_linear([a,b,c], coefficients=[2,3,5], comparator=pk.Comparator.LessEq, k=6, conditions=[~p])
+    cnf.add_linear([a,b,c]) # a + b + c >= 1 == a \/ b \/ c
+
+    for clause in cnf:
+        for lit in clause:
+            print(f"{lit}, ", end="")
+        print("\n", end="")
+
+    wcnf = pk.Wcnf()
+    a = wcnf.add_variable()
+    b,c = wcnf.add_variables(2)
+    wcnf.add_clause([~a,b]) # ~a \/ b
+    wcnf.add_clause([(~b).var(),c]) # b \/ c
+    # TODO add weighted clause
+
+    cadical = pk.Cadical() # should "inherit" from Cnf/ClauseDatabase
+    a = cadical.add_variable()
+    b = cadical.add_variable()
+    cadical.add_clause([a,b])
+    cadical.add_clause([~a,~b])
+    assert cadical.solve([a,b]) is True # Return True (SAT), False (UNSAT), None (UNKNOWN)
+    assert cadical.value(a) is not cadical.value(b)
+
+    kissat = pk.Kissat()
+    a = kissat.add_variable()
+    kissat.add_clause([a])
+    assert kissat.solve([a,b]) is True
+    assert kissat.value(a) is True
+
+    # TODO translate pysat's pigeonhole problem to pindakaas
+
+    # print(f"{solver.value(a)}") # Also True/False/None
+    # assert solver.value(a) != solver.value(b)
+    # TODO: for completing CPMpy standard: timeouts
+    # assert solver.solve(time_limit=datetime.duration(10))
+
+    # TODO: all solutions
+    # for sol in solver.solutions():
+    #     print(f"{sol}")
+
+    # TODO beyond: solver selection, encoder selection, improve implied constraints
+    # `pip install pindakaas[solver]`
+    # solver = pk.Solver(name="kissat")
+
+    # print(f"2nd {solver.value(a)}") # Also True/False/None
+    # TODO nice to have:
+    # cnf.add_linear(cnf, (2*a) + (3*b) + (5*c) <= 6) # Low priority: more overloading to create constraint objects
+
+if __name__ in "__main__":
+    main()

crates/pyndakaas/pyproject.toml

@@ -1,9 +1,10 @@
 [build-system]
-requires = ["maturin>=0.11,<0.12"]
+requires = ["maturin>=1.0,<2.0"]
 build-backend = "maturin"
 
 [project]
 name = "pindakaas"
+dynamic = ["version"]
 description = "Encoding Integer and Pseudo Boolean constraints into CNF"
 requires-python = ">=3.8"
 classifiers = [
@@ -13,4 +14,7 @@ classifiers = [
 	"Intended Audience :: Science/Research",
 	"Programming Language :: Python",
 	"Programming Language :: Rust",
-]
+]
+
+[tool.maturin]
+features = ["pyo3/extension-module"]

crates/pyndakaas/src/lib.rs

@@ -3,105 +3,319 @@
 	reason = "pyo3 macro will generate unused qualified types"
 )]
 
-use std::{fmt::Display, ops::DerefMut, path::PathBuf};
+// TODO features -> extra installs via pip (e.g. pip install pindakaas[cadical,kissat])
+// TODO better type checking and errors (e.g. adding non-list to add_clause currently gives `TypeError: argument 'clause': 'Lit' object cannot be converted to 'Sequence'`)
+use itertools::Itertools;
+use pindakaas_derive::{PythonClauseDatabase, PythonClauseDatabaseTools, PythonSolver};
+use std::fmt::Display;
 
-use ::pindakaas as base;
+use ::pindakaas::{self as base, solver::Solver, MapSol, Valuation};
 use base::{
-	bool_linear::{BoolLinExp, BoolLinear, Comparator, LinearEncoder},
-	ClauseDatabaseTools, Encoder,
+	bool_linear::{BoolLinExp, BoolLinear, LinearEncoder},
+	Encoder,
 };
-use pyo3::{exceptions::PyArithmeticError, prelude::*};
+use pyo3::{exceptions::PyException, prelude::*};
 
 type Clause = Vec<Lit>;
 
-#[pyclass]
-struct ClauseIter {
-	inner: std::vec::IntoIter<Clause>,
+#[pyclass(subclass)]
+struct ClauseDatabase();
+
+#[pymethods]
+impl ClauseDatabase {
+	#[new]
+	fn new() -> Self {
+		Self()
+	}
+
+	#[allow(unused_variables, reason = "Pseudo-abstract method")]
+	fn add_clause_from_slice(&mut self, clause: Vec<Lit>) -> Result {
+		unimplemented!("ABSTRACT")
+	}
+
+	#[allow(unused_variables, reason = "Pseudo-abstract method")]
+	fn new_var_range(&mut self, len: usize) -> VarRange {
+		unimplemented!("ABSTRACT")
+	}
 }
 
-#[pyclass(name = "CNF")]
-struct Cnf(base::Cnf);
+#[pyclass]
+#[derive(Clone)]
+struct VarRange(base::VarRange);
 
 #[pyclass]
 #[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub struct Lit(base::Lit);
-
-#[pyfunction]
-fn adder_encode(mut db: PyRefMut<'_, Cnf>) -> Result<(), PyErr> {
-	let pref = db.deref_mut();
-	let db = &mut pref.0;
-	let x = BoolLinExp::from_slices(
-		&[1, 2, 3],
-		&[
-			db.new_var().into(),
-			db.new_var().into(),
-			db.new_var().into(),
-		],
-	);
-	let con = BoolLinear::new(x, Comparator::Equal, 2);
-	let enc: LinearEncoder = LinearEncoder::default();
-	enc.encode(db, &con)
-		.map_err(|_e| PyArithmeticError::new_err("Unsatisfiable"))
+struct Lit(base::Lit);
+
+#[pyclass]
+struct VarRangeIter(std::vec::IntoIter<Lit>);
+
+#[pymethods]
+impl VarRangeIter {
+	fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> {
+		slf
+	}
+
+	fn __next__(mut slf: PyRefMut<'_, Self>) -> Option<Lit> {
+		slf.0.next()
+	}
+}
+
+#[pymethods]
+impl VarRange {
+	fn __iter__(&mut self) -> VarRangeIter {
+		VarRangeIter(self.0.iter_lits().map(Lit).collect_vec().into_iter())
+		// TODO Non-collect version WIP, might require unsupported lifetimes: VarRangeIter(self.0.iter_lits().map(|l| Lit(l)))
+	}
+}
+
+// TODO use create_exception! ?
+#[pyclass(extends = PyException)]
+struct Unsatisfiable;
+
+type Result<T = (), E = Unsatisfiable> = std::result::Result<T, E>;
+
+#[pymethods]
+impl Unsatisfiable {
+	#[new]
+	fn new() -> Self {
+		Self
+	}
+	fn __str__(&self) -> String {
+		"Unsatisfiable".to_owned()
+	}
+}
+
+impl From<base::Unsatisfiable> for Unsatisfiable {
+	fn from(_: base::Unsatisfiable) -> Self {
+		Self
+	}
+}
+
+impl From<Unsatisfiable> for PyErr {
+	fn from(_: Unsatisfiable) -> PyErr {
+		PyErr::new::<Unsatisfiable, _>(())
+	}
+}
+
+impl From<Lit> for base::Lit {
+	fn from(val: Lit) -> Self {
+		val.0
+	}
+}
+
+// TODO [?] How to avoid this duplication?
+#[pyclass(eq, eq_int)]
+#[derive(Clone, PartialEq, Default)]
+enum Comparator {
+	LessEq,
+	Equal,
+	#[default]
+	GreaterEq,
 }
 
+impl From<Comparator> for base::bool_linear::Comparator {
+	fn from(val: Comparator) -> Self {
+		match val {
+			Comparator::LessEq => base::bool_linear::Comparator::LessEq,
+			Comparator::Equal => base::bool_linear::Comparator::Equal,
+			Comparator::GreaterEq => base::bool_linear::Comparator::GreaterEq,
+		}
+	}
+}
+
+// TODO [?] why not export Coeff from lib?
+type Coeff = i64;
+
 #[pymodule]
 fn pindakaas(m: &Bound<'_, PyModule>) -> PyResult<()> {
 	m.add_class::<Cnf>()?;
-	m.add_function(wrap_pyfunction!(adder_encode, m)?)?;
+	m.add_class::<Wcnf>()?;
+	m.add_class::<Cadical>()?;
+	m.add_class::<Kissat>()?;
+	m.add_class::<Unsatisfiable>()?;
+	m.add_class::<Comparator>()?;
 	Ok(())
 }
 
+#[pyclass(extends=ClauseDatabase)]
+#[derive(PythonClauseDatabase, PythonClauseDatabaseTools)]
+struct Cnf(base::Cnf);
+
+#[pyclass]
+struct ClauseIter(std::vec::IntoIter<Clause>);
+
 #[pymethods]
 impl ClauseIter {
 	fn __iter__(slf: PyRef<'_, Self>) -> PyRef<'_, Self> {
 		slf
 	}
+
 	fn __next__(mut slf: PyRefMut<'_, Self>) -> Option<Clause> {
-		slf.inner.next()
+		slf.0.next()
 	}
 }
 
 #[pymethods]
 impl Cnf {
+	#[new]
+	fn new() -> (Self, ClauseDatabase) {
+		(Self(base::Cnf::default()), ClauseDatabase::new())
+	}
+
 	fn __iter__(&self) -> ClauseIter {
 		// FIXME: It would be great if this could be made lazily instead of copying everything when creating the iterator
-		// ClauseIter {
-		// 	inner: Vec::from_iter(self.0.iter().map(Vec::from)).into_iter(),
-		// }
-		todo!()
+		ClauseIter(
+			Vec::from_iter(
+				self.0
+					.iter()
+					.map(|clause| clause.iter().map(|l| Lit(*l)).collect_vec()),
+			)
+			.into_iter(),
+		)
 	}
 
 	fn __str__(&self) -> String {
-		self.0.to_string()
-	}
-	#[staticmethod]
-	fn from_file(path: PathBuf) -> Result<Self, std::io::Error> {
-		Ok(Self(base::Cnf::from_file(&path)?))
+		format!("{}", self.0)
 	}
+
+	// TODO [?] Shouldn't we make reading from_file part of ClauseDatabaseTools?
+	// TODO [?] Doesn't compile, seems like a PyO3 bug
+	// #[staticmethod]
+	// fn from_file(path: PathBuf) -> std::result::Result<Cnf, std::io::Error> {
+	// 	Ok(Self(base::Cnf::from_file(&path)?))
+	// }
+}
+
+#[pyclass(extends=ClauseDatabase)]
+#[derive(PythonClauseDatabase, PythonClauseDatabaseTools)]
+struct Wcnf(base::Wcnf);
+
+#[pymethods]
+impl Wcnf {
 	#[new]
-	fn new() -> Self {
-		Self(base::Cnf::default())
+	fn new() -> (Self, ClauseDatabase) {
+		(Self(base::Wcnf::default()), ClauseDatabase::new())
 	}
 }
+
+#[pymethods]
 impl Lit {
-	pub fn is_negated(&self) -> bool {
+	/// Returns whether the literal is a negation of the underlying variable.
+	fn is_negated(&self) -> bool {
 		self.0.is_negated()
 	}
-	pub fn var(&self) -> Self {
-		Self(self.0.var().into()) // TODO
+
+	fn __invert__(&self) -> Self {
+		Self(!self.0)
+	}
+
+	/// Returns the underlying variable of the literal, whether negated or not.
+	fn var(&self) -> Self {
+		Self(self.0.var().into())
 	}
+
+	fn __str__(&self) -> String {
+		format!("{}", self.0)
+	}
+
+	// TODO Bit* operations
 }
+
 impl Display for Lit {
 	fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
 		self.0.fmt(f)
 	}
 }
 
+// SOLVING
+//
+
+#[pyclass(unsendable)]
+#[derive(Default, PythonClauseDatabase, PythonClauseDatabaseTools, PythonSolver)]
+// TODO can we derive PythonClauseDatabase by PythonSolver?
+#[python_clause_database(db = solver)]
+#[python_clause_database_tools(db = solver)]
+#[python_solver(slv = solver)]
+struct Cadical {
+	solver: base::solver::cadical::Cadical,
+	solution: Option<base::MapSol>,
+}
+
+#[pyclass(unsendable)]
+#[derive(Default, PythonClauseDatabase, PythonClauseDatabaseTools, PythonSolver)]
+#[python_clause_database(db = solver)]
+#[python_clause_database_tools(db = solver)]
+#[python_solver(slv = solver)]
+struct Kissat {
+	solver: base::solver::kissat::Kissat,
+	solution: Option<base::MapSol>,
+}
+
+// solution: Solution,
+// solve_result: base::solver::SolveResult<
+// 	base::solver::cadical::CadicalSol<'a>,
+// 	base::solver::cadical::CadicalFailed<'a>,
+// >,
+
+#[pyclass]
+struct SolveResult(base::solver::SolveResult<MapSol>);
+
+#[pymethods]
+impl SolveResult {
+	// #[new]
+	// fn new() -> Self {
+	// 	Self(base::solver::SolveResult::default())
+	// }
+
+	fn __str__(&self) -> String {
+		match &self.0 {
+			::pindakaas::solver::SolveResult::Satisfied(sol) => format!("{}", sol),
+			::pindakaas::solver::SolveResult::Unsatisfiable(_) => {
+				format!("{}", base::Unsatisfiable)
+			}
+			::pindakaas::solver::SolveResult::Unknown => "UNKNOWN".to_owned(),
+		}
+	}
+}
+
+// #[pyclass]
+// struct Solution(base::solver::cadical::CadicalSol); // TODO can't because of lifetime
+// 													// struct Solution(M);
+
 #[cfg(test)]
 mod tests {
+
+	use std::ffi::CString;
+
+	use super::*;
+	use pyo3::{ffi::c_str, Python};
+
+	#[pyclass]
+	struct LoggingStdout;
+	#[pymethods]
+	impl LoggingStdout {
+		fn write(&self, data: &str) {
+			print!("{}", data);
+		}
+	}
+
 	#[test]
-	fn it_works() {
-		let result = 2 + 2;
-		assert_eq!(result, 4);
+	fn test_interface() {
+		pyo3::append_to_inittab!(pindakaas);
+		pyo3::prepare_freethreaded_python();
+		Python::with_gil(|py| {
+			let sys = py.import("sys").unwrap();
+			_ = sys.setattr("stdout", LoggingStdout.into_pyobject(py).unwrap());
+			_ = PyModule::from_code(
+				py,
+				CString::new(include_str!("../example.py"))
+					.unwrap()
+					.as_c_str(),
+				c_str!("example.py"),
+				c_str!("__main__"),
+			)
+			.unwrap_or_else(|e| panic!("{e}"));
+		});
 	}
 }