diff --git a/crates/huub/src/helpers/opt_field.rs b/crates/huub/src/helpers/opt_field.rs index eed4f806..044ac8bc 100644 --- a/crates/huub/src/helpers/opt_field.rs +++ b/crates/huub/src/helpers/opt_field.rs @@ -10,6 +10,9 @@ impl OptField { pub(crate) fn get(&self) -> Option<&T> { self.value.first() } + pub(crate) fn is_some(&self) -> bool { + !self.value.is_empty() + } } impl OptField<1, T> { pub(crate) fn new(value: T) -> Self { diff --git a/crates/huub/src/propagator/all_different_int.rs b/crates/huub/src/propagator/all_different_int.rs index 70ec11e5..74346b99 100644 --- a/crates/huub/src/propagator/all_different_int.rs +++ b/crates/huub/src/propagator/all_different_int.rs @@ -71,6 +71,7 @@ impl Poster for AllDifferentIntValuePoster { for &v in prop.vars.iter() { actions.enqueue_on_int_change(v, IntPropCond::Fixed); } + actions.enqueue_when_n_fixed(prop.vars.len(), &[], &prop.vars); Ok(( Box::new(prop), QueuePreferences { diff --git a/crates/huub/src/propagator/array_int_minimum.rs b/crates/huub/src/propagator/array_int_minimum.rs index 9b1d8a69..a81945bb 100644 --- a/crates/huub/src/propagator/array_int_minimum.rs +++ b/crates/huub/src/propagator/array_int_minimum.rs @@ -94,6 +94,12 @@ impl Poster for ArrayIntMinimumBoundsPoster { actions.enqueue_on_int_change(v, IntPropCond::Bounds); } actions.enqueue_on_int_change(prop.min, IntPropCond::LowerBound); + + actions.enqueue_when_n_fixed( + prop.vars.len() + 1, + &[], + &[prop.vars.as_slice(), &[prop.min]].concat(), + ); Ok(( Box::new(prop), QueuePreferences { diff --git a/crates/huub/src/propagator/array_var_int_element.rs b/crates/huub/src/propagator/array_var_int_element.rs index ba18ab77..0f073c9c 100644 --- a/crates/huub/src/propagator/array_var_int_element.rs +++ b/crates/huub/src/propagator/array_var_int_element.rs @@ -226,6 +226,12 @@ impl Poster for ArrayVarIntElementBoundsPoster { }; actions.enqueue_on_int_change(prop.result, IntPropCond::Bounds); actions.enqueue_on_int_change(prop.index, IntPropCond::Domain); + + actions.enqueue_when_n_fixed( + prop.vars.len() + 1, + &[], + &[prop.vars.as_slice(), &[prop.result, prop.index]].concat(), + ); Ok(( Box::new(prop), QueuePreferences { diff --git a/crates/huub/src/propagator/disjunctive_strict.rs b/crates/huub/src/propagator/disjunctive_strict.rs index c2182581..8bfc3a44 100644 --- a/crates/huub/src/propagator/disjunctive_strict.rs +++ b/crates/huub/src/propagator/disjunctive_strict.rs @@ -556,6 +556,8 @@ impl Poster for DisjunctiveEdgeFindingPoster { actions.enqueue_on_int_change(v, IntPropCond::Bounds); } + actions.enqueue_when_n_fixed(prop.start_times.len(), &[], &prop.start_times); + Ok(( Box::new(prop), QueuePreferences { diff --git a/crates/huub/src/propagator/int_abs.rs b/crates/huub/src/propagator/int_abs.rs index 4abe798f..3fb18fa1 100644 --- a/crates/huub/src/propagator/int_abs.rs +++ b/crates/huub/src/propagator/int_abs.rs @@ -94,6 +94,8 @@ impl Poster for IntAbsBoundsPoster { // Subscribe only to the upper bound of the absolute value variable actions.enqueue_on_int_change(self.abs, IntPropCond::UpperBound); + actions.enqueue_when_n_fixed(2, &[], &[self.origin, self.abs]); + Ok(( Box::new(IntAbsBounds { origin: self.origin, diff --git a/crates/huub/src/propagator/int_div.rs b/crates/huub/src/propagator/int_div.rs index e9eaae8d..db9c8357 100644 --- a/crates/huub/src/propagator/int_div.rs +++ b/crates/huub/src/propagator/int_div.rs @@ -213,6 +213,8 @@ impl Poster for IntDivBoundsPoster { actions.enqueue_on_int_change(self.denominator, IntPropCond::Bounds); actions.enqueue_on_int_change(self.result, IntPropCond::Bounds); + actions.enqueue_when_n_fixed(3, &[], &[self.numerator, self.denominator, self.result]); + // Ensure the consistency of the signs of the three variables using the following clauses. if actions.get_int_lower_bound(self.numerator) < 0 || actions.get_int_lower_bound(self.denominator) < 0 diff --git a/crates/huub/src/propagator/int_lin_le.rs b/crates/huub/src/propagator/int_lin_le.rs index 93458005..a60a97b3 100644 --- a/crates/huub/src/propagator/int_lin_le.rs +++ b/crates/huub/src/propagator/int_lin_le.rs @@ -171,6 +171,19 @@ impl Poster for IntLinearLessEqBoundsPoster { if let Some(r) = prop.reification.get() { actions.enqueue_on_bool_change(BoolView(BoolViewInner::Lit(*r))); } + + let bool_vec: Vec = prop + .reification + .get() + .map(|&l| BoolView(BoolViewInner::Lit(l))) + .into_iter() + .collect(); + actions.enqueue_when_n_fixed( + prop.vars.len() + if prop.reification.is_some() { 1 } else { 0 }, + &bool_vec, + &prop.vars, + ); + Ok(( Box::new(prop), QueuePreferences { diff --git a/crates/huub/src/propagator/int_lin_ne.rs b/crates/huub/src/propagator/int_lin_ne.rs index 02639013..44eb9152 100644 --- a/crates/huub/src/propagator/int_lin_ne.rs +++ b/crates/huub/src/propagator/int_lin_ne.rs @@ -8,7 +8,7 @@ use crate::{ Propagator, }, solver::{ - engine::{activation_list::IntPropCond, queue::PriorityLevel, trail::TrailedInt}, + engine::{queue::PriorityLevel, trail::TrailedInt}, poster::{BoxedPropagator, Poster, QueuePreferences}, value::IntVal, view::{BoolViewInner, IntView, IntViewInner}, @@ -163,12 +163,17 @@ impl Poster for IntLinearNotEqValuePoster { reification: self.reification, num_fixed: actions.new_trailed_int(0), }; - for &v in prop.vars.iter() { - actions.enqueue_on_int_change(v, IntPropCond::Fixed); - } - if let Some(r) = prop.reification.get() { - actions.enqueue_on_bool_change(BoolView(BoolViewInner::Lit(*r))); - } + let bool_vec: Vec = prop + .reification + .get() + .map(|&l| BoolView(BoolViewInner::Lit(l))) + .into_iter() + .collect(); + actions.enqueue_when_n_fixed( + prop.vars.len() + if prop.reification.is_some() { 1 } else { 0 } - 1, + &bool_vec, + &prop.vars, + ); Ok(( Box::new(prop), QueuePreferences { diff --git a/crates/huub/src/propagator/int_pow.rs b/crates/huub/src/propagator/int_pow.rs index 385f6d76..bc24809e 100644 --- a/crates/huub/src/propagator/int_pow.rs +++ b/crates/huub/src/propagator/int_pow.rs @@ -255,6 +255,8 @@ impl Poster for IntPowBoundsPoster { actions.enqueue_on_int_change(self.exponent, IntPropCond::Bounds); actions.enqueue_on_int_change(self.result, IntPropCond::Bounds); + actions.enqueue_when_n_fixed(3, &[], &[self.base, self.exponent, self.result]); + // Ensure that if the base is negative, then the exponent cannot be zero let (exp_lb, exp_ub) = actions.get_int_bounds(self.exponent); let (base_lb, base_ub) = actions.get_int_bounds(self.base); diff --git a/crates/huub/src/propagator/int_times.rs b/crates/huub/src/propagator/int_times.rs index 1ab97d81..f612f5d6 100644 --- a/crates/huub/src/propagator/int_times.rs +++ b/crates/huub/src/propagator/int_times.rs @@ -126,6 +126,7 @@ impl Poster for IntTimesBoundsPoster { actions.enqueue_on_int_change(self.x, IntPropCond::Bounds); actions.enqueue_on_int_change(self.y, IntPropCond::Bounds); actions.enqueue_on_int_change(self.z, IntPropCond::Bounds); + actions.enqueue_when_n_fixed(3, &[], &[self.x, self.y, self.z]); Ok(( Box::new(IntTimesBounds { x: self.x, diff --git a/crates/huub/src/solver.rs b/crates/huub/src/solver.rs index 5b5e3a97..08d3c2c5 100644 --- a/crates/huub/src/solver.rs +++ b/crates/huub/src/solver.rs @@ -207,6 +207,8 @@ impl> Solver { debug_assert_eq!(prop_ref, p); let p = self.engine_mut().state.enqueued.push(false); debug_assert_eq!(prop_ref, p); + let p = self.engine_mut().state.enqueued_inactive.push(false); + debug_assert_eq!(prop_ref, p); let p = self.engine_mut().state.activity_scores.push(1.0); debug_assert_eq!(prop_ref, p); let p = self.engine_mut().state.functional.push(functional); @@ -217,6 +219,7 @@ impl> Solver { .propagator_queue .insert(state.propagator_priority[prop_ref], prop_ref); state.enqueued[prop_ref] = true; + state.enqueued_inactive[prop_ref] = true; } Ok(()) } diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs index bdca05be..c1c8f220 100644 --- a/crates/huub/src/solver/engine.rs +++ b/crates/huub/src/solver/engine.rs @@ -148,6 +148,8 @@ pub(crate) struct State { pub(crate) propagator_priority: IndexVec, /// Flag for whether a propagator is enqueued pub(crate) enqueued: IndexVec, + /// Flag for whether a propagator is enqueued into inactive level (i.e., not active) + pub(crate) enqueued_inactive: IndexVec, /// Activity scores for propagators to determine whether they are active or not pub(crate) activity_scores: IndexVec, /// Whether the propagator is functional @@ -181,6 +183,7 @@ impl Default for State { propagator_queue: Default::default(), propagator_priority: Default::default(), enqueued: Default::default(), + enqueued_inactive: Default::default(), activity_scores: Default::default(), functional: Default::default(), propagator_types: Default::default(), @@ -352,7 +355,7 @@ impl PropagatorExtension for Engine { debug_assert!(self.state.conflict.is_empty()); let check_multiple_conflicts = self.state.config.check_multiple_conflicts; // If there is a known conflict, return false - if !self.state.propagation_queue.is_empty() || self.state.conflict.len() > 0 { + if !self.state.propagation_queue.is_empty() || !self.state.conflict.is_empty() { self.state.ensure_clause_changes(&mut self.propagators); debug!(accept = false, "check model"); return false; @@ -590,6 +593,7 @@ impl State { // Empty propagation queue while let Some(p) = self.propagator_queue.pop::() { self.enqueued[p] = false; + self.enqueued_inactive[p] = false; } if ARTIFICIAL { return; @@ -632,72 +636,174 @@ impl State { } } + // Three types of events: + // 1. Not fixed event Or fixed event but not the last variable: + // - propogator enqueued in normal level: no actions + // - propogator enqueued in inactive level: no actions + // - propogator not enqueued: enqueue according to the activity score + // 2. Fixed event and the last variable: + // - propogator enqueued in normal level: no actions + // - propogator enqueued in inactive level: enqueue to the normal level + // - propogator not enqueued: enqueue to the normal level + // Assume that there is a copy for every PropRef in both `self.int_activation[int_var].fixed_daemons` + // and `self.int_activation[int_var].activations` fn enqueue_int_propagators( &mut self, int_var: IntVarRef, event: IntEvent, skip: Option, ) { - for prop in self.int_activation[int_var].activated_by(event) { - if Some(prop) != skip && !self.enqueued[prop] { - if !self.vsids - || self.activity_scores[prop] >= self.config.propagator_activity_threshold - || (self.config.enqueue_functional && self.functional[prop]) - { - self.propagator_queue - .insert(self.propagator_priority[prop], prop); - } else { - trace!(propagator = usize::from(prop), "deactivate propagator"); - self.propagator_queue.insert(PriorityLevel::Inactive, prop); - } - self.enqueued[prop] = true; - } - } + let mut force_enqueue = Vec::new(); + let mut possible_enqueue = Vec::new(); if event == IntEvent::Fixed { + // Decrement the variable counter for fixed events for prop in self.int_activation[int_var].fixed_daemons() { let counter = self.fixed_daemons[&prop]; let count = self.trail.get_trailed_int(counter) - 1; let _ = self.trail.set_trailed_int(counter, count); - if count <= 0 && !self.enqueued[prop] { - self.propagator_queue - .insert(self.propagator_priority[prop], prop); - self.enqueued[prop] = true; + if Some(prop) != skip { + if count == 0 { + force_enqueue.push(prop); + } else { + possible_enqueue.push(prop); + } + } + } + } else { + for prop in self.int_activation[int_var].activated_by(event) { + if Some(prop) != skip { + possible_enqueue.push(prop); } } } + + for prop in force_enqueue { + if !self.enqueued[prop] { + self.propagator_queue + .insert(self.propagator_priority[prop], prop); + self.enqueued[prop] = true; + } + } + + for prop in possible_enqueue { + if self.enqueued[prop] || self.enqueued_inactive[prop] { + continue; + } + if (!self.vsids + || self.activity_scores[prop] >= self.config.propagator_activity_threshold) + || (self.config.enqueue_functional && self.functional[prop]) + { + self.propagator_queue + .insert(self.propagator_priority[prop], prop); + self.enqueued[prop] = true; + } else { + self.propagator_queue.insert(PriorityLevel::Inactive, prop); + self.enqueued_inactive[prop] = false; + } + } + + // for prop in self.int_activation[int_var].activated_by(event) { + // if Some(prop) != skip && !self.enqueued[prop] { + // if !self.vsids + // || self.activity_scores[prop] >= self.config.propagator_activity_threshold + // || (self.config.enqueue_functional && self.functional[prop]) + // { + // self.propagator_queue + // .insert(self.propagator_priority[prop], prop); + // self.enqueued[prop] = true; // Mark as enqueued to the normal level + // } else { + // trace!(propagator = usize::from(prop), "deactivate propagator"); + // self.propagator_queue.insert(PriorityLevel::Inactive, prop); + // self.enqueued_deactivate[prop] = true; // Mark as enqueued to the inactive level + // } + // } + // } + // if event == IntEvent::Fixed { + // for prop in self.int_activation[int_var].fixed_daemons() { + // let counter = self.fixed_daemons[&prop]; + // let count = self.trail.get_trailed_int(counter) - 1; + // let _ = self.trail.set_trailed_int(counter, count); + // if count == 0 && !self.enqueued[prop] { + // self.propagator_queue + // .insert(self.propagator_priority[prop], prop); + // self.enqueued[prop] = true; + // } + // } + // } } fn enqueue_propagators(&mut self, lit: RawLit, skip: Option) { if let Some(activator) = self.bool_activation.get(&lit.var()) { - // Enqueue all propagators that are directly activated by the given literal - for prop in activator.activations() { - if Some(prop) != skip && !self.enqueued[prop] { - if !self.vsids - || self.activity_scores[prop] >= self.config.propagator_activity_threshold - || (self.config.enqueue_functional && self.functional[prop]) - { - self.propagator_queue - .insert(self.propagator_priority[prop], prop); + let mut force_enqueue = Vec::new(); + let mut possible_enqueue = Vec::new(); + // Decrement the variable counter for fixed events + for prop in activator.fixed_daemons() { + let counter = self.fixed_daemons[&prop]; + let count = self.trail.get_trailed_int(counter) - 1; + let _ = self.trail.set_trailed_int(counter, count); + if Some(prop) != skip { + if count == 0 { + force_enqueue.push(prop); } else { - trace!(propagator = usize::from(prop), "deactivate propagator"); - self.propagator_queue.insert(PriorityLevel::Inactive, prop); + possible_enqueue.push(prop); } + } + } + + for prop in force_enqueue { + if !self.enqueued[prop] { + self.propagator_queue + .insert(self.propagator_priority[prop], prop); self.enqueued[prop] = true; } } - // Decrease all fixed daemons that are associated with the given literal and - // activate them if they are now zero - for prop in activator.fixed_daemons() { - let counter = self.fixed_daemons[&prop]; - let count = self.trail.get_trailed_int(counter) - 1; - let _ = self.trail.set_trailed_int(counter, count); - if count <= 0 && !self.enqueued[prop] { + for prop in possible_enqueue { + if self.enqueued[prop] || self.enqueued_inactive[prop] { + continue; + } + if (!self.vsids + || self.activity_scores[prop] >= self.config.propagator_activity_threshold) + || (self.config.enqueue_functional && self.functional[prop]) + { self.propagator_queue .insert(self.propagator_priority[prop], prop); self.enqueued[prop] = true; + } else { + self.propagator_queue.insert(PriorityLevel::Inactive, prop); + self.enqueued_inactive[prop] = false; } } + + // // Enqueue all propagators that are directly activated by the given literal + // for prop in activator.activations() { + // if Some(prop) != skip && !self.enqueued[prop] { + // if !self.vsids + // || self.activity_scores[prop] >= self.config.propagator_activity_threshold + // || (self.config.enqueue_functional && self.functional[prop]) + // { + // self.propagator_queue + // .insert(self.propagator_priority[prop], prop); + // } else { + // trace!(propagator = usize::from(prop), "deactivate propagator"); + // self.propagator_queue.insert(PriorityLevel::Inactive, prop); + // } + // self.enqueued[prop] = true; + // } + // } + + // // Decrease all fixed daemons that are associated with the given literal and + // // activate them if they are now zero + // for prop in activator.fixed_daemons() { + // let counter = self.fixed_daemons[&prop]; + // let count = self.trail.get_trailed_int(counter) - 1; + // let _ = self.trail.set_trailed_int(counter, count); + // if count == 0 && !self.enqueued[prop] { + // self.propagator_queue + // .insert(self.propagator_priority[prop], prop); + // self.enqueued[prop] = true; + // } + // } } // Process Integer consequences diff --git a/crates/huub/src/solver/engine/activation_list.rs b/crates/huub/src/solver/engine/activation_list.rs index 37461ede..de9c2911 100644 --- a/crates/huub/src/solver/engine/activation_list.rs +++ b/crates/huub/src/solver/engine/activation_list.rs @@ -83,6 +83,7 @@ impl BoolActivationList { self.fixed_daemons.push(prop); } + #[allow(dead_code, reason = "TODO: testing demon with normal propagator")] pub(crate) fn activations(&self) -> impl Iterator + '_ { self.activations.iter().copied() } diff --git a/crates/huub/src/solver/engine/solving_context.rs b/crates/huub/src/solver/engine/solving_context.rs index 75dac801..aab3aa09 100644 --- a/crates/huub/src/solver/engine/solving_context.rs +++ b/crates/huub/src/solver/engine/solving_context.rs @@ -86,6 +86,7 @@ impl<'a> SolvingContext<'a> { debug_assert!(self.state.conflict.is_empty()); let propagation_before = self.state.propagation_queue.len(); self.state.enqueued[p] = false; + self.state.enqueued_inactive[p] = false; self.current_prop = p; let prop = propagators[p].as_mut(); let res = prop.propagate(self); @@ -109,7 +110,7 @@ impl<'a> SolvingContext<'a> { self.state.no_propagations += 1; } - if self.state.conflict.len() > 0 || !self.state.propagation_queue.is_empty() { + if !self.state.conflict.is_empty() || !self.state.propagation_queue.is_empty() { break; } } @@ -122,6 +123,7 @@ impl<'a> SolvingContext<'a> { let checking_before = self.state.propagation_queue.len(); while let Some(p) = self.state.propagator_queue.pop::() { self.state.enqueued[p] = false; + self.state.enqueued_inactive[p] = false; self.current_prop = p; let prop = propagators[p].as_mut(); let res = prop.propagate(self); diff --git a/crates/huub/src/solver/initialization_context.rs b/crates/huub/src/solver/initialization_context.rs index 18bf4442..25112288 100644 --- a/crates/huub/src/solver/initialization_context.rs +++ b/crates/huub/src/solver/initialization_context.rs @@ -124,9 +124,9 @@ impl<'a, Oracle: PropagatingSolver> InitializationActions } } - if n <= 0 { - todo!("immediately enqueue the propagator") - } + // if n <= 0 { + // todo!("immediately enqueue the propagator") + // } for lit in lits { self.slv.engine_mut().state.trail.grow_to_boolvar(lit.var()); @@ -140,7 +140,7 @@ impl<'a, Oracle: PropagatingSolver> InitializationActions .add_fixed_daemon(prop); } for var in ints { - self.slv.engine_mut().state.int_activation[var].add_fixed_daemon(prop) + self.slv.engine_mut().state.int_activation[var].add_fixed_daemon(prop); } let count = self.slv.engine_mut().state.trail.track_int(n as i64);