oxiz_solver/
context.rs

1//! Solver context
2
3#[allow(unused_imports)]
4use crate::prelude::*;
5use crate::solver::{Solver, SolverResult};
6use oxiz_core::ast::{TermId, TermKind, TermManager};
7#[cfg(feature = "std")]
8use oxiz_core::error::Result;
9#[cfg(feature = "std")]
10use oxiz_core::smtlib::{Command, parse_script};
11use oxiz_core::sort::SortId;
12#[cfg(feature = "std")]
13use std::path::{Path, PathBuf};
14
15/// A declared constant
16#[derive(Debug, Clone)]
17struct DeclaredConst {
18    /// The term ID for this constant
19    term: TermId,
20    /// The sort of this constant
21    sort: SortId,
22    /// The name of this constant
23    name: String,
24}
25
26/// A declared function
27#[derive(Debug, Clone)]
28struct DeclaredFun {
29    /// The function name
30    name: String,
31    /// Argument sorts
32    arg_sorts: Vec<SortId>,
33    /// Return sort
34    ret_sort: SortId,
35}
36
37/// Solver context for managing the solving process
38///
39/// The `Context` provides a high-level API for SMT solving, similar to
40/// the SMT-LIB2 standard. It manages declarations, assertions, and solver state.
41///
42/// # Examples
43///
44/// ## Basic Usage
45///
46/// ```
47/// use oxiz_solver::Context;
48///
49/// let mut ctx = Context::new();
50/// ctx.set_logic("QF_UF");
51///
52/// // Declare boolean constants
53/// let p = ctx.declare_const("p", ctx.terms.sorts.bool_sort);
54/// let q = ctx.declare_const("q", ctx.terms.sorts.bool_sort);
55///
56/// // Assert p AND q
57/// let formula = ctx.terms.mk_and(vec![p, q]);
58/// ctx.assert(formula);
59///
60/// // Check satisfiability
61/// ctx.check_sat();
62/// ```
63///
64/// ## SMT-LIB2 Script Execution
65///
66/// ```
67/// use oxiz_solver::Context;
68///
69/// let mut ctx = Context::new();
70///
71/// let script = r#"
72/// (set-logic QF_LIA)
73/// (declare-const x Int)
74/// (assert (>= x 0))
75/// (assert (<= x 10))
76/// (check-sat)
77/// "#;
78///
79/// let _ = ctx.execute_script(script);
80/// ```
81#[derive(Debug)]
82pub struct Context {
83    /// Term manager
84    pub terms: TermManager,
85    /// Solver instance
86    solver: Solver,
87    /// Current logic
88    logic: Option<String>,
89    /// Assertions
90    assertions: Vec<TermId>,
91    /// Assertion stack for push/pop
92    assertion_stack: Vec<usize>,
93    /// Declared constants
94    declared_consts: Vec<DeclaredConst>,
95    /// Declared constants stack for push/pop
96    const_stack: Vec<usize>,
97    /// Mapping from constant names to indices (for efficient removal)
98    const_name_to_index: crate::prelude::HashMap<String, usize>,
99    /// Declared functions
100    declared_funs: Vec<DeclaredFun>,
101    /// Declared functions stack for push/pop
102    fun_stack: Vec<usize>,
103    /// Mapping from function names to indices
104    fun_name_to_index: crate::prelude::HashMap<String, usize>,
105    /// Last check-sat result
106    last_result: Option<SolverResult>,
107    /// Options
108    options: crate::prelude::HashMap<String, String>,
109    /// Optional path for binary proof logging.
110    ///
111    /// When set, `check_sat` creates a `ProofLogger` at this path, records
112    /// proof steps derived from the solver result, and flushes/closes the log
113    /// before returning.
114    #[cfg(feature = "std")]
115    proof_log_path: Option<PathBuf>,
116}
117
118impl Default for Context {
119    fn default() -> Self {
120        Self::new()
121    }
122}
123
124impl Context {
125    /// Create a new context
126    #[must_use]
127    pub fn new() -> Self {
128        Self {
129            terms: TermManager::new(),
130            solver: Solver::new(),
131            logic: None,
132            assertions: Vec::new(),
133            assertion_stack: Vec::new(),
134            declared_consts: Vec::new(),
135            const_stack: Vec::new(),
136            const_name_to_index: crate::prelude::HashMap::new(),
137            declared_funs: Vec::new(),
138            fun_stack: Vec::new(),
139            fun_name_to_index: crate::prelude::HashMap::new(),
140            last_result: None,
141            options: crate::prelude::HashMap::new(),
142            #[cfg(feature = "std")]
143            proof_log_path: None,
144        }
145    }
146
147    /// Configure a path for binary proof logging.
148    ///
149    /// When a path is configured, every subsequent call to `check_sat` opens a
150    /// [`oxiz_proof::logging::ProofLogger`] at that path, writes a structural
151    /// summary of the proof, and flushes/closes the log before returning.
152    /// Pass `None` to disable proof logging.
153    #[cfg(feature = "std")]
154    pub fn set_proof_log_path(&mut self, path: Option<PathBuf>) {
155        self.proof_log_path = path;
156    }
157
158    /// Return the currently configured proof log path, if any.
159    #[cfg(feature = "std")]
160    #[must_use]
161    pub fn proof_log_path(&self) -> Option<&Path> {
162        self.proof_log_path.as_deref()
163    }
164
165    /// Verify a binary proof log produced by a previous `check_sat` call with
166    /// proof logging enabled.
167    ///
168    /// Delegates to [`oxiz_proof::replay::ProofReplayer::replay_from_file`].
169    ///
170    /// # Errors
171    ///
172    /// Returns `Err` only for hard I/O or binary-format failures; logical
173    /// invalidity is encoded as `Ok(VerificationResult::Invalid(_))`.
174    #[cfg(feature = "std")]
175    pub fn verify_proof_log(
176        path: &Path,
177    ) -> std::result::Result<oxiz_proof::replay::VerificationResult, oxiz_proof::replay::ProofError>
178    {
179        oxiz_proof::replay::ProofReplayer::replay_from_file(path)
180    }
181
182    /// Declare a constant
183    pub fn declare_const(&mut self, name: &str, sort: SortId) -> TermId {
184        let term = self.terms.mk_var(name, sort);
185        let index = self.declared_consts.len();
186        self.declared_consts.push(DeclaredConst {
187            term,
188            sort,
189            name: name.to_string(),
190        });
191        self.const_name_to_index.insert(name.to_string(), index);
192        term
193    }
194
195    /// Declare a function
196    ///
197    /// Registers a function signature in the context. For nullary functions (constants),
198    /// use `declare_const` instead.
199    pub fn declare_fun(&mut self, name: &str, arg_sorts: Vec<SortId>, ret_sort: SortId) {
200        let index = self.declared_funs.len();
201        self.declared_funs.push(DeclaredFun {
202            name: name.to_string(),
203            arg_sorts,
204            ret_sort,
205        });
206        self.fun_name_to_index.insert(name.to_string(), index);
207    }
208
209    /// Get function signature if it exists
210    pub fn get_fun_signature(&self, name: &str) -> Option<(Vec<SortId>, SortId)> {
211        self.fun_name_to_index.get(name).and_then(|&idx| {
212            self.declared_funs
213                .get(idx)
214                .map(|f| (f.arg_sorts.clone(), f.ret_sort))
215        })
216    }
217
218    /// Set the logic
219    pub fn set_logic(&mut self, logic: &str) {
220        self.logic = Some(logic.to_string());
221        self.solver.set_logic(logic);
222    }
223
224    /// Get the current logic
225    #[must_use]
226    pub fn logic(&self) -> Option<&str> {
227        self.logic.as_deref()
228    }
229
230    /// Add an assertion
231    pub fn assert(&mut self, term: TermId) {
232        self.assertions.push(term);
233        self.solver.assert(term, &mut self.terms);
234    }
235
236    /// Check satisfiability
237    pub fn check_sat(&mut self) -> SolverResult {
238        let result = self.solver.check(&mut self.terms);
239        self.last_result = Some(result);
240
241        // Write a binary proof log if a path is configured (std-only).
242        #[cfg(feature = "std")]
243        if let Some(ref path) = self.proof_log_path.clone() {
244            if let Err(e) = self.write_proof_log(path, result) {
245                // Non-fatal: warn but do not abort the solve.
246                #[cfg(feature = "tracing")]
247                tracing::warn!("proof log write failed for {:?}: {}", path, e);
248                let _ = e;
249            }
250        }
251
252        result
253    }
254
255    /// Serialise a proof log entry for the given result.
256    ///
257    /// For `Unsat`, resolution proof steps are emitted when available;
258    /// for `Sat` and `Unknown`, a single axiom node is written so the log is
259    /// never empty and can be cleanly replayed.
260    #[cfg(feature = "std")]
261    fn write_proof_log(
262        &self,
263        path: &Path,
264        result: SolverResult,
265    ) -> std::result::Result<(), oxiz_proof::logging::LoggingError> {
266        use oxiz_proof::logging::ProofLogger;
267        use oxiz_proof::proof::{ProofNodeId, ProofStep};
268        use smallvec::SmallVec;
269
270        let mut logger = ProofLogger::create(path)?;
271
272        match result {
273            SolverResult::Unsat => {
274                if let Some(proof) = self.solver.get_proof() {
275                    let mut counter: u32 = 0;
276                    for step in proof.steps() {
277                        let entry = match step {
278                            crate::solver::ProofStep::Input { index, .. } => ProofStep::Axiom {
279                                conclusion: format!("input-clause-{}", index),
280                            },
281                            crate::solver::ProofStep::Resolution {
282                                index,
283                                left,
284                                right,
285                                pivot,
286                                ..
287                            } => {
288                                let mut premises: SmallVec<[ProofNodeId; 4]> = SmallVec::new();
289                                premises.push(ProofNodeId(*left));
290                                premises.push(ProofNodeId(*right));
291                                let mut args: SmallVec<[String; 2]> = SmallVec::new();
292                                args.push(format!("{:?}", pivot));
293                                ProofStep::Inference {
294                                    rule: "resolution".to_string(),
295                                    premises,
296                                    conclusion: format!("resolution-{}", index),
297                                    args,
298                                }
299                            }
300                            crate::solver::ProofStep::TheoryLemma { index, theory, .. } => {
301                                ProofStep::Axiom {
302                                    conclusion: format!("theory-lemma-{}-{}", theory, index),
303                                }
304                            }
305                        };
306                        logger.log_step(ProofNodeId(counter), &entry)?;
307                        counter += 1;
308                    }
309                    if counter == 0 {
310                        // Proof object present but empty — emit minimal witness.
311                        logger.log_step(
312                            ProofNodeId(0),
313                            &ProofStep::Axiom {
314                                conclusion: "unsat".to_string(),
315                            },
316                        )?;
317                    }
318                } else {
319                    logger.log_step(
320                        ProofNodeId(0),
321                        &ProofStep::Axiom {
322                            conclusion: "unsat".to_string(),
323                        },
324                    )?;
325                }
326            }
327            SolverResult::Sat => {
328                logger.log_step(
329                    ProofNodeId(0),
330                    &ProofStep::Axiom {
331                        conclusion: "sat".to_string(),
332                    },
333                )?;
334            }
335            SolverResult::Unknown => {
336                logger.log_step(
337                    ProofNodeId(0),
338                    &ProofStep::Axiom {
339                        conclusion: "unknown".to_string(),
340                    },
341                )?;
342            }
343        }
344
345        logger.flush()?;
346        logger.close()
347    }
348
349    /// Get the model (if SAT)
350    /// Returns a list of (name, sort, value) tuples
351    pub fn get_model(&self) -> Option<Vec<(String, String, String)>> {
352        if self.last_result != Some(SolverResult::Sat) {
353            return None;
354        }
355
356        let mut model = Vec::new();
357        let solver_model = self.solver.model()?;
358
359        for decl in &self.declared_consts {
360            let value = if let Some(val) = solver_model.get(decl.term) {
361                self.format_value(val)
362            } else {
363                // Default value based on sort
364                self.default_value(decl.sort)
365            };
366            let sort_name = self.format_sort_name(decl.sort);
367            model.push((decl.name.clone(), sort_name, value));
368        }
369
370        Some(model)
371    }
372
373    /// Format a sort ID to its SMT-LIB2 name
374    fn format_sort_name(&self, sort: SortId) -> String {
375        if sort == self.terms.sorts.bool_sort {
376            "Bool".to_string()
377        } else if sort == self.terms.sorts.int_sort {
378            "Int".to_string()
379        } else if sort == self.terms.sorts.real_sort {
380            "Real".to_string()
381        } else if let Some(s) = self.terms.sorts.get(sort) {
382            if let Some(w) = s.bitvec_width() {
383                format!("(_ BitVec {})", w)
384            } else {
385                "Unknown".to_string()
386            }
387        } else {
388            "Unknown".to_string()
389        }
390    }
391
392    /// Format a model value
393    fn format_value(&self, term: TermId) -> String {
394        match self.terms.get(term).map(|t| &t.kind) {
395            Some(TermKind::True) => "true".to_string(),
396            Some(TermKind::False) => "false".to_string(),
397            Some(TermKind::IntConst(n)) => n.to_string(),
398            Some(TermKind::RealConst(r)) => {
399                if *r.denom() == 1 {
400                    format!("{}.0", r.numer())
401                } else {
402                    format!("(/ {} {})", r.numer(), r.denom())
403                }
404            }
405            Some(TermKind::BitVecConst { value, width }) => {
406                format!(
407                    "#b{:0>width$}",
408                    format!("{:b}", value),
409                    width = *width as usize
410                )
411            }
412            _ => "?".to_string(),
413        }
414    }
415
416    /// Get a default value for a sort
417    fn default_value(&self, sort: SortId) -> String {
418        if sort == self.terms.sorts.bool_sort {
419            "false".to_string()
420        } else if sort == self.terms.sorts.int_sort {
421            "0".to_string()
422        } else if sort == self.terms.sorts.real_sort {
423            "0.0".to_string()
424        } else if let Some(s) = self.terms.sorts.get(sort) {
425            if let Some(w) = s.bitvec_width() {
426                format!("#b{:0>width$}", "0", width = w as usize)
427            } else {
428                "?".to_string()
429            }
430        } else {
431            "?".to_string()
432        }
433    }
434
435    /// Format the model as SMT-LIB2
436    pub fn format_model(&self) -> String {
437        match self.get_model() {
438            None => "(error \"No model available\")".to_string(),
439            Some(model) if model.is_empty() => "(model)".to_string(),
440            Some(model) => {
441                let mut lines = vec!["(model".to_string()];
442                for (name, sort, value) in model {
443                    lines.push(format!("  (define-fun {} () {} {})", name, sort, value));
444                }
445                lines.push(")".to_string());
446                lines.join("\n")
447            }
448        }
449    }
450
451    /// Push a context level
452    pub fn push(&mut self) {
453        self.assertion_stack.push(self.assertions.len());
454        self.const_stack.push(self.declared_consts.len());
455        self.fun_stack.push(self.declared_funs.len());
456        self.solver.push();
457    }
458
459    /// Pop a context level with incremental declaration removal
460    pub fn pop(&mut self) {
461        if let Some(len) = self.assertion_stack.pop() {
462            self.assertions.truncate(len);
463            if let Some(const_len) = self.const_stack.pop() {
464                // Remove constants from the name-to-index mapping
465                while self.declared_consts.len() > const_len {
466                    if let Some(decl) = self.declared_consts.pop() {
467                        self.const_name_to_index.remove(&decl.name);
468                    }
469                }
470            }
471            if let Some(fun_len) = self.fun_stack.pop() {
472                // Remove functions from the name-to-index mapping
473                while self.declared_funs.len() > fun_len {
474                    if let Some(decl) = self.declared_funs.pop() {
475                        self.fun_name_to_index.remove(&decl.name);
476                    }
477                }
478            }
479            self.solver.pop();
480        }
481    }
482
483    /// Reset the context
484    pub fn reset(&mut self) {
485        self.solver.reset();
486        self.assertions.clear();
487        self.assertion_stack.clear();
488        self.declared_consts.clear();
489        self.const_stack.clear();
490        self.const_name_to_index.clear();
491        self.declared_funs.clear();
492        self.fun_stack.clear();
493        self.fun_name_to_index.clear();
494        self.logic = None;
495        self.last_result = None;
496        self.options.clear();
497    }
498
499    /// Reset assertions (keep declarations and options)
500    pub fn reset_assertions(&mut self) {
501        self.solver.reset();
502        self.assertions.clear();
503        self.assertion_stack.clear();
504        // Keep declared_consts, const_stack, const_name_to_index,
505        // declared_funs, fun_stack, and fun_name_to_index
506        // Re-assert nothing - solver is fresh
507        self.last_result = None;
508    }
509
510    /// Get all current assertions
511    #[must_use]
512    pub fn get_assertions(&self) -> &[TermId] {
513        &self.assertions
514    }
515
516    /// Format assertions as SMT-LIB2
517    #[cfg(feature = "std")]
518    pub fn format_assertions(&self) -> String {
519        if self.assertions.is_empty() {
520            return "()".to_string();
521        }
522        let printer = oxiz_core::smtlib::Printer::new(&self.terms);
523        let mut parts = Vec::new();
524        for &term in &self.assertions {
525            parts.push(printer.print_term(term));
526        }
527        format!("({})", parts.join("\n "))
528    }
529
530    /// Set an option
531    pub fn set_option(&mut self, key: &str, value: &str) {
532        self.options.insert(key.to_string(), value.to_string());
533
534        // Handle special options that affect the solver
535        match key {
536            "produce-proofs" => {
537                let mut config = self.solver.config().clone();
538                config.proof = value == "true";
539                self.solver.set_config(config);
540            }
541            "produce-unsat-cores" => {
542                self.solver.set_produce_unsat_cores(value == "true");
543            }
544            _ => {}
545        }
546    }
547
548    /// Get an option
549    #[must_use]
550    pub fn get_option(&self, key: &str) -> Option<&str> {
551        self.options.get(key).map(String::as_str)
552    }
553
554    /// Format an option value
555    fn format_option(&self, key: &str) -> String {
556        match self.get_option(key) {
557            Some(val) => val.to_string(),
558            None => {
559                // Return default values for well-known options
560                match key {
561                    "produce-models" => "false".to_string(),
562                    "produce-unsat-cores" => "false".to_string(),
563                    "produce-proofs" => "false".to_string(),
564                    "produce-assignments" => "false".to_string(),
565                    "print-success" => "true".to_string(),
566                    _ => "unsupported".to_string(),
567                }
568            }
569        }
570    }
571
572    /// Get assignment (for propositional variables with :named attribute)
573    /// Returns an empty list as we don't track named literals yet
574    pub fn get_assignment(&self) -> String {
575        "()".to_string()
576    }
577
578    /// Get proof (if proof generation is enabled and result is unsat)
579    pub fn get_proof(&self) -> String {
580        if self.last_result != Some(SolverResult::Unsat) {
581            return "(error \"Proof is only available after unsat result\")".to_string();
582        }
583
584        match self.solver.get_proof() {
585            Some(proof) => proof.format(),
586            None => {
587                "(error \"Proof generation not enabled. Set :produce-proofs to true\")".to_string()
588            }
589        }
590    }
591
592    /// Get solver statistics
593    /// Returns statistics about the last solving run
594    pub fn get_statistics(&self) -> String {
595        let stats = self.solver.get_statistics();
596        format!(
597            "(:decisions {} :conflicts {} :propagations {} :restarts {} :learned-clauses {} :theory-propagations {} :theory-conflicts {})",
598            stats.decisions,
599            stats.conflicts,
600            stats.propagations,
601            stats.restarts,
602            stats.learned_clauses,
603            stats.theory_propagations,
604            stats.theory_conflicts
605        )
606    }
607
608    /// Parse a sort name and return its SortId
609    fn parse_sort_name(&mut self, name: &str) -> SortId {
610        match name {
611            "Bool" => self.terms.sorts.bool_sort,
612            "Int" => self.terms.sorts.int_sort,
613            "Real" => self.terms.sorts.real_sort,
614            _ => {
615                // Check for BitVec
616                if let Some(width_str) = name.strip_prefix("BitVec")
617                    && let Ok(width) = width_str.trim().parse::<u32>()
618                {
619                    return self.terms.sorts.bitvec(width);
620                }
621                // Default to Bool for unknown sorts
622                self.terms.sorts.bool_sort
623            }
624        }
625    }
626
627    /// Execute an SMT-LIB2 script
628    #[cfg(feature = "std")]
629    pub fn execute_script(&mut self, script: &str) -> Result<Vec<String>> {
630        let commands = parse_script(script, &mut self.terms)?;
631        let mut output = Vec::new();
632
633        for cmd in commands {
634            match cmd {
635                Command::SetLogic(logic) => {
636                    self.set_logic(&logic);
637                }
638                Command::DeclareConst(name, sort_name) => {
639                    let sort = self.parse_sort_name(&sort_name);
640                    self.declare_const(&name, sort);
641                }
642                Command::DeclareFun(name, arg_sorts, ret_sort) => {
643                    // Treat nullary functions as constants
644                    if arg_sorts.is_empty() {
645                        let sort = self.parse_sort_name(&ret_sort);
646                        self.declare_const(&name, sort);
647                    } else {
648                        // Parse argument sorts and return sort
649                        let parsed_arg_sorts: Vec<SortId> =
650                            arg_sorts.iter().map(|s| self.parse_sort_name(s)).collect();
651                        let parsed_ret_sort = self.parse_sort_name(&ret_sort);
652                        self.declare_fun(&name, parsed_arg_sorts, parsed_ret_sort);
653                    }
654                }
655                Command::Assert(term) => {
656                    self.assert(term);
657                }
658                Command::CheckSat => {
659                    let result = self.check_sat();
660                    output.push(match result {
661                        SolverResult::Sat => "sat".to_string(),
662                        SolverResult::Unsat => "unsat".to_string(),
663                        SolverResult::Unknown => "unknown".to_string(),
664                    });
665                }
666                Command::Push(n) => {
667                    for _ in 0..n {
668                        self.push();
669                    }
670                }
671                Command::Pop(n) => {
672                    for _ in 0..n {
673                        self.pop();
674                    }
675                }
676                Command::Reset => {
677                    self.reset();
678                }
679                Command::ResetAssertions => {
680                    self.reset_assertions();
681                }
682                Command::Exit => {
683                    break;
684                }
685                Command::Echo(msg) => {
686                    output.push(msg);
687                }
688                Command::GetModel => {
689                    output.push(self.format_model());
690                }
691                Command::GetAssertions => {
692                    output.push(self.format_assertions());
693                }
694                Command::GetAssignment => {
695                    output.push(self.get_assignment());
696                }
697                Command::GetProof => {
698                    output.push(self.get_proof());
699                }
700                Command::GetOption(key) => {
701                    output.push(self.format_option(&key));
702                }
703                Command::SetOption(key, value) => {
704                    self.set_option(&key, &value);
705                }
706                Command::CheckSatAssuming(assumptions) => {
707                    // For now, we push, assert all assumptions, check, then pop
708                    self.push();
709                    for assumption in assumptions {
710                        self.assert(assumption);
711                    }
712                    let result = self.check_sat();
713                    self.pop();
714                    output.push(match result {
715                        SolverResult::Sat => "sat".to_string(),
716                        SolverResult::Unsat => "unsat".to_string(),
717                        SolverResult::Unknown => "unknown".to_string(),
718                    });
719                }
720                Command::Simplify(term) => {
721                    // Simplify and output the term
722                    let simplified = self.terms.simplify(term);
723                    let printer = oxiz_core::smtlib::Printer::new(&self.terms);
724                    output.push(printer.print_term(simplified));
725                }
726                Command::GetUnsatCore => {
727                    if let Some(core) = self.solver.get_unsat_core() {
728                        if core.names.is_empty() {
729                            output.push("()".to_string());
730                        } else {
731                            output.push(format!("({})", core.names.join(" ")));
732                        }
733                    } else {
734                        output.push("(error \"No unsat core available\")".to_string());
735                    }
736                }
737                Command::GetValue(terms) => {
738                    if self.last_result != Some(SolverResult::Sat) {
739                        output.push("(error \"No model available\")".to_string());
740                    } else if let Some(model) = self.solver.model() {
741                        let mut values = Vec::new();
742                        for term in terms {
743                            // Evaluate the term in the model first
744                            let value = model.eval(term, &mut self.terms);
745                            // Then create printer and format
746                            let printer = oxiz_core::smtlib::Printer::new(&self.terms);
747                            let term_str = printer.print_term(term);
748                            let value_str = printer.print_term(value);
749                            values.push(format!("({} {})", term_str, value_str));
750                        }
751                        output.push(format!("({})", values.join("\n ")));
752                    } else {
753                        output.push("(error \"No model available\")".to_string());
754                    }
755                }
756                Command::GetInfo(keyword) => {
757                    // Handle get-info command
758                    if keyword == ":all-statistics" {
759                        output.push(self.get_statistics());
760                    } else {
761                        output.push(format!("(error \"Unsupported info keyword: {}\")", keyword));
762                    }
763                }
764                Command::SetInfo(_, _)
765                | Command::DeclareSort(_, _)
766                | Command::DefineSort(_, _, _)
767                | Command::DefineFun(_, _, _, _)
768                | Command::DeclareDatatype { .. } => {
769                    // Ignore these commands for now
770                }
771            }
772        }
773
774        Ok(output)
775    }
776
777    /// Get solver statistics
778    #[must_use]
779    pub fn stats(&self) -> &oxiz_sat::SolverStats {
780        self.solver.stats()
781    }
782}
783
784#[cfg(test)]
785mod tests {
786    use super::*;
787
788    #[test]
789    fn test_context_basic() {
790        let mut ctx = Context::new();
791
792        ctx.set_logic("QF_UF");
793        assert_eq!(ctx.logic(), Some("QF_UF"));
794
795        let t = ctx.terms.mk_true();
796        ctx.assert(t);
797
798        let result = ctx.check_sat();
799        assert_eq!(result, SolverResult::Sat);
800    }
801
802    #[test]
803    fn test_context_push_pop() {
804        let mut ctx = Context::new();
805
806        let t = ctx.terms.mk_true();
807        ctx.assert(t);
808        ctx.push();
809
810        let f = ctx.terms.mk_false();
811        ctx.assert(f);
812
813        // Should be unsat with false asserted
814        let result = ctx.check_sat();
815        assert_eq!(result, SolverResult::Unsat);
816
817        ctx.pop();
818
819        // After pop, should be sat again
820        let result = ctx.check_sat();
821        assert_eq!(result, SolverResult::Sat);
822    }
823
824    #[test]
825    fn test_execute_script() {
826        let mut ctx = Context::new();
827
828        let script = r#"
829            (set-logic QF_UF)
830            (declare-const p Bool)
831            (assert p)
832            (check-sat)
833        "#;
834
835        let output = ctx
836            .execute_script(script)
837            .expect("test operation should succeed");
838        assert_eq!(output, vec!["sat"]);
839    }
840
841    #[test]
842    fn test_declare_const() {
843        let mut ctx = Context::new();
844
845        let bool_sort = ctx.terms.sorts.bool_sort;
846        let int_sort = ctx.terms.sorts.int_sort;
847
848        ctx.declare_const("x", bool_sort);
849        ctx.declare_const("y", int_sort);
850
851        let t = ctx.terms.mk_true();
852        ctx.assert(t);
853        let result = ctx.check_sat();
854        assert_eq!(result, SolverResult::Sat);
855
856        // Model should include both constants
857        let model = ctx.get_model();
858        assert!(model.is_some());
859        let model = model.expect("test operation should succeed");
860        assert_eq!(model.len(), 2);
861    }
862
863    #[test]
864    fn test_format_model() {
865        let mut ctx = Context::new();
866
867        let bool_sort = ctx.terms.sorts.bool_sort;
868        ctx.declare_const("p", bool_sort);
869
870        let t = ctx.terms.mk_true();
871        ctx.assert(t);
872        let _ = ctx.check_sat();
873
874        let model_str = ctx.format_model();
875        assert!(model_str.contains("(model"));
876        assert!(model_str.contains("define-fun p () Bool"));
877    }
878
879    #[test]
880    fn test_get_model_script() {
881        let mut ctx = Context::new();
882
883        let script = r#"
884            (set-logic QF_LIA)
885            (declare-const x Int)
886            (declare-const y Bool)
887            (assert true)
888            (check-sat)
889            (get-model)
890        "#;
891
892        let output = ctx
893            .execute_script(script)
894            .expect("test operation should succeed");
895        assert_eq!(output.len(), 2);
896        assert_eq!(output[0], "sat");
897        assert!(
898            output[1].contains("(model"),
899            "Expected '(model' in: {}",
900            output[1]
901        );
902        // Note: Sorts may not always appear in model output if values are default
903        // The model format is: (define-fun name () Sort value)
904    }
905
906    #[test]
907    fn test_push_pop_consts() {
908        let mut ctx = Context::new();
909
910        let bool_sort = ctx.terms.sorts.bool_sort;
911        ctx.declare_const("a", bool_sort);
912        ctx.push();
913        ctx.declare_const("b", bool_sort);
914
915        let t = ctx.terms.mk_true();
916        ctx.assert(t);
917        let _ = ctx.check_sat();
918
919        let model = ctx.get_model().expect("test operation should succeed");
920        assert_eq!(model.len(), 2);
921
922        ctx.pop();
923        let _ = ctx.check_sat();
924
925        let model = ctx.get_model().expect("test operation should succeed");
926        assert_eq!(model.len(), 1);
927        assert_eq!(model[0].0, "a");
928    }
929
930    #[test]
931    fn test_get_assertions() {
932        let mut ctx = Context::new();
933
934        let script = r#"
935            (set-logic QF_UF)
936            (declare-const p Bool)
937            (assert p)
938            (assert (not p))
939            (get-assertions)
940        "#;
941
942        let output = ctx
943            .execute_script(script)
944            .expect("test operation should succeed");
945        assert_eq!(output.len(), 1);
946        assert!(output[0].starts_with('('));
947        // Should contain both assertions
948        assert!(output[0].contains("p"));
949    }
950
951    #[test]
952    fn test_check_sat_assuming_script() {
953        let mut ctx = Context::new();
954
955        let script = r#"
956            (set-logic QF_UF)
957            (declare-const p Bool)
958            (declare-const q Bool)
959            (assert p)
960            (check-sat-assuming (q))
961        "#;
962
963        let output = ctx
964            .execute_script(script)
965            .expect("test operation should succeed");
966        assert_eq!(output.len(), 1);
967        assert_eq!(output[0], "sat");
968    }
969
970    #[test]
971    fn test_get_option_script() {
972        let mut ctx = Context::new();
973
974        let script = r#"
975            (set-option :produce-models true)
976            (get-option :produce-models)
977        "#;
978
979        let output = ctx
980            .execute_script(script)
981            .expect("test operation should succeed");
982        assert_eq!(output.len(), 1);
983        assert_eq!(output[0], "true");
984    }
985
986    #[test]
987    fn test_reset_assertions() {
988        let mut ctx = Context::new();
989
990        let script = r#"
991            (set-logic QF_UF)
992            (declare-const p Bool)
993            (assert p)
994            (reset-assertions)
995            (get-assertions)
996            (check-sat)
997        "#;
998
999        let output = ctx
1000            .execute_script(script)
1001            .expect("test operation should succeed");
1002        assert_eq!(output.len(), 2);
1003        assert_eq!(output[0], "()"); // No assertions after reset
1004        assert_eq!(output[1], "sat"); // Empty formula is SAT
1005    }
1006
1007    #[test]
1008    fn test_simplify_command() {
1009        let mut ctx = Context::new();
1010
1011        let script = r#"
1012            (simplify (+ 1 2))
1013        "#;
1014
1015        let output = ctx
1016            .execute_script(script)
1017            .expect("test operation should succeed");
1018        assert_eq!(output.len(), 1);
1019        // Should simplify to 3
1020        assert_eq!(output[0], "3");
1021    }
1022
1023    #[test]
1024    fn test_simplify_complex() {
1025        let mut ctx = Context::new();
1026
1027        let script = r#"
1028            (simplify (* 2 3 4))
1029        "#;
1030
1031        let output = ctx
1032            .execute_script(script)
1033            .expect("test operation should succeed");
1034        assert_eq!(output.len(), 1);
1035        // Should simplify to 24
1036        assert_eq!(output[0], "24");
1037    }
1038
1039    #[test]
1040    fn test_get_value() {
1041        let mut ctx = Context::new();
1042
1043        let script = r#"
1044            (set-logic QF_UF)
1045            (declare-const p Bool)
1046            (declare-const q Bool)
1047            (assert p)
1048            (assert (not q))
1049            (check-sat)
1050            (get-value (p q (and p q) (or p q)))
1051        "#;
1052
1053        let output = ctx
1054            .execute_script(script)
1055            .expect("test operation should succeed");
1056        assert_eq!(output.len(), 2);
1057        assert_eq!(output[0], "sat");
1058
1059        // Parse the get-value output
1060        let value_output = &output[1];
1061        assert!(value_output.contains("p"));
1062        assert!(value_output.contains("q"));
1063        // p should evaluate to true
1064        assert!(value_output.contains("true"));
1065        // q should evaluate to false
1066        assert!(value_output.contains("false"));
1067    }
1068
1069    #[test]
1070    fn test_get_value_no_model() {
1071        let mut ctx = Context::new();
1072
1073        let script = r#"
1074            (set-logic QF_UF)
1075            (declare-const p Bool)
1076            (get-value (p))
1077        "#;
1078
1079        let output = ctx
1080            .execute_script(script)
1081            .expect("test operation should succeed");
1082        assert_eq!(output.len(), 1);
1083        assert!(output[0].contains("error") || output[0].contains("No model"));
1084    }
1085
1086    #[test]
1087    fn test_get_value_after_unsat() {
1088        let mut ctx = Context::new();
1089
1090        let script = r#"
1091            (set-logic QF_UF)
1092            (declare-const p Bool)
1093            (assert p)
1094            (assert (not p))
1095            (check-sat)
1096            (get-value (p))
1097        "#;
1098
1099        let output = ctx
1100            .execute_script(script)
1101            .expect("test operation should succeed");
1102        assert_eq!(output.len(), 2);
1103        assert_eq!(output[0], "unsat");
1104        assert!(output[1].contains("error") || output[1].contains("No model"));
1105    }
1106}
oxiz_solver/context.rs

oxiz_solver/
context.rs
