From fb337211d12c2b81662c3200f2318090b0650a94 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Fri, 26 Apr 2024 19:30:07 +1000 Subject: [PATCH] Update library to work with the newest version of pindakaas --- Cargo.lock | 36 +++++++---------- clippy.toml | 2 + crates/huub/src/lib.rs | 4 +- crates/huub/src/model.rs | 21 ++++++++-- crates/huub/src/model/bool.rs | 21 ++++++---- crates/huub/src/model/int.rs | 11 ++++- crates/huub/src/propagator.rs | 13 +++++- crates/huub/src/propagator/all_different.rs | 15 +++++-- crates/huub/src/propagator/init_action.rs | 14 +++++-- crates/huub/src/solver.rs | 45 +++++++++++++-------- crates/huub/src/solver/engine.rs | 29 +++++-------- crates/huub/src/solver/engine/int_var.rs | 13 +++--- crates/huub/src/solver/view.rs | 11 ++++- 13 files changed, 149 insertions(+), 86 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 624b932d..02aec926 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -114,12 +114,6 @@ dependencies = [ "backtrace", ] -[[package]] -name = "bitflags" -version = "1.3.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" - [[package]] name = "bitflags" version = "2.5.0" @@ -482,9 +476,9 @@ checksum = "01cda141df6706de531b6c46c3a33ecca755538219bd484262fa09410c13539c" [[package]] name = "lock_api" -version = "0.4.11" +version = "0.4.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3c168f8615b12bc01f9c17e2eb0cc07dcae1940121185446edc3744920e8ef45" +checksum = "07af8b9cdd281b7915f413fa73f29ebd5d55d0d3f0155584dade1ff18cea1b17" dependencies = [ "autocfg", "scopeguard", @@ -581,9 +575,9 @@ checksum = "caff54706df99d2a78a5a4e3455ff45448d81ef1bb63c22cd14052ca0e993a3f" [[package]] name = "parking_lot" -version = "0.12.1" +version = "0.12.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3742b2c103b9f06bc9fff0a37ff4912935851bee6d36f3c02bcc755bcfec228f" +checksum = "7e4af0ca4f6caed20e900d564c242b8e5d4903fdacf31d3daf527b66fe6f42fb" dependencies = [ "lock_api", "parking_lot_core", @@ -591,15 +585,15 @@ dependencies = [ [[package]] name = "parking_lot_core" -version = "0.9.9" +version = "0.9.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c42a9226546d68acdd9c0a280d17ce19bfe27a46bf68784e4066115788d008e" +checksum = "1e401f977ab385c9e4e3ab30627d6f26d00e2c73eef317493c4ec6d468726cf8" dependencies = [ "cfg-if", "libc", "redox_syscall", "smallvec", - "windows-targets 0.48.5", + "windows-targets 0.52.5", ] [[package]] @@ -617,7 +611,7 @@ checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02" [[package]] name = "pindakaas" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#9ee5ae6a39d50ebeeddf0051cfc70646331c51d3" +source = "git+https://github.com/pindakaashq/pindakaas.git#99414311396d994684efb915b153ddcc40b5ba41" dependencies = [ "cached", "iset", @@ -631,7 +625,7 @@ dependencies = [ [[package]] name = "pindakaas-build-macros" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#9ee5ae6a39d50ebeeddf0051cfc70646331c51d3" +source = "git+https://github.com/pindakaashq/pindakaas.git#99414311396d994684efb915b153ddcc40b5ba41" dependencies = [ "cc", "paste", @@ -640,7 +634,7 @@ dependencies = [ [[package]] name = "pindakaas-cadical" version = "1.9.5" -source = "git+https://github.com/pindakaashq/pindakaas.git#9ee5ae6a39d50ebeeddf0051cfc70646331c51d3" +source = "git+https://github.com/pindakaashq/pindakaas.git#99414311396d994684efb915b153ddcc40b5ba41" dependencies = [ "cc", "pindakaas-build-macros", @@ -649,7 +643,7 @@ dependencies = [ [[package]] name = "pindakaas-derive" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#9ee5ae6a39d50ebeeddf0051cfc70646331c51d3" +source = "git+https://github.com/pindakaashq/pindakaas.git#99414311396d994684efb915b153ddcc40b5ba41" dependencies = [ "darling 0.20.8", "quote", @@ -676,11 +670,11 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.4.1" +version = "0.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4722d768eff46b75989dd134e5c353f0d6296e5aaa3132e776cbdb56be7731aa" +checksum = "469052894dcb553421e483e4209ee581a45100d31b4018de03e5a7ad86374a7e" dependencies = [ - "bitflags 1.3.2", + "bitflags", ] [[package]] @@ -701,7 +695,7 @@ version = "0.38.34" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "70dc5ec042f7a43c4a73241207cecc9873a06d45debb38b329f8541d85c2730f" dependencies = [ - "bitflags 2.5.0", + "bitflags", "errno", "libc", "linux-raw-sys", diff --git a/clippy.toml b/clippy.toml index 14963f7a..b1d250cd 100644 --- a/clippy.toml +++ b/clippy.toml @@ -1,4 +1,6 @@ enforced-import-renames = [ { path = "pindakaas::Lit", rename = "RawLit" }, { path = "pindakaas::Var", rename = "RawVar" }, + { path = "pindakaas::solver::Solver", rename = "SolverTrait" }, + { path = "pindakaas::Valuation", rename = "SatValuation" }, ] diff --git a/crates/huub/src/lib.rs b/crates/huub/src/lib.rs index c4da190f..cdff5c0f 100644 --- a/crates/huub/src/lib.rs +++ b/crates/huub/src/lib.rs @@ -8,9 +8,7 @@ pub use solver::{BoolView, IntVal, IntView, LitMeaning, Solver, SolverView, Valu #[cfg(test)] mod tests { - use crate::{ - Constraint, Model, SimplifiedBool, SimplifiedVariable, SolveResult, Solver, Variable, - }; + use crate::{Constraint, Model, SolveResult, Solver, Variable}; #[test] fn it_works() { diff --git a/crates/huub/src/model.rs b/crates/huub/src/model.rs index ec1e3424..692a429f 100644 --- a/crates/huub/src/model.rs +++ b/crates/huub/src/model.rs @@ -6,7 +6,10 @@ mod reformulate; use std::ops::AddAssign; use flatzinc_serde::RangeList; -use pindakaas::{ClauseDatabase, Cnf, Lit as RawLit, Var as RawVar}; +use pindakaas::{ + solver::{PropagatorAccess, Solver as SolverTrait}, + ClauseDatabase, Cnf, Lit as RawLit, Valuation as SatValuation, Var as RawVar, +}; use self::{ bool::{BoolExpr, BoolVar}, @@ -39,7 +42,12 @@ impl Model { } // TODO: Make generic on Solver again (need var range trait) - pub fn to_solver(&self) -> (Solver, VariableMap) { + pub fn to_solver< + Sol: PropagatorAccess + SatValuation, + Sat: SatSolver + SolverTrait, + >( + &self, + ) -> (Solver, VariableMap) { let mut map = VariableMap::default(); // TODO: run SAT simplification @@ -87,7 +95,14 @@ pub enum Constraint { } impl Constraint { - fn to_solver(&self, slv: &mut Solver, map: &mut VariableMap) { + fn to_solver< + Sol: PropagatorAccess + SatValuation, + Sat: SatSolver + SolverTrait, + >( + &self, + slv: &mut Solver, + map: &mut VariableMap, + ) { struct Satisfied; match self { Constraint::Clause(v) => { diff --git a/crates/huub/src/model/bool.rs b/crates/huub/src/model/bool.rs index 967b8369..d7fd7740 100644 --- a/crates/huub/src/model/bool.rs +++ b/crates/huub/src/model/bool.rs @@ -4,7 +4,10 @@ use std::{ ops::Not, }; -use pindakaas::{Lit as RawLit, Var as RawVar}; +use pindakaas::{ + solver::{PropagatorAccess, Solver as SolverTrait}, + Lit as RawLit, Valuation as SatValuation, Var as RawVar, +}; use super::reformulate::{ReifContext, VariableMap}; use crate::{ @@ -20,10 +23,13 @@ pub enum BoolExpr { } impl BoolExpr { - pub(crate) fn to_arg( + pub(crate) fn to_arg< + Sol: PropagatorAccess + SatValuation, + Sat: SatSolver + SolverTrait, + >( &self, ctx: ReifContext, - slv: &mut Solver, + slv: &mut Solver, map: &mut VariableMap, ) -> BoolView { match self { @@ -33,10 +39,13 @@ impl BoolExpr { } } - fn to_negated_arg( + fn to_negated_arg< + Sol: PropagatorAccess + SatValuation, + Sat: SatSolver + SolverTrait, + >( &self, ctx: ReifContext, - slv: &mut Solver, + slv: &mut Solver, map: &mut VariableMap, ) -> BoolView { match self { @@ -54,7 +63,6 @@ impl Not for BoolExpr { BoolExpr::Lit(l) => BoolExpr::Lit(!l), BoolExpr::Val(v) => BoolExpr::Val(!v), BoolExpr::Not(e) => *e, - // e => BoolExpr::Not(Box::new(e)), } } } @@ -66,7 +74,6 @@ impl Not for &BoolExpr { BoolExpr::Lit(l) => BoolExpr::Lit(!*l), BoolExpr::Val(v) => BoolExpr::Val(!*v), BoolExpr::Not(e) => (**e).clone(), - // e => BoolExpr::Not(Box::new(e.clone())), } } } diff --git a/crates/huub/src/model/int.rs b/crates/huub/src/model/int.rs index 0c3414b2..a3d2a390 100644 --- a/crates/huub/src/model/int.rs +++ b/crates/huub/src/model/int.rs @@ -1,4 +1,8 @@ use flatzinc_serde::RangeList; +use pindakaas::{ + solver::{PropagatorAccess, Solver as SolverTrait}, + Valuation as SatValuation, +}; use super::reformulate::{ReifContext, VariableMap}; use crate::{ @@ -13,10 +17,13 @@ pub enum IntExpr { } impl IntExpr { - pub(crate) fn to_arg( + pub(crate) fn to_arg< + Sol: PropagatorAccess + SatValuation, + Sat: SatSolver + SolverTrait, + >( &self, _ctx: ReifContext, - _slv: &mut Solver, + _slv: &mut Solver, map: &mut VariableMap, ) -> IntView { match self { diff --git a/crates/huub/src/propagator.rs b/crates/huub/src/propagator.rs index 391d62cd..ea18d2cd 100644 --- a/crates/huub/src/propagator.rs +++ b/crates/huub/src/propagator.rs @@ -7,7 +7,10 @@ pub(crate) mod reason; use std::fmt::Debug; -use pindakaas::Lit as RawLit; +use pindakaas::{ + solver::{PropagatorAccess, Solver as SolverTrait}, + Lit as RawLit, Valuation as SatValuation, +}; use crate::{ propagator::{ @@ -70,7 +73,13 @@ pub(crate) trait Initialize { /// /// This method is generally used to register variable event /// subscriptions with the solver. - fn initialize(&mut self, actions: &mut InitializationActions<'_, Sat>) -> bool { + fn initialize< + Sol: PropagatorAccess + SatValuation, + Sat: SatSolver + SolverTrait, + >( + &mut self, + actions: &mut InitializationActions<'_, Sat>, + ) -> bool { let _ = actions; false } diff --git a/crates/huub/src/propagator/all_different.rs b/crates/huub/src/propagator/all_different.rs index 62294798..03a2b303 100644 --- a/crates/huub/src/propagator/all_different.rs +++ b/crates/huub/src/propagator/all_different.rs @@ -1,3 +1,7 @@ +use pindakaas::{ + solver::{PropagatorAccess, Solver as SolverTrait}, + Valuation as SatValuation, +}; use tracing::trace; use super::reason::ReasonBuilder; @@ -75,7 +79,13 @@ impl Propagator for AllDifferentValue { } impl Initialize for AllDifferentValue { - fn initialize(&mut self, actions: &mut InitializationActions<'_, Sat>) -> bool { + fn initialize< + Sol: PropagatorAccess + SatValuation, + Sat: SatSolver + SolverTrait, + >( + &mut self, + actions: &mut InitializationActions<'_, Sat>, + ) -> bool { for (i, v) in self.vars.iter().enumerate() { actions.subscribe_int(*v, IntEvent::Fixed, i as u32) } @@ -93,8 +103,7 @@ mod tests { }; use crate::{ - propagator::all_different::AllDifferentValue, - solver::engine::int_var::{IntVal, IntVar}, + propagator::all_different::AllDifferentValue, solver::engine::int_var::IntVar, IntVal, IntView, Solver, }; diff --git a/crates/huub/src/propagator/init_action.rs b/crates/huub/src/propagator/init_action.rs index 71f27fe7..1cdcef92 100644 --- a/crates/huub/src/propagator/init_action.rs +++ b/crates/huub/src/propagator/init_action.rs @@ -1,4 +1,7 @@ -use pindakaas::solver::PropagatingSolver; +use pindakaas::{ + solver::{PropagatingSolver, PropagatorAccess, Solver as SolverTrait}, + Valuation as SatValuation, +}; use crate::{ propagator::int_event::IntEvent, @@ -6,12 +9,17 @@ use crate::{ Solver, }; -pub(crate) struct InitializationActions<'a, Sat: SatSolver> { +pub(crate) struct InitializationActions<'a, Sat: SatSolver> +where + ::ValueFn: PropagatorAccess, +{ pub(crate) prop_ref: PropRef, pub(crate) slv: &'a mut Solver, } -impl InitializationActions<'_, Sat> { +impl> + InitializationActions<'_, Sat> +{ #[allow(dead_code)] // TODO pub(crate) fn subscribe_bool(&mut self, var: BoolView, data: u32) { match var.0 { diff --git a/crates/huub/src/solver.rs b/crates/huub/src/solver.rs index e0c3ae21..6f01ec8a 100644 --- a/crates/huub/src/solver.rs +++ b/crates/huub/src/solver.rs @@ -4,10 +4,10 @@ pub(crate) mod view; use pindakaas::{ solver::{ - cadical::Cadical, LearnCallback, NextVarRange, PropagatingSolver, SolveAssuming, - SolveResult, TermCallback, + cadical::Cadical, LearnCallback, NextVarRange, PropagatingSolver, PropagatorAccess, + SolveAssuming, SolveResult, Solver as SolverTrait, TermCallback, }, - Cnf, Lit as RawLit, + Cnf, Lit as RawLit, Valuation as SatValuation, }; use tracing::debug; @@ -26,11 +26,16 @@ use crate::{ }; #[derive(Debug)] -pub struct Solver { +pub struct Solver +where + ::ValueFn: PropagatorAccess, +{ pub(crate) core: Sat, } -impl Solver { +impl> + Solver +{ pub(crate) fn engine(&self) -> &Engine { self.core.propagator().unwrap() } @@ -40,18 +45,17 @@ impl Solver { } pub fn solve(&mut self, mut on_sol: impl FnMut(&dyn Valuation)) -> SolveResult { - // TODO: This is bad, but we cannot access propagator in the value function. - // If we could, then we could (hopefully) just access the current domain - let int_vars = self.engine().int_vars.clone(); - - self.core.solve(|sat_value| { + self.core.solve(|model| { + let engine: &Engine = model.propagator().unwrap(); let wrapper: &dyn Valuation = &|x| match x { SolverView::Bool(lit) => match lit.0 { - BoolViewInner::Lit(lit) => sat_value(lit).map(Value::Bool), + 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(int_vars[iv].get_value(sat_value))), + IntViewInner::VarRef(iv) => { + Some(Value::Int(engine.int_vars[iv].get_value(model))) + } IntViewInner::Const(i) => Some(Value::Int(i)), }, }; @@ -64,7 +68,9 @@ impl Solver { } } -impl> From for Solver { +impl> From + for Solver +{ fn from(value: Cnf) -> Self { let mut core: Sat = value.into(); let None = core.set_external_propagator(Some(Box::::default())) else { @@ -79,7 +85,9 @@ fn learn_clause_cb(clause: &mut dyn Iterator) { debug!(clause = ?clause.map(i32::from).collect::>(), "learn clause"); } -impl Solver { +impl> + Solver +{ pub(crate) fn add_propagator(&mut self, mut prop: impl Propagator + Initialize + 'static) { let prop_ref = PropRef::from(self.engine().propagators.len()); let mut actions = InitializationActions { @@ -100,10 +108,13 @@ impl Solver { pub trait SatSolver: PropagatingSolver + TermCallback + LearnCallback + SolveAssuming + NextVarRange + From +where + ::ValueFn: PropagatorAccess, { } -impl< - X: PropagatingSolver + TermCallback + LearnCallback + SolveAssuming + NextVarRange + From, - > SatSolver for X +impl SatSolver for X +where + X: PropagatingSolver + TermCallback + LearnCallback + SolveAssuming + NextVarRange + From, + ::ValueFn: PropagatorAccess, { } diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs index 595def78..0b780854 100644 --- a/crates/huub/src/solver/engine.rs +++ b/crates/huub/src/solver/engine.rs @@ -240,14 +240,18 @@ impl IpasirPropagator for Engine { reason } - fn check_model(&mut self, sat_value: &dyn pindakaas::Valuation) -> bool { + fn check_model( + &mut self, + slv: &mut dyn SolvingActions, + model: &dyn pindakaas::Valuation, + ) -> bool { trace!("check model"); for (r, iv) in self.int_vars.iter_mut().enumerate() { let r = IntVarRef::new(r); let lb = self.int_trail[iv.lower_bound]; let ub = self.int_trail[iv.upper_bound]; if lb != ub { - let val = iv.get_value(sat_value); + let val = iv.get_value(model); self.int_trail.assign(iv.lower_bound, val); self.int_trail.assign(iv.upper_bound, val); @@ -261,21 +265,7 @@ impl IpasirPropagator for Engine { } } } - struct NoOp {} - impl SolvingActions for NoOp { - fn new_var(&mut self) -> RawVar { - todo!() - } - - fn add_observed_var(&mut self, _var: RawVar) { - todo!() - } - - fn is_decision(&mut self, _lit: pindakaas::Lit) -> bool { - todo!() - } - } - let lits = self.propagate(&mut NoOp {}); + let lits = self.propagate(slv); for lit in lits { let clause = self.add_reason_clause(lit); self.external_queue.push(clause); @@ -283,7 +273,10 @@ impl IpasirPropagator for Engine { self.external_queue.is_empty() } - fn add_external_clause(&mut self) -> Option> { + fn add_external_clause( + &mut self, + _slv: &mut dyn SolvingActions, + ) -> Option> { self.external_queue.pop() } diff --git a/crates/huub/src/solver/engine/int_var.rs b/crates/huub/src/solver/engine/int_var.rs index 480e4e2c..fc1b3354 100644 --- a/crates/huub/src/solver/engine/int_var.rs +++ b/crates/huub/src/solver/engine/int_var.rs @@ -3,8 +3,8 @@ use std::ops::{Not, RangeBounds}; use flatzinc_serde::RangeList; use itertools::Itertools; use pindakaas::{ - solver::{PropagatingSolver, VarRange}, - Lit as RawLit, + solver::{PropagatingSolver, PropagatorAccess, Solver as SolverTrait, VarRange}, + Lit as RawLit, Valuation as SatValuation, }; use super::TrailedInt; @@ -50,7 +50,10 @@ impl IntVar { } } - pub(crate) fn new_in( + pub(crate) fn new_in< + Sol: PropagatorAccess + SatValuation, + Sat: SatSolver + SolverTrait, + >( slv: &mut Solver, domain: RangeList, direct_encoding: bool, @@ -206,10 +209,10 @@ impl IntVar { BoolView(BoolViewInner::Lit(if negate { !lit } else { lit })) } - pub(crate) fn get_value(&self, value: &dyn pindakaas::Valuation) -> i64 { + pub(crate) fn get_value(&self, model: &V) -> i64 { let mut val_iter = self.orig_domain.clone().into_iter().flatten(); for l in self.order_vars() { - match value(l.into()) { + match model.value(l.into()) { Some(false) => return val_iter.next().unwrap(), Some(true) => { let _ = val_iter.next(); diff --git a/crates/huub/src/solver/view.rs b/crates/huub/src/solver/view.rs index 49125634..22d73cdd 100644 --- a/crates/huub/src/solver/view.rs +++ b/crates/huub/src/solver/view.rs @@ -1,6 +1,9 @@ use std::num::NonZeroI32; -use pindakaas::Lit as RawLit; +use pindakaas::{ + solver::{PropagatorAccess, Solver as SolverTrait}, + Lit as RawLit, Valuation as SatValuation, +}; use super::engine::int_var::LitMeaning; use crate::{ @@ -65,7 +68,11 @@ pub(crate) enum BoolViewInner { pub struct IntView(pub(crate) IntViewInner); impl IntView { - pub fn add_to_lit_reverse_map>( + pub fn add_to_lit_reverse_map< + Sol: PropagatorAccess + SatValuation, + Sat: SatSolver + SolverTrait, + M: Extend<(NonZeroI32, (usize, LitMeaning))>, + >( &self, slv: &Solver, map: &mut M,