diff --git a/.gitmodules b/.gitmodules index 3399bd3ba3..bb758f9e93 100644 --- a/.gitmodules +++ b/.gitmodules @@ -4,3 +4,6 @@ [submodule "crates/pindakaas-intel-sat/vendor/intel_sat"] path = crates/pindakaas-intel-sat/vendor/intel_sat url = https://github.com/alexander-nadel/intel_sat_solver.git +[submodule "crates/pindakaas-kissat/vendor/kissat"] + path = crates/pindakaas-kissat/vendor/kissat + url = https://github.com/arminbiere/kissat.git diff --git a/crates/pindakaas-kissat/Cargo.toml b/crates/pindakaas-kissat/Cargo.toml new file mode 100644 index 0000000000..b8d79bf45c --- /dev/null +++ b/crates/pindakaas-kissat/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "pindakaas-kissat" +version = "3.1.1" +edition = "2021" +build = "build.rs" +links = "kissat" +exclude = ["vendor/kissat"] +include = ["vendor/kissat/src/*.c"] + +[build-dependencies] +cc = { version = "1.0", features = ["parallel"] } + +[dependencies] +pindakaas-build-macros = { path = "../pindakaas-build-macros" } diff --git a/crates/pindakaas-kissat/build.rs b/crates/pindakaas-kissat/build.rs new file mode 100644 index 0000000000..04b872c20d --- /dev/null +++ b/crates/pindakaas-kissat/build.rs @@ -0,0 +1,148 @@ +use std::process::Command; + +fn main() { + let src = [ + "vendor/kissat/src/allocate.c", + "vendor/kissat/src/analyze.c", + "vendor/kissat/src/ands.c", + "vendor/kissat/src/application.c", + "vendor/kissat/src/arena.c", + "vendor/kissat/src/assign.c", + "vendor/kissat/src/averages.c", + "vendor/kissat/src/backbone.c", + "vendor/kissat/src/backtrack.c", + "vendor/kissat/src/build.c", + "vendor/kissat/src/bump.c", + "vendor/kissat/src/check.c", + "vendor/kissat/src/clause.c", + "vendor/kissat/src/collect.c", + "vendor/kissat/src/colors.c", + "vendor/kissat/src/compact.c", + "vendor/kissat/src/config.c", + "vendor/kissat/src/decide.c", + "vendor/kissat/src/deduce.c", + "vendor/kissat/src/definition.c", + "vendor/kissat/src/dense.c", + "vendor/kissat/src/dump.c", + "vendor/kissat/src/eliminate.c", + "vendor/kissat/src/equivalences.c", + "vendor/kissat/src/error.c", + "vendor/kissat/src/extend.c", + "vendor/kissat/src/file.c", + "vendor/kissat/src/flags.c", + "vendor/kissat/src/format.c", + "vendor/kissat/src/forward.c", + "vendor/kissat/src/gates.c", + "vendor/kissat/src/handle.c", + "vendor/kissat/src/heap.c", + "vendor/kissat/src/ifthenelse.c", + "vendor/kissat/src/import.c", + "vendor/kissat/src/internal.c", + "vendor/kissat/src/kimits.c", + "vendor/kissat/src/kitten.c", + "vendor/kissat/src/learn.c", + "vendor/kissat/src/logging.c", + "vendor/kissat/src/minimize.c", + "vendor/kissat/src/mode.c", + "vendor/kissat/src/options.c", + "vendor/kissat/src/parse.c", + "vendor/kissat/src/phases.c", + "vendor/kissat/src/print.c", + "vendor/kissat/src/probe.c", + "vendor/kissat/src/profile.c", + "vendor/kissat/src/promote.c", + "vendor/kissat/src/proof.c", + "vendor/kissat/src/propbeyond.c", + "vendor/kissat/src/propdense.c", + "vendor/kissat/src/proprobe.c", + "vendor/kissat/src/propsearch.c", + "vendor/kissat/src/queue.c", + "vendor/kissat/src/reduce.c", + "vendor/kissat/src/reluctant.c", + "vendor/kissat/src/rephase.c", + "vendor/kissat/src/report.c", + "vendor/kissat/src/resize.c", + "vendor/kissat/src/resolve.c", + "vendor/kissat/src/resources.c", + "vendor/kissat/src/restart.c", + "vendor/kissat/src/search.c", + "vendor/kissat/src/shrink.c", + "vendor/kissat/src/smooth.c", + "vendor/kissat/src/sort.c", + "vendor/kissat/src/stack.c", + "vendor/kissat/src/statistics.c", + "vendor/kissat/src/strengthen.c", + "vendor/kissat/src/substitute.c", + "vendor/kissat/src/sweep.c", + "vendor/kissat/src/terminate.c", + "vendor/kissat/src/trail.c", + "vendor/kissat/src/transitive.c", + "vendor/kissat/src/utilities.c", + "vendor/kissat/src/vector.c", + "vendor/kissat/src/vivify.c", + "vendor/kissat/src/walk.c", + "vendor/kissat/src/warmup.c", + "vendor/kissat/src/watch.c", + "vendor/kissat/src/weaken.c", + "vendor/kissat/src/witness.c", + "src/ipasir.c", + ]; + + let mut builder = cc::Build::new(); + + let compiler = builder.try_get_compiler().unwrap(); + let version = include_str!("vendor/kissat/VERSION").trim(); + let git_id = String::from_utf8( + Command::new("git") + .current_dir("vendor/kissat") + .args(&["rev-parse", "HEAD"]) + .output() + .unwrap() + .stdout, + ) + .unwrap(); + let date = String::from_utf8( + Command::new("date") + .env("LC_LANG", "en_US") + .output() + .unwrap() + .stdout, + ) + .unwrap(); + let uname = String::from_utf8( + Command::new("uname") + .args(&["-srmn"]) + .output() + .unwrap() + .stdout, + ) + .unwrap(); + + assert_eq!(env!("CARGO_PKG_VERSION"), version); + + let build = builder + .include("./src") + .define("VERSION", format!("\"{version}\"").as_str()) + .define( + "COMPILER", + format!( + "{:?}", + format!( + "{} {}", + compiler.path().to_str().unwrap(), + compiler.args().join(" ".as_ref()).to_str().unwrap() + ) + ) + .as_ref(), + ) + .define("ID", format!("\"{}\"", git_id.trim()).as_ref()) + .define( + "BUILD", + format!("\"{} {}\"", date.trim(), uname.trim()).as_ref(), + ) + .define("QUIET", None); + + build.files(src); + + build.compile("kissat"); +} diff --git a/crates/pindakaas-kissat/src/build.h b/crates/pindakaas-kissat/src/build.h new file mode 100644 index 0000000000..6dd3645de0 --- /dev/null +++ b/crates/pindakaas-kissat/src/build.h @@ -0,0 +1 @@ +// Empty file, defines are set in build.rs diff --git a/crates/pindakaas-kissat/src/ipasir.c b/crates/pindakaas-kissat/src/ipasir.c new file mode 100644 index 0000000000..c31000ba21 --- /dev/null +++ b/crates/pindakaas-kissat/src/ipasir.c @@ -0,0 +1,19 @@ +#include "../vendor/kissat/src/kissat.h" +#include +#include + +/// Empty function to complete IPASIR default interface +void kissar_set_learn(void *solver, void *state, int max_length, + void (*learn)(void *state, int *clause)) { + assert(0); +} + +int32_t kissat_val(void *solver, int32_t lit) { + return kissat_value(solver, lit); +} + +int kissat_failed(void *solver, int32_t lit) { + assert(0); + return 0; +} +void kissat_assume(void *solver, int32_t lit) { assert(0); } diff --git a/crates/pindakaas-kissat/src/lib.rs b/crates/pindakaas-kissat/src/lib.rs new file mode 100644 index 0000000000..beac21e541 --- /dev/null +++ b/crates/pindakaas-kissat/src/lib.rs @@ -0,0 +1,29 @@ +use std::ffi::{c_char, c_int, c_uint, c_void}; + +use pindakaas_build_macros::ipasir_definitions; + +ipasir_definitions!(kissat); + +extern "C" { + pub fn kissat_terminate(slv: *mut c_void); + pub fn kissat_reserve(slv: *mut c_void, max_var: c_int); + + pub fn kissat_id() -> *const c_char; + pub fn kissat_version() -> *const c_char; + pub fn kissat_compiler() -> *const c_char; + + pub fn kissat_copyright() -> *const *const c_char; + pub fn kissat_build(line_prefix: *const c_char); + pub fn kissat_banner(line_prefix: *const c_char, name_of_app: *const c_char); + + pub fn kissat_get_option(slv: *mut c_void, name: *const c_char) -> c_int; + pub fn kissat_set_option(slv: *mut c_void, name: *const c_char, new_value: c_int) -> c_int; + + pub fn kissat_has_configuration(name: *const c_char) -> c_int; + pub fn kissat_set_configuration(slv: *mut c_void, name: *const c_char) -> c_int; + + pub fn kissat_set_conflict_limit(slv: *mut c_void, limit: c_uint); + pub fn kissat_set_decision_limit(slv: *mut c_void, limit: c_uint); + + pub fn kissat_print_statistics(slv: *mut c_void); +} diff --git a/crates/pindakaas-kissat/vendor/kissat b/crates/pindakaas-kissat/vendor/kissat new file mode 160000 index 0000000000..71caafb4d1 --- /dev/null +++ b/crates/pindakaas-kissat/vendor/kissat @@ -0,0 +1 @@ +Subproject commit 71caafb4d182ced9f76cef45b00f37cc598f2a37 diff --git a/crates/pindakaas/Cargo.toml b/crates/pindakaas/Cargo.toml index cef666cd69..9d835c8d34 100644 --- a/crates/pindakaas/Cargo.toml +++ b/crates/pindakaas/Cargo.toml @@ -24,6 +24,7 @@ tracing = { version = "0.1", optional = true } # Optional Solver Interfaces pindakaas-cadical = { path = "../pindakaas-cadical", optional = true } pindakaas-intel-sat = { path = "../pindakaas-intel-sat", optional = true } +pindakaas-kissat = { path = "../pindakaas-kissat", optional = true } splr = { version = "0.17", optional = true } [dev-dependencies] @@ -31,7 +32,8 @@ splr = { version = "0.17", features = ["incremental_solver"] } traced_test = { path = "../traced_test" } [features] -trace = ["tracing"] cadical = ["pindakaas-cadical"] intel-sat = ["pindakaas-intel-sat"] -default = [] +kissat = ["pindakaas-kissat"] +trace = ["tracing"] +default = ["cadical", "intel-sat", "kissat"] diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index af9c9a104b..71e63b810c 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -8,23 +8,30 @@ pub mod libloading; pub mod cadical; #[cfg(feature = "intel-sat")] pub mod intel_sat; +#[cfg(feature = "kissat")] +pub mod kissat; #[cfg(feature = "splr")] pub mod splr; pub trait Solver: ClauseDatabase { - /// Return the name and the version of SAT solving library. + /// Return the name and the version of SAT solver. fn signature(&self) -> &str; /// Solve the formula with specified clauses. /// /// If the search is interrupted (see [`set_terminate_callback`]) the function /// returns unknown - fn solve)>( - &mut self, - on_sol: SolCb, - on_fail: FailCb, - ) -> SolveResult; + fn solve(&mut self, on_sol: SolCb) -> SolveResult; +} + +#[derive(PartialEq, Eq, Clone, Copy, Hash, Debug)] +pub enum SolveResult { + Sat, + Unsat, + Unknown, +} +pub trait SolveAssuming: Solver { /// Solve the formula with specified clauses under the given assumptions. /// /// If the search is interrupted (see [`set_terminate_callback`]) the function @@ -39,15 +46,16 @@ pub trait Solver: ClauseDatabase { on_sol: SolCb, on_fail: FailCb, ) -> SolveResult; +} - /// Set a callback function used to indicate a termination requirement to the - /// solver. - /// - /// The solver will periodically call this function and check its return value - /// during the search. Subsequent calls to this method override the previously - /// set callback function. - fn set_terminate_callback SolverAction>(&mut self, cb: Option); +/// Check if the given assumption literal was used to prove the unsatisfiability +/// of the formula under the assumptions used for the last SAT search. +/// +/// Note that for literals 'lit' which are not assumption literals, the behavior +/// of is not specified. +pub type FailFn<'a> = dyn Fn(Lit) -> bool + 'a; +pub trait LearnCallback: Solver { /// Set a callback function used to extract learned clauses up to a given /// length from the solver. /// @@ -61,30 +69,26 @@ pub trait Solver: ClauseDatabase { ); } -#[derive(PartialEq, Eq, Clone, Copy, Hash, Debug)] -pub enum SolveResult { - Sat, - Unsat, - Unknown, +pub trait TermCallback: Solver { + /// Set a callback function used to indicate a termination requirement to the + /// solver. + /// + /// The solver will periodically call this function and check its return value + /// during the search. Subsequent calls to this method override the previously + /// set callback function. + fn set_terminate_callback SolverAction>(&mut self, cb: Option); } -/// Check if the given assumption literal was used to prove the unsatisfiability -/// of the formula under the assumptions used for the last SAT search. -/// -/// Note that for literals 'lit' which are not assumption literals, the behavior -/// of is not specified. -pub type FailFn<'a> = dyn Fn(Lit) -> bool + 'a; +pub enum SolverAction { + Continue, + Terminate, +} #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct VarFactory { pub(crate) next_var: Option, } -pub enum SolverAction { - Continue, - Terminate, -} - impl VarFactory { const MAX_VARS: usize = NonZeroI32::MAX.get() as usize; @@ -129,7 +133,7 @@ macro_rules! ipasir_solver { fn default() -> Self { Self { ptr: unsafe { $loc::ipasir_init() }, - vars: crate::solver::VarFactory::default(), + vars: $crate::solver::VarFactory::default(), } } } @@ -140,15 +144,15 @@ macro_rules! ipasir_solver { } } - impl crate::ClauseDatabase for $name { - fn new_var(&mut self) -> crate::Lit { + impl $crate::ClauseDatabase for $name { + fn new_var(&mut self) -> $crate::Lit { self.vars.next().expect("variable pool exhaused").into() } - fn add_clause>( + fn add_clause>( &mut self, clause: I, - ) -> crate::Result { + ) -> $crate::Result { let mut added = false; for lit in clause.into_iter() { unsafe { $loc::ipasir_add(self.ptr, lit.into()) }; @@ -161,26 +165,22 @@ macro_rules! ipasir_solver { } } - impl crate::solver::Solver for $name { + impl $crate::solver::Solver for $name { fn signature(&self) -> &str { unsafe { std::ffi::CStr::from_ptr($loc::ipasir_signature()) } .to_str() .unwrap() } - fn solve< - SolCb: FnOnce(&dyn crate::Valuation), - FailCb: FnOnce(&crate::solver::FailFn<'_>), - >( + fn solve( &mut self, on_sol: SolCb, - on_fail: FailCb, - ) -> crate::solver::SolveResult { + ) -> $crate::solver::SolveResult { let res = unsafe { $loc::ipasir_solve(self.ptr) }; match res { 10 => { // 10 -> Sat - let val_fn = |lit: crate::Lit| { + let val_fn = |lit: $crate::Lit| { let var: i32 = lit.var().into(); // WARN: Always ask about variable (positive) literal, otherwise solvers sometimes seem incorrect let ret = unsafe { $loc::ipasir_val(self.ptr, var) }; @@ -194,95 +194,125 @@ macro_rules! ipasir_solver { } }; on_sol(&val_fn); - crate::solver::SolveResult::Sat - } - 20 => { - // 20 -> Unsat - let fail_fn = |lit: crate::Lit| { - let lit: i32 = lit.into(); - let failed = unsafe { $loc::ipasir_failed(self.ptr, lit) }; - failed != 0 - }; - on_fail(&fail_fn); - crate::solver::SolveResult::Unsat + $crate::solver::SolveResult::Sat } + 20 => $crate::solver::SolveResult::Unsat, // 20 -> Unsat _ => { debug_assert_eq!(res, 0); // According to spec should be 0, unknown - crate::solver::SolveResult::Unknown + $crate::solver::SolveResult::Unknown } } } + } + }; +} +#[allow(unused_imports)] +pub(crate) use ipasir_solver; +#[allow(unused_macros)] +macro_rules! ipasir_solve_assuming { + ($loc:ident, $name:ident) => { + impl $crate::solver::SolveAssuming for $name { fn solve_assuming< - I: IntoIterator, - SolCb: FnOnce(&dyn crate::Valuation), - FailCb: FnOnce(&crate::solver::FailFn<'_>), + I: IntoIterator, + SolCb: FnOnce(&dyn $crate::Valuation), + FailCb: FnOnce(&$crate::solver::FailFn<'_>), >( &mut self, assumptions: I, on_sol: SolCb, on_fail: FailCb, - ) -> crate::solver::SolveResult { + ) -> $crate::solver::SolveResult { + use $crate::solver::Solver; for i in assumptions { unsafe { $loc::ipasir_assume(self.ptr, i.into()) } } - self.solve(on_sol, on_fail) + match self.solve(on_sol) { + $crate::solver::SolveResult::Unsat => { + let fail_fn = |lit: $crate::Lit| { + let lit: i32 = lit.into(); + let failed = unsafe { $loc::ipasir_failed(self.ptr, lit) }; + failed != 0 + }; + on_fail(&fail_fn); + $crate::solver::SolveResult::Unsat + } + r => r, + } } + } + }; +} +#[allow(unused_imports)] +pub(crate) use ipasir_solve_assuming; - fn set_terminate_callback crate::solver::SolverAction>( +#[allow(unused_macros)] +macro_rules! ipasir_learn_callback { + ($loc:ident, $name:ident) => { + impl $crate::solver::LearnCallback for $name { + fn set_learn_callback)>( &mut self, + max_len: usize, cb: Option, ) { + let max_len = max_len as std::ffi::c_int; if let Some(mut cb) = cb { - let mut wrapped_cb = || -> std::ffi::c_int { - match cb() { - crate::solver::SolverAction::Continue => std::ffi::c_int::from(0), - crate::solver::SolverAction::Terminate => std::ffi::c_int::from(1), - } + let mut wrapped_cb = |clause: *const i32| { + let mut iter = $crate::solver::ExplIter(clause) + .map(|i: i32| $crate::Lit(std::num::NonZeroI32::new(i).unwrap())); + cb(&mut iter) }; let data = &mut wrapped_cb as *mut _ as *mut std::ffi::c_void; unsafe { - $loc::ipasir_set_terminate( + $loc::ipasir_set_learn( self.ptr, data, - Some(crate::solver::get_trampoline0(&wrapped_cb)), + max_len, + Some($crate::solver::get_trampoline1(&wrapped_cb)), ) } } else { - unsafe { $loc::ipasir_set_terminate(self.ptr, std::ptr::null_mut(), None) } + unsafe { $loc::ipasir_set_learn(self.ptr, std::ptr::null_mut(), max_len, None) } } } + } + }; +} +#[allow(unused_imports)] +pub(crate) use ipasir_learn_callback; - fn set_learn_callback)>( +#[allow(unused_macros)] +macro_rules! ipasir_term_callback { + ($loc:ident, $name:ident) => { + impl $crate::solver::TermCallback for $name { + fn set_terminate_callback $crate::solver::SolverAction>( &mut self, - max_len: usize, cb: Option, ) { - let max_len = max_len as std::ffi::c_int; if let Some(mut cb) = cb { - let mut wrapped_cb = |clause: *const i32| { - let mut iter = crate::solver::ExplIter(clause) - .map(|i: i32| crate::Lit(std::num::NonZeroI32::new(i).unwrap())); - cb(&mut iter) + let mut wrapped_cb = || -> std::ffi::c_int { + match cb() { + $crate::solver::SolverAction::Continue => std::ffi::c_int::from(0), + $crate::solver::SolverAction::Terminate => std::ffi::c_int::from(1), + } }; let data = &mut wrapped_cb as *mut _ as *mut std::ffi::c_void; unsafe { - $loc::ipasir_set_learn( + $loc::ipasir_set_terminate( self.ptr, data, - max_len, - Some(crate::solver::get_trampoline1(&wrapped_cb)), + Some($crate::solver::get_trampoline0(&wrapped_cb)), ) } } else { - unsafe { $loc::ipasir_set_learn(self.ptr, std::ptr::null_mut(), max_len, None) } + unsafe { $loc::ipasir_set_terminate(self.ptr, std::ptr::null_mut(), None) } } } } }; } #[allow(unused_imports)] -pub(crate) use ipasir_solver; +pub(crate) use ipasir_term_callback; type CB0 = unsafe extern "C" fn(*mut c_void) -> R; unsafe extern "C" fn trampoline0 R>(user_data: *mut c_void) -> R { diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index 6896f4eca2..4d5f1ee2d1 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -1,6 +1,9 @@ -use super::ipasir_solver; +use super::{ipasir_learn_callback, ipasir_solve_assuming, ipasir_solver, ipasir_term_callback}; ipasir_solver!(pindakaas_cadical, Cadical); +ipasir_solve_assuming!(pindakaas_cadical, Cadical); +ipasir_learn_callback!(pindakaas_cadical, Cadical); +ipasir_term_callback!(pindakaas_cadical, Cadical); #[cfg(test)] mod tests { @@ -30,15 +33,12 @@ mod tests { }, ) .unwrap(); - let res = slv.solve( - |value| { - assert!( - (value(!a).unwrap() && value(b).unwrap()) - || (value(a).unwrap() && value(!b).unwrap()), - ) - }, - |_| {}, - ); + let res = slv.solve(|value| { + assert!( + (value(!a).unwrap() && value(b).unwrap()) + || (value(a).unwrap() && value(!b).unwrap()), + ) + }); assert_eq!(res, SolveResult::Sat); } } diff --git a/crates/pindakaas/src/solver/intel_sat.rs b/crates/pindakaas/src/solver/intel_sat.rs index ac82812be4..1f49ba54be 100644 --- a/crates/pindakaas/src/solver/intel_sat.rs +++ b/crates/pindakaas/src/solver/intel_sat.rs @@ -1,6 +1,9 @@ -use super::ipasir_solver; +use super::{ipasir_learn_callback, ipasir_solve_assuming, ipasir_solver, ipasir_term_callback}; ipasir_solver!(pindakaas_intel_sat, IntelSat); +ipasir_solve_assuming!(pindakaas_intel_sat, IntelSat); +ipasir_learn_callback!(pindakaas_intel_sat, IntelSat); +ipasir_term_callback!(pindakaas_intel_sat, IntelSat); #[cfg(test)] mod tests { @@ -29,15 +32,12 @@ mod tests { }, ) .unwrap(); - let res = slv.solve( - |value| { - assert!( - (value(!a).unwrap() && value(b).unwrap()) - || (value(a).unwrap() && value(!b).unwrap()), - ) - }, - |_| {}, - ); + let res = slv.solve(|value| { + assert!( + (value(!a).unwrap() && value(b).unwrap()) + || (value(a).unwrap() && value(!b).unwrap()), + ) + }); assert_eq!(res, SolveResult::Sat); } } diff --git a/crates/pindakaas/src/solver/kissat.rs b/crates/pindakaas/src/solver/kissat.rs new file mode 100644 index 0000000000..cfd51a6607 --- /dev/null +++ b/crates/pindakaas/src/solver/kissat.rs @@ -0,0 +1,41 @@ +use super::ipasir_solver; + +ipasir_solver!(pindakaas_kissat, Kissat); + +#[cfg(test)] +mod tests { + #[cfg(feature = "trace")] + use traced_test::test; + + use super::*; + use crate::{ + linear::LimitComp, + solver::{SolveResult, Solver}, + CardinalityOne, ClauseDatabase, Encoder, PairwiseEncoder, + }; + + #[test] + fn test_kissat() { + let mut slv = Kissat::default(); + assert!(slv.signature().starts_with("kissat")); + + let a = slv.new_var(); + let b = slv.new_var(); + PairwiseEncoder::default() + .encode( + &mut slv, + &CardinalityOne { + lits: vec![a, b], + cmp: LimitComp::Equal, + }, + ) + .unwrap(); + let res = slv.solve(|value| { + assert!( + (value(!a).unwrap() && value(b).unwrap()) + || (value(a).unwrap() && value(!b).unwrap()), + ) + }); + assert_eq!(res, SolveResult::Sat); + } +} diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index 0f11fdbc0c..ba24ebbcee 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -7,8 +7,8 @@ use std::{ use libloading::{Library, Symbol}; use super::{ - get_trampoline0, get_trampoline1, ExplIter, FailFn, SolveResult, Solver, SolverAction, - VarFactory, + get_trampoline0, get_trampoline1, ExplIter, FailFn, LearnCallback, SolveAssuming, SolveResult, + Solver, SolverAction, TermCallback, VarFactory, }; use crate::{ClauseDatabase, Lit, Result, Valuation}; @@ -169,11 +169,7 @@ impl<'lib> Solver for IpasirSolver<'lib> { .unwrap() } - fn solve)>( - &mut self, - on_sol: SolCb, - on_fail: FailCb, - ) -> SolveResult { + fn solve(&mut self, on_sol: SolCb) -> SolveResult { let res = (self.solve_fn)(self.slv); match res { 10 => { @@ -193,23 +189,16 @@ impl<'lib> Solver for IpasirSolver<'lib> { on_sol(&val_fn); SolveResult::Sat } - 20 => { - // 20 -> Unsat - let fail_fn = |lit: Lit| { - let lit: i32 = lit.into(); - let failed = (self.failed_fn)(self.slv, lit); - failed != 0 - }; - on_fail(&fail_fn); - SolveResult::Unsat - } + 20 => SolveResult::Unsat, // 20 -> Unsat _ => { debug_assert_eq!(res, 0); // According to spec should be 0, unknown SolveResult::Unknown } } } +} +impl<'lib> SolveAssuming for IpasirSolver<'lib> { fn solve_assuming< I: IntoIterator, SolCb: FnOnce(&dyn Valuation), @@ -223,9 +212,22 @@ impl<'lib> Solver for IpasirSolver<'lib> { for i in assumptions { (self.assume_fn)(self.slv, i.into()); } - self.solve(on_sol, on_fail) + match self.solve(on_sol) { + SolveResult::Unsat => { + let fail_fn = |lit: Lit| { + let lit: i32 = lit.into(); + let failed = (self.failed_fn)(self.slv, lit); + failed != 0 + }; + on_fail(&fail_fn); + SolveResult::Unsat + } + r => r, + } } +} +impl<'lib> TermCallback for IpasirSolver<'lib> { fn set_terminate_callback SolverAction>(&mut self, cb: Option) { if let Some(mut cb) = cb { let mut wrapped_cb = || -> c_int { @@ -240,7 +242,9 @@ impl<'lib> Solver for IpasirSolver<'lib> { (self.set_terminate_fn)(self.slv, ptr::null_mut(), None); } } +} +impl<'lib> LearnCallback for IpasirSolver<'lib> { fn set_learn_callback)>( &mut self, max_len: usize, diff --git a/crates/pindakaas/src/solver/splr.rs b/crates/pindakaas/src/solver/splr.rs index ff96ddf150..fbe584a164 100644 --- a/crates/pindakaas/src/solver/splr.rs +++ b/crates/pindakaas/src/solver/splr.rs @@ -68,48 +68,6 @@ impl Solver for SplrSolver { }, } } - - fn solve_assuming< - I: IntoIterator, - SolCb: FnOnce(&dyn crate::Valuation), - FailCb: FnOnce(&super::FailFn<'_>), - >( - &mut self, - assumptions: I, - on_sol: SolCb, - on_fail: FailCb, - ) -> SolveResult { - let mut copy = self.clone(); - for l in assumptions { - match copy.add_assignment(l.into()) { - Ok(_) => {} - Err(e) => match e { - InvalidLiteral => panic!("clause referenced a non-existing variable"), - Inconsistent => { - let fail = |x| l == x; - on_fail(&fail); - return SolveResult::Unsat; - } - _ => unreachable!(), - }, - } - } - Solver::solve(&mut copy, on_sol, on_fail) - } - - fn set_terminate_callback SolverAction>(&mut self, _cb: Option) { - unimplemented!("SPLR does not support setting a callback that is checked to determine whether to terminate termination") - } - - fn set_learn_callback)>( - &mut self, - _max_len: usize, - _cb: Option, - ) { - unimplemented!( - "SPLR does not support setting a callback that is called when learning a new clause" - ) - } } impl From for SplrSolver {