oxiz_solver/mbqi/
integration.rs

1//! MBQI Integration with Main Solver
2//!
3//! This module handles the integration of MBQI with the main SMT solver.
4//! It provides callbacks, communication interfaces, and coordination logic.
5
6#![allow(missing_docs)]
7#![allow(dead_code)]
8
9use lasso::Spur;
10use oxiz_core::ast::{TermId, TermManager};
11use oxiz_core::sort::SortId;
12use rustc_hash::FxHashMap;
13use smallvec::SmallVec;
14use std::fmt;
15use std::time::{Duration, Instant};
16
17use super::counterexample::CounterExampleGenerator;
18use super::finite_model::FiniteModelFinder;
19use super::instantiation::InstantiationEngine;
20use super::lazy_instantiation::LazyInstantiator;
21use super::model_completion::ModelCompleter;
22use super::{Instantiation, MBQIResult, MBQIStats, QuantifiedFormula};
23
24/// Callback trait for solver communication
25pub trait SolverCallback: fmt::Debug {
26    /// Called when new instantiations are generated
27    fn on_instantiation(&mut self, inst: &Instantiation);
28
29    /// Called when a conflict is detected
30    fn on_conflict(&mut self, quantifier: TermId, reason: &[TermId]);
31
32    /// Called when MBQI starts a new round
33    fn on_round_start(&mut self, round: usize);
34
35    /// Called when MBQI completes a round
36    fn on_round_end(&mut self, round: usize, result: &MBQIResult);
37
38    /// Check if solver should stop (e.g., timeout)
39    fn should_stop(&self) -> bool;
40}
41
42/// MBQI integration manager
43#[derive(Debug)]
44pub struct MBQIIntegration {
45    /// Model completer
46    model_completer: ModelCompleter,
47    /// Instantiation engine
48    instantiation_engine: InstantiationEngine,
49    /// Lazy instantiator
50    lazy_instantiator: LazyInstantiator,
51    /// Finite model finder
52    finite_model_finder: FiniteModelFinder,
53    /// Counterexample generator
54    cex_generator: CounterExampleGenerator,
55    /// Tracked quantifiers
56    quantifiers: Vec<QuantifiedFormula>,
57    /// Generated instantiations (for deduplication)
58    generated_instantiations: FxHashMap<InstantiationKey, usize>,
59    /// Current round number
60    current_round: usize,
61    /// Maximum rounds
62    max_rounds: usize,
63    /// Time limit
64    time_limit: Option<Duration>,
65    /// Start time
66    start_time: Option<Instant>,
67    /// Statistics
68    stats: MBQIStats,
69}
70
71impl MBQIIntegration {
72    /// Create a new MBQI integration
73    pub fn new() -> Self {
74        Self {
75            model_completer: ModelCompleter::new(),
76            instantiation_engine: InstantiationEngine::new(),
77            lazy_instantiator: LazyInstantiator::new(),
78            finite_model_finder: FiniteModelFinder::new(),
79            cex_generator: CounterExampleGenerator::new(),
80            quantifiers: Vec::new(),
81            generated_instantiations: FxHashMap::default(),
82            current_round: 0,
83            max_rounds: 100,
84            time_limit: Some(Duration::from_secs(60)),
85            start_time: None,
86            stats: MBQIStats::new(),
87        }
88    }
89
90    /// Add a quantified formula
91    pub fn add_quantifier(&mut self, term: TermId, manager: &TermManager) {
92        let Some(t) = manager.get(term) else {
93            return;
94        };
95
96        match &t.kind {
97            oxiz_core::ast::TermKind::Forall { vars, body, .. } => {
98                let bound_vars: SmallVec<[(Spur, SortId); 4]> = vars.iter().copied().collect();
99                self.quantifiers
100                    .push(QuantifiedFormula::new(term, bound_vars, *body, true));
101                self.stats.num_quantifiers += 1;
102            }
103            oxiz_core::ast::TermKind::Exists { vars, body, .. } => {
104                let bound_vars: SmallVec<[(Spur, SortId); 4]> = vars.iter().copied().collect();
105                self.quantifiers
106                    .push(QuantifiedFormula::new(term, bound_vars, *body, false));
107                self.stats.num_quantifiers += 1;
108            }
109            _ => {}
110        }
111    }
112
113    /// Run MBQI with a partial model
114    pub fn run(
115        &mut self,
116        partial_model: &FxHashMap<TermId, TermId>,
117        manager: &mut TermManager,
118        callback: &mut dyn SolverCallback,
119    ) -> MBQIResult {
120        self.start_time = Some(Instant::now());
121        self.current_round = 0;
122
123        if self.quantifiers.is_empty() {
124            return MBQIResult::NoQuantifiers;
125        }
126
127        // Main MBQI loop
128        while self.current_round < self.max_rounds {
129            if self.check_timeout() || callback.should_stop() {
130                return MBQIResult::Unknown;
131            }
132
133            self.current_round += 1;
134            callback.on_round_start(self.current_round);
135            self.stats.num_checks += 1;
136
137            let round_start = Instant::now();
138
139            // Step 1: Complete the model
140            let completed_model =
141                match self
142                    .model_completer
143                    .complete(partial_model, &self.quantifiers, manager)
144                {
145                    Ok(model) => {
146                        self.stats.num_completions += 1;
147                        model
148                    }
149                    Err(_) => {
150                        callback.on_round_end(self.current_round, &MBQIResult::Unknown);
151                        return MBQIResult::Unknown;
152                    }
153                };
154
155            // Step 2: Generate instantiations
156            let mut all_instantiations = Vec::new();
157
158            // Collect quantifiers first to avoid borrow checker issues
159            let quantifiers: Vec<_> = self.quantifiers.to_vec();
160            for quantifier in quantifiers {
161                if !quantifier.can_instantiate() {
162                    continue;
163                }
164
165                let instantiations =
166                    self.instantiation_engine
167                        .instantiate(&quantifier, &completed_model, manager);
168
169                for inst in instantiations {
170                    if !self.is_duplicate(&inst) {
171                        self.record_instantiation(&inst);
172                        callback.on_instantiation(&inst);
173                        all_instantiations.push(inst);
174                    }
175                }
176            }
177
178            self.stats.completion_time_us += round_start.elapsed().as_micros() as u64;
179
180            // Step 3: Check result
181            if all_instantiations.is_empty() {
182                let result = MBQIResult::Satisfied;
183                callback.on_round_end(self.current_round, &result);
184                self.update_final_stats();
185                return result;
186            }
187
188            // Step 4: Check instantiation limit
189            if self.stats.total_instantiations >= self.stats.max_instantiations {
190                let result = MBQIResult::InstantiationLimit;
191                callback.on_round_end(self.current_round, &result);
192                self.update_final_stats();
193                return result;
194            }
195
196            let result = MBQIResult::NewInstantiations(all_instantiations);
197            callback.on_round_end(self.current_round, &result);
198        }
199
200        self.update_final_stats();
201        MBQIResult::Unknown
202    }
203
204    /// Check if an instantiation is a duplicate
205    fn is_duplicate(&self, inst: &Instantiation) -> bool {
206        let key = InstantiationKey::from(inst);
207        self.generated_instantiations.contains_key(&key)
208    }
209
210    /// Record an instantiation
211    fn record_instantiation(&mut self, inst: &Instantiation) {
212        let key = InstantiationKey::from(inst);
213        let count = self.generated_instantiations.entry(key).or_insert(0);
214        *count += 1;
215        self.stats.total_instantiations += 1;
216        self.stats.unique_instantiations = self.generated_instantiations.len();
217    }
218
219    /// Check for timeout
220    fn check_timeout(&self) -> bool {
221        if let (Some(limit), Some(start)) = (self.time_limit, self.start_time) {
222            start.elapsed() >= limit
223        } else {
224            false
225        }
226    }
227
228    /// Update final statistics
229    fn update_final_stats(&mut self) {
230        if let Some(start) = self.start_time {
231            self.stats.total_time_us = start.elapsed().as_micros() as u64;
232        }
233    }
234
235    /// Clear all state
236    pub fn clear(&mut self) {
237        self.quantifiers.clear();
238        self.generated_instantiations.clear();
239        self.current_round = 0;
240        self.start_time = None;
241        self.instantiation_engine.clear_caches();
242        self.lazy_instantiator.clear();
243    }
244
245    /// Collect ground terms from trigger patterns
246    pub fn collect_ground_terms(&mut self, _term: TermId, _manager: &TermManager) {
247        // Stub implementation - would collect ground terms for E-matching
248        // This is a placeholder for future E-matching integration
249    }
250
251    /// Check quantifiers with a given model
252    pub fn check_with_model(
253        &mut self,
254        model: &FxHashMap<TermId, TermId>,
255        manager: &mut TermManager,
256    ) -> MBQIResult {
257        // Use a no-op callback for this convenience method
258        #[derive(Debug)]
259        struct NoOpCallback;
260        impl SolverCallback for NoOpCallback {
261            fn on_instantiation(&mut self, _: &Instantiation) {}
262            fn on_round_start(&mut self, _: usize) {}
263            fn on_round_end(&mut self, _: usize, _: &MBQIResult) {}
264            fn on_conflict(&mut self, _: TermId, _: &[TermId]) {}
265            fn should_stop(&self) -> bool {
266                false
267            }
268        }
269        let mut callback = NoOpCallback;
270        self.run(model, manager, &mut callback)
271    }
272
273    /// Get statistics
274    pub fn stats(&self) -> &MBQIStats {
275        &self.stats
276    }
277
278    /// Set maximum rounds
279    pub fn set_max_rounds(&mut self, max: usize) {
280        self.max_rounds = max;
281    }
282
283    /// Set time limit
284    pub fn set_time_limit(&mut self, limit: Duration) {
285        self.time_limit = Some(limit);
286    }
287
288    /// Add a candidate term for model-based instantiation
289    pub fn add_candidate(&mut self, _term: TermId, _sort: SortId) {
290        // Candidate terms are tracked for model-based instantiation
291        // This is a placeholder - full implementation would store candidates
292    }
293
294    /// Check if MBQI is enabled
295    pub fn is_enabled(&self) -> bool {
296        // MBQI is always enabled when the struct exists
297        true
298    }
299}
300
301impl Default for MBQIIntegration {
302    fn default() -> Self {
303        Self::new()
304    }
305}
306
307/// Key for instantiation deduplication
308#[derive(Debug, Clone, PartialEq, Eq, Hash)]
309struct InstantiationKey {
310    quantifier: TermId,
311    binding: Vec<(lasso::Spur, TermId)>,
312}
313
314impl From<&Instantiation> for InstantiationKey {
315    fn from(inst: &Instantiation) -> Self {
316        let mut binding: Vec<_> = inst.substitution.iter().map(|(&k, &v)| (k, v)).collect();
317        binding.sort_by_key(|(k, _)| *k);
318        Self {
319            quantifier: inst.quantifier,
320            binding,
321        }
322    }
323}
324
325/// Default callback implementation (no-op)
326#[derive(Debug)]
327pub struct DefaultCallback {
328    stop_requested: bool,
329}
330
331impl DefaultCallback {
332    pub fn new() -> Self {
333        Self {
334            stop_requested: false,
335        }
336    }
337
338    pub fn request_stop(&mut self) {
339        self.stop_requested = true;
340    }
341}
342
343impl Default for DefaultCallback {
344    fn default() -> Self {
345        Self::new()
346    }
347}
348
349impl SolverCallback for DefaultCallback {
350    fn on_instantiation(&mut self, _inst: &Instantiation) {}
351    fn on_conflict(&mut self, _quantifier: TermId, _reason: &[TermId]) {}
352    fn on_round_start(&mut self, _round: usize) {}
353    fn on_round_end(&mut self, _round: usize, _result: &MBQIResult) {}
354    fn should_stop(&self) -> bool {
355        self.stop_requested
356    }
357}
358
359#[cfg(test)]
360mod tests {
361    use super::*;
362
363    #[test]
364    fn test_mbqi_integration_creation() {
365        let integration = MBQIIntegration::new();
366        assert_eq!(integration.quantifiers.len(), 0);
367        assert_eq!(integration.current_round, 0);
368    }
369
370    #[test]
371    fn test_default_callback() {
372        let mut callback = DefaultCallback::new();
373        assert!(!callback.should_stop());
374        callback.request_stop();
375        assert!(callback.should_stop());
376    }
377
378    #[test]
379    fn test_integration_clear() {
380        let mut integration = MBQIIntegration::new();
381        integration.current_round = 5;
382        integration.clear();
383        assert_eq!(integration.current_round, 0);
384        assert_eq!(integration.quantifiers.len(), 0);
385    }
386
387    #[test]
388    fn test_set_max_rounds() {
389        let mut integration = MBQIIntegration::new();
390        integration.set_max_rounds(50);
391        assert_eq!(integration.max_rounds, 50);
392    }
393
394    #[test]
395    fn test_set_time_limit() {
396        let mut integration = MBQIIntegration::new();
397        let limit = Duration::from_secs(30);
398        integration.set_time_limit(limit);
399        assert_eq!(integration.time_limit, Some(limit));
400    }
401}
oxiz_solver/mbqi/integration.rs

oxiz_solver/mbqi/
integration.rs
