oxiz_solver/solver/
config.rs

1//! Solver configuration helpers: logic selection, polarity analysis, and
2//! datatype constructor extraction.
3//!
4//! These methods are extracted from `mod.rs` to keep that file under the
5//! 2000-line refactoring threshold.
6
7use oxiz_core::ast::{TermId, TermKind, TermManager};
8use oxiz_theories::arithmetic::ArithSolver;
9
10use super::Solver;
11use super::types::Polarity;
12
13impl Solver {
14    /// Set the logic
15    pub fn set_logic(&mut self, logic: &str) {
16        self.logic = Some(logic.to_string());
17
18        // Switch ArithSolver based on logic
19        // QF_NIA and QF_NRA use NLSAT solver for nonlinear arithmetic
20        if logic.contains("NIA") {
21            // Nonlinear integer arithmetic - use NLSAT with integer mode
22            #[cfg(feature = "std")]
23            {
24                self.nlsat = Some(oxiz_theories::nlsat::NlsatTheory::new(true));
25            }
26            self.arith = ArithSolver::lia(); // Keep LIA as fallback for linear constraints
27            #[cfg(feature = "tracing")]
28            tracing::info!("Using NLSAT solver for QF_NIA (nonlinear integer arithmetic)");
29        } else if logic.contains("NRA") {
30            // Nonlinear real arithmetic - use NLSAT with real mode
31            #[cfg(feature = "std")]
32            {
33                self.nlsat = Some(oxiz_theories::nlsat::NlsatTheory::new(false));
34            }
35            self.arith = ArithSolver::lra(); // Keep LRA as fallback for linear constraints
36            #[cfg(feature = "tracing")]
37            tracing::info!("Using NLSAT solver for QF_NRA (nonlinear real arithmetic)");
38        } else if logic.contains("LIA") || logic.contains("IDL") {
39            // Integer arithmetic logic (QF_LIA, LIA, QF_AUFLIA, QF_IDL, etc.)
40            self.arith = ArithSolver::lia();
41        } else if logic.contains("LRA") || logic.contains("RDL") {
42            // Real arithmetic logic (QF_LRA, LRA, QF_RDL, etc.)
43            self.arith = ArithSolver::lra();
44        } else if logic.contains("BV") {
45            // Bitvector logic - use LIA since BV comparisons are handled
46            // as bounded integer arithmetic
47            self.arith = ArithSolver::lia();
48        }
49        // For other logics (QF_UF, etc.) keep the default LRA
50    }
51
52    /// Extract (variable, constructor) pair from an equality if one side is a variable
53    /// and the other is a DtConstructor
54    pub(super) fn extract_dt_var_constructor(
55        &self,
56        lhs: TermId,
57        rhs: TermId,
58        manager: &TermManager,
59    ) -> Option<(TermId, oxiz_core::interner::Spur)> {
60        let lhs_term = manager.get(lhs)?;
61        let rhs_term = manager.get(rhs)?;
62
63        // lhs is var, rhs is constructor
64        if matches!(lhs_term.kind, TermKind::Var(_)) {
65            if let TermKind::DtConstructor { constructor, .. } = &rhs_term.kind {
66                return Some((lhs, *constructor));
67            }
68        }
69        // rhs is var, lhs is constructor
70        if matches!(rhs_term.kind, TermKind::Var(_)) {
71            if let TermKind::DtConstructor { constructor, .. } = &lhs_term.kind {
72                return Some((rhs, *constructor));
73            }
74        }
75        None
76    }
77
78    /// Collect polarity information for all subterms
79    /// This is used for polarity-aware encoding optimization
80    pub(super) fn collect_polarities(
81        &mut self,
82        term: TermId,
83        polarity: Polarity,
84        manager: &TermManager,
85    ) {
86        // Update the polarity for this term
87        let current = self.polarities.get(&term).copied();
88        let new_polarity = match (current, polarity) {
89            (Some(Polarity::Both), _) | (_, Polarity::Both) => Polarity::Both,
90            (Some(Polarity::Positive), Polarity::Negative)
91            | (Some(Polarity::Negative), Polarity::Positive) => Polarity::Both,
92            (Some(p), _) => p,
93            (None, p) => p,
94        };
95        self.polarities.insert(term, new_polarity);
96
97        // If we've reached Both polarity, no need to recurse further
98        if current == Some(Polarity::Both) {
99            return;
100        }
101
102        // Recursively collect polarities for subterms
103        let Some(t) = manager.get(term) else {
104            return;
105        };
106
107        match &t.kind {
108            TermKind::Not(arg) => {
109                let neg_polarity = match polarity {
110                    Polarity::Positive => Polarity::Negative,
111                    Polarity::Negative => Polarity::Positive,
112                    Polarity::Both => Polarity::Both,
113                };
114                self.collect_polarities(*arg, neg_polarity, manager);
115            }
116            TermKind::And(args) | TermKind::Or(args) => {
117                for &arg in args {
118                    self.collect_polarities(arg, polarity, manager);
119                }
120            }
121            TermKind::Implies(lhs, rhs) => {
122                let neg_polarity = match polarity {
123                    Polarity::Positive => Polarity::Negative,
124                    Polarity::Negative => Polarity::Positive,
125                    Polarity::Both => Polarity::Both,
126                };
127                self.collect_polarities(*lhs, neg_polarity, manager);
128                self.collect_polarities(*rhs, polarity, manager);
129            }
130            TermKind::Ite(cond, then_br, else_br) => {
131                self.collect_polarities(*cond, Polarity::Both, manager);
132                self.collect_polarities(*then_br, polarity, manager);
133                self.collect_polarities(*else_br, polarity, manager);
134            }
135            TermKind::Xor(lhs, rhs) | TermKind::Eq(lhs, rhs) => {
136                // For XOR and Eq, both sides appear in both polarities
137                self.collect_polarities(*lhs, Polarity::Both, manager);
138                self.collect_polarities(*rhs, Polarity::Both, manager);
139            }
140            _ => {
141                // For other terms (constants, variables, theory atoms), stop recursion
142            }
143        }
144    }
145}
oxiz_solver/solver/config.rs

oxiz_solver/solver/
config.rs
