From b747605c86934b6cc519b03a5902acce07018d3b Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 29 Oct 2024 12:37:12 +1100 Subject: [PATCH 1/2] Update to pindakaas with generic propagator interface --- Cargo.lock | 121 +++--- crates/fzn-huub/src/lib.rs | 12 +- crates/huub/Cargo.toml | 2 +- crates/huub/src/model.rs | 37 +- crates/huub/src/model/bool.rs | 43 +-- crates/huub/src/model/branching.rs | 17 +- crates/huub/src/model/constraint.rs | 17 +- crates/huub/src/model/flatzinc.rs | 13 +- crates/huub/src/model/int.rs | 17 +- crates/huub/src/model/reformulate.rs | 39 +- .../huub/src/propagator/all_different_int.rs | 20 +- .../src/propagator/array_var_int_element.rs | 6 +- .../huub/src/propagator/disjunctive_strict.rs | 4 +- crates/huub/src/propagator/int_abs.rs | 4 +- crates/huub/src/propagator/int_div.rs | 4 +- crates/huub/src/propagator/int_lin_le.rs | 6 +- crates/huub/src/propagator/int_lin_ne.rs | 4 +- crates/huub/src/propagator/int_pow.rs | 4 +- crates/huub/src/propagator/int_times.rs | 4 +- crates/huub/src/solver.rs | 349 ++++++++---------- crates/huub/src/solver/engine.rs | 14 +- crates/huub/src/solver/engine/bool_to_int.rs | 2 +- crates/huub/src/solver/engine/int_var.rs | 48 +-- .../huub/src/solver/engine/solving_context.rs | 3 +- crates/huub/src/solver/engine/trail.rs | 4 +- .../huub/src/solver/initialization_context.rs | 43 +-- crates/huub/src/solver/value.rs | 4 +- crates/huub/src/solver/view.rs | 20 +- crates/huub/src/tests.rs | 2 +- 29 files changed, 354 insertions(+), 509 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 28895b15..cb68319d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -9,7 +9,6 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011" dependencies = [ "cfg-if", - "getrandom", "once_cell", "version_check", "zerocopy", @@ -32,9 +31,9 @@ checksum = "4b46cbb362ab8752921c97e041f5e366ee6297bd428a31275b9fcf1e380f7299" [[package]] name = "anstyle" -version = "1.0.8" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1bec1de6f59aedf83baf9ff929c98f2ad654b97c9510f4e70cf6f661d49fd5b1" +checksum = "8365de52b16c035ff4fcafe0092ba9390540e3e352870ac09933bebcaa2c8c56" [[package]] name = "autocfg" @@ -77,9 +76,9 @@ dependencies = [ [[package]] name = "cc" -version = "1.1.28" +version = "1.1.31" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2e80e3b6a3ab07840e1cae9b0666a63970dc28e8ed5ffbcdacbfc760c281bfc1" +checksum = "c2e7962b54006dcfcc61cb72735f4d89bb97061dd6a7ed882ec6b8ee53714c6f" dependencies = [ "jobserver", "libc", @@ -360,17 +359,6 @@ dependencies = [ "ustr", ] -[[package]] -name = "getrandom" -version = "0.2.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7" -dependencies = [ - "cfg-if", - "libc", - "wasi", -] - [[package]] name = "half" version = "2.4.1" @@ -473,9 +461,9 @@ dependencies = [ [[package]] name = "js-sys" -version = "0.3.71" +version = "0.3.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0cb94a0ffd3f3ee755c20f7d8752f45cac88605a4dcf808abcff72873296ec7b" +checksum = "6a88f1bda2bd75b0452a14784937d796722fdebfe50df998aeb3f0b7603019a9" dependencies = [ "wasm-bindgen", ] @@ -488,19 +476,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "libc" -version = "0.2.159" +version = "0.2.161" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "561d97a539a36e26a9a5fad1ea11a3039a67714694aaa379433e580854bc3dc5" - -[[package]] -name = "libloading" -version = "0.8.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4979f22fdb869068da03c9f7528f8297c6fd2606bc3a4affe42e6a823fdb8da4" -dependencies = [ - "cfg-if", - "windows-targets 0.52.6", -] +checksum = "8e9489c2807c139ffd9c1794f4af0ebe86a828db53ecdc7fea2111d0fed085d1" [[package]] name = "lock_api" @@ -683,18 +661,17 @@ checksum = "5be167a7af36ee22fe3115051bc51f6e6c7054c9348e28deb4f49bd6f705a315" [[package]] name = "pin-project-lite" -version = "0.2.14" +version = "0.2.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02" +checksum = "915a1e146535de9163f3987b8944ed8cf49a18bb0056bcebcdcece385cece4ff" [[package]] name = "pindakaas" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#90631db0d4ccaaf59d354b325e56a663bb9ee956" +source = "git+https://github.com/pindakaashq/pindakaas.git#424559578c95d714f9fd44b6f81c4eaa437cd83c" dependencies = [ "iset", "itertools 0.13.0", - "libloading", "pindakaas-cadical", "pindakaas-derive", "rustc-hash", @@ -703,7 +680,7 @@ dependencies = [ [[package]] name = "pindakaas-build-macros" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#90631db0d4ccaaf59d354b325e56a663bb9ee956" +source = "git+https://github.com/pindakaashq/pindakaas.git#424559578c95d714f9fd44b6f81c4eaa437cd83c" dependencies = [ "cc", "paste", @@ -712,7 +689,7 @@ dependencies = [ [[package]] name = "pindakaas-cadical" version = "2.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#90631db0d4ccaaf59d354b325e56a663bb9ee956" +source = "git+https://github.com/pindakaashq/pindakaas.git#424559578c95d714f9fd44b6f81c4eaa437cd83c" dependencies = [ "cc", "pindakaas-build-macros", @@ -721,7 +698,7 @@ dependencies = [ [[package]] name = "pindakaas-derive" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#90631db0d4ccaaf59d354b325e56a663bb9ee956" +source = "git+https://github.com/pindakaashq/pindakaas.git#424559578c95d714f9fd44b6f81c4eaa437cd83c" dependencies = [ "darling", "quote", @@ -758,9 +735,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.87" +version = "1.0.89" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b3e4daa0dcf6feba26f985457cdf104d4b4256fc5a09547140f3631bb076b19a" +checksum = "f139b0662de085916d1fb67d2b4169d1addddda1919e696f3252b740b629986e" dependencies = [ "unicode-ident", ] @@ -815,9 +792,9 @@ dependencies = [ [[package]] name = "regex" -version = "1.11.0" +version = "1.11.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "38200e5ee88914975b69f657f0801b6f6dccafd44fd9326302a4aaeecfacb1d8" +checksum = "b544ef1b4eac5dc2db33ea63606ae9ffcfac26c1416a2806ae0bf5f56b201191" dependencies = [ "aho-corasick", "memchr", @@ -865,9 +842,9 @@ checksum = "583034fd73374156e66797ed8e5b0d5690409c9226b22d87cb7f19821c05d152" [[package]] name = "rustversion" -version = "1.0.17" +version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "955d28af4278de8121b7ebeb796b6a45735dc01436d898801014aced2773a3d6" +checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248" [[package]] name = "ryu" @@ -892,18 +869,18 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "serde" -version = "1.0.210" +version = "1.0.214" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c8e3592472072e6e22e0a54d5904d9febf8508f65fb8552499a1abc7d1078c3a" +checksum = "f55c3193aca71c12ad7890f1785d2b73e1b9f63a0bbc353c08ef26fe03fc56b5" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.210" +version = "1.0.214" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" +checksum = "de523f781f095e28fa605cdce0f8307e451cc0fd14e2eb4cd2e98a355b147766" dependencies = [ "proc-macro2", "quote", @@ -912,9 +889,9 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.128" +version = "1.0.132" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8" +checksum = "d726bfaff4b320266d395898905d0eba0345aae23b54aee3a737e260fd46db03" dependencies = [ "itoa", "memchr", @@ -951,9 +928,9 @@ checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" [[package]] name = "syn" -version = "2.0.79" +version = "2.0.85" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" +checksum = "5023162dfcd14ef8f32034d8bcd4cc5ddc61ef7a247c024a33e24e1f24d21b56" dependencies = [ "proc-macro2", "quote", @@ -962,18 +939,18 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.64" +version = "1.0.65" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d50af8abc119fb8bb6dbabcfa89656f46f84aa0ac7688088608076ad2b459a84" +checksum = "5d11abd9594d9b38965ef50805c5e469ca9cc6f197f883f717e0269a3057b3d5" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.64" +version = "1.0.65" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3" +checksum = "ae71770322cbd277e69d762a16c444af02aa0575ac0d174f0b9562d3b37f8602" dependencies = [ "proc-macro2", "quote", @@ -1090,9 +1067,9 @@ checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" [[package]] name = "ustr" -version = "1.0.0" +version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7e904a2279a4a36d2356425bb20be271029cc650c335bc82af8bfae30085a3d0" +checksum = "18b19e258aa08450f93369cf56dd78063586adf19e92a75b338a800f799a0208" dependencies = [ "ahash", "byteorder", @@ -1123,17 +1100,11 @@ dependencies = [ "winapi-util", ] -[[package]] -name = "wasi" -version = "0.11.0+wasi-snapshot-preview1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" - [[package]] name = "wasm-bindgen" -version = "0.2.94" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ef073ced962d62984fb38a36e5fdc1a2b23c9e0e1fa0689bb97afa4202ef6887" +checksum = "128d1e363af62632b8eb57219c8fd7877144af57558fb2ef0368d0087bddeb2e" dependencies = [ "cfg-if", "once_cell", @@ -1142,9 +1113,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-backend" -version = "0.2.94" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c4bfab14ef75323f4eb75fa52ee0a3fb59611977fd3240da19b2cf36ff85030e" +checksum = "cb6dd4d3ca0ddffd1dd1c9c04f94b868c37ff5fac97c30b97cff2d74fce3a358" dependencies = [ "bumpalo", "log", @@ -1157,9 +1128,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro" -version = "0.2.94" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a7bec9830f60924d9ceb3ef99d55c155be8afa76954edffbb5936ff4509474e7" +checksum = "e79384be7f8f5a9dd5d7167216f022090cf1f9ec128e6e6a482a2cb5c5422c56" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -1167,9 +1138,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.94" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c74f6e152a76a2ad448e223b0fc0b6b5747649c3d769cc6bf45737bf97d0ed6" +checksum = "26c6ab57572f7a24a4985830b120de1594465e5d500f24afe89e16b4e833ef68" dependencies = [ "proc-macro2", "quote", @@ -1180,15 +1151,15 @@ dependencies = [ [[package]] name = "wasm-bindgen-shared" -version = "0.2.94" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a42f6c679374623f295a8623adfe63d9284091245c3504bde47c17a3ce2777d9" +checksum = "65fc09f10666a9f147042251e0dda9c18f166ff7de300607007e96bdebc1068d" [[package]] name = "web-sys" -version = "0.3.71" +version = "0.3.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44188d185b5bdcae1052d08bcbcf9091a5524038d4572cc4f4f2bb9d5554ddd9" +checksum = "f6488b90108c040df0fe62fa815cbdee25124641df01814dd7282749234c6112" dependencies = [ "js-sys", "wasm-bindgen", diff --git a/crates/fzn-huub/src/lib.rs b/crates/fzn-huub/src/lib.rs index 46b475f8..8abda39f 100644 --- a/crates/fzn-huub/src/lib.rs +++ b/crates/fzn-huub/src/lib.rs @@ -17,7 +17,7 @@ use std::{ use flatzinc_serde::{FlatZinc, Literal, Method}; use huub::{ FlatZincError, FlatZincStatistics, Goal, InitConfig, LitMeaning, ReformulationError, - SlvTermSignal, SolveResult, Solver, SolverView, Valuation, + SlvTermSignal, SolveResult, Solver, SolverView, Valuation, Value, }; use pico_args::Arguments; use tracing::{subscriber::set_default, warn}; @@ -342,7 +342,7 @@ where warn!("--all-solutions is ignored when optimizing, use --intermediate-solutions or --all-optimal instead"); } let mut no_good_vals = vec![ - None; + Value::Bool(false); if self.all_optimal { output_vars.len() } else { @@ -608,7 +608,7 @@ impl Solution<'_> { Literal::Int(i) => format!("{i}"), Literal::Float(f) => format!("{f}"), Literal::Identifier(ident) => { - format!("{}", (self.value)(self.var_map[ident]).unwrap()) + format!("{}", (self.value)(self.var_map[ident])) } Literal::Bool(b) => format!("{b}"), Literal::IntSet(is) => is @@ -640,11 +640,7 @@ impl Display for Solution<'_> { .join(",") )?; } else { - writeln!( - f, - "{ident} = {};", - (self.value)(self.var_map[ident]).unwrap() - )?; + writeln!(f, "{ident} = {};", (self.value)(self.var_map[ident]))?; } } writeln!(f, "{}", FZN_SEPERATOR) diff --git a/crates/huub/Cargo.toml b/crates/huub/Cargo.toml index 78c4df2b..66c75a04 100644 --- a/crates/huub/Cargo.toml +++ b/crates/huub/Cargo.toml @@ -16,7 +16,7 @@ flatzinc-serde = { workspace = true } index_vec = "0.1.3" itertools = "0.13.0" pindakaas = { git = "https://github.com/pindakaashq/pindakaas.git", features = [ - "ipasir-up", + "external-propagation", ] } rangelist = "0.2" thiserror = "1.0.63" diff --git a/crates/huub/src/model.rs b/crates/huub/src/model.rs index 4243c4b9..20049c16 100644 --- a/crates/huub/src/model.rs +++ b/crates/huub/src/model.rs @@ -13,9 +13,8 @@ use std::{ }; use pindakaas::{ - solver::{cadical::Cadical, NextVarRange, PropagatorAccess, Solver as SolverTrait}, - ClauseDatabase, Cnf, ConditionalDatabase, Lit as RawLit, Valuation as SatValuation, - Var as RawVar, + solver::{cadical::Cadical, propagation::PropagatingSolver}, + ClauseDatabase, Cnf, ConditionalDatabase, Lit as RawLit, Unsatisfiable, }; use rangelist::{IntervalIterator, RangeList}; use tracing::warn; @@ -27,9 +26,9 @@ use crate::{ int::{IntVar, IntVarDef, IntView}, reformulate::{InitConfig, ReformulationError, VariableMap}, }, - solver::{ - engine::int_var::{EncodingType, IntVar as SlvIntVar}, - SatSolver, + solver::engine::{ + int_var::{EncodingType, IntVar as SlvIntVar}, + Engine, }, Constraint, Solver, }; @@ -46,13 +45,12 @@ pub struct Model { impl Model { pub fn new_bool_var(&mut self) -> BoolView { - BoolView::Lit(self.cnf.new_var().into()) + BoolView::Lit(self.cnf.new_lit()) } pub fn new_bool_vars(&mut self, len: usize) -> Vec { self.cnf - .next_var_range(len) - .unwrap() + .new_var_range(len) .map(|v| BoolView::Lit(v.into())) .collect() } @@ -70,18 +68,19 @@ impl Model { (0..len).map(|i| IntVar(iv.0 + i as u32)).collect() } - pub fn to_solver< - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait + 'static, - >( + pub fn to_solver>( &mut self, config: &InitConfig, - ) -> Result<(Solver, VariableMap), ReformulationError> { + ) -> Result<(Solver, VariableMap), ReformulationError> + where + Solver: for<'a> From<&'a Cnf>, + Oracle::Slv: 'static, + { let mut map = VariableMap::default(); // TODO: run SAT simplification - let mut slv = Solver::::from(&self.cnf); - let any_slv: &mut dyn Any = &mut slv.oracle; + let mut slv = Solver::::from(&self.cnf); + let any_slv: &mut dyn Any = slv.oracle.solver_mut(); if let Some(r) = any_slv.downcast_mut::() { r.set_option("restart", config.restart() as i32); r.set_option("vivify", config.vivification() as i32); @@ -180,11 +179,11 @@ impl AddAssign for Model { } impl ClauseDatabase for Model { - fn new_var(&mut self) -> RawVar { - self.cnf.new_var() + fn new_var_range(&mut self, len: usize) -> pindakaas::VarRange { + self.cnf.new_var_range(len) } - fn add_clause>(&mut self, cl: I) -> pindakaas::Result { + fn add_clause>(&mut self, cl: I) -> Result<(), Unsatisfiable> { self.cnf.add_clause(cl) } diff --git a/crates/huub/src/model/bool.rs b/crates/huub/src/model/bool.rs index ed6e2b3c..365560d8 100644 --- a/crates/huub/src/model/bool.rs +++ b/crates/huub/src/model/bool.rs @@ -1,8 +1,9 @@ use std::{iter::once, ops::Not}; use pindakaas::{ - solver::{PropagatorAccess, Solver as SolverTrait}, - Formula, Lit as RawLit, TseitinEncoder, Valuation as SatValuation, + propositional_logic::{Formula, TseitinEncoder}, + solver::propagation::PropagatingSolver, + Lit as RawLit, }; use crate::{ @@ -11,8 +12,8 @@ use crate::{ reformulate::{ReformulationError, VariableMap}, }, solver::{ + engine::Engine, view::{self, BoolViewInner}, - SatSolver, }, IntVal, Solver, }; @@ -34,15 +35,11 @@ pub enum BoolExpr { } impl BoolExpr { - pub(crate) fn constrain( + pub(crate) fn constrain>( &self, - slv: &mut Solver, + slv: &mut Solver, map: &mut VariableMap, - ) -> Result<(), ReformulationError> - where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, - { + ) -> Result<(), ReformulationError> { match self { BoolExpr::View(bv) => { let v = map.get_bool(slv, bv); @@ -163,17 +160,13 @@ impl BoolExpr { } } - pub(crate) fn to_arg( + pub(crate) fn to_arg>( &self, - slv: &mut Solver, + slv: &mut Solver, map: &mut VariableMap, name: Option, - ) -> Result - where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, - { - let bind_lit = |oracle: &mut Sat, lit| { + ) -> Result { + let bind_lit = |oracle: &mut Oracle, lit| { Ok(view::BoolView(BoolViewInner::Lit( if let Some(name) = name { oracle @@ -188,7 +181,7 @@ impl BoolExpr { }, ))) }; - let bind_const = |oracle: &mut Sat, val| { + let bind_const = |oracle: &mut Oracle, val| { if let Some(name) = name { oracle .add_clause([if val { name } else { !name }]) @@ -196,7 +189,7 @@ impl BoolExpr { } Ok(view::BoolView(BoolViewInner::Const(val))) }; - let bind_view = |oracle: &mut Sat, view: view::BoolView| match view.0 { + let bind_view = |oracle: &mut Oracle, view: view::BoolView| match view.0 { BoolViewInner::Lit(l) => bind_lit(oracle, l), BoolViewInner::Const(c) => bind_const(oracle, c), }; @@ -222,7 +215,7 @@ impl BoolExpr { BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), } } - let r = name.unwrap_or_else(|| slv.oracle.new_var().into()); + let r = name.unwrap_or_else(|| slv.oracle.new_lit()); slv.oracle .encode( &Formula::Equiv(vec![Formula::Atom(r), Formula::Or(lits)]), @@ -240,7 +233,7 @@ impl BoolExpr { BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), } } - let name = name.unwrap_or_else(|| slv.oracle.new_var().into()); + let name = name.unwrap_or_else(|| slv.oracle.new_lit()); slv.oracle .encode( &Formula::Equiv(vec![Formula::Atom(name), Formula::And(lits)]), @@ -261,7 +254,7 @@ impl BoolExpr { BoolViewInner::Const(true) => bind_const(&mut slv.oracle, true), BoolViewInner::Const(false) => bind_lit(&mut slv.oracle, !a), BoolViewInner::Lit(b) => { - let name = name.unwrap_or_else(|| slv.oracle.new_var().into()); + let name = name.unwrap_or_else(|| slv.oracle.new_lit()); slv.oracle .encode( &Formula::Equiv(vec![ @@ -293,7 +286,7 @@ impl BoolExpr { BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), } } - let name = name.unwrap_or_else(|| slv.oracle.new_var().into()); + let name = name.unwrap_or_else(|| slv.oracle.new_lit()); let f = match res { Some(b) => { Formula::And(lits.into_iter().map(|e| if b { e } else { !e }).collect()) @@ -318,7 +311,7 @@ impl BoolExpr { BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), } } - let name = name.unwrap_or_else(|| slv.oracle.new_var().into()); + let name = name.unwrap_or_else(|| slv.oracle.new_lit()); let mut formula = Formula::Xor(lits); if count % 2 == 1 { formula = !formula; diff --git a/crates/huub/src/model/branching.rs b/crates/huub/src/model/branching.rs index ab8e1477..9b2bb91a 100644 --- a/crates/huub/src/model/branching.rs +++ b/crates/huub/src/model/branching.rs @@ -1,12 +1,9 @@ -use pindakaas::{ - solver::{PropagatorAccess, Solver as SolverTrait}, - Valuation as SatValuation, -}; +use pindakaas::solver::propagation::PropagatingSolver; use crate::{ brancher::{BoolBrancher, IntBrancher, WarmStartBrancher}, model::{bool::BoolView, int::IntView, reformulate::VariableMap}, - solver::SatSolver, + solver::engine::Engine, Solver, }; @@ -36,11 +33,11 @@ pub enum Branching { } impl Branching { - pub(crate) fn to_solver(&self, slv: &mut Solver, map: &mut VariableMap) - where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, - { + pub(crate) fn to_solver>( + &self, + slv: &mut Solver, + map: &mut VariableMap, + ) { match self { Branching::Bool(vars, var_sel, val_sel) => { let vars = vars.iter().map(|v| map.get_bool(slv, v)).collect(); diff --git a/crates/huub/src/model/constraint.rs b/crates/huub/src/model/constraint.rs index 98ef9cbd..5e860154 100644 --- a/crates/huub/src/model/constraint.rs +++ b/crates/huub/src/model/constraint.rs @@ -1,10 +1,7 @@ use std::iter::once; use itertools::Itertools; -use pindakaas::{ - solver::{PropagatorAccess, Solver as SolverTrait}, - Valuation as SatValuation, -}; +use pindakaas::solver::propagation::PropagatingSolver; use rangelist::RangeList; use crate::{ @@ -24,8 +21,8 @@ use crate::{ int_times::IntTimesBounds, }, solver::{ + engine::Engine, view::{BoolViewInner, IntViewInner}, - SatSolver, }, BoolExpr, IntSetVal, IntVal, LitMeaning, Model, NonZeroIntVal, ReformulationError, Solver, }; @@ -57,15 +54,11 @@ pub enum Constraint { } impl Constraint { - pub(crate) fn to_solver( + pub(crate) fn to_solver>( &self, - slv: &mut Solver, + slv: &mut Solver, map: &mut VariableMap, - ) -> Result<(), ReformulationError> - where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, - { + ) -> Result<(), ReformulationError> { match self { Constraint::AllDifferentInt(v) => { let vars: Vec<_> = v.iter().map(|v| v.to_arg(slv, map)).collect(); diff --git a/crates/huub/src/model/flatzinc.rs b/crates/huub/src/model/flatzinc.rs index d50df95b..3ae78971 100644 --- a/crates/huub/src/model/flatzinc.rs +++ b/crates/huub/src/model/flatzinc.rs @@ -12,10 +12,7 @@ use flatzinc_serde::{ Literal, Type, }; use itertools::Itertools; -use pindakaas::{ - solver::{PropagatorAccess, Solver as SolverTrait}, - Valuation as SatValuation, -}; +use pindakaas::{solver::propagation::PropagatingSolver, Cnf}; use rangelist::{IntervalIterator, RangeList}; use thiserror::Error; use tracing::warn; @@ -28,7 +25,7 @@ use crate::{ reformulate::ReformulationError, ModelView, }, - solver::SatSolver, + solver::engine::Engine, BoolExpr, Constraint, InitConfig, IntSetVal, IntVal, Model, NonZeroIntVal, Solver, SolverView, }; @@ -1511,10 +1508,10 @@ impl Model { } } -impl Solver +impl> Solver where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait + 'static, + Solver: for<'a> From<&'a Cnf>, + Oracle::Slv: 'static, { pub fn from_fzn( fzn: &FlatZinc, diff --git a/crates/huub/src/model/int.rs b/crates/huub/src/model/int.rs index 11838a7d..16893299 100644 --- a/crates/huub/src/model/int.rs +++ b/crates/huub/src/model/int.rs @@ -1,28 +1,21 @@ use std::ops::{Add, Mul, Neg}; -use pindakaas::{ - solver::{PropagatorAccess, Solver as SolverTrait}, - ClauseDatabase, Valuation as SatValuation, -}; +use pindakaas::{solver::propagation::PropagatingSolver, ClauseDatabase}; use rangelist::{IntervalIterator, RangeList}; use crate::{ helpers::linear_transform::LinearTransform, model::{bool::BoolView, reformulate::VariableMap}, - solver::{view, SatSolver}, + solver::{engine::Engine, view}, IntVal, LitMeaning, Model, NonZeroIntVal, ReformulationError, Solver, }; impl IntView { - pub(crate) fn to_arg( + pub(crate) fn to_arg>( &self, - slv: &mut Solver, + slv: &mut Solver, map: &mut VariableMap, - ) -> view::IntView - where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, - { + ) -> view::IntView { map.get_int(slv, self) } } diff --git a/crates/huub/src/model/reformulate.rs b/crates/huub/src/model/reformulate.rs index db5cf7a1..fe22dc97 100644 --- a/crates/huub/src/model/reformulate.rs +++ b/crates/huub/src/model/reformulate.rs @@ -1,9 +1,6 @@ use std::collections::HashMap; -use pindakaas::{ - solver::{PropagatorAccess, Solver as SolverTrait}, - Valuation as SatValuation, Var as RawVar, -}; +use pindakaas::{solver::propagation::PropagatingSolver, Var as RawVar}; use thiserror::Error; use crate::{ @@ -13,8 +10,8 @@ use crate::{ ModelView, }, solver::{ + engine::Engine, view::{BoolView, BoolViewInner, IntViewInner, SolverView}, - SatSolver, }, IntVal, IntView, LitMeaning, Solver, }; @@ -103,23 +100,23 @@ impl From for Variable { } impl VariableMap { - pub fn get(&self, slv: &mut Solver, index: &ModelView) -> SolverView - where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, - { + pub fn get>( + &self, + slv: &mut Solver, + index: &ModelView, + ) -> SolverView { match index { ModelView::Bool(b) => SolverView::Bool(self.get_bool(slv, b)), ModelView::Int(i) => SolverView::Int(self.get_int(slv, i)), } } - pub fn get_bool(&self, slv: &mut Solver, bv: &bool::BoolView) -> BoolView - where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, - { - let get_int_lit = |slv: &mut Solver, iv: &int::IntView, lit_meaning: LitMeaning| { + pub fn get_bool>( + &self, + slv: &mut Solver, + bv: &bool::BoolView, + ) -> BoolView { + let get_int_lit = |slv: &mut Solver, iv: &int::IntView, lit_meaning: LitMeaning| { let iv = self.get_int(slv, iv); slv.get_int_lit(iv, lit_meaning) }; @@ -152,11 +149,11 @@ impl VariableMap { } } - pub fn get_int(&self, slv: &mut Solver, iv: &int::IntView) -> IntView - where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, - { + pub fn get_int>( + &self, + slv: &mut Solver, + iv: &int::IntView, + ) -> IntView { let get_int_var = |v: &IntVar| { let SolverView::Int(i) = self.map.get(&Variable::Int(*v)).cloned().unwrap() else { unreachable!() diff --git a/crates/huub/src/propagator/all_different_int.rs b/crates/huub/src/propagator/all_different_int.rs index 9524e55f..7f9c29ac 100644 --- a/crates/huub/src/propagator/all_different_int.rs +++ b/crates/huub/src/propagator/all_different_int.rs @@ -84,7 +84,7 @@ impl Poster for AllDifferentIntValuePoster { #[cfg(test)] mod tests { use itertools::Itertools; - use pindakaas::{solver::cadical::Cadical, Cnf}; + use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; use rangelist::RangeList; use tracing_test::traced_test; @@ -97,7 +97,7 @@ mod tests { #[test] #[traced_test] fn test_all_different_value_sat() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, RangeList::from_iter([1..=4]), @@ -125,7 +125,7 @@ mod tests { #[test] #[traced_test] fn test_all_different_value_unsat() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, RangeList::from_iter([1..=2]), @@ -151,7 +151,7 @@ mod tests { } fn test_sudoku(grid: &[&str], expected: SolveResult) { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let mut all_vars = vec![]; // create variables and add all different propagator for each row grid.iter().for_each(|row| { @@ -195,10 +195,7 @@ mod tests { assert_eq!( slv.solve(|val| { (0..9).for_each(|r| { - let row = all_vars[r] - .iter() - .map(|v| val(v.into()).unwrap()) - .collect_vec(); + let row = all_vars[r].iter().map(|v| val(v.into())).collect_vec(); assert!( row.iter().all_unique(), "Values in row {} are not all different: {:?}", @@ -207,10 +204,7 @@ mod tests { ); }); (0..9).for_each(|c| { - let col = all_vars - .iter() - .map(|row| val(row[c].into()).unwrap()) - .collect_vec(); + let col = all_vars.iter().map(|row| val(row[c].into())).collect_vec(); assert!( col.iter().all_unique(), "Values in column {} are not all different: {:?}", @@ -222,7 +216,7 @@ mod tests { (0..3).for_each(|j| { let block = (0..3) .flat_map(|x| (0..3).map(move |y| (x, y))) - .map(|(x, y)| val(all_vars[3 * i + x][3 * j + y].into()).unwrap()) + .map(|(x, y)| val(all_vars[3 * i + x][3 * j + y].into())) .collect_vec(); assert!( block.iter().all_unique(), diff --git a/crates/huub/src/propagator/array_var_int_element.rs b/crates/huub/src/propagator/array_var_int_element.rs index e9afb952..00069996 100644 --- a/crates/huub/src/propagator/array_var_int_element.rs +++ b/crates/huub/src/propagator/array_var_int_element.rs @@ -239,7 +239,7 @@ impl Poster for ArrayVarIntElementBoundsPoster { #[cfg(test)] mod tests { use expect_test::expect; - use pindakaas::{solver::cadical::Cadical, Cnf}; + use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; use rangelist::RangeList; use tracing_test::traced_test; @@ -252,7 +252,7 @@ mod tests { #[test] #[traced_test] fn test_element_bounds_sat() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, RangeList::from_iter([3..=4]), @@ -325,7 +325,7 @@ mod tests { #[test] #[traced_test] fn test_element_holes() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, RangeList::from_iter([1..=3]), diff --git a/crates/huub/src/propagator/disjunctive_strict.rs b/crates/huub/src/propagator/disjunctive_strict.rs index 7960eda1..9607f295 100644 --- a/crates/huub/src/propagator/disjunctive_strict.rs +++ b/crates/huub/src/propagator/disjunctive_strict.rs @@ -570,7 +570,7 @@ impl Poster for DisjunctiveEdgeFindingPoster { mod tests { use expect_test::expect; use flatzinc_serde::RangeList; - use pindakaas::{solver::cadical::Cadical, Cnf}; + use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; use tracing_test::traced_test; use crate::{ @@ -582,7 +582,7 @@ mod tests { #[test] #[traced_test] fn test_disjunctive_sat() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, RangeList::from_iter([0..=4]), diff --git a/crates/huub/src/propagator/int_abs.rs b/crates/huub/src/propagator/int_abs.rs index 538ce3cc..b2071348 100644 --- a/crates/huub/src/propagator/int_abs.rs +++ b/crates/huub/src/propagator/int_abs.rs @@ -110,7 +110,7 @@ impl Poster for IntAbsBoundsPoster { #[cfg(test)] mod tests { use expect_test::expect; - use pindakaas::{solver::cadical::Cadical, Cnf}; + use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; use rangelist::RangeList; use tracing_test::traced_test; @@ -123,7 +123,7 @@ mod tests { #[test] #[traced_test] fn test_int_abs_sat() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, (-3..=3).into(), diff --git a/crates/huub/src/propagator/int_div.rs b/crates/huub/src/propagator/int_div.rs index ebe17448..95a5ec10 100644 --- a/crates/huub/src/propagator/int_div.rs +++ b/crates/huub/src/propagator/int_div.rs @@ -252,7 +252,7 @@ impl Poster for IntDivBoundsPoster { #[cfg(test)] mod tests { use expect_test::expect; - use pindakaas::{solver::cadical::Cadical, Cnf}; + use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; use rangelist::RangeList; use tracing_test::traced_test; @@ -265,7 +265,7 @@ mod tests { #[test] #[traced_test] fn test_int_div_sat() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, (-7..=7).into(), diff --git a/crates/huub/src/propagator/int_lin_le.rs b/crates/huub/src/propagator/int_lin_le.rs index 75278ba9..44399733 100644 --- a/crates/huub/src/propagator/int_lin_le.rs +++ b/crates/huub/src/propagator/int_lin_le.rs @@ -184,7 +184,7 @@ impl Poster for IntLinearLessEqBoundsPoster { #[cfg(test)] mod tests { use expect_test::expect; - use pindakaas::{solver::cadical::Cadical, Cnf}; + use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; use rangelist::RangeList; use tracing_test::traced_test; @@ -197,7 +197,7 @@ mod tests { #[test] #[traced_test] fn test_linear_le_sat() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, RangeList::from_iter([1..=2]), @@ -249,7 +249,7 @@ mod tests { #[test] #[traced_test] fn test_linear_ge_sat() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, RangeList::from_iter([1..=2]), diff --git a/crates/huub/src/propagator/int_lin_ne.rs b/crates/huub/src/propagator/int_lin_ne.rs index 1b4b3675..b2b3761f 100644 --- a/crates/huub/src/propagator/int_lin_ne.rs +++ b/crates/huub/src/propagator/int_lin_ne.rs @@ -182,7 +182,7 @@ impl Poster for IntLinearNotEqValuePoster { #[cfg(test)] mod tests { use expect_test::expect; - use pindakaas::{solver::cadical::Cadical, Cnf}; + use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; use rangelist::RangeList; use tracing_test::traced_test; @@ -195,7 +195,7 @@ mod tests { #[test] #[traced_test] fn test_linear_ne_sat() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, RangeList::from_iter([1..=2]), diff --git a/crates/huub/src/propagator/int_pow.rs b/crates/huub/src/propagator/int_pow.rs index 2328246c..b3453d34 100644 --- a/crates/huub/src/propagator/int_pow.rs +++ b/crates/huub/src/propagator/int_pow.rs @@ -315,7 +315,7 @@ fn pow(base: IntVal, exponent: IntVal) -> Option { #[cfg(test)] mod tests { use expect_test::expect; - use pindakaas::{solver::cadical::Cadical, Cnf}; + use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; use tracing_test::traced_test; use crate::{ @@ -327,7 +327,7 @@ mod tests { #[test] #[traced_test] fn test_int_pow_sat() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, (-2..=3).into(), diff --git a/crates/huub/src/propagator/int_times.rs b/crates/huub/src/propagator/int_times.rs index 3f4ee8cb..3342504f 100644 --- a/crates/huub/src/propagator/int_times.rs +++ b/crates/huub/src/propagator/int_times.rs @@ -143,7 +143,7 @@ impl Poster for IntTimesBoundsPoster { #[cfg(test)] mod tests { use expect_test::expect; - use pindakaas::{solver::cadical::Cadical, Cnf}; + use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; use tracing_test::traced_test; use crate::{ @@ -155,7 +155,7 @@ mod tests { #[test] #[traced_test] fn test_int_times_sat() { - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, (-2..=1).into(), diff --git a/crates/huub/src/solver.rs b/crates/huub/src/solver.rs index 0b03b5c8..cf73db7f 100644 --- a/crates/huub/src/solver.rs +++ b/crates/huub/src/solver.rs @@ -10,9 +10,9 @@ use delegate::delegate; use itertools::Itertools; use pindakaas::{ solver::{ - cadical::Cadical, LearnCallback, NextVarRange, PropagatingSolver, PropagatorAccess, - SlvTermSignal, SolveAssuming, SolveResult as SatSolveResult, Solver as SolverTrait, - TermCallback, + cadical::PropagatingCadical, + propagation::{PropagatingSolver, WithPropagator}, + LearnCallback, SlvTermSignal, SolveResult as SatSolveResult, TermCallback, }, Cnf, Lit as RawLit, Valuation as SatValuation, }; @@ -39,20 +39,6 @@ use crate::{ BoolView, IntVal, LitMeaning, ReformulationError, }; -#[derive(Clone, Debug, Default, PartialEq, Eq)] -pub(crate) struct SolverConfiguration { - /// Switch between the activity-based search heuristic and the user-specific search heuristic after each restart. - /// - /// This option is ignored if [`vsids_only`] is set to `true`. - toggle_vsids: bool, - /// Switch to the activity-based search heuristic after the given number of conflicts. - /// - /// This option is ignored if [`toggle_vsids`] or [`vsids_only`] is set to `true`. - vsids_after: Option, - /// Only use the activity-based search heuristic provided by the SAT solver. Ignore the user-specific search heuristic. - vsids_only: bool, -} - #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Goal { Maximize, @@ -71,26 +57,6 @@ pub struct InitStatistics { propagators: usize, } -pub trait SatSolver: - PropagatingSolver - + TermCallback - + LearnCallback - + SolveAssuming - + NextVarRange - + for<'a> From<&'a Cnf> -where - ::ValueFn: PropagatorAccess, -{ -} - -pub struct Solver -where - Sat: SatSolver, - ::ValueFn: PropagatorAccess, -{ - pub(crate) oracle: Sat, -} - #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum SolveResult { Satisfied, @@ -99,6 +65,25 @@ pub enum SolveResult { Unknown, } +#[derive(Clone)] +pub struct Solver> { + pub(crate) oracle: Oracle, +} + +#[derive(Clone, Debug, Default, PartialEq, Eq)] +pub(crate) struct SolverConfiguration { + /// Switch between the activity-based search heuristic and the user-specific search heuristic after each restart. + /// + /// This option is ignored if [`vsids_only`] is set to `true`. + toggle_vsids: bool, + /// Switch to the activity-based search heuristic after the given number of conflicts. + /// + /// This option is ignored if [`toggle_vsids`] or [`vsids_only`] is set to `true`. + vsids_after: Option, + /// Only use the activity-based search heuristic provided by the SAT solver. Ignore the user-specific search heuristic. + vsids_only: bool, +} + fn trace_learned_clause(clause: &mut dyn Iterator) { debug!(clause = ?clause.map(i32::from).collect::>(), "learn clause"); } @@ -112,11 +97,43 @@ impl InitStatistics { } } -impl Solver +impl Solver +where + Oracle: PropagatingSolver, + Oracle::Slv: LearnCallback, +{ + pub fn set_learn_callback) + 'static>( + &mut self, + cb: Option, + ) { + if let Some(mut f) = cb { + self.oracle.solver_mut().set_learn_callback(Some( + move |clause: &mut dyn Iterator| { + trace_learned_clause(clause); + f(clause); + }, + )); + } else { + self.oracle + .solver_mut() + .set_learn_callback(Some(trace_learned_clause)); + } + } +} + +impl Solver where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, + Oracle: PropagatingSolver, + Oracle::Slv: TermCallback, { + delegate! { + to self.oracle.solver_mut() { + pub fn set_terminate_callback SlvTermSignal + 'static>(&mut self, cb: Option); + } + } +} + +impl> Solver { pub(crate) fn add_brancher(&mut self, poster: P) { let mut actions = InitializationContext { slv: self, @@ -154,23 +171,22 @@ where pub fn add_no_good( &mut self, vars: &[SolverView], - vals: &[Option], + vals: &[Value], ) -> Result<(), ReformulationError> { let clause = vars .iter() .zip_eq(vals) - .filter_map(|(var, val)| match var { - SolverView::Bool(bv) => { - let Value::Bool(val) = val.clone()? else { - unreachable!() - }; - Some(if val { !bv } else { *bv }) - } + .map(|(var, val)| match var { + SolverView::Bool(bv) => match val { + Value::Bool(true) => !bv, + Value::Bool(false) => *bv, + _ => unreachable!(), + }, SolverView::Int(iv) => { - let Value::Int(val) = val.clone()? else { + let Value::Int(val) = val.clone() else { unreachable!() }; - Some(self.get_int_lit(*iv, LitMeaning::NotEq(val))) + self.get_int_lit(*iv, LitMeaning::NotEq(val)) } }) .collect_vec(); @@ -273,13 +289,11 @@ where let status = self.solve_assuming( assump, |value| { - obj_curr = value(SolverView::Int(objective)).map(|val| { - if let Value::Int(i) = val { - i - } else { - unreachable!() - } - }); + obj_curr = if let Value::Int(i) = value(SolverView::Int(objective)) { + Some(i) + } else { + unreachable!() + }; on_sol(value); }, |_| {}, @@ -330,11 +344,11 @@ where } pub(crate) fn engine(&self) -> &Engine { - self.oracle.propagator().unwrap() + self.oracle.propagator() } pub(crate) fn engine_mut(&mut self) -> &mut Engine { - self.oracle.propagator_mut().unwrap() + self.oracle.propagator_mut() } /// Wrapper function for `all_solutions` that collects all solutions and returns them in a vector @@ -349,7 +363,7 @@ where let status = self.all_solutions(vars, |sol| { let mut sol_vec = Vec::with_capacity(vars.len()); for v in vars { - sol_vec.push(sol(*v).unwrap()); + sol_vec.push(sol(*v)); } solutions.push(sol_vec); }); @@ -370,35 +384,13 @@ where } } - pub fn search_statistics(&self) -> &SearchStatistics { - &self.engine().state.statistics + /// Deconstruct the Solver object and return the Oracle object. + pub fn into_oracle(self) -> Oracle::Slv { + self.oracle.into_parts().0 } - pub fn set_learn_callback) + 'static>( - &mut self, - cb: Option, - ) { - if let Some(mut f) = cb { - self.oracle.set_learn_callback(Some( - move |clause: &mut dyn Iterator| { - trace_learned_clause(clause); - f(clause); - }, - )); - } else { - self.oracle.set_learn_callback(Some(trace_learned_clause)); - } - } - - delegate! { - to self.oracle { - pub fn set_terminate_callback SlvTermSignal + 'static>(&mut self, cb: Option); - } - to self.engine_mut().state { - pub fn set_vsids_after(&mut self, conflicts: Option); - pub fn set_vsids_only(&mut self, enable: bool); - pub fn set_toggle_vsids(&mut self, enable: bool); - } + pub fn search_statistics(&self) -> &SearchStatistics { + &self.engine().state.statistics } /// Try and find a solution to the problem for which the Solver was initialized. @@ -428,113 +420,60 @@ where return SolveResult::Unsatisfiable; }; - let status = self.oracle.solve_assuming( - assumptions, - |model| { - let engine: &Engine = model.propagator().unwrap(); + let (engine, result) = self.oracle.solve_assuming(assumptions); + match result { + SatSolveResult::Satisfied(sol) => { let wrapper: &dyn Valuation = &|x| match x { - SolverView::Bool(lit) => match lit.0 { - BoolViewInner::Lit(lit) => model.value(lit).map(Value::Bool), - BoolViewInner::Const(b) => Some(Value::Bool(b)), - }, - SolverView::Int(var) => match var.0 { - IntViewInner::VarRef(iv) => { - Some(Value::Int(engine.state.int_vars[iv].get_value(model))) - } - IntViewInner::Const(i) => Some(Value::Int(i)), + SolverView::Bool(lit) => Value::Bool(match lit.0 { + BoolViewInner::Lit(lit) => sol.value(lit), + BoolViewInner::Const(b) => b, + }), + SolverView::Int(var) => Value::Int(match var.0 { + IntViewInner::VarRef(iv) => engine.state.int_vars[iv].get_value(&sol), + IntViewInner::Const(i) => i, IntViewInner::Linear { transformer: transform, var, } => { - let val = engine.state.int_vars[var].get_value(model); - Some(Value::Int(transform.transform(val))) + let val = engine.state.int_vars[var].get_value(&sol); + transform.transform(val) } - IntViewInner::Bool { transformer, lit } => model - .value(lit) - .map(|v| Value::Int(transformer.transform(v as IntVal))), - }, + IntViewInner::Bool { transformer, lit } => { + transformer.transform(sol.value(lit) as IntVal) + } + }), }; on_sol(wrapper); - }, - |fail_fn| on_fail(fail_fn), - ); - match status { - SatSolveResult::Sat => SolveResult::Satisfied, - SatSolveResult::Unsat => SolveResult::Unsatisfiable, + SolveResult::Satisfied + } + SatSolveResult::Unsatisfiable(fail) => { + on_fail(&fail); + SolveResult::Unsatisfiable + } SatSolveResult::Unknown => SolveResult::Unknown, } } -} -impl SatSolver for Slv -where - Slv: PropagatingSolver - + TermCallback - + LearnCallback - + SolveAssuming - + NextVarRange - + for<'a> From<&'a Cnf>, - ::ValueFn: PropagatorAccess, -{ -} - -impl fmt::Debug for Solver -where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait + fmt::Debug, -{ - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("Solver") - .field("oracle", &self.oracle) - .field("engine", self.engine()) - .finish() - } -} - -impl From<&Cnf> for Solver -where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, -{ - fn from(value: &Cnf) -> Self { - let mut core: Sat = value.into(); - core.set_external_propagator(Some(Engine::default())); - core.set_learn_callback(Some(trace_learned_clause)); - Self { oracle: core } - } -} - -impl Clone for Solver -where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait + Clone, -{ - fn clone(&self) -> Self { - let mut core = self.oracle.clone(); - let engine = self.engine().clone(); - core.set_external_propagator(Some(engine)); - core.set_learn_callback(Some(trace_learned_clause)); - Self { oracle: core } + delegate! { + to self.engine_mut().state { + pub fn set_toggle_vsids(&mut self, enable: bool); + pub fn set_vsids_after(&mut self, conflicts: Option); + pub fn set_vsids_only(&mut self, enable: bool); + } } } -impl DecisionActions for Solver -where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, -{ +impl> DecisionActions for Solver { fn get_intref_lit(&mut self, iv: IntVarRef, meaning: LitMeaning) -> BoolView { - // TODO: We currently copy the integer variable struct here to avoid - // borrowing issues. Hopefully the compiler sees that this is unnecessary, - // but we should check and see if we can avoid this. - let mut var = self.engine_mut().state.int_vars[iv].clone(); + let mut clauses = Vec::new(); + let (oracle, engine) = self.oracle.access_solving(); + let var = &mut engine.state.int_vars[iv]; let new_var = |def: LazyLitDef| { // Create new variable - let v = self.oracle.new_var(); + let v = oracle.new_var(); trace_new_lit!(iv, def, v); - self.engine_mut().state.trail.grow_to_boolvar(v); - self.oracle.add_observed_var(v); - self.engine_mut() + engine.state.trail.grow_to_boolvar(v); + engine .state .bool_to_int .insert_lazy(v, iv, def.meaning.clone()); @@ -545,12 +484,16 @@ where def.next.map(Into::into), ) { trace!(clause = ?cl.iter().map(|&x| i32::from(x)).collect::>(), "add clause"); - self.oracle.add_clause(cl).unwrap(); + clauses.push(cl); } v }; let bv = var.bool_lit(meaning, new_var); - self.engine_mut().state.int_vars[iv] = var; + for cl in clauses { + self.oracle + .add_clause(cl) + .expect("functional definition cannot make the problem unsatisfiable"); + } bv } @@ -559,49 +502,50 @@ where } } -impl ExplanationActions for Solver -where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, -{ +impl> ExplanationActions for Solver { + fn get_int_val_lit(&mut self, var: IntView) -> Option { + let val = self.get_int_val(var)?; + Some(self.get_int_lit(var, LitMeaning::Eq(val))) + } + delegate! { to self.engine().state { fn try_int_lit(&self, var: IntView, meaning: LitMeaning) -> Option; } to self.engine_mut().state { + fn get_int_lit_relaxed(&mut self, var: IntView, meaning: LitMeaning) -> (BoolView, LitMeaning); fn get_int_lower_bound_lit(&mut self, var: IntView) -> BoolView; fn get_int_upper_bound_lit(&mut self, var: IntView) -> BoolView; - fn get_int_lit_relaxed(&mut self, var: IntView, meaning: LitMeaning) -> (BoolView, LitMeaning); } } - - fn get_int_val_lit(&mut self, var: IntView) -> Option { - let val = self.get_int_val(var)?; - Some(self.get_int_lit(var, LitMeaning::Eq(val))) - } } -impl InspectionActions for Solver +impl From<&Cnf> for Solver where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, + Base: for<'a> From<&'a Cnf> + WithPropagator + LearnCallback, + Oracle: PropagatingSolver, { + fn from(value: &Cnf) -> Self { + let mut slv: Base = value.into(); + slv.set_learn_callback(Some(trace_learned_clause)); + let oracle = slv.with_propagator(Engine::default()); + Self { oracle } + } +} + +impl> InspectionActions for Solver { delegate! { to self.engine().state { + fn check_int_in_domain(&self, var: IntView, val: IntVal) -> bool; + fn get_int_bounds(&self, var: IntView) -> (IntVal, IntVal); fn get_int_lower_bound(&self, var: IntView) -> IntVal; fn get_int_upper_bound(&self, var: IntView) -> IntVal; - fn get_int_bounds(&self, var: IntView) -> (IntVal, IntVal); fn get_int_val(&self, var: IntView) -> Option; - fn check_int_in_domain(&self, var: IntView, val: IntVal) -> bool; } } } -impl TrailingActions for Solver -where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, -{ +impl> TrailingActions for Solver { delegate! { to self.engine().state { fn get_bool_val(&self, bv: BoolView) -> Option; @@ -612,3 +556,12 @@ where } } } + +impl> fmt::Debug for Solver { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.debug_struct("Solver") + .field("oracle", &self.oracle) + .field("engine", self.engine()) + .finish() + } +} diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs index 6be29dee..539f6a3d 100644 --- a/crates/huub/src/solver/engine.rs +++ b/crates/huub/src/solver/engine.rs @@ -6,7 +6,6 @@ pub(crate) mod solving_context; pub(crate) mod trail; use std::{ - any::Any, collections::{HashMap, VecDeque}, mem, }; @@ -14,7 +13,7 @@ use std::{ use delegate::delegate; use index_vec::IndexVec; use pindakaas::{ - solver::{ + solver::propagation::{ ClausePersistence, Propagator as PropagatorExtension, SearchDecision, SolvingActions, }, Lit as RawLit, Var as RawVar, @@ -63,7 +62,7 @@ macro_rules! trace_new_lit { pub(crate) use trace_new_lit; #[derive(Debug, Default, Clone)] -pub(crate) struct Engine { +pub struct Engine { /// Storage of the propagators pub(crate) propagators: IndexVec, /// Storage of the branchers @@ -279,7 +278,7 @@ impl PropagatorExtension for Engine { } #[tracing::instrument(level = "debug", skip(self, slv, model))] - fn check_model( + fn check_solution( &mut self, slv: &mut dyn SolvingActions, model: &dyn pindakaas::Valuation, @@ -364,13 +363,6 @@ impl PropagatorExtension for Engine { None } } - - fn as_any(&self) -> &dyn Any { - self - } - fn as_mut_any(&mut self) -> &mut dyn Any { - self - } } impl SearchStatistics { diff --git a/crates/huub/src/solver/engine/bool_to_int.rs b/crates/huub/src/solver/engine/bool_to_int.rs index 3982ebf2..76180985 100644 --- a/crates/huub/src/solver/engine/bool_to_int.rs +++ b/crates/huub/src/solver/engine/bool_to_int.rs @@ -1,6 +1,6 @@ use std::collections::HashMap; -use pindakaas::{solver::VarRange, Var as RawVar}; +use pindakaas::{Var as RawVar, VarRange}; use crate::{solver::engine::int_var::IntVarRef, LitMeaning}; diff --git a/crates/huub/src/solver/engine/int_var.rs b/crates/huub/src/solver/engine/int_var.rs index daed4c0c..d7557ed2 100644 --- a/crates/huub/src/solver/engine/int_var.rs +++ b/crates/huub/src/solver/engine/int_var.rs @@ -9,17 +9,17 @@ use std::{ use itertools::Itertools; use pindakaas::{ - solver::{PropagatingSolver, PropagatorAccess, Solver as SolverTrait, VarRange}, - Lit as RawLit, Valuation as SatValuation, Var as RawVar, + solver::propagation::PropagatingSolver, Lit as RawLit, Valuation as SatValuation, + Var as RawVar, VarRange, }; use rangelist::RangeList; use crate::{ actions::trailing::TrailingActions, solver::{ - engine::trail::TrailedInt, + engine::{trail::TrailedInt, Engine}, view::{BoolViewInner, IntViewInner}, - IntView, SatSolver, + IntView, }, BoolView, Clause, IntVal, LinearTransform, NonZeroIntVal, Solver, }; @@ -62,16 +62,12 @@ pub(crate) struct IntVar { } impl IntVar { - pub(crate) fn new_in( - slv: &mut Solver, + pub(crate) fn new_in>( + slv: &mut Solver, domain: RangeList, order_encoding: EncodingType, direct_encoding: EncodingType, - ) -> IntView - where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, - { + ) -> IntView { let orig_domain_len: usize = domain .iter() .map(|x| (x.end() - x.start() + 1) as usize) @@ -86,7 +82,7 @@ impl IntVar { let lb = *domain.lower_bound().unwrap(); let ub = *domain.upper_bound().unwrap(); if orig_domain_len == 2 { - let lit = slv.oracle.new_var().into(); + let lit = slv.oracle.new_lit(); return IntView(IntViewInner::Bool { transformer: LinearTransform { scale: NonZeroIntVal::new(ub - lb).unwrap(), @@ -103,10 +99,7 @@ impl IntVar { let order_encoding = match order_encoding { EncodingType::Eager => OrderStorage::Eager { lower_bound: slv.engine_mut().state.trail.track_int(lb), - storage: slv - .oracle - .next_var_range(orig_domain_len - 1) - .expect("Boolean variable pool exhausted"), + storage: slv.oracle.new_var_range(orig_domain_len - 1), }, EncodingType::Lazy => OrderStorage::Lazy(LazyOrderStorage { min_index: 0, @@ -117,11 +110,9 @@ impl IntVar { }), }; let direct_encoding = match direct_encoding { - EncodingType::Eager => DirectStorage::Eager( - slv.oracle - .next_var_range(orig_domain_len - 2) - .expect("Boolean variable pool exhausted"), - ), + EncodingType::Eager => { + DirectStorage::Eager(slv.oracle.new_var_range(orig_domain_len - 2)) + } EncodingType::Lazy => DirectStorage::Lazy(HashMap::default()), }; @@ -180,7 +171,7 @@ impl IntVar { .trail .grow_to_boolvar(vars.clone().last().unwrap()); for l in vars { - ::add_observed_var(&mut slv.oracle, l); + slv.oracle.add_observed_var(l); } } @@ -389,11 +380,10 @@ impl IntVar { let mut val_iter = self.domain.clone().into_iter().flatten(); for l in storage.clone() { match model.value(l.into()) { - Some(false) => return val_iter.next().unwrap(), - Some(true) => { + false => return val_iter.next().unwrap(), + true => { let _ = val_iter.next(); } - None => unreachable!(), } } *self.domain.upper_bound().unwrap() @@ -404,7 +394,7 @@ impl IntVar { return last_val; } let mut i = storage.min_index as usize; - while model.value(storage.storage[i].var.into()).unwrap() { + while model.value(storage.storage[i].var.into()) { last_val = storage.storage[i].val; if !storage.storage[i].has_next { break; @@ -1183,7 +1173,7 @@ impl Not for LitMeaning { #[cfg(test)] mod tests { - use pindakaas::{solver::cadical::Cadical, Cnf}; + use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; use rangelist::RangeList; use crate::{ @@ -1203,7 +1193,7 @@ mod tests { unreachable!() } }; - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, RangeList::from(1..=4), @@ -1233,7 +1223,7 @@ mod tests { let lit = a.get_bool_lit(LitMeaning::Eq(4)).unwrap(); assert_eq!(get_lit(lit), 3); - let mut slv = Solver::::from(&Cnf::default()); + let mut slv = Solver::>::from(&Cnf::default()); let a = IntVar::new_in( &mut slv, RangeList::from_iter([1..=3, 8..=10]), diff --git a/crates/huub/src/solver/engine/solving_context.rs b/crates/huub/src/solver/engine/solving_context.rs index 05efce30..5f55d4c8 100644 --- a/crates/huub/src/solver/engine/solving_context.rs +++ b/crates/huub/src/solver/engine/solving_context.rs @@ -1,6 +1,6 @@ use delegate::delegate; use index_vec::IndexVec; -use pindakaas::{solver::SolvingActions, Lit as RawLit}; +use pindakaas::{solver::propagation::SolvingActions, Lit as RawLit}; use tracing::trace; use crate::{ @@ -153,7 +153,6 @@ impl DecisionActions for SolvingContext<'_> { let v = self.slv.new_var(); self.state.trail.grow_to_boolvar(v); trace_new_lit!(iv, def, v); - self.slv.add_observed_var(v); self.state .bool_to_int .insert_lazy(v, iv, def.meaning.clone()); diff --git a/crates/huub/src/solver/engine/trail.rs b/crates/huub/src/solver/engine/trail.rs index dfa748a6..ab8a5945 100644 --- a/crates/huub/src/solver/engine/trail.rs +++ b/crates/huub/src/solver/engine/trail.rs @@ -361,7 +361,7 @@ impl TrailEvent { #[cfg(test)] mod tests { - use pindakaas::solver::{cadical::Cadical, NextVarRange}; + use pindakaas::{solver::cadical::Cadical, ClauseDatabase}; use crate::{ solver::engine::trail::{Trail, TrailEvent}, @@ -372,7 +372,7 @@ mod tests { fn test_trail_event() { let mut slv = Cadical::default(); let mut trail = Trail::default(); - let lits = slv.next_var_range(10).unwrap(); + let lits = slv.new_var_range(10); trail.grow_to_boolvar(lits.clone().end()); let int_events: Vec<_> = [ 0, diff --git a/crates/huub/src/solver/initialization_context.rs b/crates/huub/src/solver/initialization_context.rs index ec1bce1a..d2b72b2d 100644 --- a/crates/huub/src/solver/initialization_context.rs +++ b/crates/huub/src/solver/initialization_context.rs @@ -1,8 +1,5 @@ use delegate::delegate; -use pindakaas::{ - solver::{PropagatingSolver, PropagatorAccess, Solver as SolverTrait}, - Valuation as SatValuation, -}; +use pindakaas::solver::propagation::PropagatingSolver; use crate::{ actions::{ @@ -10,9 +7,10 @@ use crate::{ inspection::InspectionActions, trailing::TrailingActions, }, solver::{ - engine::{activation_list::IntPropCond, int_var::IntVarRef, trail::TrailedInt, PropRef}, + engine::{ + activation_list::IntPropCond, int_var::IntVarRef, trail::TrailedInt, Engine, PropRef, + }, view::{BoolViewInner, IntViewInner}, - SatSolver, }, BoolView, IntVal, IntView, LitMeaning, Solver, }; @@ -25,18 +23,13 @@ pub(crate) enum InitRef { Propagator(PropRef), } -pub(crate) struct InitializationContext<'a, Sat: SatSolver + 'a> -where - ::ValueFn: PropagatorAccess, -{ +pub(crate) struct InitializationContext<'a, Oracle: 'a> { pub(crate) init_ref: InitRef, - pub(crate) slv: &'a mut Solver, + pub(crate) slv: &'a mut Solver, } -impl<'a, Sol, Sat> InitializationActions for InitializationContext<'a, Sat> -where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, +impl<'a, Oracle: PropagatingSolver> InitializationActions + for InitializationContext<'a, Oracle> { fn add_clause>( &mut self, @@ -53,7 +46,7 @@ where match var.0 { BoolViewInner::Lit(lit) => { self.slv.engine_mut().state.trail.grow_to_boolvar(lit.var()); - ::add_observed_var(&mut self.slv.oracle, lit.var()); + self.slv.oracle.add_observed_var(lit.var()); if let InitRef::Propagator(prop) = self.init_ref { self.slv .engine_mut() @@ -97,11 +90,7 @@ where } } -impl<'a, Sol, Sat> TrailingActions for InitializationContext<'a, Sat> -where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, -{ +impl<'a, Oracle: PropagatingSolver> TrailingActions for InitializationContext<'a, Oracle> { delegate! { to self.slv.engine().state { fn get_bool_val(&self, bv: BoolView) -> Option; @@ -113,10 +102,8 @@ where } } -impl<'a, Sol, Sat> InspectionActions for InitializationContext<'a, Sat> -where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, +impl<'a, Oracle: PropagatingSolver> InspectionActions + for InitializationContext<'a, Oracle> { delegate! { to self.slv.engine().state { @@ -129,11 +116,7 @@ where } } -impl<'a, Sol, Sat> DecisionActions for InitializationContext<'a, Sat> -where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, -{ +impl<'a, Oracle: PropagatingSolver> DecisionActions for InitializationContext<'a, Oracle> { delegate! { to self.slv { fn get_intref_lit(&mut self, var: IntVarRef, meaning: LitMeaning) -> BoolView; diff --git a/crates/huub/src/solver/value.rs b/crates/huub/src/solver/value.rs index 1d0811e7..1fa4841a 100644 --- a/crates/huub/src/solver/value.rs +++ b/crates/huub/src/solver/value.rs @@ -37,8 +37,8 @@ pub type NonZeroIntVal = NonZeroI64; pub type IntSetVal = RangeList; -pub trait Valuation: Fn(SolverView) -> Option {} -impl Option> Valuation for F {} +pub trait Valuation: Fn(SolverView) -> Value {} +impl Value> Valuation for F {} impl Display for Value { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { diff --git a/crates/huub/src/solver/view.rs b/crates/huub/src/solver/view.rs index 28aba6c1..1bdede77 100644 --- a/crates/huub/src/solver/view.rs +++ b/crates/huub/src/solver/view.rs @@ -3,17 +3,16 @@ use std::{ ops::{Add, Mul, Neg, Not}, }; -use pindakaas::{ - solver::{PropagatorAccess, Solver as SolverTrait}, - Lit as RawLit, Valuation as SatValuation, -}; +use pindakaas::{solver::propagation::PropagatingSolver, Lit as RawLit}; use crate::{ helpers::linear_transform::LinearTransform, solver::{ - engine::int_var::{DirectStorage, IntVarRef, LitMeaning, OrderStorage}, + engine::{ + int_var::{DirectStorage, IntVarRef, LitMeaning, OrderStorage}, + Engine, + }, value::NonZeroIntVal, - SatSolver, }, IntVal, Solver, }; @@ -95,11 +94,10 @@ impl From for BoolView { pub struct IntView(pub(crate) IntViewInner); impl IntView { - pub fn lit_reverse_map_info(&self, slv: &Solver) -> Vec<(NonZeroI32, LitMeaning)> - where - Sol: PropagatorAccess + SatValuation, - Sat: SatSolver + SolverTrait, - { + pub fn lit_reverse_map_info>( + &self, + slv: &Solver, + ) -> Vec<(NonZeroI32, LitMeaning)> { let transformer = match self.0 { IntViewInner::Bool { transformer, .. } | IntViewInner::Linear { transformer, .. } => { transformer diff --git a/crates/huub/src/tests.rs b/crates/huub/src/tests.rs index 51494789..d3e07fce 100644 --- a/crates/huub/src/tests.rs +++ b/crates/huub/src/tests.rs @@ -46,7 +46,7 @@ impl Solver { let status = self.all_solutions(&vars, |value| { let mut soln = Vec::with_capacity(vars.len()); for var in &vars { - soln.push(value(*var).unwrap()); + soln.push(value(*var)); } assert!(pred(&soln)); }); From 059f7f41653b7393f7c933affbdefe1119bf3c91 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 29 Oct 2024 12:34:46 +1100 Subject: [PATCH 2/2] Use lower bounds of integer variables to determine solution values --- crates/huub/src/solver.rs | 18 ++++++++---- crates/huub/src/solver/engine.rs | 5 ++-- crates/huub/src/solver/engine/int_var.rs | 37 +----------------------- 3 files changed, 15 insertions(+), 45 deletions(-) diff --git a/crates/huub/src/solver.rs b/crates/huub/src/solver.rs index cf73db7f..66c18ac3 100644 --- a/crates/huub/src/solver.rs +++ b/crates/huub/src/solver.rs @@ -26,7 +26,7 @@ use crate::{ }, solver::{ engine::{ - int_var::{IntVarRef, LazyLitDef}, + int_var::{IntVarRef, LazyLitDef, OrderStorage}, trace_new_lit, trail::TrailedInt, Engine, PropRef, SearchStatistics, @@ -421,6 +421,15 @@ impl> Solver { }; let (engine, result) = self.oracle.solve_assuming(assumptions); + let get_int_val = |engine: &Engine, iv: IntVarRef| { + let var_def = &engine.state.int_vars[iv]; + let val = var_def.get_lower_bound(&engine.state.trail); + debug_assert!( + matches!(var_def.order_encoding, OrderStorage::Lazy(_)) + || val == var_def.get_upper_bound(&engine.state.trail) + ); + val + }; match result { SatSolveResult::Satisfied(sol) => { let wrapper: &dyn Valuation = &|x| match x { @@ -429,15 +438,12 @@ impl> Solver { BoolViewInner::Const(b) => b, }), SolverView::Int(var) => Value::Int(match var.0 { - IntViewInner::VarRef(iv) => engine.state.int_vars[iv].get_value(&sol), + IntViewInner::VarRef(iv) => get_int_val(engine, iv), IntViewInner::Const(i) => i, IntViewInner::Linear { transformer: transform, var, - } => { - let val = engine.state.int_vars[var].get_value(&sol); - transform.transform(val) - } + } => transform.transform(get_int_val(engine, var)), IntViewInner::Bool { transformer, lit } => { transformer.transform(sol.value(lit) as IntVal) } diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs index 539f6a3d..1a37a908 100644 --- a/crates/huub/src/solver/engine.rs +++ b/crates/huub/src/solver/engine.rs @@ -277,11 +277,11 @@ impl PropagatorExtension for Engine { clause } - #[tracing::instrument(level = "debug", skip(self, slv, model))] + #[tracing::instrument(level = "debug", skip(self, slv, _sol))] fn check_solution( &mut self, slv: &mut dyn SolvingActions, - model: &dyn pindakaas::Valuation, + _sol: &dyn pindakaas::Valuation, ) -> bool { debug_assert!(self.state.conflict.is_none()); // If there is a known conflict, return false @@ -309,7 +309,6 @@ impl PropagatorExtension for Engine { ctx.state.int_vars[r].order_encoding, OrderStorage::Lazy(_) )); - debug_assert_eq!(lb, ctx.state.int_vars[r].get_value(model)); // Ensure the lazy literal for the upper bound exists let ub_lit = ctx.get_intref_lit(r, LitMeaning::Less(lb + 1)); diff --git a/crates/huub/src/solver/engine/int_var.rs b/crates/huub/src/solver/engine/int_var.rs index d7557ed2..d28d1916 100644 --- a/crates/huub/src/solver/engine/int_var.rs +++ b/crates/huub/src/solver/engine/int_var.rs @@ -8,10 +8,7 @@ use std::{ }; use itertools::Itertools; -use pindakaas::{ - solver::propagation::PropagatingSolver, Lit as RawLit, Valuation as SatValuation, - Var as RawVar, VarRange, -}; +use pindakaas::{solver::propagation::PropagatingSolver, Lit as RawLit, Var as RawVar, VarRange}; use rangelist::RangeList; use crate::{ @@ -374,38 +371,6 @@ impl IntVar { } } - pub(crate) fn get_value(&self, model: &V) -> IntVal { - match &self.order_encoding { - OrderStorage::Eager { storage, .. } => { - let mut val_iter = self.domain.clone().into_iter().flatten(); - for l in storage.clone() { - match model.value(l.into()) { - false => return val_iter.next().unwrap(), - true => { - let _ = val_iter.next(); - } - } - } - *self.domain.upper_bound().unwrap() - } - OrderStorage::Lazy(storage) => { - let mut last_val = *self.domain.lower_bound().unwrap(); - if storage.storage.is_empty() { - return last_val; - } - let mut i = storage.min_index as usize; - while model.value(storage.storage[i].var.into()) { - last_val = storage.storage[i].val; - if !storage.storage[i].has_next { - break; - } - i = storage.storage[i].next as usize; - } - last_val - } - } - } - /// Returns the boolean view associated with `< v` if it exists or weaker version otherwise. /// /// ## Warning