tmp

Cargo.toml

@@ -14,6 +14,7 @@ members = [
   "examples/knapsack",
   "validator",
 ]
+resolver = "2"
 
 [workspace.dependencies]
 anyhow = { version = "1.0"}
@@ -22,6 +23,7 @@ regex = { version = "1" }
 tracing = { version = "0.1", features = ["release_max_level_debug"] }
 tracing-subscriber = "0.3"
 itertools = { version = "0.11.0" }
+rand = { version = "0.8.5", features = ["small_rng"] }
 
 [profile.dev]
 opt-level = 0

solver/Cargo.toml

@@ -29,6 +29,7 @@ smallvec = "1.4.2"
 num-integer = { default-features = false, version = "0.1.44" }
 tracing = { workspace = true }
 lru = "0.10.0"
+rand = {  workspace = true }
 
 [dev-dependencies]
 rand = "0.8"

solver/src/backtrack/queues.rs

@@ -214,6 +214,7 @@ impl<V> ObsTrail<V> {
         ObsTrailCursor {
             next_read: EventIndex::from(0u32),
             last_backtrack: None,
+            pristine: true,
             _phantom: Default::default(),
         }
     }
@@ -420,6 +421,7 @@ pub struct TrailEvent<'a, V> {
 pub struct ObsTrailCursor<V> {
     next_read: EventIndex,
     last_backtrack: Option<u64>,
+    pristine: bool,
     _phantom: PhantomData<V>,
 }
 
@@ -437,10 +439,19 @@ impl<V> ObsTrailCursor<V> {
         ObsTrailCursor {
             next_read: EventIndex::from(0u32),
             last_backtrack: None,
+            pristine: true,
             _phantom: Default::default(),
         }
     }
 
+    pub fn is_pristine(&self) -> bool {
+        self.pristine
+    }
+
+    pub fn mark_used(&mut self) {
+        self.pristine = false
+    }
+
     // TODO: check correctness if more than one backtrack occurred between two synchronisations
     fn sync_backtrack(&mut self, queue: &ObsTrail<V>) {
         if let Some(x) = &queue.last_backtrack {
@@ -468,6 +479,7 @@ impl<V> ObsTrailCursor<V> {
     }
 
     pub fn pop<'q>(&mut self, queue: &'q ObsTrail<V>) -> Option<&'q V> {
+        self.mark_used();
         self.sync_backtrack(queue);
 
         let next = self.next_read;
@@ -480,6 +492,7 @@ impl<V> ObsTrailCursor<V> {
     }
 
     pub fn move_to_end(&mut self, queue: &ObsTrail<V>) {
+        self.mark_used();
         self.sync_backtrack(queue);
         self.next_read = queue.next_slot();
     }

solver/src/core/state/int_domains.rs

@@ -102,10 +102,12 @@ impl IntDomains {
                     new_value: new,
                     previous: current,
                 };
+                // println!("UPDATE: {lit:?} {cause:?}");
                 self.events.push(event);
                 // update occurred and is consistent
                 Ok(true)
             } else {
+                // println!("INVALID UPDATE: {lit:?} {cause:?}");
                 Err(InvalidUpdate(lit, cause))
             }
         }

solver/src/core/variable.rs

@@ -5,13 +5,13 @@ use std::{fmt::Debug, hash::Hash};
 /// Type representing an integer constant.
 pub type IntCst = i32;
 
-/// Overflow tolerant min value for integer constants.
-/// It is used as a default for the lower bound of integer variable domains
-pub const INT_CST_MIN: IntCst = IntCst::MIN / 4;
-
 /// Overflow tolerant max value for integer constants.
 /// It is used as a default for the upper bound of integer variable domains
-pub const INT_CST_MAX: IntCst = IntCst::MAX / 4;
+pub const INT_CST_MAX: IntCst = IntCst::MAX / 4 - 1;
+
+/// Overflow tolerant min value for integer constants.
+/// It is used as a default for the lower bound of integer variable domains
+pub const INT_CST_MIN: IntCst = -INT_CST_MAX;
 
 create_ref_type!(VarRef);
 

solver/src/model/extensions/format.rs

@@ -4,6 +4,7 @@ use crate::model::lang::{Atom, FAtom, IAtom, IVar, Kind, SAtom, Type};
 use crate::model::symbols::{SymId, SymbolTable};
 use crate::model::types::TypeId;
 use crate::model::ModelShape;
+use crate::reif::{DifferenceExpression, ReifExpr};
 use crate::utils::input::Sym;
 use crate::utils::Fmt;
 
@@ -40,6 +41,10 @@ where
     fn get_symbol_table(&self) -> &SymbolTable {
         &self.get_shape().symbols
     }
+
+    fn get_reified_expr(&self, lit: Lit) -> Option<&ReifExpr> {
+        self.get_shape().expressions.original(lit)
+    }
 }
 
 /// Wraps an atom into a custom object that can be formatted with the standard library `Display`
