Add 'Send' to glucose

chrjabs · Apr 2, 2024 · 6d743a5 · 6d743a5
1 parent 4de2035
commit 6d743a5
Showing 1 changed file with 62 additions and 0 deletions.
diff --git a/glucose/src/core.rs b/glucose/src/core.rs
@@ -23,6 +23,8 @@ pub struct Glucose {
     stats: SolverStats,
 }
 
+unsafe impl Send for Glucose {}
+
 impl Default for Glucose {
     fn default() -> Self {
         Self {
@@ -321,6 +323,11 @@ impl Drop for Glucose {
 
 #[cfg(test)]
 mod test {
+    use std::{
+        sync::{Arc, Mutex},
+        thread,
+    };
+
     use super::Glucose;
     use rustsat::{
         lit,
@@ -351,6 +358,61 @@ mod test {
         }
     }
 
+    #[test]
+    fn tiny_instance_multithreaded_sat() {
+        let mutex_solver = Arc::new(Mutex::new(Glucose::default()));
+        let ret = {
+            let mut solver = mutex_solver.lock().unwrap();
+            solver.add_binary(lit![0], !lit![1]).unwrap();
+            solver.add_binary(lit![1], !lit![2]).unwrap();
+            solver.solve()
+        };
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Sat),
+        }
+
+        // Now in another thread
+        let s = mutex_solver.clone();
+        let ret = thread::spawn(move || {
+            let mut solver = s.lock().unwrap();
+            solver.solve()
+        })
+        .join()
+        .unwrap();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Sat),
+        }
+
+        // Now add to solver in other thread
+        let s = mutex_solver.clone();
+        let ret = thread::spawn(move || {
+            let mut solver = s.lock().unwrap();
+            solver.add_unit(!lit![0]).unwrap();
+            solver.add_unit(lit![2]).unwrap();
+            solver.solve()
+        })
+        .join()
+        .unwrap();
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Unsat),
+        }
+
+        let ret = {
+            let mut solver = mutex_solver.lock().unwrap();
+            solver.add_binary(lit![0], !lit![1]).unwrap();
+            solver.add_binary(lit![1], !lit![2]).unwrap();
+            solver.solve()
+        };
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Unsat),
+        }
+        // Finally, back in the main thread
+    }
+
     #[test]
     fn tiny_instance_unsat() {
         let mut solver = Glucose::default();