From 7d648249a2fd358f6325df50e8101902e7b75622 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 6 Aug 2024 10:13:20 +1000 Subject: [PATCH] Workaround an issue where Cadical might backtrack to an unknown level This happens when Cadical uses the vivify in-processing techniques --- crates/huub/src/solver/engine/trail.rs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/crates/huub/src/solver/engine/trail.rs b/crates/huub/src/solver/engine/trail.rs index 594f2877..78db05f6 100644 --- a/crates/huub/src/solver/engine/trail.rs +++ b/crates/huub/src/solver/engine/trail.rs @@ -5,7 +5,7 @@ use std::{ use index_vec::IndexVec; use pindakaas::{Lit as RawLit, Var as RawVar}; -use tracing::{debug, trace}; +use tracing::{debug, trace, warn}; use crate::{actions::trailing::TrailingActions, IntVal}; @@ -163,6 +163,16 @@ impl Trail { self.prev_len.push(self.trail.len()); } pub(crate) fn notify_backtrack(&mut self, level: usize) { + // TODO: this is a fix for an issue in the Cadical implementation of the IPASIR UP interface: https://github.com/arminbiere/cadical/issues/92 + if level >= self.prev_len.len() { + warn!( + current = self.prev_len.len(), + requested = level, + "backtrack to unknown level" + ); + return; + } + let len = self.prev_len[level]; self.prev_len.truncate(level); debug_assert!(