@@ -78,6 +83,8 @@ fn format_impl_bool<Lbl: Label>(ctx: &impl Shaped<Lbl>, b: Lit, f: &mut std::fmt
         write!(f, "true")
     } else if b == Lit::FALSE {
         write!(f, "false")
+    } else if let Some(reified) = ctx.get_reified_expr(b) {
+        format_reif(ctx, reified, f)
     } else if let Some(Type::Bool) = tpe {
         if b == t {
             format_impl_var(ctx, b.variable(), Kind::Bool, f)
@@ -153,3 +160,40 @@ fn format_impl_var<Lbl: Label>(
         write!(f, "{}{}", prefix, usize::from(v))
     }
 }
+
+fn format_reif<Lbl: Label>(ctx: &impl Shaped<Lbl>, e: &ReifExpr, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+    match e {
+        ReifExpr::Lit(l) => format_impl_bool(ctx, *l, f),
+        ReifExpr::MaxDiff(DifferenceExpression { a, b, ub }) => {
+            format_impl_var(ctx, *b, Kind::Sym, f)?;
+            write!(f, " - ")?;
+            format_impl_var(ctx, *a, Kind::Sym, f)?;
+            write!(f, " <= {ub}")
+        }
+        ReifExpr::Eq(v1, v2) => {
+            format_impl_var(ctx, *v1, Kind::Sym, f)?;
+            write!(f, " = ")?;
+            format_impl_var(ctx, *v2, Kind::Sym, f)
+        }
+        ReifExpr::Neq(v1, v2) => {
+            format_impl_var(ctx, *v1, Kind::Sym, f)?;
+            write!(f, " != ")?;
+            format_impl_var(ctx, *v2, Kind::Sym, f)
+        }
+        ReifExpr::EqVal(v1, v2) => {
+            format_impl_var(ctx, *v1, Kind::Sym, f)?;
+            let sym_id = SymId::from_u32(*v2 as u32);
+            let sym = ctx.get_symbol(sym_id);
+            write!(f, " = {sym}")
+        }
+        ReifExpr::NeqVal(v1, v2) => {
+            format_impl_var(ctx, *v1, Kind::Sym, f)?;
+            let sym_id = SymId::from_u32(*v2 as u32);
+            let sym = ctx.get_symbol(sym_id);
+            write!(f, " != {sym}")
+        }
+        ReifExpr::Or(_) => todo!(),
+        ReifExpr::And(_) => todo!(),
+        ReifExpr::Linear(_) => todo!(),
+    }
+}

solver/src/model/lang/reification.rs

@@ -9,6 +9,7 @@ use std::collections::HashMap;
 pub struct Reification {
     /// Associates each canonical atom to a single literal.
     map: HashMap<ReifExpr, Lit>,
+    inv: HashMap<Lit, ReifExpr>,
 }
 
 impl Reification {
@@ -25,7 +26,13 @@ impl Reification {
     pub fn intern_as(&mut self, e: ReifExpr, lit: Lit) {
         assert!(!self.map.contains_key(&e));
         self.map.insert(e.clone(), lit);
-        self.map.insert(!e, !lit);
+        self.map.insert(!e.clone(), !lit);
+        self.inv.insert(lit, e.clone());
+        self.inv.insert(!lit, !e.clone());
+    }
+
+    pub fn original(&self, lit: Lit) -> Option<&ReifExpr> {
+        self.inv.get(&lit)
     }
 }
 

solver/src/reasoners/eq/domain.rs

@@ -35,15 +35,24 @@ impl Domain {
         self.value_literals.push(lit);
     }
 
-    pub fn get(&self, value: IntCst) -> Lit {
-        debug_assert!(self.bounds().contains(&value));
-        self.value_literals[(value - self.first_value) as usize]
+    pub fn get(&self, value: IntCst) -> Option<Lit> {
+        if !self.bounds().contains(&value) {
+            None
+        } else {
+            Some(self.value_literals[(value - self.first_value) as usize])
+        }
     }
 
     fn values(&self, first: IntCst, last: IntCst) -> &[Lit] {
-        let first = (first - self.first_value) as usize;
-        let last = (last - self.first_value) as usize;
-        &self.value_literals[first..=last]
+        let first = (first as i64 - self.first_value as i64).max(0) as usize;
+        if let Ok(last) = usize::try_from(last as i64 - self.first_value as i64) {
+            let last = last.min(self.value_literals.len() - 1);
+            &self.value_literals[first..=last]
+        } else {
+            // last is before the start of the slice
+            // return empty slice
+            &self.value_literals[0..0]
+        }
     }
 }
 
@@ -75,7 +84,7 @@ impl Domains {
         self.neq_watches.watches_on(l)
     }
 
-    pub fn value(&self, v: SignedVar, value: IntCst) -> Lit {
+    pub fn value(&self, v: SignedVar, value: IntCst) -> Option<Lit> {
         let dom = &self.domains[&v.variable()];
         if v.is_plus() {
             dom.get(value)