pull request for Sat backend

Cargo.toml

@@ -4,7 +4,7 @@ resolver = "2"
 default-members = [
     "conjure_oxide",
     "crates/conjure_core",
-    "solvers/kissat",
+    "solvers/sat_rs",
     "solvers/minion",
 ]
 
@@ -13,8 +13,8 @@ members = [
     "crates/conjure_core",
     "crates/enum_compatability_macro",
     "crates/conjure_macros",
-    "solvers/kissat",
-    "solvers/minion",
+    "solvers/minion", 
+    "solvers/sat_rs",
 ]
 
 [workspace.lints.clippy]

conjure_oxide/Cargo.toml

@@ -31,6 +31,8 @@ schemars = "0.8.21"
 toml = "0.8.19"
 glob = "0.3.1"
 rand = "0.8.5"
+rustsat = "0.6.1"
+rustsat-minisat = "0.4.1"
 
 [features]
 

crates/conjure_core/Cargo.toml

@@ -26,6 +26,9 @@ schemars = "0.8.21"
 clap = { version = "4.5.20", features = ["derive"] }
 itertools = "0.13.0"
 im = "15.1.0"
+sat_rs = { version = "0.1.0", path = "../../solvers/sat_rs" }
+rustsat-minisat = "0.4.0"
+rustsat = "0.6.1"
 
 [lints]
 workspace = true

crates/conjure_core/src/solver/adaptors/common.rs.txt

@@ -0,0 +1,45 @@
+use crate::solver::SolverFamily;
+
+use rustsat::instances::SatInstance;
+
+use sat_rs::{sat_solvers::SatSolverInst, sat_tree};
+
+// use rustsat_minisat: 
+
+trait SolverAdaptor {
+    fn prep_dat();
+
+    fn get_soln();
+
+    fn print_soln() -> ();
+}
+
+impl SolverAdaptor for SatSolverInst<SolverType: > {
+    fn prep_dat(vec_problem: &Vec<Vec<i16>>, inst_in_use: &mut SatInstance) -> () {
+        // todo!()
+        sat_tree::conv_to_formula(&vec_problem, &mut self.inst);
+    }
+
+    fn get_soln() -> Result<bool, String>{
+        // todo!()
+        self.solver.solve()
+    }
+
+    fn print_soln() {
+        // todo!()
+        match problem.solve() {
+            Ok(true) => {
+                println!("SATISFIABLE");
+                println!("a = {}", problem.get_assignment(a).unwrap());
+                println!("b = {}", problem.get_assignment(b).unwrap());
+            }
+            Ok(false) => println!("UNSATISFIABLE"),
+            Err(e) => println!("Error during solving: {:?}", e),
+        }
+    }
+
+
+}
+
+struct MinionAdaptor {
+}

crates/conjure_core/src/solver/adaptors/mod.rs

@@ -1,11 +1,13 @@
 //! Solver adaptors.
 
-#[doc(inline)]
-pub use kissat::Kissat;
+// #[doc(inline)]
+// pub use kissat::Kissat;
 #[doc(inline)]
 pub use minion::Minion;
+pub use sat_adaptor::SAT;
+// mod sat_common;
 
-mod sat_common;
-
-mod kissat;
+// mod kissat;
 mod minion;
+pub mod sat_adaptor;                                //temp visibility
+// mod common;