oxiz_theories/string/
solver.rs

1//! String Theory Solver
2//!
3//! Implements the SMT-LIB theory of strings (QF_S, QF_SLIA) using:
4//! - Word equation solving via Levi's lemma and Nielsen transformations
5//! - Length abstraction for interaction with arithmetic
6//! - Brzozowski derivatives for regex membership
7//! - Lazy axiom instantiation
8
9use super::regex::{Regex, RegexAutomaton};
10use crate::theory::{Theory, TheoryId, TheoryResult};
11use oxiz_core::ast::TermId;
12use oxiz_core::error::Result;
13use rustc_hash::FxHashMap;
14use smallvec::SmallVec;
15use std::sync::Arc;
16
17/// String constraint kinds
18#[allow(dead_code)]
19#[derive(Debug, Clone)]
20pub enum StringConstraint {
21    /// String equality: s1 = s2
22    Eq(StringExpr, StringExpr, TermId),
23    /// String disequality: s1 ≠ s2
24    Neq(StringExpr, StringExpr, TermId),
25    /// Length constraint: len(s) = n
26    Length(u32, i64, TermId),
27    /// Prefix: str.prefixof(s1, s2)
28    Prefix(StringExpr, StringExpr, TermId),
29    /// Suffix: str.suffixof(s1, s2)
30    Suffix(StringExpr, StringExpr, TermId),
31    /// Contains: str.contains(s1, s2)
32    Contains(StringExpr, StringExpr, TermId),
33    /// Regex membership: str.in_re(s, re)
34    InRegex(u32, Arc<Regex>, TermId),
35    /// Not in regex
36    NotInRegex(u32, Arc<Regex>, TermId),
37    /// String to integer: int = str.to_int(s)
38    StrToInt(u32, i64, TermId),
39    /// Integer to string: s = str.from_int(int)
40    IntToStr(u32, i64, TermId),
41}
42
43/// A string expression (concatenation of atoms)
44#[derive(Debug, Clone, PartialEq, Eq, Hash)]
45pub struct StringExpr {
46    /// Atoms in left-to-right order
47    pub atoms: SmallVec<[StringAtom; 4]>,
48}
49
50impl StringExpr {
51    /// Empty string
52    pub fn empty() -> Self {
53        Self {
54            atoms: SmallVec::new(),
55        }
56    }
57
58    /// Single variable
59    pub fn var(id: u32) -> Self {
60        let mut atoms = SmallVec::new();
61        atoms.push(StringAtom::Var(id));
62        Self { atoms }
63    }
64
65    /// String literal
66    pub fn literal(s: &str) -> Self {
67        if s.is_empty() {
68            Self::empty()
69        } else {
70            let mut atoms = SmallVec::new();
71            atoms.push(StringAtom::Const(s.to_string()));
72            Self { atoms }
73        }
74    }
75
76    /// Concatenate two expressions
77    pub fn concat(self, other: Self) -> Self {
78        let mut atoms = self.atoms;
79        // Merge adjacent constants
80        if let (Some(StringAtom::Const(a)), Some(StringAtom::Const(b))) =
81            (atoms.last_mut(), other.atoms.first())
82        {
83            a.push_str(b);
84            atoms.extend(other.atoms.into_iter().skip(1));
85        } else {
86            atoms.extend(other.atoms);
87        }
88        Self { atoms }
89    }
90
91    /// Check if this is a constant string
92    pub fn as_const(&self) -> Option<&str> {
93        if self.atoms.len() == 1 {
94            if let StringAtom::Const(s) = &self.atoms[0] {
95                return Some(s);
96            }
97        } else if self.atoms.is_empty() {
98            return Some("");
99        }
100        None
101    }
102
103    /// Check if this is a single variable
104    pub fn as_var(&self) -> Option<u32> {
105        if self.atoms.len() == 1
106            && let StringAtom::Var(id) = &self.atoms[0]
107        {
108            return Some(*id);
109        }
110        None
111    }
112
113    /// Check if empty
114    pub fn is_empty(&self) -> bool {
115        self.atoms.is_empty()
116            || (self.atoms.len() == 1
117                && matches!(&self.atoms[0], StringAtom::Const(s) if s.is_empty()))
118    }
119
120    /// Minimum possible length
121    pub fn min_length(&self) -> usize {
122        self.atoms
123            .iter()
124            .map(|a| match a {
125                StringAtom::Const(s) => s.len(),
126                StringAtom::Var(_) => 0,
127            })
128            .sum()
129    }
130
131    /// First character (if constant prefix)
132    pub fn first_char(&self) -> Option<char> {
133        self.atoms.first().and_then(|a| match a {
134            StringAtom::Const(s) => s.chars().next(),
135            StringAtom::Var(_) => None,
136        })
137    }
138}
139
140/// A string atom (variable or constant)
141#[derive(Debug, Clone, PartialEq, Eq, Hash)]
142pub enum StringAtom {
143    /// String variable
144    Var(u32),
145    /// String constant
146    Const(String),
147}
148
149/// Word equation of the form lhs = rhs (both are concatenations)
150#[derive(Debug, Clone)]
151pub struct WordEquation {
152    /// Left-hand side atoms
153    pub lhs: StringExpr,
154    /// Right-hand side atoms
155    pub rhs: StringExpr,
156    /// Origin term for conflict explanation
157    pub origin: TermId,
158}
159
160impl WordEquation {
161    /// Check if this equation is trivially satisfied (both sides equal)
162    pub fn is_solved(&self) -> bool {
163        self.lhs == self.rhs
164    }
165
166    /// Check if this equation has an obvious conflict
167    pub fn has_conflict(&self) -> bool {
168        // If both sides are constants and differ, conflict
169        if let (Some(l), Some(r)) = (self.lhs.as_const(), self.rhs.as_const()) {
170            return l != r;
171        }
172        // If one side is empty but other has constants, conflict
173        if self.lhs.is_empty() && !self.rhs.is_empty() && self.rhs.min_length() > 0 {
174            return true;
175        }
176        if self.rhs.is_empty() && !self.lhs.is_empty() && self.lhs.min_length() > 0 {
177            return true;
178        }
179        // Different constant prefixes
180        if let (Some(l), Some(r)) = (self.lhs.first_char(), self.rhs.first_char()) {
181            return l != r;
182        }
183        false
184    }
185}
186
187/// A length constraint for interaction with arithmetic
188#[derive(Debug, Clone)]
189pub struct LengthConstraint {
190    /// Variable ID
191    pub var: u32,
192    /// Lower bound (inclusive)
193    pub lower: Option<i64>,
194    /// Upper bound (inclusive)
195    pub upper: Option<i64>,
196    /// Equality constraint
197    pub equal: Option<i64>,
198}
199
200/// String theory solver
201#[derive(Debug)]
202pub struct StringSolver {
203    /// Next variable ID
204    next_var: u32,
205    /// Term to variable mapping
206    term_to_var: FxHashMap<TermId, u32>,
207    /// Variable to term mapping
208    var_to_term: Vec<Option<TermId>>,
209    /// String variable assignments (if known)
210    assignments: FxHashMap<u32, String>,
211    /// Active word equations
212    equations: Vec<WordEquation>,
213    /// Length constraints
214    lengths: Vec<LengthConstraint>,
215    /// Regex membership constraints
216    regex_constraints: Vec<(u32, Arc<Regex>, bool, TermId)>,
217    /// Disequalities
218    diseqs: Vec<(StringExpr, StringExpr, TermId)>,
219    /// Prefix constraints
220    prefixes: Vec<(StringExpr, StringExpr, TermId)>,
221    /// Suffix constraints
222    suffixes: Vec<(StringExpr, StringExpr, TermId)>,
223    /// Contains constraints
224    contains: Vec<(StringExpr, StringExpr, TermId)>,
225    /// String-to-int constraints: (str_var, int_value, origin)
226    str_to_int: Vec<(u32, i64, TermId)>,
227    /// Int-to-string constraints: (str_var, int_value, origin)
228    int_to_str: Vec<(u32, i64, TermId)>,
229    /// Context stack for push/pop
230    context_stack: Vec<ContextState>,
231    /// Current conflict (if any)
232    current_conflict: Option<Vec<TermId>>,
233    /// Cached regex automata
234    regex_automata: FxHashMap<u64, RegexAutomaton>,
235    /// Propagated equalities
236    propagated: Vec<(TermId, Vec<TermId>)>,
237}
238
239/// Context state for push/pop
240#[derive(Debug, Clone)]
241struct ContextState {
242    num_vars: usize,
243    num_equations: usize,
244    num_lengths: usize,
245    num_regex: usize,
246    num_diseqs: usize,
247    num_prefixes: usize,
248    num_suffixes: usize,
249    num_contains: usize,
250    num_str_to_int: usize,
251    num_int_to_str: usize,
252    assignments_snapshot: FxHashMap<u32, String>,
253}
254
255impl StringSolver {
256    /// Create a new string solver
257    pub fn new() -> Self {
258        Self {
259            next_var: 0,
260            term_to_var: FxHashMap::default(),
261            var_to_term: Vec::new(),
262            assignments: FxHashMap::default(),
263            equations: Vec::new(),
264            lengths: Vec::new(),
265            regex_constraints: Vec::new(),
266            diseqs: Vec::new(),
267            prefixes: Vec::new(),
268            suffixes: Vec::new(),
269            contains: Vec::new(),
270            str_to_int: Vec::new(),
271            int_to_str: Vec::new(),
272            context_stack: Vec::new(),
273            current_conflict: None,
274            regex_automata: FxHashMap::default(),
275            propagated: Vec::new(),
276        }
277    }
278
279    /// Get or create a variable for a term
280    fn get_or_create_var(&mut self, term: TermId) -> u32 {
281        if let Some(&var) = self.term_to_var.get(&term) {
282            return var;
283        }
284        let var = self.next_var;
285        self.next_var += 1;
286        self.term_to_var.insert(term, var);
287        self.var_to_term.push(Some(term));
288        var
289    }
290
291    /// Add a string equality
292    pub fn add_equality(&mut self, lhs: StringExpr, rhs: StringExpr, origin: TermId) {
293        let eq = WordEquation { lhs, rhs, origin };
294        if eq.has_conflict() {
295            self.current_conflict = Some(vec![origin]);
296        } else if !eq.is_solved() {
297            self.equations.push(eq);
298        }
299    }
300
301    /// Add a string disequality
302    pub fn add_disequality(&mut self, lhs: StringExpr, rhs: StringExpr, origin: TermId) {
303        // Check for immediate conflict if both are the same constant
304        if let (Some(l), Some(r)) = (lhs.as_const(), rhs.as_const())
305            && l == r
306        {
307            self.current_conflict = Some(vec![origin]);
308            return;
309        }
310        self.diseqs.push((lhs, rhs, origin));
311    }
312
313    /// Add a length constraint
314    pub fn add_length_eq(&mut self, var: u32, len: i64, origin: TermId) {
315        if len < 0 {
316            self.current_conflict = Some(vec![origin]);
317            return;
318        }
319        self.lengths.push(LengthConstraint {
320            var,
321            lower: None,
322            upper: None,
323            equal: Some(len),
324        });
325    }
326
327    /// Add regex membership constraint
328    pub fn add_regex_membership(
329        &mut self,
330        var: u32,
331        regex: Arc<Regex>,
332        positive: bool,
333        origin: TermId,
334    ) {
335        // Quick check for empty regex
336        if regex.is_empty() && positive {
337            self.current_conflict = Some(vec![origin]);
338            return;
339        }
340        if regex.is_all() && !positive {
341            self.current_conflict = Some(vec![origin]);
342            return;
343        }
344        self.regex_constraints.push((var, regex, positive, origin));
345    }
346
347    /// Add prefix constraint: str.prefixof(prefix, s)
348    pub fn add_prefix(&mut self, prefix: StringExpr, s: StringExpr, origin: TermId) {
349        // Check for immediate conflict
350        if let (Some(p), Some(s_str)) = (prefix.as_const(), s.as_const())
351            && !s_str.starts_with(p)
352        {
353            self.current_conflict = Some(vec![origin]);
354            return;
355        }
356        self.prefixes.push((prefix, s, origin));
357    }
358
359    /// Add suffix constraint: str.suffixof(suffix, s)
360    pub fn add_suffix(&mut self, suffix: StringExpr, s: StringExpr, origin: TermId) {
361        if let (Some(suf), Some(s_str)) = (suffix.as_const(), s.as_const())
362            && !s_str.ends_with(suf)
363        {
364            self.current_conflict = Some(vec![origin]);
365            return;
366        }
367        self.suffixes.push((suffix, s, origin));
368    }
369
370    /// Add contains constraint: str.contains(s, substr)
371    pub fn add_contains(&mut self, s: StringExpr, substr: StringExpr, origin: TermId) {
372        if let (Some(s_str), Some(sub)) = (s.as_const(), substr.as_const())
373            && !s_str.contains(sub)
374        {
375            self.current_conflict = Some(vec![origin]);
376            return;
377        }
378        self.contains.push((s, substr, origin));
379    }
380
381    /// Add string-to-int constraint: int = str.to_int(s)
382    /// Returns the integer value that string s represents
383    /// Returns -1 if s is not a valid numeral
384    pub fn add_str_to_int(&mut self, str_var: u32, int_value: i64, origin: TermId) {
385        // Check if we have a concrete assignment for the string variable
386        if let Some(s) = self.assignments.get(&str_var) {
387            // Try to parse the string as an integer
388            match s.parse::<i64>() {
389                Ok(parsed) => {
390                    if parsed != int_value {
391                        self.current_conflict = Some(vec![origin]);
392                        return;
393                    }
394                }
395                Err(_) => {
396                    // Invalid numeral should return -1
397                    if int_value != -1 {
398                        self.current_conflict = Some(vec![origin]);
399                        return;
400                    }
401                }
402            }
403        }
404        self.str_to_int.push((str_var, int_value, origin));
405    }
406
407    /// Add int-to-string constraint: s = str.from_int(int)
408    /// Converts integer to its decimal string representation
409    pub fn add_int_to_str(&mut self, str_var: u32, int_value: i64, origin: TermId) {
410        // Check if we have a concrete assignment for the string variable
411        if let Some(s) = self.assignments.get(&str_var) {
412            let expected = if int_value < 0 {
413                // Negative integers should produce empty string in SMT-LIB2
414                String::new()
415            } else {
416                int_value.to_string()
417            };
418
419            if s != &expected {
420                self.current_conflict = Some(vec![origin]);
421                return;
422            }
423        }
424        self.int_to_str.push((str_var, int_value, origin));
425    }
426
427    /// Solve word equations using Nielsen transformation
428    fn solve_equations(&mut self) -> Option<Vec<TermId>> {
429        // Simple equation solving via substitution and case analysis
430        let mut changed = true;
431        let mut iterations = 0;
432        const MAX_ITERATIONS: usize = 1000;
433
434        while changed && iterations < MAX_ITERATIONS {
435            changed = false;
436            iterations += 1;
437
438            let mut i = 0;
439            while i < self.equations.len() {
440                let eq = &self.equations[i];
441
442                // Check for conflict
443                if eq.has_conflict() {
444                    return Some(vec![eq.origin]);
445                }
446
447                // Check if solved
448                if eq.is_solved() {
449                    self.equations.swap_remove(i);
450                    changed = true;
451                    continue;
452                }
453
454                // Try to make progress via Levi's lemma
455                if let Some(result) = self.apply_levi(&self.equations[i].clone()) {
456                    match result {
457                        LeviResult::Solved => {
458                            self.equations.swap_remove(i);
459                            changed = true;
460                            continue;
461                        }
462                        LeviResult::Conflict(origin) => {
463                            return Some(vec![origin]);
464                        }
465                        LeviResult::Progress(new_eqs) => {
466                            let origin = self.equations[i].origin;
467                            self.equations.swap_remove(i);
468                            for (lhs, rhs) in new_eqs {
469                                self.equations.push(WordEquation { lhs, rhs, origin });
470                            }
471                            changed = true;
472                            continue;
473                        }
474                        LeviResult::NoProgress => {}
475                    }
476                }
477
478                i += 1;
479            }
480        }
481
482        None
483    }
484
485    /// Apply Levi's lemma to an equation
486    fn apply_levi(&self, eq: &WordEquation) -> Option<LeviResult> {
487        let lhs = &eq.lhs;
488        let rhs = &eq.rhs;
489
490        // Empty = Empty
491        if lhs.is_empty() && rhs.is_empty() {
492            return Some(LeviResult::Solved);
493        }
494
495        // Empty = non-empty with constants -> conflict
496        if lhs.is_empty() && rhs.min_length() > 0 {
497            return Some(LeviResult::Conflict(eq.origin));
498        }
499        if rhs.is_empty() && lhs.min_length() > 0 {
500            return Some(LeviResult::Conflict(eq.origin));
501        }
502
503        // Both start with same constant prefix
504        if let (Some(l), Some(r)) = (lhs.first_char(), rhs.first_char()) {
505            if l == r {
506                // Strip common prefix
507                let mut new_lhs = lhs.clone();
508                let mut new_rhs = rhs.clone();
509                self.strip_common_prefix(&mut new_lhs, &mut new_rhs);
510                if new_lhs != *lhs || new_rhs != *rhs {
511                    return Some(LeviResult::Progress(vec![(new_lhs, new_rhs)]));
512                }
513            } else {
514                return Some(LeviResult::Conflict(eq.origin));
515            }
516        }
517
518        // x . α = y . β where x, y are variables
519        // Case split: x = y ∧ α = β, or x = y.γ ∧ γ.α = β, or y = x.γ ∧ α = γ.β
520        // For now, we just handle simple cases
521
522        None
523    }
524
525    /// Strip common prefix from two expressions
526    fn strip_common_prefix(&self, lhs: &mut StringExpr, rhs: &mut StringExpr) {
527        while !lhs.atoms.is_empty() && !rhs.atoms.is_empty() {
528            match (&lhs.atoms[0], &rhs.atoms[0]) {
529                (StringAtom::Const(a), StringAtom::Const(b)) => {
530                    let common_len = a.chars().zip(b.chars()).take_while(|(x, y)| x == y).count();
531                    if common_len == 0 {
532                        break;
533                    }
534                    let a_chars: Vec<char> = a.chars().collect();
535                    let b_chars: Vec<char> = b.chars().collect();
536                    if common_len == a_chars.len() && common_len == b_chars.len() {
537                        lhs.atoms.remove(0);
538                        rhs.atoms.remove(0);
539                    } else if common_len == a_chars.len() {
540                        lhs.atoms.remove(0);
541                        rhs.atoms[0] = StringAtom::Const(b_chars[common_len..].iter().collect());
542                    } else if common_len == b_chars.len() {
543                        rhs.atoms.remove(0);
544                        lhs.atoms[0] = StringAtom::Const(a_chars[common_len..].iter().collect());
545                    } else {
546                        lhs.atoms[0] = StringAtom::Const(a_chars[common_len..].iter().collect());
547                        rhs.atoms[0] = StringAtom::Const(b_chars[common_len..].iter().collect());
548                        break;
549                    }
550                }
551                (StringAtom::Var(x), StringAtom::Var(y)) if x == y => {
552                    lhs.atoms.remove(0);
553                    rhs.atoms.remove(0);
554                }
555                _ => break,
556            }
557        }
558    }
559
560    /// Check regex constraints
561    fn check_regex_constraints(&mut self) -> Option<Vec<TermId>> {
562        for (var, regex, positive, origin) in &self.regex_constraints {
563            if let Some(value) = self.assignments.get(var) {
564                let matches = regex.matches(value);
565                if *positive && !matches {
566                    return Some(vec![*origin]);
567                }
568                if !*positive && matches {
569                    return Some(vec![*origin]);
570                }
571            }
572        }
573        None
574    }
575
576    /// Check disequality constraints
577    fn check_diseqs(&self) -> Option<Vec<TermId>> {
578        for (lhs, rhs, origin) in &self.diseqs {
579            if let (Some(l), Some(r)) = (self.eval_expr(lhs), self.eval_expr(rhs))
580                && l == r
581            {
582                return Some(vec![*origin]);
583            }
584        }
585        None
586    }
587
588    /// Check str.to_int constraints
589    fn check_str_to_int(&self) -> Option<Vec<TermId>> {
590        for (str_var, expected_int, origin) in &self.str_to_int {
591            if let Some(s) = self.assignments.get(str_var) {
592                // Invalid numeral returns -1
593                let actual_int = s.parse::<i64>().unwrap_or(-1);
594                if actual_int != *expected_int {
595                    return Some(vec![*origin]);
596                }
597            }
598        }
599        None
600    }
601
602    /// Check str.from_int constraints
603    fn check_int_to_str(&self) -> Option<Vec<TermId>> {
604        for (str_var, int_value, origin) in &self.int_to_str {
605            if let Some(s) = self.assignments.get(str_var) {
606                let expected = if *int_value < 0 {
607                    // Negative integers produce empty string
608                    String::new()
609                } else {
610                    int_value.to_string()
611                };
612                if s != &expected {
613                    return Some(vec![*origin]);
614                }
615            }
616        }
617        None
618    }
619
620    /// Evaluate a string expression under current assignments
621    fn eval_expr(&self, expr: &StringExpr) -> Option<String> {
622        let mut result = String::new();
623        for atom in &expr.atoms {
624            match atom {
625                StringAtom::Const(s) => result.push_str(s),
626                StringAtom::Var(v) => {
627                    if let Some(s) = self.assignments.get(v) {
628                        result.push_str(s);
629                    } else {
630                        return None;
631                    }
632                }
633            }
634        }
635        Some(result)
636    }
637
638    /// Check length constraints
639    fn check_lengths(&self) -> Option<Vec<TermId>> {
640        for lc in &self.lengths {
641            if let Some(value) = self.assignments.get(&lc.var) {
642                let len = value.len() as i64;
643                if let Some(eq) = lc.equal
644                    && len != eq
645                {
646                    // Find origin term - would need to track this
647                    continue;
648                }
649                if let Some(lo) = lc.lower
650                    && len < lo
651                {
652                    continue;
653                }
654                if let Some(hi) = lc.upper
655                    && len > hi
656                {
657                    continue;
658                }
659            }
660        }
661        None
662    }
663
664    /// Check prefix constraints
665    fn check_prefixes(&self) -> Option<Vec<TermId>> {
666        for (prefix, s, origin) in &self.prefixes {
667            if let (Some(p), Some(s_val)) = (self.eval_expr(prefix), self.eval_expr(s))
668                && !s_val.starts_with(&p)
669            {
670                return Some(vec![*origin]);
671            }
672        }
673        None
674    }
675
676    /// Check suffix constraints
677    fn check_suffixes(&self) -> Option<Vec<TermId>> {
678        for (suffix, s, origin) in &self.suffixes {
679            if let (Some(suf), Some(s_val)) = (self.eval_expr(suffix), self.eval_expr(s))
680                && !s_val.ends_with(&suf)
681            {
682                return Some(vec![*origin]);
683            }
684        }
685        None
686    }
687
688    /// Check contains constraints
689    fn check_contains(&self) -> Option<Vec<TermId>> {
690        for (s, substr, origin) in &self.contains {
691            if let (Some(s_val), Some(sub)) = (self.eval_expr(s), self.eval_expr(substr))
692                && !s_val.contains(&sub)
693            {
694                return Some(vec![*origin]);
695            }
696        }
697        None
698    }
699}
700
701/// Result of applying Levi's lemma
702#[allow(dead_code)]
703#[derive(Debug)]
704enum LeviResult {
705    /// Equation is solved
706    Solved,
707    /// Equation leads to conflict
708    Conflict(TermId),
709    /// Made progress with new equations
710    Progress(Vec<(StringExpr, StringExpr)>),
711    /// No progress possible
712    NoProgress,
713}
714
715impl Default for StringSolver {
716    fn default() -> Self {
717        Self::new()
718    }
719}
720
721impl Theory for StringSolver {
722    fn id(&self) -> TheoryId {
723        TheoryId::Strings
724    }
725
726    fn name(&self) -> &str {
727        "Strings"
728    }
729
730    fn can_handle(&self, _term: TermId) -> bool {
731        // Would check if term is a string operation
732        false
733    }
734
735    fn assert_true(&mut self, term: TermId) -> Result<TheoryResult> {
736        // Would parse term and add appropriate constraint
737        let _var = self.get_or_create_var(term);
738        if let Some(conflict) = self.current_conflict.take() {
739            return Ok(TheoryResult::Unsat(conflict));
740        }
741        Ok(TheoryResult::Sat)
742    }
743
744    fn assert_false(&mut self, term: TermId) -> Result<TheoryResult> {
745        let _var = self.get_or_create_var(term);
746        if let Some(conflict) = self.current_conflict.take() {
747            return Ok(TheoryResult::Unsat(conflict));
748        }
749        Ok(TheoryResult::Sat)
750    }
751
752    fn check(&mut self) -> Result<TheoryResult> {
753        // Check for pending conflicts
754        if let Some(conflict) = self.current_conflict.take() {
755            return Ok(TheoryResult::Unsat(conflict));
756        }
757
758        // Solve word equations
759        if let Some(conflict) = self.solve_equations() {
760            return Ok(TheoryResult::Unsat(conflict));
761        }
762
763        // Check regex constraints
764        if let Some(conflict) = self.check_regex_constraints() {
765            return Ok(TheoryResult::Unsat(conflict));
766        }
767
768        // Check disequalities
769        if let Some(conflict) = self.check_diseqs() {
770            return Ok(TheoryResult::Unsat(conflict));
771        }
772
773        // Check length constraints
774        if let Some(conflict) = self.check_lengths() {
775            return Ok(TheoryResult::Unsat(conflict));
776        }
777
778        // Check prefix constraints
779        if let Some(conflict) = self.check_prefixes() {
780            return Ok(TheoryResult::Unsat(conflict));
781        }
782
783        // Check suffix constraints
784        if let Some(conflict) = self.check_suffixes() {
785            return Ok(TheoryResult::Unsat(conflict));
786        }
787
788        // Check contains constraints
789        if let Some(conflict) = self.check_contains() {
790            return Ok(TheoryResult::Unsat(conflict));
791        }
792
793        // Check str.to_int constraints
794        if let Some(conflict) = self.check_str_to_int() {
795            return Ok(TheoryResult::Unsat(conflict));
796        }
797
798        // Check str.from_int constraints
799        if let Some(conflict) = self.check_int_to_str() {
800            return Ok(TheoryResult::Unsat(conflict));
801        }
802
803        // Check propagations
804        if !self.propagated.is_empty() {
805            let props = std::mem::take(&mut self.propagated);
806            return Ok(TheoryResult::Propagate(props));
807        }
808
809        Ok(TheoryResult::Sat)
810    }
811
812    fn push(&mut self) {
813        self.context_stack.push(ContextState {
814            num_vars: self.next_var as usize,
815            num_equations: self.equations.len(),
816            num_lengths: self.lengths.len(),
817            num_regex: self.regex_constraints.len(),
818            num_diseqs: self.diseqs.len(),
819            num_prefixes: self.prefixes.len(),
820            num_suffixes: self.suffixes.len(),
821            num_contains: self.contains.len(),
822            num_str_to_int: self.str_to_int.len(),
823            num_int_to_str: self.int_to_str.len(),
824            assignments_snapshot: self.assignments.clone(),
825        });
826    }
827
828    fn pop(&mut self) {
829        if let Some(state) = self.context_stack.pop() {
830            // Restore variable count
831            self.next_var = state.num_vars as u32;
832            self.var_to_term.truncate(state.num_vars);
833
834            // Remove terms that were added after the push
835            self.term_to_var
836                .retain(|_, v| (*v as usize) < state.num_vars);
837
838            // Restore constraints
839            self.equations.truncate(state.num_equations);
840            self.lengths.truncate(state.num_lengths);
841            self.regex_constraints.truncate(state.num_regex);
842            self.diseqs.truncate(state.num_diseqs);
843            self.prefixes.truncate(state.num_prefixes);
844            self.suffixes.truncate(state.num_suffixes);
845            self.contains.truncate(state.num_contains);
846            self.str_to_int.truncate(state.num_str_to_int);
847            self.int_to_str.truncate(state.num_int_to_str);
848
849            // Restore assignments
850            self.assignments = state.assignments_snapshot;
851
852            // Clear conflict
853            self.current_conflict = None;
854            self.propagated.clear();
855        }
856    }
857
858    fn reset(&mut self) {
859        self.next_var = 0;
860        self.term_to_var.clear();
861        self.var_to_term.clear();
862        self.assignments.clear();
863        self.equations.clear();
864        self.lengths.clear();
865        self.regex_constraints.clear();
866        self.diseqs.clear();
867        self.prefixes.clear();
868        self.suffixes.clear();
869        self.contains.clear();
870        self.str_to_int.clear();
871        self.int_to_str.clear();
872        self.context_stack.clear();
873        self.current_conflict = None;
874        self.regex_automata.clear();
875        self.propagated.clear();
876    }
877}
878
879#[cfg(test)]
880mod tests {
881    use super::*;
882
883    #[test]
884    fn test_string_expr_concat() {
885        let a = StringExpr::literal("hello");
886        let b = StringExpr::literal(" world");
887        let c = a.concat(b);
888        assert_eq!(c.as_const(), Some("hello world"));
889    }
890
891    #[test]
892    fn test_string_expr_var_concat() {
893        let a = StringExpr::var(0);
894        let b = StringExpr::literal("!");
895        let c = a.concat(b);
896        assert_eq!(c.atoms.len(), 2);
897    }
898
899    #[test]
900    fn test_word_equation_solved() {
901        let eq = WordEquation {
902            lhs: StringExpr::literal("test"),
903            rhs: StringExpr::literal("test"),
904            origin: TermId(0),
905        };
906        assert!(eq.is_solved());
907    }
908
909    #[test]
910    fn test_word_equation_conflict() {
911        let eq = WordEquation {
912            lhs: StringExpr::literal("abc"),
913            rhs: StringExpr::literal("def"),
914            origin: TermId(0),
915        };
916        assert!(eq.has_conflict());
917    }
918
919    #[test]
920    fn test_solver_basic() {
921        let mut solver = StringSolver::new();
922        let term = TermId(0);
923
924        solver.add_equality(
925            StringExpr::literal("hello"),
926            StringExpr::literal("hello"),
927            term,
928        );
929
930        let result = solver.check().unwrap();
931        assert!(matches!(result, TheoryResult::Sat));
932    }
933
934    #[test]
935    fn test_solver_conflict() {
936        let mut solver = StringSolver::new();
937        let term = TermId(0);
938
939        solver.add_equality(
940            StringExpr::literal("hello"),
941            StringExpr::literal("world"),
942            term,
943        );
944
945        let result = solver.check().unwrap();
946        assert!(matches!(result, TheoryResult::Unsat(_)));
947    }
948
949    #[test]
950    fn test_solver_diseq() {
951        let mut solver = StringSolver::new();
952        let term = TermId(0);
953
954        solver.add_disequality(
955            StringExpr::literal("hello"),
956            StringExpr::literal("world"),
957            term,
958        );
959
960        let result = solver.check().unwrap();
961        assert!(matches!(result, TheoryResult::Sat));
962    }
963
964    #[test]
965    fn test_solver_diseq_conflict() {
966        let mut solver = StringSolver::new();
967        let term = TermId(0);
968
969        solver.add_disequality(
970            StringExpr::literal("same"),
971            StringExpr::literal("same"),
972            term,
973        );
974
975        let result = solver.check().unwrap();
976        assert!(matches!(result, TheoryResult::Unsat(_)));
977    }
978
979    #[test]
980    fn test_solver_prefix() {
981        let mut solver = StringSolver::new();
982        let term = TermId(0);
983
984        solver.add_prefix(
985            StringExpr::literal("hello"),
986            StringExpr::literal("hello world"),
987            term,
988        );
989
990        let result = solver.check().unwrap();
991        assert!(matches!(result, TheoryResult::Sat));
992    }
993
994    #[test]
995    fn test_solver_prefix_conflict() {
996        let mut solver = StringSolver::new();
997        let term = TermId(0);
998
999        solver.add_prefix(
1000            StringExpr::literal("world"),
1001            StringExpr::literal("hello"),
1002            term,
1003        );
1004
1005        let result = solver.check().unwrap();
1006        assert!(matches!(result, TheoryResult::Unsat(_)));
1007    }
1008
1009    #[test]
1010    fn test_solver_suffix() {
1011        let mut solver = StringSolver::new();
1012        let term = TermId(0);
1013
1014        solver.add_suffix(
1015            StringExpr::literal("world"),
1016            StringExpr::literal("hello world"),
1017            term,
1018        );
1019
1020        let result = solver.check().unwrap();
1021        assert!(matches!(result, TheoryResult::Sat));
1022    }
1023
1024    #[test]
1025    fn test_solver_contains() {
1026        let mut solver = StringSolver::new();
1027        let term = TermId(0);
1028
1029        solver.add_contains(
1030            StringExpr::literal("hello world"),
1031            StringExpr::literal("lo wo"),
1032            term,
1033        );
1034
1035        let result = solver.check().unwrap();
1036        assert!(matches!(result, TheoryResult::Sat));
1037    }
1038
1039    #[test]
1040    fn test_solver_contains_conflict() {
1041        let mut solver = StringSolver::new();
1042        let term = TermId(0);
1043
1044        solver.add_contains(
1045            StringExpr::literal("hello"),
1046            StringExpr::literal("xyz"),
1047            term,
1048        );
1049
1050        let result = solver.check().unwrap();
1051        assert!(matches!(result, TheoryResult::Unsat(_)));
1052    }
1053
1054    #[test]
1055    fn test_solver_regex() {
1056        let mut solver = StringSolver::new();
1057        let term = TermId(0);
1058        let var = solver.get_or_create_var(term);
1059
1060        // Assign value
1061        solver.assignments.insert(var, "aaa".to_string());
1062
1063        // Should match a+
1064        let regex = Regex::plus(Regex::char('a'));
1065        solver.add_regex_membership(var, regex, true, term);
1066
1067        let result = solver.check().unwrap();
1068        assert!(matches!(result, TheoryResult::Sat));
1069    }
1070
1071    #[test]
1072    fn test_solver_regex_conflict() {
1073        let mut solver = StringSolver::new();
1074        let term = TermId(0);
1075        let var = solver.get_or_create_var(term);
1076
1077        // Assign value
1078        solver.assignments.insert(var, "abc".to_string());
1079
1080        // Should NOT match a+ (contains b and c)
1081        let regex = Regex::plus(Regex::char('a'));
1082        solver.add_regex_membership(var, regex, true, term);
1083
1084        let result = solver.check().unwrap();
1085        assert!(matches!(result, TheoryResult::Unsat(_)));
1086    }
1087
1088    #[test]
1089    fn test_solver_push_pop() {
1090        let mut solver = StringSolver::new();
1091        let term = TermId(0);
1092
1093        solver.push();
1094
1095        solver.add_equality(
1096            StringExpr::literal("hello"),
1097            StringExpr::literal("world"),
1098            term,
1099        );
1100
1101        let result = solver.check().unwrap();
1102        assert!(matches!(result, TheoryResult::Unsat(_)));
1103
1104        solver.pop();
1105
1106        let result = solver.check().unwrap();
1107        assert!(matches!(result, TheoryResult::Sat));
1108    }
1109
1110    #[test]
1111    fn test_strip_common_prefix() {
1112        let solver = StringSolver::new();
1113        let mut lhs = StringExpr::literal("hello world");
1114        let mut rhs = StringExpr::literal("hello there");
1115        solver.strip_common_prefix(&mut lhs, &mut rhs);
1116        assert_eq!(lhs.as_const(), Some("world"));
1117        assert_eq!(rhs.as_const(), Some("there"));
1118    }
1119
1120    #[test]
1121    fn test_theory_trait() {
1122        let mut solver = StringSolver::new();
1123        assert_eq!(solver.id(), TheoryId::Strings);
1124        assert_eq!(solver.name(), "Strings");
1125
1126        let term = TermId(1);
1127        let result = solver.assert_true(term).unwrap();
1128        assert!(matches!(result, TheoryResult::Sat));
1129    }
1130
1131    #[test]
1132    fn test_str_to_int_valid() {
1133        let mut solver = StringSolver::new();
1134        let term = TermId(0);
1135        let var = solver.get_or_create_var(term);
1136
1137        // Assign string value "42"
1138        solver.assignments.insert(var, "42".to_string());
1139
1140        // Add constraint: int = str.to_int("42")
1141        solver.add_str_to_int(var, 42, term);
1142
1143        let result = solver.check().unwrap();
1144        assert!(matches!(result, TheoryResult::Sat));
1145    }
1146
1147    #[test]
1148    fn test_str_to_int_invalid() {
1149        let mut solver = StringSolver::new();
1150        let term = TermId(0);
1151        let var = solver.get_or_create_var(term);
1152
1153        // Assign string value "hello" (not a number)
1154        solver.assignments.insert(var, "hello".to_string());
1155
1156        // Add constraint: int = str.to_int("hello"), should be -1
1157        solver.add_str_to_int(var, -1, term);
1158
1159        let result = solver.check().unwrap();
1160        assert!(matches!(result, TheoryResult::Sat));
1161    }
1162
1163    #[test]
1164    fn test_str_to_int_conflict() {
1165        let mut solver = StringSolver::new();
1166        let term = TermId(0);
1167        let var = solver.get_or_create_var(term);
1168
1169        // Assign string value "42"
1170        solver.assignments.insert(var, "42".to_string());
1171
1172        // Add constraint: int = str.to_int("42"), but claim it's 99
1173        solver.add_str_to_int(var, 99, term);
1174
1175        let result = solver.check().unwrap();
1176        assert!(matches!(result, TheoryResult::Unsat(_)));
1177    }
1178
1179    #[test]
1180    fn test_int_to_str_positive() {
1181        let mut solver = StringSolver::new();
1182        let term = TermId(0);
1183        let var = solver.get_or_create_var(term);
1184
1185        // Assign string value "123"
1186        solver.assignments.insert(var, "123".to_string());
1187
1188        // Add constraint: s = str.from_int(123)
1189        solver.add_int_to_str(var, 123, term);
1190
1191        let result = solver.check().unwrap();
1192        assert!(matches!(result, TheoryResult::Sat));
1193    }
1194
1195    #[test]
1196    fn test_int_to_str_negative() {
1197        let mut solver = StringSolver::new();
1198        let term = TermId(0);
1199        let var = solver.get_or_create_var(term);
1200
1201        // Assign empty string (negative numbers produce empty string)
1202        solver.assignments.insert(var, String::new());
1203
1204        // Add constraint: s = str.from_int(-5), should be empty
1205        solver.add_int_to_str(var, -5, term);
1206
1207        let result = solver.check().unwrap();
1208        assert!(matches!(result, TheoryResult::Sat));
1209    }
1210
1211    #[test]
1212    fn test_int_to_str_conflict() {
1213        let mut solver = StringSolver::new();
1214        let term = TermId(0);
1215        let var = solver.get_or_create_var(term);
1216
1217        // Assign string value "99"
1218        solver.assignments.insert(var, "99".to_string());
1219
1220        // Add constraint: s = str.from_int(123), but s is "99"
1221        solver.add_int_to_str(var, 123, term);
1222
1223        let result = solver.check().unwrap();
1224        assert!(matches!(result, TheoryResult::Unsat(_)));
1225    }
1226}
oxiz_theories/string/solver.rs

oxiz_theories/string/
solver.rs
