semitone/
lib.rs

1#![doc = include_str!("../README.md")]
2
3//! # API overview
4//! [`SeMiTONE`] owns all solver state. Create expressions with the types in
5//! [`ast`], assert a [`ast::BoolExpr`], then call [`SeMiTONE::propagate`] after
6//! each assertion or decision. Applications that need a complete SAT/SMT search
7//! loop can use the decision, trail, and clause APIs exposed by [`SeMiTONE`].
8
9pub mod ast;
10mod dl_theory;
11mod enum_theory;
12mod euf_theory;
13mod lra_theory;
14#[cfg(feature = "parser")]
15pub mod parser;
16mod proxy;
17pub mod rational;
18mod sat_solver;
19#[cfg(feature = "solver")]
20pub mod solver;
21
22use crate::{
23    ast::{ArithExpr, BoolExpr, BoolVar, DlVar, EnumExpr, EnumVar, EufExpr, EufNode, Expr, FuncId, IntVar, RealVar},
24    dl_theory::DlTheory,
25    enum_theory::EnumTheory,
26    euf_theory::EufTheory,
27    lra_theory::{LraTheory, SparseRow, tighten_int_bound},
28    proxy::{ProxyRegistry, TheoryConstraint},
29    rational::{InfRational, Rational},
30    sat_solver::SatSolver,
31};
32use rug::Assign;
33pub use sat_solver::Lit;
34use tracing::trace;
35
36/// Main solver entry point for propositional, linear arithmetic, and enum constraints.
37///
38/// The solver combines a SAT core with theory propagation for linear rational
39/// arithmetic and finite-domain enum reasoning.
40pub struct SeMiTONE {
41    registry: ProxyRegistry,
42    sat_solver: SatSolver,
43    lra_theory: LraTheory,
44    enum_theory: EnumTheory,
45    dl_theory: DlTheory,
46    euf_theory: EufTheory,
47    notified_len: usize,
48    user_scopes: Vec<(usize, usize)>,
49}
50
51impl Default for SeMiTONE {
52    fn default() -> Self {
53        Self::new()
54    }
55}
56
57impl SeMiTONE {
58    /// Creates a new empty solver instance.
59    pub fn new() -> Self {
60        Self {
61            registry: ProxyRegistry::new(),
62            sat_solver: SatSolver::new(),
63            lra_theory: LraTheory::new(),
64            enum_theory: EnumTheory::new(),
65            dl_theory: DlTheory::new(),
66            euf_theory: EufTheory::new(),
67            notified_len: 0,
68            user_scopes: Vec::new(),
69        }
70    }
71
72    /// Allocates a new SAT literal.
73    pub fn new_lit(&mut self) -> Lit {
74        Lit::new(self.sat_solver.mk_var(), false)
75    }
76
77    /// Allocates a new Boolean variable.
78    pub fn new_bool(&mut self) -> BoolExpr {
79        BoolExpr::Var(BoolVar(self.sat_solver.mk_var()))
80    }
81
82    /// Allocates a new integer variable.
83    pub fn new_int(&mut self) -> ArithExpr {
84        ArithExpr::IntVar(IntVar(self.lra_theory.mk_int()))
85    }
86
87    /// Allocates a new real variable.
88    pub fn new_real(&mut self) -> ArithExpr {
89        ArithExpr::RealVar(RealVar(self.lra_theory.mk_real()))
90    }
91
92    /// Allocates a new enum variable with the given finite domain.
93    pub fn new_enum(&mut self, domain: impl IntoIterator<Item = i32>) -> EnumExpr {
94        EnumExpr::Var(EnumVar(self.enum_theory.mk_var(domain.into_iter().collect())))
95    }
96
97    /// Allocates a new difference logic variable.
98    pub fn new_dl_var(&mut self) -> DlVar {
99        DlVar(self.dl_theory.new_var())
100    }
101
102    /// Allocates a new EUF variable.
103    pub fn new_euf_var(&mut self) -> EufExpr {
104        EufExpr::Var(EufNode(self.euf_theory.new_var()))
105    }
106
107    /// Allocates a new uninterpreted function symbol.
108    pub fn new_euf_func(&mut self) -> FuncId {
109        FuncId(self.euf_theory.new_func_id())
110    }
111
112    /// Allocates a new EUF function application with the given function ID and arguments.
113    pub fn new_euf_app(&mut self, func_id: FuncId, args: Vec<Expr>) -> EufExpr {
114        let mut internal_args = Vec::with_capacity(args.len());
115        for arg in &args {
116            if let Expr::Euf(euf_arg) = arg {
117                let node_id = match euf_arg {
118                    EufExpr::Var(node) => node.0,
119                    EufExpr::App(node, _, _) => node.0,
120                };
121                internal_args.push(node_id);
122            } else {
123                panic!("EUF application arguments must be EUF expressions, but got: {:?}", arg);
124            }
125        }
126
127        let node_id = self.euf_theory.new_app(func_id.0, internal_args);
128        EufExpr::App(EufNode(node_id), func_id, args)
129    }
130
131    /// Returns the current number of SAT variables allocated in the solver core.
132    ///
133    /// This includes user-visible Boolean variables and internal proxy variables
134    /// introduced while encoding compound constraints.
135    pub fn num_vars(&self) -> usize {
136        self.sat_solver.num_vars()
137    }
138
139    /// Adds a clause directly to the SAT core.
140    ///
141    /// Returns `Ok(())` when the clause is accepted, or `Err(conflict_clause)` if
142    /// the clause is immediately contradictory at the current root context.
143    ///
144    /// This is useful for integrating external search/learning loops that produce
145    /// learned no-goods.
146    pub fn add_clause(&mut self, clause: impl IntoIterator<Item = Lit>) -> Result<(), Vec<Lit>> {
147        self.sat_solver.add_clause(clause)
148    }
149
150    /// Adds a Boolean constraint to the current solver context.
151    ///
152    /// Returns `true` if the assertion was successfully added, or `false` if it
153    /// led to an immediate, trivial conflict while translating/asserting.
154    ///
155    /// Note that `true` does not imply global feasibility: call [`SeMiTONE::propagate`]
156    /// to detect conflicts that emerge after propagation through SAT/theory state.
157    pub fn assert(&mut self, expr: impl AsRef<BoolExpr>) -> bool {
158        self.assert_internal(expr.as_ref(), true)
159    }
160
161    fn assert_internal(&mut self, expr: &BoolExpr, polarity: bool) -> bool {
162        match (expr, polarity) {
163            (BoolExpr::Not(inner), _) => self.assert_internal(inner, !polarity),
164            (BoolExpr::And(args), true) | (BoolExpr::Or(args), false) => {
165                for arg in args {
166                    if !self.assert_internal(arg, polarity) {
167                        return false;
168                    }
169                }
170                true
171            }
172            (BoolExpr::Or(args), true) | (BoolExpr::And(args), false) => {
173                let mut clause = Vec::with_capacity(args.len());
174                for arg in args {
175                    let mut lit = self.encode_bool(arg);
176                    if !polarity {
177                        lit = !lit;
178                    }
179                    clause.push(lit);
180                }
181                self.sat_solver.add_clause(clause).is_ok()
182            }
183            (BoolExpr::Lt(e1, e2), _) | (BoolExpr::Le(e1, e2), _) | (BoolExpr::Ge(e1, e2), _) | (BoolExpr::Gt(e1, e2), _) => {
184                let (vars, const_term) = self.diff(e1, e2);
185                if vars.is_empty() {
186                    let is_sat = match expr {
187                        BoolExpr::Lt(_, _) => const_term.is_negative(),
188                        BoolExpr::Le(_, _) => const_term.is_negative() || const_term.is_zero(),
189                        BoolExpr::Ge(_, _) => !const_term.is_negative(),
190                        BoolExpr::Gt(_, _) => const_term.is_positive(),
191                        _ => unreachable!(),
192                    };
193                    return if polarity { is_sat } else { !is_sat };
194                }
195
196                let (is_upper_bound, is_strict) = match (expr, polarity) {
197                    (BoolExpr::Lt(_, _), true) => (true, true),
198                    (BoolExpr::Lt(_, _), false) => (false, false),
199                    (BoolExpr::Le(_, _), true) => (true, false),
200                    (BoolExpr::Le(_, _), false) => (false, true),
201                    (BoolExpr::Ge(_, _), true) => (false, false),
202                    (BoolExpr::Ge(_, _), false) => (true, true),
203                    (BoolExpr::Gt(_, _), true) => (false, true),
204                    (BoolExpr::Gt(_, _), false) => (true, false),
205                    _ => unreachable!(),
206                };
207
208                if vars.len() == 1 {
209                    let (var, coeff) = vars.iter().next().unwrap();
210                    let is_int = self.lra_theory.is_int_var(*var);
211                    let is_upper_for_var = is_upper_bound == coeff.is_positive();
212
213                    let bound = if is_int {
214                        let val = -const_term / coeff.clone();
215                        let tight_val = tighten_int_bound(val, is_upper_for_var, is_strict);
216                        InfRational::new(Rational::Finite(tight_val), rug::Rational::from(0))
217                    } else {
218                        let eps_shift = if is_strict { if is_upper_bound { rug::Rational::from(-1) } else { rug::Rational::from(1) } } else { rug::Rational::from(0) };
219                        InfRational::new(Rational::Finite(-const_term / coeff.clone()), eps_shift / coeff)
220                    };
221
222                    if is_upper_for_var { self.lra_theory.set_ub(None, *var, bound).is_ok() } else { self.lra_theory.set_lb(None, *var, bound).is_ok() }
223                } else {
224                    let slack = self.lra_theory.get_or_create_slack(vars);
225                    let is_int = self.lra_theory.is_int_var(slack);
226
227                    let bound = if is_int {
228                        let tight_val = tighten_int_bound(-const_term, is_upper_bound, is_strict);
229                        InfRational::new(Rational::Finite(tight_val), rug::Rational::from(0))
230                    } else {
231                        let eps_shift = if is_strict { if is_upper_bound { rug::Rational::from(-1) } else { rug::Rational::from(1) } } else { rug::Rational::from(0) };
232                        InfRational::new(Rational::Finite(-const_term), eps_shift)
233                    };
234
235                    if is_upper_bound { self.lra_theory.set_ub(None, slack, bound).is_ok() } else { self.lra_theory.set_lb(None, slack, bound).is_ok() }
236                }
237            }
238            (BoolExpr::Eq(e1, e2), _) => {
239                if let (Expr::Arith(a1), Expr::Arith(a2)) = (&**e1, &**e2) {
240                    let (vars, const_term) = self.diff(a1, a2);
241
242                    if vars.is_empty() {
243                        let is_sat = const_term.is_zero();
244                        return if polarity { is_sat } else { !is_sat };
245                    }
246
247                    if polarity {
248                        let bound = InfRational::new(Rational::Finite(-const_term), rug::Rational::from(0));
249
250                        if vars.len() == 1 {
251                            let (var, coeff) = vars.iter().next().unwrap();
252                            let final_bound = bound / coeff.clone();
253                            self.lra_theory.set_lb(None, *var, final_bound.clone()).is_ok() && self.lra_theory.set_ub(None, *var, final_bound).is_ok()
254                        } else {
255                            let slack = self.lra_theory.get_or_create_slack(vars);
256                            self.lra_theory.set_lb(None, slack, bound.clone()).is_ok() && self.lra_theory.set_ub(None, slack, bound).is_ok()
257                        }
258                    } else {
259                        let lt_lit = self.mk_le(a1, a2, true);
260                        let gt_lit = self.mk_ge(a1, a2, true);
261                        self.sat_solver.add_clause([lt_lit, gt_lit]).is_ok()
262                    }
263                } else {
264                    let mut lit = self.encode_eq(e1, e2);
265                    if !polarity {
266                        lit = !lit;
267                    }
268                    self.sat_solver.add_clause([lit]).is_ok()
269                }
270            }
271            _ => {
272                let mut lit = self.encode_bool(expr);
273                if !polarity {
274                    lit = !lit;
275                }
276                self.sat_solver.add_clause([lit]).is_ok()
277            }
278        }
279    }
280
281    /// Encodes a Boolean expression and returns its equivalent SAT literal.
282    ///
283    /// The returned literal may refer to an internal proxy variable. Encoding
284    /// a compound expression can therefore add auxiliary variables and
285    /// clauses to the solver. The literal preserves the expression's polarity
286    /// and can be inspected with [`SeMiTONE::get_lit_val`] or used with
287    /// [`SeMiTONE::decide`]. This method does not assert the expression.
288    pub fn track_expr(&mut self, expr: impl AsRef<BoolExpr>) -> Lit {
289        self.encode_bool(expr.as_ref())
290    }
291
292    fn encode_bool(&mut self, expr: &BoolExpr) -> Lit {
293        match expr {
294            BoolExpr::True => Lit::TRUE,
295            BoolExpr::False => Lit::FALSE,
296            BoolExpr::Var(v) => Lit::new(v.0, false),
297            BoolExpr::Not(inner) => match inner.as_ref() {
298                BoolExpr::Lt(a1, a2) => self.mk_ge(a1, a2, false),
299                BoolExpr::Le(a1, a2) => self.mk_ge(a1, a2, true),
300                BoolExpr::Ge(a1, a2) => self.mk_le(a1, a2, true),
301                BoolExpr::Gt(a1, a2) => self.mk_le(a1, a2, false),
302                BoolExpr::DlLt(f, t, b) => self.mk_dl_ge(f.0, t.0, b.clone(), false), // !(x < y) => x >= y
303                BoolExpr::DlLe(f, t, b) => self.mk_dl_ge(f.0, t.0, b.clone(), true),  // !(x <= y) => x > y
304                BoolExpr::DlGe(f, t, b) => self.mk_dl_le(f.0, t.0, b.clone(), true),  // !(x >= y) => x < y
305                BoolExpr::DlGt(f, t, b) => self.mk_dl_le(f.0, t.0, b.clone(), false), // !(x > y) => x <= y
306                _ => !self.encode_bool(inner),
307            },
308            BoolExpr::And(terms) => {
309                let mut lits = Vec::with_capacity(terms.len());
310                for term in terms {
311                    lits.push(self.encode_bool(term));
312                }
313
314                let proxy_var = self.sat_solver.mk_var();
315                let proxy_lit = Lit::new(proxy_var, true);
316
317                for &lit in &lits {
318                    self.sat_solver.add_clause([!proxy_lit, lit]).expect("Failed to add clause");
319                }
320
321                let mut big_clause: Vec<Lit> = lits.into_iter().map(|l| !l).collect();
322                big_clause.push(proxy_lit);
323                self.sat_solver.add_clause(big_clause).expect("Failed to add clause");
324
325                proxy_lit
326            }
327            BoolExpr::Or(terms) => {
328                let mut lits = Vec::with_capacity(terms.len());
329                for term in terms {
330                    lits.push(self.encode_bool(term));
331                }
332
333                let proxy_var = self.sat_solver.mk_var();
334                let proxy_lit = Lit::new(proxy_var, true);
335
336                for &lit in &lits {
337                    self.sat_solver.add_clause([!lit, proxy_lit]).expect("Failed to add clause");
338                }
339
340                let mut big_clause = lits;
341                big_clause.push(!proxy_lit);
342                self.sat_solver.add_clause(big_clause).expect("Failed to add clause");
343
344                proxy_lit
345            }
346            BoolExpr::Lt(e1, e2) => self.mk_le(e1, e2, true),
347            BoolExpr::Le(e1, e2) => self.mk_le(e1, e2, false),
348            BoolExpr::Ge(e1, e2) => self.mk_ge(e1, e2, false),
349            BoolExpr::Gt(e1, e2) => self.mk_ge(e1, e2, true),
350            BoolExpr::Eq(e1, e2) => self.encode_eq(e1, e2),
351            BoolExpr::DlLt(from, to, b) => self.mk_dl_le(from.0, to.0, b.clone(), true),
352            BoolExpr::DlLe(from, to, b) => self.mk_dl_le(from.0, to.0, b.clone(), false),
353            BoolExpr::DlGt(from, to, b) => self.mk_dl_ge(from.0, to.0, b.clone(), true),
354            BoolExpr::DlGe(from, to, b) => self.mk_dl_ge(from.0, to.0, b.clone(), false),
355            BoolExpr::DlEq(from, to, b) => self.mk_dl_eq(from.0, to.0, b.clone()),
356        }
357    }
358
359    fn encode_eq(&mut self, expr1: &Expr, expr2: &Expr) -> Lit {
360        match (expr1, expr2) {
361            (Expr::Arith(a1), Expr::Arith(a2)) => self.mk_arith_eq(a1, a2),
362            (Expr::Bool(b1), Expr::Bool(b2)) => {
363                let l1 = self.encode_bool(b1);
364                let l2 = self.encode_bool(b2);
365                let proxy_var = self.sat_solver.mk_var();
366                let p = Lit::new(proxy_var, true);
367
368                self.sat_solver.add_clause([!p, l1, !l2]).expect("Failed to add clause");
369                self.sat_solver.add_clause([!p, !l1, l2]).expect("Failed to add clause");
370                self.sat_solver.add_clause([p, l1, l2]).expect("Failed to add clause");
371                self.sat_solver.add_clause([p, !l1, !l2]).expect("Failed to add clause");
372
373                p
374            }
375            (Expr::Enum(e1), Expr::Enum(e2)) => self.mk_enum_eq(e1, e2),
376            (Expr::Euf(u1), Expr::Euf(u2)) => {
377                let id1 = match u1 {
378                    crate::ast::EufExpr::Var(n) => n.0,
379                    crate::ast::EufExpr::App(n, _, _) => n.0,
380                };
381                let id2 = match u2 {
382                    crate::ast::EufExpr::Var(n) => n.0,
383                    crate::ast::EufExpr::App(n, _, _) => n.0,
384                };
385
386                if id1 == id2 {
387                    return Lit::TRUE;
388                }
389
390                let (min_id, max_id) = if id1 < id2 { (id1, id2) } else { (id2, id1) };
391
392                self.get_or_create_proxy(TheoryConstraint::EufEq(min_id, max_id))
393            }
394            _ => panic!("Type mismatch in Eq: cannot compare different domains.\nLeft: {:?}\nRight: {:?}", expr1, expr2),
395        }
396    }
397
398    fn mk_enum_eq(&mut self, e1: &EnumExpr, e2: &EnumExpr) -> Lit {
399        match (e1, e2) {
400            (EnumExpr::Const(c1), EnumExpr::Const(c2)) => {
401                if c1 == c2 {
402                    Lit::TRUE
403                } else {
404                    Lit::FALSE
405                }
406            }
407            (EnumExpr::Var(v), EnumExpr::Const(c)) | (EnumExpr::Const(c), EnumExpr::Var(v)) => self.get_or_create_proxy(TheoryConstraint::EnumEq(v.0, *c)),
408            (EnumExpr::Var(v1), EnumExpr::Var(v2)) => {
409                if v1 == v2 {
410                    return Lit::TRUE;
411                }
412
413                let domain1 = self.enum_theory.initial_domains[v1.0].clone();
414                let domain2 = self.enum_theory.initial_domains[v2.0].clone();
415                let common: Vec<i32> = domain1.intersection(&domain2).copied().collect();
416
417                if common.is_empty() {
418                    return Lit::FALSE;
419                }
420
421                let mut lits = Vec::with_capacity(common.len());
422                for val in common {
423                    let p1 = self.get_or_create_proxy(TheoryConstraint::EnumEq(v1.0, val));
424                    let p2 = self.get_or_create_proxy(TheoryConstraint::EnumEq(v2.0, val));
425
426                    let and_proxy_var = self.sat_solver.mk_var();
427                    let and_proxy = Lit::new(and_proxy_var, false);
428
429                    self.sat_solver.add_clause([!and_proxy, p1]).unwrap();
430                    self.sat_solver.add_clause([!and_proxy, p2]).unwrap();
431                    self.sat_solver.add_clause([!p1, !p2, and_proxy]).unwrap();
432
433                    lits.push(and_proxy);
434                }
435
436                let or_proxy_var = self.sat_solver.mk_var();
437                let or_proxy = Lit::new(or_proxy_var, false);
438
439                for &lit in &lits {
440                    self.sat_solver.add_clause([!lit, or_proxy]).unwrap();
441                }
442
443                let mut big_clause = lits;
444                big_clause.push(!or_proxy);
445                self.sat_solver.add_clause(big_clause).unwrap();
446
447                or_proxy
448            }
449        }
450    }
451
452    fn mk_le(&mut self, e1: &ArithExpr, e2: &ArithExpr, strict: bool) -> Lit {
453        let (vars, const_term) = self.diff(e1, e2);
454
455        match vars.len() {
456            0 => {
457                if if strict { const_term.is_negative() } else { const_term.is_negative() || const_term.is_zero() } {
458                    Lit::TRUE
459                } else {
460                    Lit::FALSE
461                }
462            }
463            1 => {
464                let (var, coeff) = vars.iter().next().unwrap();
465                let is_int = self.lra_theory.is_int_var(*var);
466                let is_upper_bound = coeff.is_positive();
467
468                let bound = if is_int {
469                    let val = -const_term / coeff.clone();
470                    let tight_val = tighten_int_bound(val, is_upper_bound, strict);
471                    InfRational::new(Rational::Finite(tight_val), rug::Rational::from(0))
472                } else {
473                    let eps_shift = if strict { rug::Rational::from(-1) } else { rug::Rational::from(0) };
474                    InfRational::new(Rational::Finite(-const_term / coeff.clone()), eps_shift / coeff)
475                };
476
477                if self.sat_solver.decision_level() == 0 {
478                    if is_upper_bound {
479                        if self.lra_theory.ub(*var) <= &bound {
480                            return Lit::TRUE;
481                        }
482                        if self.lra_theory.lb(*var) > &bound {
483                            return Lit::FALSE;
484                        }
485                    } else {
486                        if self.lra_theory.lb(*var) >= &bound {
487                            return Lit::TRUE;
488                        }
489                        if self.lra_theory.ub(*var) < &bound {
490                            return Lit::FALSE;
491                        }
492                    }
493                }
494
495                let bound = if is_upper_bound { TheoryConstraint::LraUb(*var, bound) } else { TheoryConstraint::LraLb(*var, bound) };
496                self.get_or_create_proxy(bound)
497            }
498            _ => {
499                let slack = self.lra_theory.get_or_create_slack(vars);
500                let is_int = self.lra_theory.is_int_var(slack);
501
502                let bound = if is_int {
503                    let tight_val = tighten_int_bound(-const_term, true, strict);
504                    InfRational::new(Rational::Finite(tight_val), rug::Rational::from(0))
505                } else {
506                    let eps_shift = if strict { rug::Rational::from(-1) } else { rug::Rational::from(0) };
507                    InfRational::new(Rational::Finite(-const_term), eps_shift)
508                };
509
510                if self.sat_solver.decision_level() == 0 {
511                    if self.lra_theory.ub(slack) <= &bound {
512                        return Lit::TRUE;
513                    }
514                    if self.lra_theory.lb(slack) > &bound {
515                        return Lit::FALSE;
516                    }
517                }
518
519                let bound = TheoryConstraint::LraUb(slack, bound);
520                self.get_or_create_proxy(bound)
521            }
522        }
523    }
524
525    fn mk_arith_eq(&mut self, e1: &ArithExpr, e2: &ArithExpr) -> Lit {
526        if e1 == e2 {
527            return Lit::TRUE;
528        }
529
530        let le_lit = self.mk_le(e1, e2, false);
531        let ge_lit = self.mk_ge(e1, e2, false);
532        if le_lit == Lit::TRUE && ge_lit == Lit::TRUE {
533            return Lit::TRUE;
534        }
535        if le_lit == Lit::FALSE || ge_lit == Lit::FALSE {
536            return Lit::FALSE;
537        }
538
539        let proxy_var = self.sat_solver.mk_var();
540        let p = Lit::new(proxy_var, false);
541
542        // p -> (x <= y)
543        self.sat_solver.add_clause([!p, le_lit]).expect("Failed to add clause");
544        // p -> (x >= y)
545        self.sat_solver.add_clause([!p, ge_lit]).expect("Failed to add clause");
546        // (x <= y) ∧ (x >= y) -> p
547        self.sat_solver.add_clause([!le_lit, !ge_lit, p]).expect("Failed to add clause");
548
549        p
550    }
551
552    fn mk_ge(&mut self, e1: &ArithExpr, e2: &ArithExpr, strict: bool) -> Lit {
553        let (vars, const_term) = self.diff(e1, e2);
554
555        match vars.len() {
556            0 => {
557                if if strict { const_term.is_positive() } else { const_term.is_positive() || const_term.is_zero() } {
558                    Lit::TRUE
559                } else {
560                    Lit::FALSE
561                }
562            }
563            1 => {
564                let (var, coeff) = vars.iter().next().unwrap();
565                let is_int = self.lra_theory.is_int_var(*var);
566
567                let is_upper_bound = !coeff.is_positive();
568
569                let bound = if is_int {
570                    let val = -const_term / coeff.clone();
571                    let tight_val = tighten_int_bound(val, is_upper_bound, strict);
572                    InfRational::new(Rational::Finite(tight_val), rug::Rational::from(0))
573                } else {
574                    let eps_shift = if strict { rug::Rational::from(1) } else { rug::Rational::from(0) };
575                    InfRational::new(Rational::Finite(-const_term / coeff.clone()), eps_shift / coeff)
576                };
577
578                if self.sat_solver.decision_level() == 0 {
579                    if is_upper_bound {
580                        if self.lra_theory.ub(*var) <= &bound {
581                            return Lit::TRUE;
582                        }
583                        if self.lra_theory.lb(*var) > &bound {
584                            return Lit::FALSE;
585                        }
586                    } else {
587                        if self.lra_theory.lb(*var) >= &bound {
588                            return Lit::TRUE;
589                        }
590                        if self.lra_theory.ub(*var) < &bound {
591                            return Lit::FALSE;
592                        }
593                    }
594                }
595
596                let bound = if is_upper_bound { TheoryConstraint::LraUb(*var, bound) } else { TheoryConstraint::LraLb(*var, bound) };
597                self.get_or_create_proxy(bound)
598            }
599            _ => {
600                let slack = self.lra_theory.get_or_create_slack(vars);
601                let is_int = self.lra_theory.is_int_var(slack);
602
603                let bound = if is_int {
604                    let tight_val = tighten_int_bound(-const_term, false, strict);
605                    InfRational::new(Rational::Finite(tight_val), rug::Rational::from(0))
606                } else {
607                    let eps_shift = if strict { rug::Rational::from(1) } else { rug::Rational::from(0) };
608                    InfRational::new(Rational::Finite(-const_term), eps_shift)
609                };
610
611                if self.sat_solver.decision_level() == 0 {
612                    if self.lra_theory.lb(slack) >= &bound {
613                        return Lit::TRUE;
614                    }
615                    if self.lra_theory.ub(slack) < &bound {
616                        return Lit::FALSE;
617                    }
618                }
619
620                let bound = TheoryConstraint::LraLb(slack, bound);
621                self.get_or_create_proxy(bound)
622            }
623        }
624    }
625
626    fn mk_dl_le(&mut self, from: usize, to: usize, bound: rug::Rational, strict: bool) -> Lit {
627        let delta = if strict { rug::Rational::from(-1) } else { rug::Rational::from(0) };
628        let inf_bound = InfRational::new(Rational::Finite(bound), delta);
629
630        let constraint = TheoryConstraint::DlLeq(from, to, inf_bound);
631        self.get_or_create_proxy(constraint)
632    }
633
634    fn mk_dl_ge(&mut self, from: usize, to: usize, bound: rug::Rational, strict: bool) -> Lit {
635        self.mk_dl_le(to, from, -bound, strict)
636    }
637
638    fn mk_dl_eq(&mut self, from: usize, to: usize, bound: rug::Rational) -> Lit {
639        let le_lit = self.mk_dl_le(from, to, bound.clone(), false);
640        let ge_lit = self.mk_dl_ge(from, to, bound, false);
641
642        let proxy_var = self.sat_solver.mk_var();
643        let p = Lit::new(proxy_var, false);
644
645        self.sat_solver.add_clause([!p, le_lit]).expect("Failed to add clause");
646        self.sat_solver.add_clause([!p, ge_lit]).expect("Failed to add clause");
647        self.sat_solver.add_clause([!le_lit, !ge_lit, p]).expect("Failed to add clause");
648
649        p
650    }
651
652    fn diff(&self, e1: &ArithExpr, e2: &ArithExpr) -> (SparseRow, rug::Rational) {
653        let mut vars = SparseRow::new();
654        let mut const_term = rug::Rational::from(0);
655
656        let pos_one = rug::Rational::from(1);
657        let neg_one = rug::Rational::from(-1);
658
659        let mut temp = rug::Rational::new();
660
661        self.accumulate_expr(e1, &pos_one, &mut vars, &mut const_term, &mut temp);
662        self.accumulate_expr(e2, &neg_one, &mut vars, &mut const_term, &mut temp);
663
664        vars.retain(|_, c| *c != 0);
665
666        (vars, const_term)
667    }
668
669    fn accumulate_expr(&self, expr: &ArithExpr, scale: &rug::Rational, vars: &mut SparseRow, const_term: &mut rug::Rational, temp: &mut rug::Rational) {
670        match expr {
671            ArithExpr::Const(c) => {
672                temp.assign(c * scale);
673                *const_term += &*temp;
674            }
675            ArithExpr::IntVar(var) => {
676                self.accumulate_var(var.0, scale, vars, temp);
677            }
678            ArithExpr::RealVar(var) => {
679                self.accumulate_var(var.0, scale, vars, temp);
680            }
681            ArithExpr::Add(terms) => {
682                for term in terms {
683                    self.accumulate_expr(term, scale, vars, const_term, temp);
684                }
685            }
686            ArithExpr::Mul(terms) => {
687                if terms.len() != 2 {
688                    panic!("Only binary multiplication is supported in linear arithmetic");
689                }
690                let (first, second) = (&terms[0], &terms[1]);
691
692                // Smart recursion: accept (Constant * SubExpression)
693                match (first, second) {
694                    (ArithExpr::Const(c), sub_expr) | (sub_expr, ArithExpr::Const(c)) => {
695                        let mut new_scale = rug::Rational::new();
696                        new_scale.assign(c * scale);
697                        self.accumulate_expr(sub_expr, &new_scale, vars, const_term, temp);
698                    }
699                    _ => {
700                        panic!("Non-linear arithmetic: multiplication between two non-constant expressions is not supported");
701                    }
702                }
703            }
704            ArithExpr::Div(numerator, denominator) => {
705                // The denominator MUST be a constant to preserve linearity
706                if let ArithExpr::Const(c) = &**denominator {
707                    if c.is_zero() {
708                        panic!("Division by zero detected in AST");
709                    }
710                    let mut div_scale = rug::Rational::new();
711                    div_scale.assign(scale / c);
712                    self.accumulate_expr(numerator, &div_scale, vars, const_term, temp);
713                } else {
714                    panic!("Non-linear arithmetic: division by a non-constant expression is not supported");
715                }
716            }
717            ArithExpr::Neg(sub_expr) => {
718                let mut neg_scale = rug::Rational::new();
719                neg_scale.assign(scale * -1);
720                self.accumulate_expr(sub_expr, &neg_scale, vars, const_term, temp);
721            }
722        }
723    }
724
725    fn accumulate_var(&self, var: usize, scale: &rug::Rational, vars: &mut SparseRow, temp: &mut rug::Rational) {
726        if let Some(basic_row) = self.lra_theory.tableau.get(&var) {
727            for (sub_var, sub_coeff) in basic_row.iter() {
728                temp.assign(sub_coeff * scale);
729                vars.add_coeff(*sub_var, temp);
730            }
731        } else {
732            vars.add_coeff(var, scale);
733        }
734    }
735
736    fn get_or_create_proxy(&mut self, constraint: TheoryConstraint) -> Lit {
737        if let Some(sat_var) = self.registry.get_proxy(&constraint) {
738            Lit::new(sat_var, false)
739        } else {
740            let sat_var = self.sat_solver.mk_var();
741            self.registry.register(constraint, sat_var);
742            Lit::new(sat_var, false)
743        }
744    }
745
746    /// Adds a decision literal to the current search branch.
747    ///
748    /// This opens a new internal decision level and enqueues `lit` as a decision.
749    /// Returns `false` only if the literal is immediately inconsistent with the
750    /// current assignment.
751    ///
752    /// After a successful decision, call [`SeMiTONE::propagate`] to derive its
753    /// consequences and detect theory conflicts.
754    pub fn decide(&mut self, lit: Lit) -> bool {
755        self.sat_solver.push();
756        self.lra_theory.push();
757        self.enum_theory.push();
758        self.dl_theory.push();
759        self.euf_theory.push();
760        self.sat_solver.enqueue_decision(lit)
761    }
762
763    /// Decides that an enum variable takes a specific value in the current branch.
764    ///
765    /// Convenience wrapper around [`SeMiTONE::decide`]. Returns `false` if the
766    /// decision cannot be enqueued consistently.
767    pub fn decide_enum(&mut self, expr: impl AsRef<EnumExpr>, value: i32) -> bool {
768        let var = match expr.as_ref() {
769            EnumExpr::Var(v) => *v,
770            EnumExpr::Const(_) => panic!("Cannot decide on a constant value"),
771        };
772
773        let lit = self.get_or_create_proxy(TheoryConstraint::EnumEq(var.0, value));
774        self.decide(lit)
775    }
776
777    /// Returns the current internal decision level.
778    ///
779    /// Level `0` corresponds to the root level (no user decision applied).
780    pub fn decision_level(&self) -> usize {
781        self.sat_solver.decision_level()
782    }
783
784    /// Cancels all decisions and theory updates at levels deeper than `level`.
785    ///
786    /// This restores SAT/theory state to the requested level and drops pending
787    /// notifications beyond the restored trail.
788    pub fn cancel_until(&mut self, level: usize) {
789        self.sat_solver.cancel_until(level);
790        self.lra_theory.cancel_until(level);
791        self.enum_theory.cancel_until(level);
792        self.dl_theory.cancel_until(level);
793        self.euf_theory.cancel_until(level);
794        self.notified_len = self.sat_solver.trail.len();
795    }
796
797    /// Returns the trail suffix starting at `from_index`.
798    ///
799    /// Useful for external heuristics that need to inspect newly assigned literals.
800    pub fn get_trail_delta(&self, from_index: usize) -> &[Lit] {
801        &self.sat_solver.trail[from_index..]
802    }
803
804    /// Returns the current size of the SAT assignment trail.
805    pub fn current_trail_len(&self) -> usize {
806        self.sat_solver.trail.len()
807    }
808
809    /// Returns the trail length recorded at a specific decision level.
810    ///
811    /// If `level` is beyond the current number of levels, returns the current
812    /// trail length.
813    pub fn get_trail_len_at_level(&self, level: usize) -> usize {
814        if level < self.sat_solver.trail_lim.len() { self.sat_solver.trail_lim[level] } else { self.sat_solver.trail.len() }
815    }
816
817    /// Returns a slice of the trail between `start` (inclusive) and `end` (exclusive).
818    pub fn get_trail_slice(&self, start: usize, end: usize) -> &[Lit] {
819        &self.sat_solver.trail[start..end]
820    }
821
822    /// Returns the number of currently active user scopes (`push`/`pop`).
823    pub fn user_scopes_len(&self) -> usize {
824        self.user_scopes.len()
825    }
826
827    /// Runs SAT + theory propagation until a fixed point or a conflict.
828    ///
829    /// Returns:
830    /// - `Ok(())` if the current branch is feasible after propagation.
831    /// - `Err((backtrack_level, no_good))` if a conflict is found.
832    ///
833    /// The returned `backtrack_level` is the suggested non-chronological level to
834    /// backtrack to, and `no_good` is a conflict explanation suitable for learning.
835    pub fn propagate(&mut self) -> Result<(), (usize, Vec<Lit>)> {
836        let base_level = self.user_scopes.last().map(|&(lvl, _)| lvl).unwrap_or(0);
837        if let Err((bt_level, conflict)) = self.sat_solver.propagate() {
838            return Err((bt_level.max(base_level), conflict));
839        }
840
841        while self.notified_len < self.sat_solver.trail.len() {
842            let lit = self.sat_solver.trail[self.notified_len];
843
844            if let Some(constraint) = self.registry.get_constraint(lit.var()) {
845                let theory_result = match (constraint, lit.sign()) {
846                    (TheoryConstraint::LraLb(var, bound), false) => self.lra_theory.set_lb(Some(lit), *var, bound.clone()),
847                    (TheoryConstraint::LraLb(var, bound), true) => {
848                        let new_bound = if self.lra_theory.is_int_var(*var) {
849                            if let Rational::Finite(r) = bound.rational_part() {
850                                let tight_val = tighten_int_bound(r.clone(), true, true);
851                                InfRational::new(Rational::Finite(tight_val), rug::Rational::from(0))
852                            } else {
853                                unreachable!()
854                            }
855                        } else {
856                            InfRational::new(bound.rational_part().clone(), if bound.infinitesimal_part().is_positive() { rug::Rational::from(0) } else { rug::Rational::from(-1) })
857                        };
858                        self.lra_theory.set_ub(Some(lit), *var, new_bound)
859                    }
860                    (TheoryConstraint::LraUb(var, bound), false) => self.lra_theory.set_ub(Some(lit), *var, bound.clone()),
861                    (TheoryConstraint::LraUb(var, bound), true) => {
862                        let new_bound = if self.lra_theory.is_int_var(*var) {
863                            if let Rational::Finite(r) = bound.rational_part() {
864                                let tight_val = tighten_int_bound(r.clone(), false, true);
865                                InfRational::new(Rational::Finite(tight_val), rug::Rational::from(0))
866                            } else {
867                                unreachable!()
868                            }
869                        } else {
870                            InfRational::new(bound.rational_part().clone(), if bound.infinitesimal_part().is_negative() { rug::Rational::from(0) } else { rug::Rational::from(1) })
871                        };
872                        self.lra_theory.set_lb(Some(lit), *var, new_bound)
873                    }
874                    (TheoryConstraint::EnumEq(var, val), false) => self.enum_theory.set_eq(Some(lit), *var, *val),
875                    (TheoryConstraint::EnumEq(var, val), true) => self.enum_theory.set_neq(Some(lit), *var, *val),
876                    (TheoryConstraint::DlLeq(from, to, bound), false) => self.dl_theory.assert_edge(*from, *to, bound.clone(), lit).map_err(|cycle| cycle.into_iter().map(|l| !l).collect()),
877                    (TheoryConstraint::DlLeq(from, to, bound), true) => {
878                        let rat_part = bound.rational_part().clone();
879                        let neg_rat = match rat_part {
880                            Rational::Finite(val) => Rational::Finite(-val),
881                            Rational::PositiveInf => Rational::NegativeInf,
882                            Rational::NegativeInf => Rational::PositiveInf,
883                        };
884
885                        let neg_inf = -bound.infinitesimal_part().clone() - rug::Rational::from(1);
886                        let neg_bound = InfRational::new(neg_rat, neg_inf);
887
888                        self.dl_theory.assert_edge(*to, *from, neg_bound, lit).map_err(|cycle| cycle.into_iter().map(|l| !l).collect())
889                    }
890                    (TheoryConstraint::EufEq(t1, t2), false) => {
891                        self.euf_theory.merge(*t1, *t2, Some(lit));
892                        self.euf_theory.propagate_congruences();
893                        self.euf_theory.check_disequalities()
894                    }
895                    (TheoryConstraint::EufEq(t1, t2), true) => {
896                        self.euf_theory.propagate_congruences();
897                        self.euf_theory.assert_disequality(*t1, *t2, lit)
898                    }
899                };
900
901                if let Err(lemma) = theory_result {
902                    return Err((self.compute_backtrack_level(&lemma, base_level), lemma));
903                }
904            }
905            self.notified_len += 1;
906        }
907
908        if let Err(conflict) = self.lra_theory.check() {
909            return Err((self.compute_backtrack_level(&conflict, base_level), conflict));
910        }
911        Ok(())
912    }
913
914    /// Returns the assigned value of a literal in the current trail.
915    pub fn get_lit_val(&self, lit: Lit) -> Option<bool> {
916        self.sat_solver.lit_value(lit)
917    }
918
919    /// Returns the assigned value of a Boolean expression when it is fully determined.
920    pub fn get_bool_val(&self, expr: &BoolExpr) -> Option<bool> {
921        match expr {
922            BoolExpr::True => Some(true),
923            BoolExpr::False => Some(false),
924            BoolExpr::Var(v) => *self.sat_solver.value(v.0),
925            BoolExpr::Not(inner) => self.get_bool_val(inner).map(|val| !val),
926            BoolExpr::And(args) => {
927                let mut result = Some(true);
928                for arg in args {
929                    match self.get_bool_val(arg) {
930                        Some(val) => {
931                            if !val {
932                                return Some(false);
933                            }
934                        }
935                        None => result = None,
936                    }
937                }
938                result
939            }
940            BoolExpr::Or(args) => {
941                let mut result = Some(false);
942                for arg in args {
943                    match self.get_bool_val(arg) {
944                        Some(val) => {
945                            if val {
946                                return Some(true);
947                            }
948                        }
949                        None => result = None,
950                    }
951                }
952                result
953            }
954            BoolExpr::Lt(e1, e2) => {
955                let (lb1, ub1) = self.get_arith_bounds(e1)?;
956                let (lb2, ub2) = self.get_arith_bounds(e2)?;
957                if ub1 < lb2 {
958                    Some(true)
959                } else if lb1 >= ub2 {
960                    Some(false)
961                } else {
962                    None
963                }
964            }
965            BoolExpr::Le(e1, e2) => {
966                let (lb1, ub1) = self.get_arith_bounds(e1)?;
967                let (lb2, ub2) = self.get_arith_bounds(e2)?;
968                if ub1 <= lb2 {
969                    Some(true)
970                } else if lb1 > ub2 {
971                    Some(false)
972                } else {
973                    None
974                }
975            }
976            BoolExpr::Ge(e1, e2) => {
977                let (lb1, ub1) = self.get_arith_bounds(e1)?;
978                let (lb2, ub2) = self.get_arith_bounds(e2)?;
979                if lb1 >= ub2 {
980                    Some(true)
981                } else if ub1 < lb2 {
982                    Some(false)
983                } else {
984                    None
985                }
986            }
987            BoolExpr::Gt(e1, e2) => {
988                let (lb1, ub1) = self.get_arith_bounds(e1)?;
989                let (lb2, ub2) = self.get_arith_bounds(e2)?;
990                if lb1 > ub2 {
991                    Some(true)
992                } else if ub1 <= lb2 {
993                    Some(false)
994                } else {
995                    None
996                }
997            }
998            BoolExpr::DlLt(from, to, bound) => {
999                let (lb_from, ub_from) = self.get_dl_bounds(*from);
1000                let (lb_to, ub_to) = self.get_dl_bounds(*to);
1001                let bound_inf = InfRational::new(Rational::Finite(bound.clone()), rug::Rational::from(0));
1002
1003                // Max possible distance: ub_to - lb_from
1004                // Min possible distance: lb_to - ub_from
1005                let max_dist = ub_to.clone() - lb_from.clone();
1006                let min_dist = lb_to - ub_from;
1007
1008                if max_dist < bound_inf {
1009                    Some(true)
1010                } else if min_dist >= bound_inf {
1011                    Some(false)
1012                } else {
1013                    None
1014                }
1015            }
1016            BoolExpr::DlLe(from, to, bound) => {
1017                let (lb_from, ub_from) = self.get_dl_bounds(*from);
1018                let (lb_to, ub_to) = self.get_dl_bounds(*to);
1019                let bound_inf = InfRational::new(Rational::Finite(bound.clone()), rug::Rational::from(0));
1020
1021                let max_dist = ub_to.clone() - lb_from.clone();
1022                let min_dist = lb_to - ub_from;
1023
1024                if max_dist <= bound_inf {
1025                    Some(true)
1026                } else if min_dist > bound_inf {
1027                    Some(false)
1028                } else {
1029                    None
1030                }
1031            }
1032            BoolExpr::DlGt(from, to, bound) => {
1033                let (lb_from, ub_from) = self.get_dl_bounds(*from);
1034                let (lb_to, ub_to) = self.get_dl_bounds(*to);
1035                let bound_inf = InfRational::new(Rational::Finite(bound.clone()), rug::Rational::from(0));
1036
1037                let max_dist = ub_to.clone() - lb_from.clone();
1038                let min_dist = lb_to - ub_from;
1039
1040                if min_dist > bound_inf {
1041                    Some(true)
1042                } else if max_dist <= bound_inf {
1043                    Some(false)
1044                } else {
1045                    None
1046                }
1047            }
1048            BoolExpr::DlGe(from, to, bound) => {
1049                let (lb_from, ub_from) = self.get_dl_bounds(*from);
1050                let (lb_to, ub_to) = self.get_dl_bounds(*to);
1051                let bound_inf = InfRational::new(Rational::Finite(bound.clone()), rug::Rational::from(0));
1052
1053                let max_dist = ub_to.clone() - lb_from.clone();
1054                let min_dist = lb_to - ub_from;
1055
1056                if min_dist >= bound_inf {
1057                    Some(true)
1058                } else if max_dist < bound_inf {
1059                    Some(false)
1060                } else {
1061                    None
1062                }
1063            }
1064            BoolExpr::DlEq(from, to, bound) => {
1065                let (lb_from, ub_from) = self.get_dl_bounds(*from);
1066                let (lb_to, ub_to) = self.get_dl_bounds(*to);
1067                let bound_inf = InfRational::new(Rational::Finite(bound.clone()), rug::Rational::from(0));
1068
1069                let max_dist = ub_to.clone() - lb_from.clone();
1070                let min_dist = lb_to - ub_from;
1071
1072                // Exact equality means max_dist and min_dist are both exactly equal to bound
1073                if max_dist == bound_inf && min_dist == bound_inf {
1074                    Some(true)
1075                } else if max_dist < bound_inf || min_dist > bound_inf {
1076                    Some(false) // It's impossible to satisfy the equality
1077                } else {
1078                    None
1079                }
1080            }
1081            BoolExpr::Eq(e1, e2) => match (e1.as_ref(), e2.as_ref()) {
1082                (Expr::Arith(a1), Expr::Arith(a2)) => {
1083                    let (lb1, ub1) = self.get_arith_bounds(a1)?;
1084                    let (lb2, ub2) = self.get_arith_bounds(a2)?;
1085                    if ub1 < lb2 || ub2 < lb1 {
1086                        Some(false)
1087                    } else if lb1 == ub1 && lb2 == ub2 && lb1 == lb2 {
1088                        Some(true)
1089                    } else {
1090                        None
1091                    }
1092                }
1093                (Expr::Bool(b1), Expr::Bool(b2)) => {
1094                    let val1 = self.get_bool_val(b1);
1095                    let val2 = self.get_bool_val(b2);
1096                    match (val1, val2) {
1097                        (Some(v1), Some(v2)) => Some(v1 == v2),
1098                        _ => None,
1099                    }
1100                }
1101                (Expr::Enum(e1), Expr::Enum(e2)) => {
1102                    let val1 = self.get_enum_val(e1);
1103                    let val2 = self.get_enum_val(e2);
1104                    match (val1, val2) {
1105                        (Some(v1), Some(v2)) => Some(v1 == v2),
1106                        _ => None,
1107                    }
1108                }
1109                _ => None,
1110            },
1111        }
1112    }
1113
1114    /// Returns the current value of an arithmetic expression when it is fixed by the model.
1115    pub fn get_arith_val(&self, expr: &ArithExpr) -> Option<InfRational> {
1116        match expr {
1117            ArithExpr::Const(c) => Some(InfRational::new(Rational::Finite(c.clone()), rug::Rational::from(0))),
1118            ArithExpr::IntVar(v) => Some(self.lra_theory.value(v.0).clone()),
1119            ArithExpr::RealVar(v) => Some(self.lra_theory.value(v.0).clone()),
1120            ArithExpr::Add(terms) => {
1121                let mut sum = InfRational::new(Rational::Finite(rug::Rational::from(0)), rug::Rational::from(0));
1122                for term in terms {
1123                    sum += self.get_arith_val(term)?;
1124                }
1125                Some(sum)
1126            }
1127            ArithExpr::Neg(term) => self.get_arith_val(term).map(|val| -val),
1128            _ => None,
1129        }
1130    }
1131
1132    /// Returns the current lower and upper bounds of an arithmetic expression when they are fixed by the model.
1133    pub fn get_arith_bounds(&self, expr: &ArithExpr) -> Option<(InfRational, InfRational)> {
1134        match expr {
1135            ArithExpr::Const(c) => {
1136                let val = InfRational::new(Rational::Finite(c.clone()), rug::Rational::from(0));
1137                Some((val.clone(), val))
1138            }
1139            ArithExpr::IntVar(v) => Some((self.lra_theory.lb(v.0).clone(), self.lra_theory.ub(v.0).clone())),
1140            ArithExpr::RealVar(v) => Some((self.lra_theory.lb(v.0).clone(), self.lra_theory.ub(v.0).clone())),
1141            ArithExpr::Add(terms) => {
1142                let mut sum_lb = InfRational::new(Rational::Finite(rug::Rational::from(0)), rug::Rational::from(0));
1143                let mut sum_ub = sum_lb.clone();
1144                for term in terms {
1145                    let (lb, ub) = self.get_arith_bounds(term)?;
1146                    sum_lb += lb;
1147                    sum_ub += ub;
1148                }
1149                Some((sum_lb, sum_ub))
1150            }
1151            ArithExpr::Neg(term) => {
1152                let (lb, ub) = self.get_arith_bounds(term)?;
1153                Some((-ub, -lb))
1154            }
1155            _ => None,
1156        }
1157    }
1158
1159    /// Returns the concrete value of an enum variable if it has been fully assigned.
1160    pub fn get_enum_val(&self, expr: &EnumExpr) -> Option<i32> {
1161        match expr {
1162            EnumExpr::Const(c) => Some(*c),
1163            EnumExpr::Var(v) => {
1164                let domain = &self.enum_theory.active_domains[v.0];
1165                if domain.len() == 1 { domain.iter().next().copied() } else { None }
1166            }
1167        }
1168    }
1169
1170    /// Returns the current value of a difference logic variable.
1171    pub fn get_dl_val(&self, var: DlVar) -> InfRational {
1172        self.dl_theory.value(var.0)
1173    }
1174
1175    /// Returns the current lower and upper bounds of a difference logic variable.
1176    pub fn get_dl_bounds(&self, var: DlVar) -> (InfRational, InfRational) {
1177        (self.dl_theory.lb(var.0), self.dl_theory.ub(var.0))
1178    }
1179
1180    /// Opens a new incremental user scope for assertions and decisions.
1181    ///
1182    /// All constraints/decisions added after this call can be discarded by
1183    /// [`SeMiTONE::pop`].
1184    pub fn push(&mut self) {
1185        let clauses_len = self.sat_solver.clauses.len();
1186
1187        self.sat_solver.push();
1188        self.lra_theory.push();
1189        self.enum_theory.push();
1190        self.dl_theory.push();
1191
1192        let current_level = self.sat_solver.decision_level();
1193        self.user_scopes.push((current_level, clauses_len));
1194    }
1195
1196    /// Restores the previous user scope and discards assertions added in it.
1197    ///
1198    /// If no user scope is open, this is a no-op.
1199    pub fn pop(&mut self) {
1200        if let Some((saved_level, saved_clauses_len)) = self.user_scopes.pop() {
1201            self.cancel_until(saved_level - 1);
1202            for watch_list in self.sat_solver.watches.iter_mut() {
1203                watch_list.retain(|&clause_idx| clause_idx < saved_clauses_len);
1204            }
1205            self.sat_solver.clauses.truncate(saved_clauses_len);
1206        }
1207    }
1208
1209    fn compute_backtrack_level(&self, lemma: &[Lit], root_level: usize) -> usize {
1210        if lemma.len() <= 1 {
1211            return root_level;
1212        }
1213
1214        let mut levels: Vec<usize> = lemma.iter().map(|lit| self.sat_solver.level(lit.var()).expect("literal should have a decision level")).collect();
1215
1216        levels.sort_unstable_by(|a, b| b.cmp(a));
1217
1218        let max_level = levels[0];
1219
1220        if max_level <= root_level {
1221            return root_level;
1222        }
1223
1224        if levels.iter().filter(|&&l| l == max_level).count() == 1 { levels[1].max(root_level) } else { (max_level - 1).max(root_level) }
1225    }
1226
1227    /// Checks integrality of integer variables under the current rational model.
1228    ///
1229    /// Returns `Ok(())` if all integer variables are integral.
1230    /// Otherwise returns `Err((backtrack_level, lemma))` with either a Gomory
1231    /// cut or a branching disjunction for branch-and-bound.
1232    pub fn check_ints(&mut self) -> Result<(), (usize, Vec<Lit>)> {
1233        if let Err((var, val)) = self.lra_theory.check_ints() {
1234            trace!("Integer variable {} has fractional value {}", var, val);
1235
1236            if let Some((cut_row, cut_rhs, explanation_bounds)) = self.lra_theory.new_gomory_cut() {
1237                let cut_slack = self.lra_theory.get_or_create_slack(cut_row);
1238                let bound = InfRational::new(Rational::Finite(cut_rhs), rug::Rational::from(0));
1239                let cut_lit = self.get_or_create_proxy(TheoryConstraint::LraLb(cut_slack, bound));
1240
1241                let mut lemma = Vec::with_capacity(explanation_bounds.len() + 1);
1242                for constraint in explanation_bounds {
1243                    let proxy = self.get_or_create_proxy(constraint);
1244                    lemma.push(!proxy);
1245                }
1246                lemma.push(cut_lit);
1247
1248                trace!("Generated global Gomory cut with {} dependencies!", lemma.len() - 1);
1249
1250                if self.sat_solver.lit_value(cut_lit) != Some(true) {
1251                    let backtrack_level = if lemma.len() == 1 { 0 } else { self.sat_solver.decision_level() };
1252                    return Err((backtrack_level, lemma));
1253                }
1254            }
1255
1256            let Rational::Finite(inner_frac) = val.rational_part() else {
1257                unreachable!("Fractional variable in Branch & Bound must be finite");
1258            };
1259
1260            let mut floor_val = inner_frac.clone();
1261            floor_val.floor_mut();
1262            let mut ceil_val = inner_frac.clone();
1263            ceil_val.ceil_mut();
1264
1265            if floor_val == ceil_val {
1266                let inf_part = val.infinitesimal_part();
1267                if inf_part > &rug::Rational::from(0) {
1268                    ceil_val += rug::Rational::from(1);
1269                } else if inf_part < &rug::Rational::from(0) {
1270                    floor_val -= rug::Rational::from(1);
1271                }
1272            }
1273
1274            let ub = InfRational::new(Rational::Finite(floor_val), rug::Rational::from(0));
1275            let lb = InfRational::new(Rational::Finite(ceil_val), rug::Rational::from(0));
1276            trace!("Branching on variable {}: x <= {} or x >= {}", var, ub, lb);
1277
1278            let lit_ub = self.get_or_create_proxy(TheoryConstraint::LraUb(var, ub));
1279            let lit_lb = self.get_or_create_proxy(TheoryConstraint::LraLb(var, lb));
1280            let lemma = vec![lit_ub, lit_lb];
1281
1282            let current_level = self.sat_solver.decision_level();
1283            return Err((current_level, lemma));
1284        }
1285        Ok(())
1286    }
1287}
1288
1289#[cold]
1290#[inline(never)]
1291pub(crate) fn out_of_bounds(var: usize) -> ! {
1292    panic!("variable index out of bounds: {}", var);
1293}
1294
1295#[cfg(test)]
1296mod tests {
1297    use super::*;
1298
1299    #[test]
1300    fn test_pure_sat_resolution() {
1301        let mut solver = SeMiTONE::new();
1302
1303        let a = solver.new_bool();
1304        let b = solver.new_bool();
1305        let c = solver.new_bool();
1306
1307        // (A ∨ B) ∧ (¬B ∨ C) ∧ (¬B ∨ ¬C) ∧ (¬A)
1308        // With ¬A, clause (A ∨ B) forces B; then B forces both C and ¬C.
1309        let expr = (&a | &b) & (&!&b | &c) & (!&b | !&c) & !&a;
1310
1311        let _ = solver.assert(expr);
1312        assert!(solver.propagate().is_err(), "The solver should detect that the system is unsatisfiable");
1313    }
1314
1315    #[test]
1316    fn test_early_bounding_unsat() {
1317        let mut solver = SeMiTONE::new();
1318        let x = solver.new_real();
1319
1320        // x > 10 ∧ x < 5
1321        let expr = (x.clone().gt(10)) & (x.lt(5));
1322
1323        let result = solver.assert(expr);
1324        assert!(!result, "The solver should detect that the system is unsatisfiable");
1325    }
1326
1327    #[test]
1328    fn test_equality_mutually_exclusive() {
1329        let mut solver = SeMiTONE::new();
1330        let x = solver.new_real();
1331
1332        // x == 5 ∧ x > 6
1333        let expr = (x.clone().eq(5)) & (x.gt(6));
1334
1335        let result = solver.assert(expr);
1336        assert!(!result, "The solver should detect that the system is unsatisfiable");
1337    }
1338
1339    #[test]
1340    fn test_simplex_system_unsat() {
1341        let mut solver = SeMiTONE::new();
1342        let x = solver.new_real();
1343        let y = solver.new_real();
1344
1345        // x + y == 10
1346        let eq_expr = (x.clone() + y.clone()).eq(10);
1347        // x > 6
1348        let gt_x = x.clone().gt(6);
1349        // y > 6
1350        let gt_y = y.clone().gt(6);
1351
1352        let expr = eq_expr & gt_x & gt_y;
1353
1354        let _ = solver.assert(expr);
1355        assert!(solver.propagate().is_err(), "The solver should detect that the system is unsatisfiable");
1356    }
1357
1358    #[test]
1359    fn test_constant_arithmetic_evaluations() {
1360        let mut solver = SeMiTONE::new();
1361
1362        assert!(solver.assert(ArithExpr::from(5).lt(10)));
1363        assert!(solver.assert(ArithExpr::from(5).le(5)));
1364        assert!(solver.assert(ArithExpr::from(10).ge(5)));
1365        assert!(solver.assert(ArithExpr::from(10).gt(5)));
1366
1367        assert!(!solver.assert(ArithExpr::from(10).lt(5)));
1368        assert!(!solver.assert(ArithExpr::from(10).le(5)));
1369        assert!(!solver.assert(ArithExpr::from(5).ge(10)));
1370        assert!(!solver.assert(ArithExpr::from(5).gt(10)));
1371
1372        assert!(solver.assert(!ArithExpr::from(10).lt(5)));
1373        assert!(!solver.assert(!ArithExpr::from(5).lt(10)));
1374    }
1375
1376    #[test]
1377    fn test_negated_variable_inequalities() {
1378        let mut solver = SeMiTONE::new();
1379        let x = solver.new_real();
1380
1381        solver.push();
1382        assert!(solver.assert(!x.clone().lt(5)));
1383        assert!(!solver.assert(x.clone().lt(4)));
1384        solver.pop();
1385
1386        solver.push();
1387        assert!(solver.assert(!x.clone().le(5)));
1388        assert!(!solver.assert(x.clone().le(5)));
1389        solver.pop();
1390
1391        solver.push();
1392        assert!(solver.assert(!x.clone().ge(5)));
1393        assert!(!solver.assert(x.clone().ge(5)));
1394        solver.pop();
1395
1396        solver.push();
1397        assert!(solver.assert(!x.clone().gt(5)));
1398        assert!(!solver.assert(x.clone().gt(5)));
1399        solver.pop();
1400    }
1401
1402    #[test]
1403    #[should_panic(expected = "Type mismatch in Eq")]
1404    fn test_encode_eq_type_mismatch_panic() {
1405        let mut solver = SeMiTONE::new();
1406        let a = solver.new_bool();
1407        let x = solver.new_real();
1408
1409        let bad_eq = BoolExpr::Eq(Box::new(Expr::Bool(a)), Box::new(Expr::Arith(x)));
1410
1411        let _ = solver.assert(bad_eq);
1412    }
1413
1414    #[test]
1415    fn test_enum_out_of_domain_unsat() {
1416        let mut solver = SeMiTONE::new();
1417        let e = solver.new_enum(vec![1, 2]);
1418
1419        let expr = e.eq(3);
1420
1421        let _ = solver.assert(expr);
1422        assert!(solver.propagate().is_err(), "The solver should detect that the enum variable cannot take a value outside its domain");
1423    }
1424
1425    #[test]
1426    fn test_enum_exhaustive_denial_integration() {
1427        let mut solver = SeMiTONE::new();
1428        let e = solver.new_enum(vec![1, 2]);
1429
1430        // (e != 1) AND (e != 2)
1431        let expr = !(e.clone().eq(1)) & !(e.clone().eq(2));
1432
1433        let _ = solver.assert(expr);
1434        assert!(solver.propagate().is_err(), "The solver should detect that the enum variable cannot take a value outside its domain");
1435    }
1436
1437    #[test]
1438    fn test_dl_chain_upper_bounds() {
1439        let mut solver = SeMiTONE::new();
1440        let zero = solver.new_dl_var(); // first difference logic variable created = reference 0 in the DL theory
1441        let t1 = solver.new_dl_var();
1442        let t2 = solver.new_dl_var();
1443
1444        let _ = solver.assert(BoolExpr::DlLe(zero, t1, rug::Rational::from(10))); // t1 - zero <= 10
1445        let _ = solver.assert(BoolExpr::DlLe(t1, t2, rug::Rational::from(5))); // t2 - t1 <= 5
1446
1447        assert!(solver.propagate().is_ok());
1448
1449        assert_eq!(solver.get_dl_bounds(t1).1, InfRational::from(10));
1450        assert_eq!(solver.get_dl_bounds(t2).1, InfRational::from(15));
1451        assert_eq!(solver.get_dl_bounds(t1).0, InfRational::from(Rational::NegativeInf), "no lower bound imposed");
1452    }
1453
1454    #[test]
1455    fn test_dl_lower_and_upper_bound_interval() {
1456        let mut solver = SeMiTONE::new();
1457        let zero = solver.new_dl_var();
1458        let t1 = solver.new_dl_var();
1459
1460        let _ = solver.assert(BoolExpr::DlLe(zero, t1, rug::Rational::from(8))); // t1 <= 8
1461        let _ = solver.assert(BoolExpr::DlGe(zero, t1, rug::Rational::from(3))); // t1 >= 3
1462
1463        assert!(solver.propagate().is_ok());
1464        assert_eq!(solver.get_dl_bounds(t1), (InfRational::from(3), InfRational::from(8)));
1465    }
1466
1467    #[test]
1468    fn test_dl_eq_pins_value() {
1469        let mut solver = SeMiTONE::new();
1470        let zero = solver.new_dl_var();
1471        let t1 = solver.new_dl_var();
1472
1473        let _ = solver.assert(BoolExpr::DlEq(zero, t1, rug::Rational::from(7)));
1474        assert!(solver.propagate().is_ok());
1475
1476        assert_eq!(solver.get_dl_bounds(t1), (InfRational::from(7), InfRational::from(7)));
1477    }
1478
1479    #[test]
1480    fn test_dl_negative_cycle_conflict() {
1481        let mut solver = SeMiTONE::new();
1482        let a = solver.new_dl_var();
1483        let b = solver.new_dl_var();
1484
1485        // b - a <= 5 and b - a >= 10 (via a - b <= -10): irreconcilable
1486        let _ = solver.assert(BoolExpr::DlLe(a, b, rug::Rational::from(5)));
1487        let _ = solver.assert(BoolExpr::DlLe(b, a, rug::Rational::from(-10)));
1488
1489        assert!(solver.propagate().is_err(), "the negative cycle must produce a conflict");
1490    }
1491
1492    #[test]
1493    fn test_dl_strict_boundary_conflict() {
1494        let mut solver = SeMiTONE::new();
1495        let a = solver.new_dl_var();
1496        let b = solver.new_dl_var();
1497
1498        // b - a <= 0 (non-strict) and a - b < 0, i.e. b - a > 0 (strict):
1499        // the weights sum to 0 but the conflict must be detected via the infinitesimal trick
1500        let _ = solver.assert(BoolExpr::DlLe(a, b, rug::Rational::from(0)));
1501        let _ = solver.assert(BoolExpr::DlLt(b, a, rug::Rational::from(0)));
1502
1503        assert!(solver.propagate().is_err());
1504    }
1505
1506    #[test]
1507    fn test_dl_non_strict_boundary_is_sat() {
1508        let mut solver = SeMiTONE::new();
1509        let a = solver.new_dl_var();
1510        let b = solver.new_dl_var();
1511
1512        let _ = solver.assert(BoolExpr::DlLe(a, b, rug::Rational::from(0)));
1513        let _ = solver.assert(BoolExpr::DlLe(b, a, rug::Rational::from(0)));
1514
1515        assert!(solver.propagate().is_ok());
1516        assert_eq!(solver.get_dl_bounds(b), solver.get_dl_bounds(a), "b == a == 0");
1517    }
1518
1519    #[test]
1520    fn test_dl_backtracking_via_push_pop() {
1521        let mut solver = SeMiTONE::new();
1522        let zero = solver.new_dl_var();
1523        let t1 = solver.new_dl_var();
1524
1525        solver.push();
1526        let _ = solver.assert(BoolExpr::DlLe(zero, t1, rug::Rational::from(4)));
1527        assert!(solver.propagate().is_ok());
1528        assert_eq!(solver.get_dl_bounds(t1).1, InfRational::from(4));
1529        solver.pop();
1530
1531        assert_eq!(solver.get_dl_bounds(t1).1, InfRational::from(Rational::PositiveInf), "the constraint must disappear after the pop");
1532    }
1533
1534    #[test]
1535    fn test_dl_negated_le_forces_strict_gt() {
1536        // `assert(!expr)` goes through the catch-all branch of `assert_internal`, which negates
1537        // at the SAT level the literal already registered for DlLe (it does not call mk_dl_ge).
1538        // This exercises the `(DlLeq(..), false)` branch of `propagate()`.
1539        let mut solver = SeMiTONE::new();
1540        let a = solver.new_dl_var();
1541        let b = solver.new_dl_var();
1542
1543        let neg_le = BoolExpr::Not(Box::new(BoolExpr::DlLe(a, b, rug::Rational::from(4))));
1544        let _ = solver.assert(neg_le);
1545        assert!(solver.propagate().is_ok());
1546
1547        let (lb_b, _) = solver.get_dl_bounds(b);
1548        assert!(lb_b > InfRational::from(4), "!(b - a <= 4) must imply b - a > 4, found lb(b) = {:?}", lb_b);
1549    }
1550}
semitone/lib.rs

semitone/
lib.rs
