Add 'Send' to solvers, and add tests

chrjabs · Apr 3, 2024 · c38a887 · c38a887
1 parent 4de2035
commit c38a887
Show file tree

Hide file tree

Showing 7 changed files with 340 additions and 0 deletions.
diff --git a/cadical/src/lib.rs b/cadical/src/lib.rs
@@ -76,6 +76,8 @@ pub struct CaDiCaL<'term, 'learn> {
     stats: SolverStats,
 }
 
+unsafe impl Send for CaDiCaL<'_, '_> {}
+
 impl Default for CaDiCaL<'_, '_> {
     fn default() -> Self {
         let solver = Self {
@@ -795,6 +797,11 @@ impl fmt::Display for Limit {
 
 #[cfg(test)]
 mod test {
+    use std::{
+        sync::{Arc, Mutex},
+        thread,
+    };
+
     use super::{CaDiCaL, Config, Limit};
     use rustsat::{
         lit,
@@ -843,6 +850,61 @@ mod test {
         }
     }
 
+    #[test]
+    fn tiny_instance_multithreaded_sat() {
+        let mutex_solver = Arc::new(Mutex::new(CaDiCaL::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),
+        }
+
+        // Finally, back in the main thread
+        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),
+        }
+    }
+
     #[test]
     fn termination_callback() {
         let mut solver = CaDiCaL::default();

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),
+        }
+
+        // Finally, back in the main thread
+        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),
+        }
+    }
+
     #[test]
     fn tiny_instance_unsat() {
         let mut solver = Glucose::default();

diff --git a/glucose/src/simp.rs b/glucose/src/simp.rs
@@ -24,6 +24,8 @@ pub struct Glucose {
     stats: SolverStats,
 }
 
+unsafe impl Send for Glucose {}
+
 impl Default for Glucose {
     fn default() -> Self {
         Self {
@@ -350,6 +352,11 @@ impl Drop for Glucose {
 
 #[cfg(test)]
 mod test {
+    use std::{
+        sync::{Arc, Mutex},
+        thread,
+    };
+
     use super::Glucose;
     use rustsat::{
         lit,
@@ -394,6 +401,44 @@ 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),
+        }
+
+        // Finally, back in the main thread
+        let ret = {
+            let mut solver = mutex_solver.lock().unwrap();
+            solver.solve()
+        };
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res, SolverResult::Sat),
+        }
+    }
+
     #[test]
     fn backend_stats() {
         let mut solver = Glucose::default();

diff --git a/ipasir/src/lib.rs b/ipasir/src/lib.rs
@@ -84,6 +84,8 @@ pub struct IpasirSolver<'term, 'learn> {
     stats: SolverStats,
 }
 
+unsafe impl Send for IpasirSolver<'_, '_> {}
+
 impl Default for IpasirSolver<'_, '_> {
     fn default() -> Self {
         Self {

diff --git a/kissat/src/lib.rs b/kissat/src/lib.rs
@@ -76,6 +76,8 @@ pub struct Kissat<'term> {
     stats: SolverStats,
 }
 
+unsafe impl Send for Kissat<'_> {}
+
 impl Default for Kissat<'_> {
     fn default() -> Self {
         let solver = Self {
@@ -422,10 +424,16 @@ impl fmt::Display for Limit {
 
 #[cfg(test)]
 mod test {
+    use std::{
+        sync::{Arc, Mutex},
+        thread,
+    };
+
     use super::{Config, Kissat, Limit};
     use rustsat::{
         lit,
         solvers::{Solve, SolverResult, SolverState, StateError},
+        types::{TernaryVal, Var},
     };
 
     #[test]
@@ -465,6 +473,43 @@ mod test {
         }
     }
 
+    #[test]
+    fn tiny_instance_multithreaded_sat() {
+        let mutex_solver = Arc::new(Mutex::new(Kissat::default()));
+
+        {
+            // Build in one thread
+            let mut solver = mutex_solver.lock().unwrap();
+            solver.add_binary(lit![0], !lit![1]).unwrap();
+            solver.add_unit(lit![0]).unwrap();
+            solver.add_binary(lit![1], !lit![2]).unwrap();
+        }
+
+        // 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),
+        }
+
+        // Finally, back in the main thread
+        let ret = {
+            let solver = mutex_solver.lock().unwrap();
+            solver.full_solution()
+        };
+
+        match ret {
+            Err(e) => panic!("got error when solving: {}", e),
+            Ok(res) => assert_eq!(res.var_value(Var::new(0)), TernaryVal::True),
+        }
+    }
+
     #[test]
     fn configure() {
         let mut solver = Kissat::default();

diff --git a/minisat/src/core.rs b/minisat/src/core.rs
@@ -23,6 +23,8 @@ pub struct Minisat {
     stats: SolverStats,
 }
 
+unsafe impl Send for Minisat {}
+
 impl Default for Minisat {
     fn default() -> Self {
         Self {
@@ -321,6 +323,11 @@ impl Drop for Minisat {
 
 #[cfg(test)]
 mod test {
+    use std::{
+        sync::{Arc, Mutex},
+        thread,
+    };
+
     use super::Minisat;
     use rustsat::{
         lit,
@@ -365,6 +372,61 @@ mod test {
         }
     }
 
+    #[test]
+    fn tiny_instance_multithreaded_sat() {
+        let mutex_solver = Arc::new(Mutex::new(Minisat::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),
+        }
+
+        // Finally, back in the main thread
+        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),
+        }
+    }
+
     #[test]
     fn backend_stats() {
         let mut solver = Minisat::default();