Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add 'Send' to glucose #77

Merged
merged 1 commit into from
Apr 3, 2024
+340 −0
Merged

Add 'Send' to glucose #77

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
62 changes: 62 additions & 0 deletions cadical/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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();
Expand Down
62 changes: 62 additions & 0 deletions glucose/src/core.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ pub struct Glucose {
stats: SolverStats,
}

unsafe impl Send for Glucose {}

impl Default for Glucose {
fn default() -> Self {
Self {
Expand Down Expand Up @@ -321,6 +323,11 @@ impl Drop for Glucose {

#[cfg(test)]
mod test {
use std::{
sync::{Arc, Mutex},
thread,
};

use super::Glucose;
use rustsat::{
lit,
Expand Down Expand Up @@ -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();
Expand Down
45 changes: 45 additions & 0 deletions glucose/src/simp.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ pub struct Glucose {
stats: SolverStats,
}

unsafe impl Send for Glucose {}

impl Default for Glucose {
fn default() -> Self {
Self {
Expand Down Expand Up @@ -350,6 +352,11 @@ impl Drop for Glucose {

#[cfg(test)]
mod test {
use std::{
sync::{Arc, Mutex},
thread,
};

use super::Glucose;
use rustsat::{
lit,
Expand Down Expand Up @@ -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();
Expand Down
2 changes: 2 additions & 0 deletions ipasir/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,8 @@ pub struct IpasirSolver<'term, 'learn> {
stats: SolverStats,
}

unsafe impl Send for IpasirSolver<'_, '_> {}

impl Default for IpasirSolver<'_, '_> {
fn default() -> Self {
Self {
Expand Down
45 changes: 45 additions & 0 deletions kissat/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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]
Expand Down Expand Up @@ -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();
Expand Down
62 changes: 62 additions & 0 deletions minisat/src/core.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ pub struct Minisat {
stats: SolverStats,
}

unsafe impl Send for Minisat {}

impl Default for Minisat {
fn default() -> Self {
Self {
Expand Down Expand Up @@ -321,6 +323,11 @@ impl Drop for Minisat {

#[cfg(test)]
mod test {
use std::{
sync::{Arc, Mutex},
thread,
};

use super::Minisat;
use rustsat::{
lit,
Expand Down Expand Up @@ -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();
Expand Down
Loading
Loading