Add reverse trailing capability

crates/huub/src/solver/engine.rs

@@ -56,7 +56,10 @@ impl IpasirPropagator for Engine {
 		// Process Boolean assignment
 		if persistent && self.state.decision_level() != 0 {
 			// Note that the assignment might already be known and trailed, but not previously marked as persistent
-			self.persistent.push(lit)
+			self.persistent.push(lit);
+			if self.state.trail.is_backtracking() {
+				return;
+			}
 		}
 		if self.state.trail.assign_sat(lit).is_some() {
 			return;

crates/huub/src/solver/engine/trail.rs

@@ -5,6 +5,7 @@ use std::{
 
 use index_vec::IndexVec;
 use pindakaas::{Lit as RawLit, Var as RawVar};
+use tracing::{debug, trace};
 
 use crate::{actions::trailing::TrailingActions, IntVal};
 
@@ -16,25 +17,30 @@ index_vec::define_index_type! {
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) struct Trail {
 	trail: Vec<u32>,
+	pos: usize,
 	prev_len: Vec<usize>,
 
 	int_value: IndexVec<TrailedInt, IntVal>,
 	sat_value: HashMap<RawVar, bool>,
+	sat_restore_value: HashMap<RawVar, bool>,
 }
 
 impl Default for Trail {
 	fn default() -> Self {
 		Self {
 			trail: Vec::new(),
+			pos: 0,
 			prev_len: Vec::new(),
 			int_value: IndexVec::new(),
 			sat_value: HashMap::new(),
+			sat_restore_value: HashMap::new(),
 		}
 	}
 }
 
 impl Trail {
 	fn push_trail(&mut self, event: TrailEvent) {
+		debug_assert_eq!(self.pos, self.trail.len());
 		match event {
 			TrailEvent::SatAssignment(r) => {
 				let r = i32::from(r);
@@ -48,43 +54,120 @@ impl Trail {
 				self.trail.push(i as u32)
 			}
 		}
+		self.pos = self.trail.len();
 	}
-	fn pop_trail(&mut self) -> Option<TrailEvent> {
-		if self.trail.is_empty() {
+	fn undo<const RESTORE: bool>(&mut self) -> Option<TrailEvent> {
+		debug_assert!(self.pos <= self.trail.len());
+		if self.pos == 0 {
 			return None;
 		}
-		let i = self.trail.pop().unwrap() as i32;
-		Some(if i.is_positive() {
+		// Find event before current position
+		let i = self.trail[self.pos - 1] as i32;
+		let event = if i.is_positive() {
+			self.pos -= 1;
 			// SAFETY: This is safe because RawVar uses the same representation as i32
 			TrailEvent::SatAssignment(unsafe { transmute(i) })
 		} else {
 			let i = -i as usize;
-			let high = self.trail.pop().unwrap() as u64;
-			let low = self.trail.pop().unwrap() as u64;
+			let high = self.trail[self.pos - 2] as u64;
+			let low = self.trail[self.pos - 3] as u64;
+			self.pos -= 3;
 			TrailEvent::IntAssignment(i.into(), ((high << 32) | low) as i64)
-		})
+		};
+
+		match event {
+			TrailEvent::SatAssignment(r) => {
+				let b = self.sat_value.remove(&r).unwrap();
+				if RESTORE {
+					let x = self.sat_restore_value.insert(r, b);
+					debug_assert!(x.is_none());
+				}
+			}
+			TrailEvent::IntAssignment(i, v) => {
+				if RESTORE {
+					self.trail.swap(self.pos, self.pos + 2);
+				}
+				self.int_value[i] = v;
+			}
+		}
+		Some(event)
 	}
-	fn undo_event(&mut self, event: TrailEvent) {
+
+	fn redo(&mut self) -> Option<TrailEvent> {
+		debug_assert!(self.pos <= self.trail.len());
+
+		if self.pos == self.trail.len() {
+			return None;
+		}
+		// Find event at current position
+		let i = self.trail[self.pos] as i32;
+		let event = if i.is_positive() {
+			self.pos += 1;
+			// SAFETY: This is safe because RawVar uses the same representation as i32
+			TrailEvent::SatAssignment(unsafe { transmute(i) })
+		} else {
+			let i = -i as usize;
+			let high = self.trail[self.pos + 1] as u64;
+			let low = self.trail[self.pos + 2] as u64;
+			self.pos += 3;
+			TrailEvent::IntAssignment(i.into(), ((high << 32) | low) as i64)
+		};
+
 		match event {
 			TrailEvent::SatAssignment(r) => {
-				let _ = self.sat_value.remove(&r);
+				let b = self.sat_restore_value.remove(&r).unwrap();
+				let x = self.sat_value.insert(r, b);
+				debug_assert!(x.is_none());
 			}
 			TrailEvent::IntAssignment(i, v) => {
+				self.trail.swap(self.pos - 1, self.pos - 3);
 				self.int_value[i] = v;
 			}
 		}
+		Some(event)
 	}
 
 	pub(crate) fn undo_until_found_lit(&mut self, lit: RawLit) {
 		let var = lit.var();
-		while let Some(event) = self.pop_trail() {
+		if !self.sat_value.contains_key(&var) {
+			if !self.sat_restore_value.contains_key(&var) {
+				panic!("literal is not present in the trail")
+			}
+			debug!(
+				lit = i32::from(lit),
+				"literal is already unset, restoring to point of setting literal"
+			);
+			while let Some(event) = self.redo() {
+				let found = matches!(event, TrailEvent::SatAssignment(r) if r == var);
+				if found {
+					trace!(
+						len = self.pos,
+						lit = i32::from(lit),
+						"reversed the trail to find literal"
+					);
+					return;
+				}
+			}
+			unreachable!("literal not on trail")
+		}
+		while let Some(event) = self.undo::<true>() {
 			let found = matches!(event, TrailEvent::SatAssignment(r) if r == var);
-			self.undo_event(event);
 			if found {
+				let e = self.redo();
+				debug_assert_eq!(e, Some(TrailEvent::SatAssignment(var)));
+				trace!(
+					len = self.pos,
+					lit = i32::from(lit),
+					"reversed the trail to find literal"
+				);
 				return;
 			}
 		}
-		panic!("literal {:?} was never assigned", lit)
+		unreachable!("literal not on trail")
+	}
+
+	pub(crate) fn is_backtracking(&self) -> bool {
+		self.pos != self.trail.len()
 	}
 
 	pub(crate) fn notify_new_decision_level(&mut self) {
@@ -98,11 +181,18 @@ impl Trail {
 			"backtracking to level {level} length {len}, but trail is already at length {}",
 			self.trail.len()
 		);
-		while self.trail.len() > len {
-			let event = self.pop_trail().unwrap();
-			self.undo_event(event);
+		if len <= self.pos {
+			while self.pos > len {
+				let _ = self.undo::<false>();
+			}
+		} else {
+			while self.pos < len {
+				let _ = self.redo();
+			}
 		}
-		debug_assert_eq!(self.trail.len(), len);
+		debug_assert_eq!(self.pos, len);
+		self.trail.truncate(len);
+		self.sat_restore_value.clear();
 	}
 	pub(crate) fn decision_level(&self) -> usize {
 		self.prev_len.len()
@@ -158,38 +248,51 @@ mod tests {
 	use pindakaas::solver::{cadical::Cadical, NextVarRange};
 
 	use crate::{
-		solver::engine::trail::{Trail, TrailEvent, TrailedInt},
+		solver::engine::trail::{Trail, TrailEvent},
 		IntVal,
 	};
 
 	#[test]
 	fn test_trail_event() {
 		let mut slv = Cadical::default();
+		let mut trail = Trail::default();
 		let lits = slv.next_var_range(10).unwrap();
-		let int_events: [(u32, IntVal); 10] = [
-			(0, 0),
-			(1, 1),
-			(2, -1),
-			(i32::MAX as u32, IntVal::MAX),
-			(9474, IntVal::MIN),
-			(6966, 4084),
-			(4099, -9967),
-			(1977, 9076),
-			(2729, -4312),
-			(941, 1718),
-		];
+		let int_events: Vec<_> = [
+			0,
+			1,
+			-1,
+			IntVal::MAX,
+			IntVal::MIN,
+			4084,
+			-9967,
+			9076,
+			-4312,
+			1718,
+		]
+		.into_iter()
+		.map(|i| (trail.track_int(0), i))
+		.collect();
 
-		let mut trail = Trail::default();
 		for (l, (i, v)) in lits.clone().zip(int_events.iter()) {
 			trail.push_trail(TrailEvent::SatAssignment(l));
-			trail.push_trail(TrailEvent::IntAssignment(TrailedInt::from_raw(*i), *v));
+			let _ = trail.assign_sat(if usize::from(*i) % 2 == 0 {
+				l.into()
+			} else {
+				!l
+			});
+			trail.push_trail(TrailEvent::IntAssignment(*i, *v));
 		}
 		for (l, (i, v)) in lits.rev().zip(int_events.iter().rev()) {
-			assert_eq!(
-				trail.pop_trail().unwrap(),
-				TrailEvent::IntAssignment(TrailedInt::from_raw(*i), *v)
-			);
-			assert_eq!(trail.pop_trail().unwrap(), TrailEvent::SatAssignment(l))
+			let e = trail.undo::<true>().unwrap();
+			assert_eq!(e, TrailEvent::IntAssignment(*i, *v));
+			let r = trail.redo().unwrap();
+			assert_eq!(r, e);
+			let _ = trail.undo::<true>().unwrap();
+			let e = trail.undo::<true>().unwrap();
+			assert_eq!(e, TrailEvent::SatAssignment(l));
+			let r = trail.redo().unwrap();
+			assert_eq!(r, e);
+			let _ = trail.undo::<true>().unwrap();
 		}
 	}
 }