semitone/
lib.rs

1#![doc = include_str!("../README.md")]
2
3//! # API overview
4//!
5//! [`SeMiTONE`] owns all solver state. Create expressions with the types in
6//! [`ast`], assert a [`ast::BoolExpr`], then call [`SeMiTONE::propagate`] after
7//! each assertion or decision. Applications that need a complete SAT/SMT search
8//! loop can use the decision, trail, and clause APIs exposed by [`SeMiTONE`].
9
10pub mod ast;
11mod enum_theory;
12mod lra_theory;
13#[cfg(feature = "parser")]
14pub mod parser;
15mod proxy;
16pub mod rational;
17mod sat_solver;
18#[cfg(feature = "solver")]
19pub mod solver;
20
21use crate::{
22    ast::{ArithExpr, BoolExpr, EnumExpr, Expr},
23    enum_theory::EnumTheory,
24    lra_theory::{LraTheory, SparseRow},
25    proxy::{ProxyRegistry, TheoryConstraint},
26    rational::{InfRational, Rational},
27    sat_solver::SatSolver,
28};
29use rug::Assign;
30pub use sat_solver::Lit;
31
32/// Main solver entry point for propositional, linear arithmetic, and enum constraints.
33///
34/// The solver combines a SAT core with theory propagation for linear rational
35/// arithmetic and finite-domain enum reasoning.
36pub struct SeMiTONE {
37    registry: ProxyRegistry,
38    sat_solver: SatSolver,
39    lra_theory: LraTheory,
40    enum_theory: EnumTheory,
41    notified_len: usize,
42    user_scopes: Vec<(usize, usize)>,
43}
44
45impl Default for SeMiTONE {
46    fn default() -> Self {
47        Self::new()
48    }
49}
50
51impl SeMiTONE {
52    /// Creates a new empty solver instance.
53    pub fn new() -> Self {
54        Self {
55            registry: ProxyRegistry::new(),
56            sat_solver: SatSolver::new(),
57            lra_theory: LraTheory::new(),
58            enum_theory: EnumTheory::new(),
59            notified_len: 0,
60            user_scopes: Vec::new(),
61        }
62    }
63
64    /// Allocates a new Boolean variable.
65    pub fn new_bool(&mut self) -> BoolExpr {
66        BoolExpr::Var(self.sat_solver.mk_var())
67    }
68
69    /// Allocates a new integer variable.
70    pub fn new_int(&mut self) -> ArithExpr {
71        ArithExpr::IntVar(self.lra_theory.mk_int())
72    }
73
74    /// Allocates a new real variable.
75    pub fn new_real(&mut self) -> ArithExpr {
76        ArithExpr::RealVar(self.lra_theory.mk_real())
77    }
78
79    /// Allocates a new enum variable with the given finite domain.
80    pub fn new_enum(&mut self, domain: impl IntoIterator<Item = i32>) -> EnumExpr {
81        EnumExpr::Var(self.enum_theory.mk_var(domain.into_iter().collect()))
82    }
83
84    /// Returns the current number of SAT variables allocated in the solver core.
85    ///
86    /// This includes user-visible Boolean variables and internal proxy variables
87    /// introduced while encoding compound constraints.
88    pub fn num_vars(&self) -> usize {
89        self.sat_solver.num_vars()
90    }
91
92    /// Adds a clause directly to the SAT core.
93    ///
94    /// Returns `Ok(())` when the clause is accepted, or `Err(conflict_clause)` if
95    /// the clause is immediately contradictory at the current root context.
96    ///
97    /// This is useful for integrating external search/learning loops that produce
98    /// learned no-goods.
99    pub fn add_clause(&mut self, clause: impl IntoIterator<Item = Lit>) -> Result<(), Vec<Lit>> {
100        self.sat_solver.add_clause(clause)
101    }
102
103    /// Adds a Boolean constraint to the current solver context.
104    ///
105    /// Returns `true` if the assertion was successfully added, or `false` if it
106    /// led to an immediate, trivial conflict while translating/asserting.
107    ///
108    /// Note that `true` does not imply global feasibility: call [`SeMiTONE::propagate`]
109    /// to detect conflicts that emerge after propagation through SAT/theory state.
110    pub fn assert(&mut self, expr: &BoolExpr) -> bool {
111        self.assert_internal(expr, true)
112    }
113
114    fn assert_internal(&mut self, expr: &BoolExpr, polarity: bool) -> bool {
115        match (expr, polarity) {
116            (BoolExpr::Not(inner), _) => self.assert_internal(inner, !polarity),
117            (BoolExpr::And(args), true) | (BoolExpr::Or(args), false) => {
118                for arg in args {
119                    if !self.assert_internal(arg, polarity) {
120                        return false;
121                    }
122                }
123                true
124            }
125            (BoolExpr::Or(args), true) | (BoolExpr::And(args), false) => {
126                let mut clause = Vec::with_capacity(args.len());
127                for arg in args {
128                    let mut lit = self.encode_bool(arg);
129                    if !polarity {
130                        lit = !lit;
131                    }
132                    clause.push(lit);
133                }
134                self.sat_solver.add_clause(clause).is_ok()
135            }
136            (BoolExpr::Lt(e1, e2), _) | (BoolExpr::Le(e1, e2), _) | (BoolExpr::Ge(e1, e2), _) | (BoolExpr::Gt(e1, e2), _) => {
137                let (vars, const_term) = self.diff(e1, e2);
138                if vars.is_empty() {
139                    let is_sat = match expr {
140                        BoolExpr::Lt(_, _) => const_term.is_negative(),
141                        BoolExpr::Le(_, _) => const_term.is_negative() || const_term.is_zero(),
142                        BoolExpr::Ge(_, _) => !const_term.is_negative(),
143                        BoolExpr::Gt(_, _) => const_term.is_positive(),
144                        _ => unreachable!(),
145                    };
146                    return if polarity { is_sat } else { !is_sat };
147                }
148
149                let (is_upper_bound, eps_val) = match (expr, polarity) {
150                    (BoolExpr::Lt(_, _), true) => (true, rug::Rational::from(-1)),
151                    (BoolExpr::Lt(_, _), false) => (false, rug::Rational::from(0)),
152                    (BoolExpr::Le(_, _), true) => (true, rug::Rational::from(0)),
153                    (BoolExpr::Le(_, _), false) => (false, rug::Rational::from(1)),
154                    (BoolExpr::Ge(_, _), true) => (false, rug::Rational::from(0)),
155                    (BoolExpr::Ge(_, _), false) => (true, rug::Rational::from(-1)),
156                    (BoolExpr::Gt(_, _), true) => (false, rug::Rational::from(1)),
157                    (BoolExpr::Gt(_, _), false) => (true, rug::Rational::from(0)),
158                    _ => unreachable!(),
159                };
160
161                let bound = InfRational::new(Rational::Finite(-const_term), eps_val);
162
163                if vars.len() == 1 {
164                    let (var, coeff) = vars.iter().next().unwrap();
165                    let final_bound = bound / coeff.clone();
166                    if is_upper_bound == coeff.is_positive() { self.lra_theory.set_ub(None, *var, final_bound).is_ok() } else { self.lra_theory.set_lb(None, *var, final_bound).is_ok() }
167                } else {
168                    let slack = self.lra_theory.get_or_create_slack(vars);
169                    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() }
170                }
171            }
172            (BoolExpr::Eq(e1, e2), _) => {
173                if let (Expr::Arith(a1), Expr::Arith(a2)) = (&**e1, &**e2) {
174                    let (vars, const_term) = self.diff(a1, a2);
175
176                    if vars.is_empty() {
177                        let is_sat = const_term.is_zero();
178                        return if polarity { is_sat } else { !is_sat };
179                    }
180
181                    if polarity {
182                        let bound = InfRational::new(Rational::Finite(-const_term), rug::Rational::from(0));
183
184                        if vars.len() == 1 {
185                            let (var, coeff) = vars.iter().next().unwrap();
186                            let final_bound = bound / coeff.clone();
187                            self.lra_theory.set_lb(None, *var, final_bound.clone()).is_ok() && self.lra_theory.set_ub(None, *var, final_bound).is_ok()
188                        } else {
189                            let slack = self.lra_theory.get_or_create_slack(vars);
190                            self.lra_theory.set_lb(None, slack, bound.clone()).is_ok() && self.lra_theory.set_ub(None, slack, bound).is_ok()
191                        }
192                    } else {
193                        let lt_lit = self.mk_le(a1, a2, true);
194                        let gt_lit = self.mk_ge(a1, a2, true);
195                        self.sat_solver.add_clause([lt_lit, gt_lit]).is_ok()
196                    }
197                } else {
198                    let mut lit = self.encode_eq(e1, e2);
199                    if !polarity {
200                        lit = !lit;
201                    }
202                    self.sat_solver.add_clause([lit]).is_ok()
203                }
204            }
205            _ => {
206                let mut lit = self.encode_bool(expr);
207                if !polarity {
208                    lit = !lit;
209                }
210                self.sat_solver.add_clause([lit]).is_ok()
211            }
212        }
213    }
214
215    /// Encodes a Boolean expression into an equivalent SAT literal.
216    ///
217    /// The returned literal is a SAT variable or proxy that is logically
218    /// equivalent to `expr`: it is satisfied exactly when the Boolean expression
219    /// evaluates to true in the current theory encoding. Compound boolean
220    /// operators create auxiliary proxy variables and CNF clauses that preserve
221    /// this equivalence, while arithmetic and enum comparisons are translated via
222    /// their theory-specific proxy constraints.
223    pub fn encode_bool(&mut self, expr: &BoolExpr) -> Lit {
224        match expr {
225            BoolExpr::True => Lit::TRUE,
226            BoolExpr::False => Lit::FALSE,
227            BoolExpr::Var(v) => Lit::new(*v, false),
228            BoolExpr::Not(inner) => match inner.as_ref() {
229                BoolExpr::Lt(a1, a2) => self.mk_ge(a1, a2, false),
230                BoolExpr::Le(a1, a2) => self.mk_ge(a1, a2, true),
231                BoolExpr::Ge(a1, a2) => self.mk_le(a1, a2, true),
232                BoolExpr::Gt(a1, a2) => self.mk_le(a1, a2, false),
233                _ => !self.encode_bool(inner),
234            },
235            BoolExpr::And(terms) => {
236                let mut lits = Vec::with_capacity(terms.len());
237                for term in terms {
238                    lits.push(self.encode_bool(term));
239                }
240
241                let proxy_var = self.sat_solver.mk_var();
242                let proxy_lit = Lit::new(proxy_var, true);
243
244                for &lit in &lits {
245                    self.sat_solver.add_clause([!proxy_lit, lit]).expect("Failed to add clause");
246                }
247
248                let mut big_clause: Vec<Lit> = lits.into_iter().map(|l| !l).collect();
249                big_clause.push(proxy_lit);
250                self.sat_solver.add_clause(big_clause).expect("Failed to add clause");
251
252                proxy_lit
253            }
254            BoolExpr::Or(terms) => {
255                let mut lits = Vec::with_capacity(terms.len());
256                for term in terms {
257                    lits.push(self.encode_bool(term));
258                }
259
260                let proxy_var = self.sat_solver.mk_var();
261                let proxy_lit = Lit::new(proxy_var, true);
262
263                for &lit in &lits {
264                    self.sat_solver.add_clause([!lit, proxy_lit]).expect("Failed to add clause");
265                }
266
267                let mut big_clause = lits;
268                big_clause.push(!proxy_lit);
269                self.sat_solver.add_clause(big_clause).expect("Failed to add clause");
270
271                proxy_lit
272            }
273            BoolExpr::Lt(e1, e2) => self.mk_le(e1, e2, true),
274            BoolExpr::Le(e1, e2) => self.mk_le(e1, e2, false),
275            BoolExpr::Ge(e1, e2) => self.mk_ge(e1, e2, false),
276            BoolExpr::Gt(e1, e2) => self.mk_ge(e1, e2, true),
277            BoolExpr::Eq(e1, e2) => self.encode_eq(e1, e2),
278        }
279    }
280
281    fn encode_eq(&mut self, expr1: &Expr, expr2: &Expr) -> Lit {
282        match (expr1, expr2) {
283            (Expr::Arith(a1), Expr::Arith(a2)) => self.mk_arith_eq(a1, a2),
284            (Expr::Bool(b1), Expr::Bool(b2)) => {
285                let l1 = self.encode_bool(b1);
286                let l2 = self.encode_bool(b2);
287                let proxy_var = self.sat_solver.mk_var();
288                let p = Lit::new(proxy_var, true);
289
290                self.sat_solver.add_clause([!p, l1, !l2]).expect("Failed to add clause");
291                self.sat_solver.add_clause([!p, !l1, l2]).expect("Failed to add clause");
292                self.sat_solver.add_clause([p, l1, l2]).expect("Failed to add clause");
293                self.sat_solver.add_clause([p, !l1, !l2]).expect("Failed to add clause");
294
295                p
296            }
297            (Expr::Enum(e1), Expr::Enum(e2)) => self.mk_enum_eq(e1, e2),
298            _ => panic!("Type mismatch in Eq: cannot compare different domains.\nLeft: {:?}\nRight: {:?}", expr1, expr2),
299        }
300    }
301
302    fn mk_enum_eq(&mut self, e1: &EnumExpr, e2: &EnumExpr) -> Lit {
303        match (e1, e2) {
304            (EnumExpr::Const(c1), EnumExpr::Const(c2)) => {
305                if c1 == c2 {
306                    Lit::TRUE
307                } else {
308                    Lit::FALSE
309                }
310            }
311            (EnumExpr::Var(v), EnumExpr::Const(c)) | (EnumExpr::Const(c), EnumExpr::Var(v)) => self.get_or_create_proxy(TheoryConstraint::EnumEq(*v, *c)),
312            (EnumExpr::Var(v1), EnumExpr::Var(v2)) => {
313                if v1 == v2 {
314                    return Lit::TRUE;
315                }
316
317                let domain1 = self.enum_theory.initial_domains[*v1].clone();
318                let domain2 = self.enum_theory.initial_domains[*v2].clone();
319                let common: Vec<i32> = domain1.intersection(&domain2).copied().collect();
320
321                if common.is_empty() {
322                    return Lit::FALSE;
323                }
324
325                let mut lits = Vec::with_capacity(common.len());
326                for val in common {
327                    let p1 = self.get_or_create_proxy(TheoryConstraint::EnumEq(*v1, val));
328                    let p2 = self.get_or_create_proxy(TheoryConstraint::EnumEq(*v2, val));
329
330                    let and_proxy_var = self.sat_solver.mk_var();
331                    let and_proxy = Lit::new(and_proxy_var, false);
332
333                    self.sat_solver.add_clause([!and_proxy, p1]).unwrap();
334                    self.sat_solver.add_clause([!and_proxy, p2]).unwrap();
335                    self.sat_solver.add_clause([!p1, !p2, and_proxy]).unwrap();
336
337                    lits.push(and_proxy);
338                }
339
340                let or_proxy_var = self.sat_solver.mk_var();
341                let or_proxy = Lit::new(or_proxy_var, false);
342
343                for &lit in &lits {
344                    self.sat_solver.add_clause([!lit, or_proxy]).unwrap();
345                }
346
347                let mut big_clause = lits;
348                big_clause.push(!or_proxy);
349                self.sat_solver.add_clause(big_clause).unwrap();
350
351                or_proxy
352            }
353        }
354    }
355
356    fn mk_le(&mut self, e1: &ArithExpr, e2: &ArithExpr, strict: bool) -> Lit {
357        let (vars, const_term) = self.diff(e1, e2);
358
359        match vars.len() {
360            0 => {
361                if if strict { const_term.is_negative() } else { const_term.is_negative() || const_term.is_zero() } {
362                    Lit::TRUE
363                } else {
364                    Lit::FALSE
365                }
366            }
367            1 => {
368                let (var, coeff) = vars.iter().next().unwrap();
369                let bound = InfRational::new(Rational::Finite(-const_term / coeff), if strict { rug::Rational::from(-1) } else { rug::Rational::from(0) } / coeff);
370                let bound = if coeff.is_positive() { TheoryConstraint::LraUb(*var, bound) } else { TheoryConstraint::LraLb(*var, bound) };
371                self.get_or_create_proxy(bound)
372            }
373            _ => {
374                let slack = self.lra_theory.get_or_create_slack(vars);
375                let bound = TheoryConstraint::LraUb(slack, InfRational::new(Rational::Finite(-const_term), if strict { rug::Rational::from(-1) } else { rug::Rational::from(0) }));
376                self.get_or_create_proxy(bound)
377            }
378        }
379    }
380
381    fn mk_arith_eq(&mut self, e1: &ArithExpr, e2: &ArithExpr) -> Lit {
382        if e1 == e2 {
383            return Lit::TRUE;
384        }
385
386        let le_lit = self.mk_le(e1, e2, false);
387        let ge_lit = self.mk_ge(e1, e2, false);
388
389        let proxy_var = self.sat_solver.mk_var();
390        let p = Lit::new(proxy_var, false);
391
392        // p -> (x <= y)
393        self.sat_solver.add_clause([!p, le_lit]).expect("Failed to add clause");
394        // p -> (x >= y)
395        self.sat_solver.add_clause([!p, ge_lit]).expect("Failed to add clause");
396        // (x <= y) ∧ (x >= y) -> p
397        self.sat_solver.add_clause([!le_lit, !ge_lit, p]).expect("Failed to add clause");
398
399        p
400    }
401
402    fn mk_ge(&mut self, e1: &ArithExpr, e2: &ArithExpr, strict: bool) -> Lit {
403        let (vars, const_term) = self.diff(e1, e2);
404
405        match vars.len() {
406            0 => {
407                if if strict { const_term.is_positive() } else { const_term.is_positive() || const_term.is_zero() } {
408                    Lit::TRUE
409                } else {
410                    Lit::FALSE
411                }
412            }
413            1 => {
414                let (var, coeff) = vars.iter().next().unwrap();
415                let bound = InfRational::new(Rational::Finite(-const_term / coeff), if strict { rug::Rational::from(1) } else { rug::Rational::from(0) } / coeff);
416                let bound = if coeff.is_positive() { TheoryConstraint::LraLb(*var, bound) } else { TheoryConstraint::LraUb(*var, bound) };
417                self.get_or_create_proxy(bound)
418            }
419            _ => {
420                let slack = self.lra_theory.get_or_create_slack(vars);
421                let bound = TheoryConstraint::LraLb(slack, InfRational::new(Rational::Finite(-const_term), if strict { rug::Rational::from(1) } else { rug::Rational::from(0) }));
422                self.get_or_create_proxy(bound)
423            }
424        }
425    }
426
427    fn diff(&self, e1: &ArithExpr, e2: &ArithExpr) -> (SparseRow, rug::Rational) {
428        let mut vars = SparseRow::new();
429        let mut const_term = rug::Rational::from(0);
430
431        let pos_one = rug::Rational::from(1);
432        let neg_one = rug::Rational::from(-1);
433
434        let mut temp = rug::Rational::new();
435
436        self.accumulate_expr(e1, &pos_one, &mut vars, &mut const_term, &mut temp);
437        self.accumulate_expr(e2, &neg_one, &mut vars, &mut const_term, &mut temp);
438
439        vars.retain(|_, c| *c != 0);
440
441        (vars, const_term)
442    }
443
444    fn accumulate_expr(&self, expr: &ArithExpr, scale: &rug::Rational, vars: &mut SparseRow, const_term: &mut rug::Rational, temp: &mut rug::Rational) {
445        match expr {
446            ArithExpr::Const(c) => {
447                temp.assign(c * scale);
448                *const_term += &*temp;
449            }
450            ArithExpr::IntVar(var) | ArithExpr::RealVar(var) => {
451                self.accumulate_var(*var, scale, vars, temp);
452            }
453            ArithExpr::Add(terms) => {
454                for term in terms {
455                    self.accumulate_expr(term, scale, vars, const_term, temp);
456                }
457            }
458            ArithExpr::Mul(terms) => {
459                if terms.len() != 2 {
460                    panic!("Only binary multiplication is supported in linear arithmetic");
461                }
462                let (first, second) = (&terms[0], &terms[1]);
463
464                // Ricorsione intelligente: accettiamo (Costante * SottoEspressione)
465                match (first, second) {
466                    (ArithExpr::Const(c), sub_expr) | (sub_expr, ArithExpr::Const(c)) => {
467                        let mut new_scale = rug::Rational::new();
468                        new_scale.assign(c * scale);
469                        self.accumulate_expr(sub_expr, &new_scale, vars, const_term, temp);
470                    }
471                    _ => {
472                        panic!("Non-linear arithmetic: multiplication between two non-constant expressions is not supported");
473                    }
474                }
475            }
476            ArithExpr::Div(numerator, denominator) => {
477                // Il denominatore DEVE essere una costante per preservare la linearità
478                if let ArithExpr::Const(c) = &**denominator {
479                    if c.is_zero() {
480                        panic!("Division by zero detected in AST");
481                    }
482                    let mut div_scale = rug::Rational::new();
483                    div_scale.assign(scale / c);
484                    self.accumulate_expr(numerator, &div_scale, vars, const_term, temp);
485                } else {
486                    panic!("Non-linear arithmetic: division by a non-constant expression is not supported");
487                }
488            }
489            ArithExpr::Neg(sub_expr) => {
490                let mut neg_scale = rug::Rational::new();
491                neg_scale.assign(scale * -1);
492                self.accumulate_expr(sub_expr, &neg_scale, vars, const_term, temp);
493            }
494        }
495    }
496
497    fn accumulate_var(&self, var: usize, scale: &rug::Rational, vars: &mut SparseRow, temp: &mut rug::Rational) {
498        if let Some(basic_row) = self.lra_theory.tableau.get(&var) {
499            for (sub_var, sub_coeff) in basic_row.iter() {
500                temp.assign(sub_coeff * scale);
501                vars.add_coeff(*sub_var, temp);
502            }
503        } else {
504            vars.add_coeff(var, scale);
505        }
506    }
507
508    fn get_or_create_proxy(&mut self, constraint: TheoryConstraint) -> Lit {
509        if let Some(&sat_var) = self.registry.get_proxy(&constraint) {
510            sat_var
511        } else {
512            let sat_var = self.sat_solver.mk_var();
513            self.registry.register(constraint, Lit::new(sat_var, false));
514            Lit::new(sat_var, false)
515        }
516    }
517
518    /// Adds a decision literal to the current search branch.
519    ///
520    /// This opens a new internal decision level and enqueues `lit` as a decision.
521    /// Returns `false` only if the literal is immediately inconsistent with the
522    /// current assignment.
523    ///
524    /// After a successful decision, call [`SeMiTONE::propagate`] to derive its
525    /// consequences and detect theory conflicts.
526    pub fn decide(&mut self, lit: Lit) -> bool {
527        self.sat_solver.push();
528        self.lra_theory.push();
529        self.enum_theory.push();
530        self.sat_solver.enqueue_decision(lit)
531    }
532
533    /// Decides that an enum variable takes a specific value in the current branch.
534    ///
535    /// Convenience wrapper around [`SeMiTONE::decide`]. Returns `false` if the
536    /// decision cannot be enqueued consistently.
537    pub fn decide_enum(&mut self, expr: &EnumExpr, value: i32) -> bool {
538        let eq_expr = TheoryConstraint::EnumEq(
539            match expr {
540                EnumExpr::Var(v) => *v,
541                EnumExpr::Const(_) => panic!("Cannot decide on a constant value"),
542            },
543            value,
544        );
545        let lit = self.get_or_create_proxy(eq_expr);
546        self.decide(lit)
547    }
548
549    /// Returns the current internal decision level.
550    ///
551    /// Level `0` corresponds to the root level (no user decision applied).
552    pub fn decision_level(&self) -> usize {
553        self.sat_solver.decision_level()
554    }
555
556    /// Cancels all decisions and theory updates at levels deeper than `level`.
557    ///
558    /// This restores SAT/theory state to the requested level and drops pending
559    /// notifications beyond the restored trail.
560    pub fn cancel_until(&mut self, level: usize) {
561        self.sat_solver.cancel_until(level);
562        self.lra_theory.cancel_until(level);
563        self.enum_theory.cancel_until(level);
564        self.notified_len = self.sat_solver.trail.len();
565    }
566
567    /// Returns the trail suffix starting at `from_index`.
568    ///
569    /// Useful for external heuristics that need to inspect newly assigned literals.
570    pub fn get_trail_delta(&self, from_index: usize) -> &[Lit] {
571        &self.sat_solver.trail[from_index..]
572    }
573
574    /// Returns the current size of the SAT assignment trail.
575    pub fn current_trail_len(&self) -> usize {
576        self.sat_solver.trail.len()
577    }
578
579    /// Returns the trail length recorded at a specific decision level.
580    ///
581    /// If `level` is beyond the current number of levels, returns the current
582    /// trail length.
583    pub fn get_trail_len_at_level(&self, level: usize) -> usize {
584        if level < self.sat_solver.trail_lim.len() { self.sat_solver.trail_lim[level] } else { self.sat_solver.trail.len() }
585    }
586
587    /// Returns a slice of the trail between `start` (inclusive) and `end` (exclusive).
588    pub fn get_trail_slice(&self, start: usize, end: usize) -> &[Lit] {
589        &self.sat_solver.trail[start..end]
590    }
591
592    /// Returns the number of currently active user scopes (`push`/`pop`).
593    pub fn user_scopes_len(&self) -> usize {
594        self.user_scopes.len()
595    }
596
597    /// Runs SAT + theory propagation until a fixed point or a conflict.
598    ///
599    /// Returns:
600    /// - `Ok(())` if the current branch is feasible after propagation.
601    /// - `Err((backtrack_level, no_good))` if a conflict is found.
602    ///
603    /// The returned `backtrack_level` is the suggested non-chronological level to
604    /// backtrack to, and `no_good` is a conflict explanation suitable for learning.
605    pub fn propagate(&mut self) -> Result<(), (usize, Vec<Lit>)> {
606        let base_level = self.user_scopes.last().map(|&(lvl, _)| lvl).unwrap_or(0);
607        if let Err((bt_level, conflict)) = self.sat_solver.propagate() {
608            return Err((bt_level.max(base_level), conflict));
609        }
610
611        while self.notified_len < self.sat_solver.trail.len() {
612            let lit = self.sat_solver.trail[self.notified_len];
613
614            if let Some(constraint) = self.registry.get_constraint(lit).or_else(|| self.registry.get_constraint(!lit)) {
615                let theory_result = match (constraint, lit.sign()) {
616                    (TheoryConstraint::LraUb(var, bound), false) => self.lra_theory.set_ub(Some(lit), *var, bound.clone()),
617                    (TheoryConstraint::LraLb(var, bound), true) => self.lra_theory.set_ub(Some(lit), *var, InfRational::new(bound.rational_part().clone(), if bound.infinitesimal_part().is_positive() { rug::Rational::from(0) } else { rug::Rational::from(-1) })),
618                    (TheoryConstraint::LraLb(var, bound), false) => self.lra_theory.set_lb(Some(lit), *var, bound.clone()),
619                    (TheoryConstraint::LraUb(var, bound), true) => self.lra_theory.set_lb(Some(lit), *var, InfRational::new(bound.rational_part().clone(), if bound.infinitesimal_part().is_negative() { rug::Rational::from(0) } else { rug::Rational::from(1) })),
620                    (TheoryConstraint::EnumEq(var, val), false) => self.enum_theory.set_eq(Some(lit), *var, *val),
621                    (TheoryConstraint::EnumEq(var, val), true) => self.enum_theory.set_neq(Some(lit), *var, *val),
622                };
623
624                if let Err(lemma) = theory_result {
625                    return Err((self.compute_backtrack_level(&lemma, base_level), lemma));
626                }
627            }
628            self.notified_len += 1;
629        }
630
631        if let Err(conflict) = self.lra_theory.check() {
632            return Err((self.compute_backtrack_level(&conflict, base_level), conflict));
633        }
634        Ok(())
635    }
636
637    /// Returns the assigned value of a literal in the current trail.
638    pub fn get_lit_val(&self, lit: Lit) -> Option<bool> {
639        self.sat_solver.lit_value(lit)
640    }
641
642    /// Returns the assigned value of a Boolean expression when it is fully determined.
643    pub fn get_bool_val(&self, expr: &BoolExpr) -> Option<bool> {
644        match expr {
645            BoolExpr::True => Some(true),
646            BoolExpr::False => Some(false),
647            BoolExpr::Var(v) => *self.sat_solver.value(*v),
648            BoolExpr::Not(inner) => self.get_bool_val(inner).map(|val| !val),
649            BoolExpr::And(args) => {
650                let mut result = Some(true);
651                for arg in args {
652                    match self.get_bool_val(arg) {
653                        Some(val) => {
654                            if !val {
655                                return Some(false);
656                            }
657                        }
658                        None => result = None,
659                    }
660                }
661                result
662            }
663            BoolExpr::Or(args) => {
664                let mut result = Some(false);
665                for arg in args {
666                    match self.get_bool_val(arg) {
667                        Some(val) => {
668                            if val {
669                                return Some(true);
670                            }
671                        }
672                        None => result = None,
673                    }
674                }
675                result
676            }
677            BoolExpr::Lt(e1, e2) => {
678                let (lb1, ub1) = self.get_arith_bounds(e1)?;
679                let (lb2, ub2) = self.get_arith_bounds(e2)?;
680                if ub1 < lb2 {
681                    Some(true)
682                } else if lb1 >= ub2 {
683                    Some(false)
684                } else {
685                    None
686                }
687            }
688            BoolExpr::Le(e1, e2) => {
689                let (lb1, ub1) = self.get_arith_bounds(e1)?;
690                let (lb2, ub2) = self.get_arith_bounds(e2)?;
691                if ub1 <= lb2 {
692                    Some(true)
693                } else if lb1 > ub2 {
694                    Some(false)
695                } else {
696                    None
697                }
698            }
699            BoolExpr::Ge(e1, e2) => {
700                let (lb1, ub1) = self.get_arith_bounds(e1)?;
701                let (lb2, ub2) = self.get_arith_bounds(e2)?;
702                if lb1 >= ub2 {
703                    Some(true)
704                } else if ub1 < lb2 {
705                    Some(false)
706                } else {
707                    None
708                }
709            }
710            BoolExpr::Gt(e1, e2) => {
711                let (lb1, ub1) = self.get_arith_bounds(e1)?;
712                let (lb2, ub2) = self.get_arith_bounds(e2)?;
713                if lb1 > ub2 {
714                    Some(true)
715                } else if ub1 <= lb2 {
716                    Some(false)
717                } else {
718                    None
719                }
720            }
721            BoolExpr::Eq(e1, e2) => match (e1.as_ref(), e2.as_ref()) {
722                (Expr::Arith(a1), Expr::Arith(a2)) => {
723                    let (lb1, ub1) = self.get_arith_bounds(a1)?;
724                    let (lb2, ub2) = self.get_arith_bounds(a2)?;
725                    if ub1 < lb2 || ub2 < lb1 {
726                        Some(false)
727                    } else if lb1 == ub1 && lb2 == ub2 && lb1 == lb2 {
728                        Some(true)
729                    } else {
730                        None
731                    }
732                }
733                (Expr::Bool(b1), Expr::Bool(b2)) => {
734                    let val1 = self.get_bool_val(b1);
735                    let val2 = self.get_bool_val(b2);
736                    match (val1, val2) {
737                        (Some(v1), Some(v2)) => Some(v1 == v2),
738                        _ => None,
739                    }
740                }
741                (Expr::Enum(e1), Expr::Enum(e2)) => {
742                    let val1 = self.get_enum_val(e1);
743                    let val2 = self.get_enum_val(e2);
744                    match (val1, val2) {
745                        (Some(v1), Some(v2)) => Some(v1 == v2),
746                        _ => None,
747                    }
748                }
749                _ => None,
750            },
751        }
752    }
753
754    /// Returns the current value of an arithmetic expression when it is fixed by the model.
755    pub fn get_arith_val(&self, expr: &ArithExpr) -> Option<InfRational> {
756        match expr {
757            ArithExpr::Const(c) => Some(InfRational::new(Rational::Finite(c.clone()), rug::Rational::from(0))),
758            ArithExpr::RealVar(v) | ArithExpr::IntVar(v) => Some(self.lra_theory.value(*v).clone()),
759            ArithExpr::Add(terms) => {
760                let mut sum = InfRational::new(Rational::Finite(rug::Rational::from(0)), rug::Rational::from(0));
761                for term in terms {
762                    sum += self.get_arith_val(term)?;
763                }
764                Some(sum)
765            }
766            ArithExpr::Neg(term) => self.get_arith_val(term).map(|val| -val),
767            _ => None,
768        }
769    }
770
771    /// Returns the current lower and upper bounds of an arithmetic expression when they are fixed by the model.
772    pub fn get_arith_bounds(&self, expr: &ArithExpr) -> Option<(InfRational, InfRational)> {
773        match expr {
774            ArithExpr::Const(c) => {
775                let val = InfRational::new(Rational::Finite(c.clone()), rug::Rational::from(0));
776                Some((val.clone(), val))
777            }
778            ArithExpr::RealVar(v) | ArithExpr::IntVar(v) => Some((self.lra_theory.lb(*v).clone(), self.lra_theory.ub(*v).clone())),
779            ArithExpr::Add(terms) => {
780                let mut sum_lb = InfRational::new(Rational::Finite(rug::Rational::from(0)), rug::Rational::from(0));
781                let mut sum_ub = sum_lb.clone();
782                for term in terms {
783                    let (lb, ub) = self.get_arith_bounds(term)?;
784                    sum_lb += lb;
785                    sum_ub += ub;
786                }
787                Some((sum_lb, sum_ub))
788            }
789            ArithExpr::Neg(term) => {
790                let (lb, ub) = self.get_arith_bounds(term)?;
791                Some((-ub, -lb))
792            }
793            _ => None,
794        }
795    }
796
797    /// Returns the concrete value of an enum variable if it has been fully assigned.
798    pub fn get_enum_val(&self, expr: &EnumExpr) -> Option<i32> {
799        match expr {
800            EnumExpr::Const(c) => Some(*c),
801            EnumExpr::Var(v) => {
802                let domain = &self.enum_theory.active_domains[*v];
803                if domain.len() == 1 { domain.iter().next().copied() } else { None }
804            }
805        }
806    }
807
808    /// Opens a new incremental user scope for assertions and decisions.
809    ///
810    /// All constraints/decisions added after this call can be discarded by
811    /// [`SeMiTONE::pop`].
812    pub fn push(&mut self) {
813        let clauses_len = self.sat_solver.clauses.len();
814
815        self.sat_solver.push();
816        self.lra_theory.push();
817        self.enum_theory.push();
818
819        let current_level = self.sat_solver.decision_level();
820        self.user_scopes.push((current_level, clauses_len));
821    }
822
823    /// Restores the previous user scope and discards assertions added in it.
824    ///
825    /// If no user scope is open, this is a no-op.
826    pub fn pop(&mut self) {
827        if let Some((saved_level, saved_clauses_len)) = self.user_scopes.pop() {
828            let target_level = saved_level - 1;
829            self.sat_solver.cancel_until(target_level);
830            self.lra_theory.cancel_until(target_level);
831            self.enum_theory.cancel_until(target_level);
832            self.notified_len = self.sat_solver.trail.len();
833
834            for watch_list in self.sat_solver.watches.iter_mut() {
835                watch_list.retain(|&clause_idx| clause_idx < saved_clauses_len);
836            }
837            self.sat_solver.clauses.truncate(saved_clauses_len);
838        }
839    }
840
841    fn compute_backtrack_level(&self, lemma: &[Lit], root_level: usize) -> usize {
842        if lemma.len() <= 1 {
843            return root_level;
844        }
845
846        let mut levels: Vec<usize> = lemma.iter().map(|lit| self.sat_solver.level(lit.var()).expect("literal should have a decision level")).collect();
847
848        levels.sort_unstable_by(|a, b| b.cmp(a));
849
850        let max_level = levels[0];
851
852        if max_level <= root_level {
853            return root_level;
854        }
855
856        if levels.iter().filter(|&&l| l == max_level).count() == 1 { levels[1].max(root_level) } else { (max_level - 1).max(root_level) }
857    }
858
859    /// Checks integrality of integer variables under the current rational model.
860    ///
861    /// Returns `Ok(())` if all integer variables are integral.
862    /// Otherwise returns `Err((backtrack_level, lemma))`, where `lemma` is either
863    /// a generated Gomory cut or a branching disjunction for branch-and-bound.
864    pub fn check_ints(&mut self) -> Result<(), (usize, Vec<Lit>)> {
865        if let Err((var, frac_val)) = self.lra_theory.check_ints() {
866            let base_level = self.user_scopes.last().map(|&(lvl, _)| lvl).unwrap_or(0);
867            if let Some((cut_row, f0)) = self.lra_theory.generate_gomory_cut(var) {
868                let cut_slack = self.lra_theory.get_or_create_slack(cut_row);
869                let bound = InfRational::new(Rational::Finite(f0), rug::Rational::from(0));
870                let cut_lit = self.get_or_create_proxy(TheoryConstraint::LraLb(cut_slack, bound));
871
872                let lemma = vec![cut_lit];
873                let base_level = self.user_scopes.last().map(|&(lvl, _)| lvl).unwrap_or(0);
874                return Err((base_level, lemma));
875            }
876
877            let Rational::Finite(inner_frac) = frac_val else {
878                unreachable!("Fractional variable in Branch & Bound must be finite");
879            };
880
881            let mut floor_val = inner_frac.clone();
882            floor_val.floor_mut();
883            let mut ceil_val = inner_frac;
884            ceil_val.ceil_mut();
885
886            let ub = InfRational::new(Rational::Finite(floor_val), rug::Rational::from(0));
887            let lb = InfRational::new(Rational::Finite(ceil_val), rug::Rational::from(0));
888
889            let lit_ub = self.get_or_create_proxy(TheoryConstraint::LraUb(var, ub));
890            let lit_lb = self.get_or_create_proxy(TheoryConstraint::LraLb(var, lb));
891
892            let lemma = vec![lit_ub, lit_lb];
893            return Err((base_level, lemma));
894        }
895        Ok(())
896    }
897}
898
899#[cold]
900#[inline(never)]
901pub(crate) fn out_of_bounds(var: usize) -> ! {
902    panic!("variable index out of bounds: {}", var);
903}
904
905#[cfg(test)]
906mod tests {
907    use super::*;
908
909    #[test]
910    fn test_pure_sat_resolution() {
911        let mut solver = SeMiTONE::new();
912
913        let a = solver.new_bool();
914        let b = solver.new_bool();
915        let c = solver.new_bool();
916
917        // (A ∨ B) ∧ (¬B ∨ C) ∧ (¬B ∨ ¬C) ∧ (¬A)
918        // With ¬A, clause (A ∨ B) forces B; then B forces both C and ¬C.
919        let expr = (&a | &b) & (&!&b | &c) & (!&b | !&c) & !&a;
920
921        let _ = solver.assert(&expr);
922        assert!(solver.propagate().is_err(), "The solver should detect that the system is unsatisfiable");
923    }
924
925    #[test]
926    fn test_early_bounding_unsat() {
927        let mut solver = SeMiTONE::new();
928        let x = solver.new_real();
929
930        // x > 10 ∧ x < 5
931        let expr = (x.clone().gt(10)) & (x.lt(5));
932
933        let result = solver.assert(&expr);
934        assert!(!result, "The solver should detect that the system is unsatisfiable");
935    }
936
937    #[test]
938    fn test_equality_mutually_exclusive() {
939        let mut solver = SeMiTONE::new();
940        let x = solver.new_real();
941
942        // x == 5 ∧ x > 6
943        let expr = (x.clone().eq(5)) & (x.gt(6));
944
945        let result = solver.assert(&expr);
946        assert!(!result, "The solver should detect that the system is unsatisfiable");
947    }
948
949    #[test]
950    fn test_simplex_system_unsat() {
951        let mut solver = SeMiTONE::new();
952        let x = solver.new_real();
953        let y = solver.new_real();
954
955        // x + y == 10
956        let eq_expr = (x.clone() + y.clone()).eq(10);
957        // x > 6
958        let gt_x = x.clone().gt(6);
959        // y > 6
960        let gt_y = y.clone().gt(6);
961
962        let expr = eq_expr & gt_x & gt_y;
963
964        let _ = solver.assert(&expr);
965        assert!(solver.propagate().is_err(), "The solver should detect that the system is unsatisfiable");
966    }
967
968    #[test]
969    fn test_constant_arithmetic_evaluations() {
970        let mut solver = SeMiTONE::new();
971
972        assert!(solver.assert(&ArithExpr::from(5).lt(10)));
973        assert!(solver.assert(&ArithExpr::from(5).le(5)));
974        assert!(solver.assert(&ArithExpr::from(10).ge(5)));
975        assert!(solver.assert(&ArithExpr::from(10).gt(5)));
976
977        assert!(!solver.assert(&ArithExpr::from(10).lt(5)));
978        assert!(!solver.assert(&ArithExpr::from(10).le(5)));
979        assert!(!solver.assert(&ArithExpr::from(5).ge(10)));
980        assert!(!solver.assert(&ArithExpr::from(5).gt(10)));
981
982        assert!(solver.assert(&!ArithExpr::from(10).lt(5)));
983        assert!(!solver.assert(&!ArithExpr::from(5).lt(10)));
984    }
985
986    #[test]
987    fn test_negated_variable_inequalities() {
988        let mut solver = SeMiTONE::new();
989        let x = solver.new_real();
990
991        solver.push();
992        assert!(solver.assert(&!x.clone().lt(5)));
993        assert!(!solver.assert(&x.clone().lt(4)));
994        solver.pop();
995
996        solver.push();
997        assert!(solver.assert(&!x.clone().le(5)));
998        assert!(!solver.assert(&x.clone().le(5)));
999        solver.pop();
1000
1001        solver.push();
1002        assert!(solver.assert(&!x.clone().ge(5)));
1003        assert!(!solver.assert(&x.clone().ge(5)));
1004        solver.pop();
1005
1006        solver.push();
1007        assert!(solver.assert(&!x.clone().gt(5)));
1008        assert!(!solver.assert(&x.clone().gt(5)));
1009        solver.pop();
1010    }
1011
1012    #[test]
1013    #[should_panic(expected = "Type mismatch in Eq")]
1014    fn test_encode_eq_type_mismatch_panic() {
1015        let mut solver = SeMiTONE::new();
1016        let a = solver.new_bool();
1017        let x = solver.new_real();
1018
1019        let bad_eq = BoolExpr::Eq(Box::new(Expr::Bool(a)), Box::new(Expr::Arith(x)));
1020
1021        let _ = solver.assert(&bad_eq);
1022    }
1023
1024    #[test]
1025    fn test_enum_out_of_domain_unsat() {
1026        let mut solver = SeMiTONE::new();
1027        let e = solver.new_enum(vec![1, 2]);
1028
1029        let expr = e.eq(3);
1030
1031        let _ = solver.assert(&expr);
1032        assert!(solver.propagate().is_err(), "The solver should detect that the enum variable cannot take a value outside its domain");
1033    }
1034
1035    #[test]
1036    fn test_enum_exhaustive_denial_integration() {
1037        let mut solver = SeMiTONE::new();
1038        let e = solver.new_enum(vec![1, 2]);
1039
1040        // (e != 1) AND (e != 2)
1041        let expr = !(e.clone().eq(1)) & !(e.clone().eq(2));
1042
1043        let _ = solver.assert(&expr);
1044        assert!(solver.propagate().is_err(), "The solver should detect that the enum variable cannot take a value outside its domain");
1045    }
1046}
semitone/lib.rs

semitone/
lib.rs
