logicaffeine_verify/
solver.rs

1//! Z3 solver wrapper for Logicaffeine verification.
2//!
3//! This module provides two APIs for Z3-based verification:
4//!
5//! ## Low-Level API: [`Verifier`] and [`VerificationContext`]
6//!
7//! Direct Z3 access for single-shot checks and custom verification logic.
8//! Use when you need fine-grained control over the solver.
9//!
10//! ```ignore
11//! use logicaffeine_verify::Verifier;
12//!
13//! let verifier = Verifier::new();
14//! assert!(verifier.check_bool(true).is_ok());
15//! assert!(verifier.check_int_greater_than(10, 5).is_ok());
16//! ```
17//!
18//! ## High-Level API: [`VerificationSession`]
19//!
20//! Works with the [`VerifyExpr`] IR for accumulating
21//! declarations and assumptions before verification. Recommended for most use cases.
22//!
23//! ```ignore
24//! use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};
25//!
26//! let mut session = VerificationSession::new();
27//! session.declare("x", VerifyType::Int);
28//! session.assume(&VerifyExpr::eq(VerifyExpr::var("x"), VerifyExpr::int(10)));
29//! assert!(session.verify(&VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5))).is_ok());
30//! ```
31
32use std::collections::HashMap;
33
34use z3::ast::{Ast, Bool, Dynamic, Int};
35use z3::{FuncDecl, Params, SatResult, Solver, Sort};
36
37use crate::error::{CounterExample, VerificationError, VerificationResult};
38use crate::ir::{VerifyExpr, VerifyOp, VerifyType};
39
40/// A solver carrying the crate-wide default timeout.
41///
42/// z3 0.20 makes the context implicit (thread-local), so the per-`Config`
43/// timeout the old API set becomes a global parameter installed exactly once.
44/// 30s is a generous safety bound (it never changes a verification *result* —
45/// only bounds how long a pathological query may run before returning Unknown).
46pub(crate) fn new_solver() -> Solver {
47    use std::sync::Once;
48    static INIT: Once = Once::new();
49    INIT.call_once(|| z3::set_global_param("timeout", "30000"));
50    Solver::new()
51}
52
53/// Low-level Z3-based verifier for single-shot validity checks.
54///
55/// The verifier uses a 10-second timeout by default. For more complex
56/// proofs with multiple constraints, use [`VerificationSession`] instead.
57///
58/// # Examples
59///
60/// ```ignore
61/// use logicaffeine_verify::Verifier;
62///
63/// let verifier = Verifier::new();
64///
65/// // Boolean validity
66/// assert!(verifier.check_bool(true).is_ok());
67/// assert!(verifier.check_bool(false).is_err());
68///
69/// // Integer bounds
70/// assert!(verifier.check_int_greater_than(10, 5).is_ok());
71/// ```
72pub struct Verifier {
73    timeout_ms: u32,
74}
75
76impl Verifier {
77    /// Create a new verifier with a 10-second timeout.
78    ///
79    /// # Examples
80    ///
81    /// ```ignore
82    /// use logicaffeine_verify::Verifier;
83    ///
84    /// let verifier = Verifier::new();
85    /// ```
86    pub fn new() -> Self {
87        Self { timeout_ms: 10000 }
88    }
89
90    /// Build a solver carrying this verifier's timeout.
91    fn solver(&self) -> Solver {
92        let solver = crate::solver::new_solver();
93        let mut params = Params::new();
94        params.set_u32("timeout", self.timeout_ms);
95        solver.set_params(&params);
96        solver
97    }
98
99    /// Check if a boolean value is valid (always true).
100    ///
101    /// Returns `Ok(())` if the value is `true`, an error otherwise.
102    ///
103    /// # Examples
104    ///
105    /// ```ignore
106    /// use logicaffeine_verify::Verifier;
107    ///
108    /// let verifier = Verifier::new();
109    /// assert!(verifier.check_bool(true).is_ok());
110    /// assert!(verifier.check_bool(false).is_err());
111    /// ```
112    pub fn check_bool(&self, value: bool) -> VerificationResult {
113        let solver = self.solver();
114
115        let assertion = Bool::from_bool(value);
116
117        // To prove P is valid: check if NOT(P) is UNSAT
118        // If NOT(P) is unsatisfiable, then P is always true
119        solver.assert(&assertion.not());
120
121        match solver.check() {
122            SatResult::Unsat => Ok(()), // NOT(P) is impossible -> P is valid
123            SatResult::Sat => {
124                // NOT(P) is satisfiable -> P is not always true
125                Err(VerificationError::contradiction(
126                    "The assertion is not always true.",
127                    None,
128                ))
129            }
130            SatResult::Unknown => Err(VerificationError::solver_unknown()),
131        }
132    }
133
134    /// Verify that `value > bound`.
135    ///
136    /// # Examples
137    ///
138    /// ```ignore
139    /// use logicaffeine_verify::Verifier;
140    ///
141    /// let verifier = Verifier::new();
142    /// assert!(verifier.check_int_greater_than(10, 5).is_ok());  // 10 > 5
143    /// assert!(verifier.check_int_greater_than(3, 5).is_err());  // 3 > 5 is false
144    /// ```
145    pub fn check_int_greater_than(&self, value: i64, bound: i64) -> VerificationResult {
146        let solver = self.solver();
147
148        let v = z3::ast::Int::from_i64(value);
149        let b = z3::ast::Int::from_i64(bound);
150        let assertion = v.gt(&b);
151
152        // To prove P is valid: check if NOT(P) is UNSAT
153        solver.assert(&assertion.not());
154
155        match solver.check() {
156            SatResult::Unsat => Ok(()),
157            SatResult::Sat => {
158                Err(VerificationError::bounds_violation(
159                    "value",
160                    format!("> {}", bound),
161                    format!("{}", value),
162                ))
163            }
164            SatResult::Unknown => Err(VerificationError::solver_unknown()),
165        }
166    }
167
168    /// Verify that `value < bound`.
169    ///
170    /// # Examples
171    ///
172    /// ```ignore
173    /// use logicaffeine_verify::Verifier;
174    ///
175    /// let verifier = Verifier::new();
176    /// assert!(verifier.check_int_less_than(3, 5).is_ok());   // 3 < 5
177    /// assert!(verifier.check_int_less_than(10, 5).is_err()); // 10 < 5 is false
178    /// ```
179    pub fn check_int_less_than(&self, value: i64, bound: i64) -> VerificationResult {
180        let solver = self.solver();
181
182        let v = z3::ast::Int::from_i64(value);
183        let b = z3::ast::Int::from_i64(bound);
184        let assertion = v.lt(&b);
185
186        solver.assert(&assertion.not());
187
188        match solver.check() {
189            SatResult::Unsat => Ok(()),
190            SatResult::Sat => Err(VerificationError::bounds_violation(
191                "value",
192                format!("< {}", bound),
193                format!("{}", value),
194            )),
195            SatResult::Unknown => Err(VerificationError::solver_unknown()),
196        }
197    }
198
199    /// Verify that `left == right`.
200    ///
201    /// # Examples
202    ///
203    /// ```ignore
204    /// use logicaffeine_verify::Verifier;
205    ///
206    /// let verifier = Verifier::new();
207    /// assert!(verifier.check_int_equals(42, 42).is_ok());
208    /// assert!(verifier.check_int_equals(1, 2).is_err());
209    /// ```
210    pub fn check_int_equals(&self, left: i64, right: i64) -> VerificationResult {
211        let solver = self.solver();
212
213        let l = z3::ast::Int::from_i64(left);
214        let r = z3::ast::Int::from_i64(right);
215        let assertion = l.eq(&r);
216
217        solver.assert(&assertion.not());
218
219        match solver.check() {
220            SatResult::Unsat => Ok(()),
221            SatResult::Sat => Err(VerificationError::contradiction(
222                format!("{} is not equal to {}", left, right),
223                Some(CounterExample {
224                    assignments: vec![
225                        ("left".to_string(), format!("{}", left)),
226                        ("right".to_string(), format!("{}", right)),
227                    ],
228                }),
229            )),
230            SatResult::Unknown => Err(VerificationError::solver_unknown()),
231        }
232    }
233
234    /// Create a verification context for more complex proofs.
235    ///
236    /// Use this when you need to build custom verification logic with
237    /// multiple variables and constraints.
238    ///
239    /// # Examples
240    ///
241    /// ```ignore
242    /// use logicaffeine_verify::Verifier;
243    /// use z3::ast::Bool;
244    ///
245    /// let verifier = Verifier::new();
246    /// let ctx = verifier.context();
247    /// let solver = ctx.solver();
248    ///
249    /// // P ∨ ¬P is a tautology
250    /// let p = ctx.bool_var("p");
251    /// let tautology = Bool::or(&[&p, &p.not()]);
252    /// assert!(ctx.check_valid(&solver, &tautology).is_ok());
253    /// ```
254    pub fn context(&self) -> VerificationContext {
255        VerificationContext::new(self.timeout_ms)
256    }
257}
258
259impl Default for Verifier {
260    fn default() -> Self {
261        Self::new()
262    }
263}
264
265/// A verification context for building constraints incrementally.
266///
267/// Provides direct access to Z3 types for constructing custom proofs.
268/// For most use cases, prefer [`VerificationSession`] which works with
269/// the higher-level [`VerifyExpr`] IR.
270pub struct VerificationContext {
271    timeout_ms: u32,
272}
273
274impl VerificationContext {
275    fn new(timeout_ms: u32) -> Self {
276        Self { timeout_ms }
277    }
278
279    /// Create a new solver for this context.
280    ///
281    /// The solver accumulates assertions and can check their satisfiability.
282    pub fn solver(&self) -> Solver {
283        let solver = crate::solver::new_solver();
284        let mut params = Params::new();
285        params.set_u32("timeout", self.timeout_ms);
286        solver.set_params(&params);
287        solver
288    }
289
290    /// Create a boolean constant.
291    pub fn bool_val(&self, value: bool) -> Bool {
292        Bool::from_bool(value)
293    }
294
295    /// Create an integer constant.
296    pub fn int_val(&self, value: i64) -> z3::ast::Int {
297        z3::ast::Int::from_i64(value)
298    }
299
300    /// Create a named boolean variable.
301    pub fn bool_var(&self, name: &str) -> Bool {
302        Bool::new_const(name)
303    }
304
305    /// Create a named integer variable.
306    pub fn int_var(&self, name: &str) -> z3::ast::Int {
307        z3::ast::Int::new_const(name)
308    }
309
310    /// Check if an assertion is valid (always true).
311    ///
312    /// Uses the standard validity check: P is valid iff ¬P is unsatisfiable.
313    /// The solver state is preserved using push/pop.
314    pub fn check_valid(&self, solver: &Solver, assertion: &Bool) -> VerificationResult {
315        solver.push();
316        solver.assert(&assertion.not());
317
318        let result = match solver.check() {
319            SatResult::Unsat => Ok(()),
320            SatResult::Sat => {
321                Err(VerificationError::contradiction(
322                    "Assertion is not valid",
323                    None,
324                ))
325            }
326            SatResult::Unknown => Err(VerificationError::solver_unknown()),
327        };
328
329        solver.pop(1);
330        result
331    }
332}
333
334// ============================================================
335// High-Level Session API
336// ============================================================
337
338/// A verification session for working with the Verification IR.
339///
340/// A session accumulates variable declarations and assumptions,
341/// then verifies assertions against that context. This is the recommended
342/// API for most verification tasks.
343///
344/// Each verification call creates a fresh Z3 context to avoid lifetime issues.
345///
346/// # Examples
347///
348/// ```ignore
349/// use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};
350///
351/// let mut session = VerificationSession::new();
352///
353/// // Declare variables
354/// session.declare("x", VerifyType::Int);
355///
356/// // Add assumptions
357/// session.assume(&VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(0)));
358///
359/// // Verify assertions
360/// let result = session.verify(&VerifyExpr::gte(VerifyExpr::var("x"), VerifyExpr::int(0)));
361/// assert!(result.is_ok());
362/// ```
363///
364/// # Modus Ponens Example
365///
366/// ```ignore
367/// use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};
368///
369/// let mut session = VerificationSession::new();
370/// session.declare("x", VerifyType::Object);
371///
372/// // All mortals are human
373/// session.assume(&VerifyExpr::implies(
374///     VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]),
375///     VerifyExpr::apply("Human", vec![VerifyExpr::var("x")]),
376/// ));
377///
378/// // x is mortal
379/// session.assume(&VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]));
380///
381/// // Therefore x is human
382/// assert!(session.verify(&VerifyExpr::apply("Human", vec![VerifyExpr::var("x")])).is_ok());
383/// ```
384pub struct VerificationSession {
385    vars: HashMap<String, VerifyType>,
386    assumptions: Vec<VerifyExpr>,
387}
388
389impl VerificationSession {
390    /// Create a new verification session.
391    ///
392    /// # Examples
393    ///
394    /// ```ignore
395    /// use logicaffeine_verify::VerificationSession;
396    ///
397    /// let session = VerificationSession::new();
398    /// ```
399    pub fn new() -> Self {
400        Self {
401            vars: HashMap::new(),
402            assumptions: Vec::new(),
403        }
404    }
405
406    /// Declare a variable with a type.
407    ///
408    /// Variables must be declared before they can be used in assumptions
409    /// or verifications.
410    ///
411    /// # Examples
412    ///
413    /// ```ignore
414    /// use logicaffeine_verify::{VerificationSession, VerifyType};
415    ///
416    /// let mut session = VerificationSession::new();
417    /// session.declare("x", VerifyType::Int);
418    /// session.declare("p", VerifyType::Bool);
419    /// session.declare("socrates", VerifyType::Object);
420    /// ```
421    pub fn declare(&mut self, name: &str, ty: VerifyType) {
422        self.vars.insert(name.to_string(), ty);
423    }
424
425    /// Add an assumption (constraint) to the session.
426    ///
427    /// Assumptions constrain the verification context. Subsequent calls to
428    /// [`verify`](Self::verify) will check validity under all assumptions.
429    ///
430    /// # Examples
431    ///
432    /// ```ignore
433    /// use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};
434    ///
435    /// let mut session = VerificationSession::new();
436    /// session.declare("x", VerifyType::Int);
437    ///
438    /// // Assume x = 10
439    /// session.assume(&VerifyExpr::eq(VerifyExpr::var("x"), VerifyExpr::int(10)));
440    ///
441    /// // Assume x > 0
442    /// session.assume(&VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(0)));
443    /// ```
444    pub fn assume(&mut self, expr: &VerifyExpr) {
445        self.assumptions.push(expr.clone());
446    }
447
448    /// Verify a predicate with a temporary variable binding.
449    ///
450    /// Used for refinement type checking. Creates a scoped context where
451    /// `var_name = value` is assumed, then verifies that `predicate` holds.
452    ///
453    /// # Examples
454    ///
455    /// ```ignore
456    /// use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};
457    ///
458    /// let session = VerificationSession::new();
459    ///
460    /// // Check that 10 satisfies the predicate x > 5
461    /// let result = session.verify_with_binding(
462    ///     "x",
463    ///     VerifyType::Int,
464    ///     &VerifyExpr::int(10),
465    ///     &VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5)),
466    /// );
467    /// assert!(result.is_ok());
468    /// ```
469    pub fn verify_with_binding(
470        &self,
471        var_name: &str,
472        var_type: VerifyType,
473        value: &VerifyExpr,
474        predicate: &VerifyExpr,
475    ) -> VerificationResult {
476        // Create a fresh solver carrying the standard timeout
477        let solver = timed_solver();
478
479        // Copy existing vars and add the bound variable
480        let mut vars = self.vars.clone();
481        vars.insert(var_name.to_string(), var_type);
482
483        let encoder = Encoder::new(&vars);
484
485        // Add all existing assumptions
486        for assumption in &self.assumptions {
487            let ast = encoder.encode(assumption);
488            if let Some(b) = ast.as_bool() {
489                solver.assert(&b);
490            }
491        }
492
493        // Add the binding: var_name == value
494        let binding = VerifyExpr::eq(
495            VerifyExpr::var(var_name),
496            value.clone(),
497        );
498        let binding_ast = encoder.encode(&binding);
499        if let Some(b) = binding_ast.as_bool() {
500            solver.assert(&b);
501        }
502
503        // Verify the predicate
504        let pred_ast = encoder.encode(predicate);
505        let assertion = pred_ast.as_bool().ok_or_else(|| {
506            VerificationError::solver_error("Refinement predicate must be boolean")
507        })?;
508
509        solver.push();
510        solver.assert(&assertion.not());
511
512        let result = match solver.check() {
513            SatResult::Unsat => Ok(()),
514            SatResult::Sat => Err(VerificationError::refinement_violation(
515                var_name,
516                "The value does not satisfy the refinement predicate.",
517            )),
518            SatResult::Unknown => Err(VerificationError::solver_unknown()),
519        };
520
521        solver.pop(1);
522        result
523    }
524
525    /// Verify that an assertion is valid given current assumptions.
526    ///
527    /// Uses the standard validity check: P is valid iff ¬P is unsatisfiable.
528    /// Returns `Ok(())` if the assertion can be proven, an error otherwise.
529    ///
530    /// # Examples
531    ///
532    /// ```ignore
533    /// use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};
534    ///
535    /// let mut session = VerificationSession::new();
536    /// session.declare("x", VerifyType::Int);
537    /// session.assume(&VerifyExpr::eq(VerifyExpr::var("x"), VerifyExpr::int(10)));
538    ///
539    /// // This should pass: 10 > 5
540    /// assert!(session.verify(&VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5))).is_ok());
541    ///
542    /// // This should fail: 10 < 5
543    /// assert!(session.verify(&VerifyExpr::lt(VerifyExpr::var("x"), VerifyExpr::int(5))).is_err());
544    /// ```
545    pub fn verify(&self, expr: &VerifyExpr) -> VerificationResult {
546        // Create a fresh solver carrying the standard timeout
547        let solver = timed_solver();
548
549        // Create an encoder for this verification
550        let encoder = Encoder::new(&self.vars);
551
552        // Add all assumptions
553        for assumption in &self.assumptions {
554            let ast = encoder.encode(assumption);
555            if let Some(b) = ast.as_bool() {
556                solver.assert(&b);
557            }
558        }
559
560        // Encode the assertion we want to verify
561        let ast = encoder.encode(expr);
562        let assertion = ast.as_bool().ok_or_else(|| {
563            VerificationError::solver_error("Assertion must be boolean")
564        })?;
565
566        // To prove P is valid: check if NOT(P) is UNSAT
567        solver.push();
568        solver.assert(&assertion.not());
569
570        let result = match solver.check() {
571            SatResult::Unsat => Ok(()),
572            SatResult::Sat => {
573                Err(VerificationError::contradiction(
574                    "Assertion cannot be proven valid",
575                    None,
576                ))
577            }
578            SatResult::Unknown => Err(VerificationError::solver_unknown()),
579        };
580
581        solver.pop(1);
582        result
583    }
584
585    /// Check the joint satisfiability of all assumptions (no goal).
586    ///
587    /// Returns `Ok(true)` when Z3 finds a model, `Ok(false)` when the
588    /// assumptions are jointly unsatisfiable, and `Err` on solver-unknown —
589    /// three-valued, so an unknown never reads as either verdict.
590    pub fn check_sat(&self) -> Result<bool, VerificationError> {
591        let solver = timed_solver();
592
593        let encoder = Encoder::new(&self.vars);
594        for assumption in &self.assumptions {
595            let ast = encoder.encode(assumption);
596            if let Some(b) = ast.as_bool() {
597                solver.assert(&b);
598            }
599        }
600
601        match solver.check() {
602            SatResult::Sat => Ok(true),
603            SatResult::Unsat => Ok(false),
604            SatResult::Unknown => Err(VerificationError::solver_unknown()),
605        }
606    }
607
608    /// Verify a temporal property via bounded model checking.
609    ///
610    /// Unrolls the transition relation `bound` steps and checks if the property
611    /// holds at every unrolled state.
612    ///
613    /// - `initial`: constraint on the initial state (e.g., `s == 0`)
614    /// - `transition`: constraint relating current state to next state
615    /// - `property`: the property to verify at each state
616    /// - `bound`: number of unrolling steps
617    ///
618    /// Returns `Ok(())` if the property holds at all unrolled states,
619    /// or an error with counterexample if a violation is found.
620    pub fn verify_temporal(
621        &self,
622        initial: &VerifyExpr,
623        transition: &VerifyExpr,
624        property: &VerifyExpr,
625        bound: u32,
626    ) -> VerificationResult {
627        let solver = timed_solver();
628
629        // Declare state variables for each step: s_0, s_1, ..., s_bound
630        let mut step_vars: HashMap<String, VerifyType> = self.vars.clone();
631
632        // For each step, create renamed variables and assert constraints
633        for step in 0..=bound {
634            let suffix = format!("_{}", step);
635
636            // Substitute "s" → "s_0", "s" → "s_1", etc. in expressions
637            let step_initial = rename_var_in_expr(initial, "s", &format!("s{}", suffix));
638            let step_property = rename_var_in_expr(property, "s", &format!("s{}", suffix));
639
640            step_vars.insert(format!("s{}", suffix), VerifyType::Int);
641
642            let encoder = Encoder::new(&step_vars);
643
644            // Assert initial condition at step 0
645            if step == 0 {
646                let init_ast = encoder.encode(&step_initial);
647                if let Some(b) = init_ast.as_bool() {
648                    solver.assert(&b);
649                }
650            }
651
652            // Assert transition between consecutive steps
653            if step < bound {
654                let next_suffix = format!("_{}", step + 1);
655                let step_trans = rename_var_in_expr(
656                    &rename_var_in_expr(transition, "s", &format!("s{}", suffix)),
657                    "s_next",
658                    &format!("s{}", next_suffix),
659                );
660                let trans_ast = encoder.encode(&step_trans);
661                if let Some(b) = trans_ast.as_bool() {
662                    solver.assert(&b);
663                }
664            }
665
666            // Check if property can be violated at this step
667            let prop_ast = encoder.encode(&step_property);
668            if let Some(b) = prop_ast.as_bool() {
669                solver.push();
670                solver.assert(&b.not());
671                if solver.check() == SatResult::Sat {
672                    solver.pop(1);
673                    return Err(VerificationError::contradiction(
674                        &format!("Property violated at step {}", step),
675                        None,
676                    ));
677                }
678                solver.pop(1);
679            }
680        }
681
682        Ok(())
683    }
684}
685
686/// Rename a variable in a VerifyExpr (simple textual substitution).
687/// Recursively traverses ALL variants — no silent drops.
688pub fn rename_var_in_expr(expr: &VerifyExpr, from: &str, to: &str) -> VerifyExpr {
689    
690    let r = |e: &VerifyExpr| rename_var_in_expr(e, from, to);
691    match expr {
692        // Leaf: variable — rename if matches
693        VerifyExpr::Var(name) => {
694            if name == from { VerifyExpr::Var(to.to_string()) } else { expr.clone() }
695        }
696        // Leaves: literals — no variables to rename
697        VerifyExpr::Int(_) | VerifyExpr::Bool(_) | VerifyExpr::BitVecConst { .. } => expr.clone(),
698
699        // Binary: recurse both sides
700        VerifyExpr::Binary { op, left, right } => VerifyExpr::Binary {
701            op: *op,
702            left: Box::new(r(left)),
703            right: Box::new(r(right)),
704        },
705        VerifyExpr::Not(inner) => VerifyExpr::Not(Box::new(r(inner))),
706        VerifyExpr::Iff(l, ri) => VerifyExpr::Iff(Box::new(r(l)), Box::new(r(ri))),
707
708        // Quantifiers: recurse body (bound vars are separate names, won't collide)
709        VerifyExpr::ForAll { vars, body } => VerifyExpr::ForAll {
710            vars: vars.clone(),
711            body: Box::new(r(body)),
712        },
713        VerifyExpr::Exists { vars, body } => VerifyExpr::Exists {
714            vars: vars.clone(),
715            body: Box::new(r(body)),
716        },
717
718        // Apply: recurse all args
719        VerifyExpr::Apply { name, args } => VerifyExpr::Apply {
720            name: name.clone(),
721            args: args.iter().map(|a| r(a)).collect(),
722        },
723        VerifyExpr::ApplyInt { name, args } => VerifyExpr::ApplyInt {
724            name: name.clone(),
725            args: args.iter().map(|a| r(a)).collect(),
726        },
727
728        // Bitvector: recurse operands
729        VerifyExpr::BitVecBinary { op, left, right } => VerifyExpr::BitVecBinary {
730            op: *op,
731            left: Box::new(r(left)),
732            right: Box::new(r(right)),
733        },
734        VerifyExpr::BitVecExtract { high, low, operand } => VerifyExpr::BitVecExtract {
735            high: *high, low: *low,
736            operand: Box::new(r(operand)),
737        },
738        VerifyExpr::BitVecConcat(l, ri) => VerifyExpr::BitVecConcat(Box::new(r(l)), Box::new(r(ri))),
739
740        // Array: recurse all sub-expressions
741        VerifyExpr::Select { array, index } => VerifyExpr::Select {
742            array: Box::new(r(array)),
743            index: Box::new(r(index)),
744        },
745        VerifyExpr::Store { array, index, value } => VerifyExpr::Store {
746            array: Box::new(r(array)),
747            index: Box::new(r(index)),
748            value: Box::new(r(value)),
749        },
750
751        // Temporal BMC: recurse sub-expressions
752        VerifyExpr::AtState { state, expr: e } => VerifyExpr::AtState {
753            state: Box::new(r(state)),
754            expr: Box::new(r(e)),
755        },
756        VerifyExpr::Transition { from: f, to: t } => VerifyExpr::Transition {
757            from: Box::new(r(f)),
758            to: Box::new(r(t)),
759        },
760    }
761}
762
763impl Default for VerificationSession {
764    fn default() -> Self {
765        Self::new()
766    }
767}
768
769/// Build a fresh solver carrying the standard 10-second timeout.
770fn timed_solver() -> Solver {
771    let solver = crate::solver::new_solver();
772    let mut params = Params::new();
773    params.set_u32("timeout", 10000);
774    solver.set_params(&params);
775    solver
776}
777
778/// Internal encoder that converts VerifyExpr to Z3 AST.
779struct Encoder<'a> {
780    vars: &'a HashMap<String, VerifyType>,
781}
782
783impl<'a> Encoder<'a> {
784    fn new(vars: &'a HashMap<String, VerifyType>) -> Self {
785        Self { vars }
786    }
787
788    fn encode(&self, expr: &VerifyExpr) -> Dynamic {
789        match expr {
790            VerifyExpr::Int(n) => Dynamic::from_ast(&Int::from_i64(*n)),
791            VerifyExpr::Bool(b) => Dynamic::from_ast(&Bool::from_bool(*b)),
792
793            VerifyExpr::Var(name) => {
794                let ty = self.vars.get(name).cloned().unwrap_or(VerifyType::Int);
795                match ty {
796                    VerifyType::Int => Dynamic::from_ast(&Int::new_const(name.as_str())),
797                    VerifyType::Bool => Dynamic::from_ast(&Bool::new_const(name.as_str())),
798                    VerifyType::Object => {
799                        Dynamic::from_ast(&Int::new_const(name.as_str()))
800                    }
801                    VerifyType::Real => {
802                        Dynamic::from_ast(&z3::ast::Real::new_const(name.as_str()))
803                    }
804                    VerifyType::BitVector(width) => {
805                        Dynamic::from_ast(&z3::ast::BV::new_const(name.as_str(), width))
806                    }
807                    VerifyType::Array(ref idx_ty, ref elem_ty) => {
808                        let idx_sort = self.type_to_sort(idx_ty);
809                        let elem_sort = self.type_to_sort(elem_ty);
810                        Dynamic::from_ast(&z3::ast::Array::new_const(name.as_str(), &idx_sort, &elem_sort))
811                    }
812                }
813            }
814
815            VerifyExpr::Binary { op, left, right } => {
816                let l = self.encode(left);
817                let r = self.encode(right);
818                self.encode_binary(op, l, r)
819            }
820
821            VerifyExpr::Not(inner) => {
822                let i = self.encode(inner);
823                if let Some(b) = i.as_bool() {
824                    Dynamic::from_ast(&b.not())
825                } else {
826                    i
827                }
828            }
829
830            VerifyExpr::Apply { name, args } => {
831                self.encode_apply(name, args)
832            }
833
834            VerifyExpr::ApplyInt { name, args } => {
835                let int_sort = Sort::int();
836                let domain: Vec<&Sort> = args.iter().map(|_| &int_sort).collect();
837                let func_decl = FuncDecl::new(name.as_str(), &domain, &int_sort);
838                let encoded_args: Vec<Dynamic> =
839                    args.iter().map(|a| self.encode(a)).collect();
840                let arg_refs: Vec<&dyn Ast> =
841                    encoded_args.iter().map(|a| a as &dyn Ast).collect();
842                Dynamic::from_ast(&func_decl.apply(&arg_refs))
843            }
844
845            VerifyExpr::ForAll { vars, body } => {
846                if vars.is_empty() {
847                    return self.encode(body);
848                }
849                let body_encoded = {
850                    let b = self.encode(body);
851                    b.as_bool().unwrap_or_else(|| Bool::from_bool(true))
852                };
853                let bound_consts: Vec<Dynamic> = vars.iter().map(|(name, ty)| {
854                    self.make_quantifier_var(name, ty)
855                }).collect();
856                let bound_refs: Vec<&dyn Ast> = bound_consts.iter().map(|d| d as &dyn Ast).collect();
857                Dynamic::from_ast(&z3::ast::forall_const(&bound_refs, &[], &body_encoded))
858            }
859
860            VerifyExpr::Exists { vars, body } => {
861                if vars.is_empty() {
862                    return self.encode(body);
863                }
864                let body_encoded = {
865                    let b = self.encode(body);
866                    b.as_bool().unwrap_or_else(|| Bool::from_bool(true))
867                };
868                let bound_consts: Vec<Dynamic> = vars.iter().map(|(name, ty)| {
869                    self.make_quantifier_var(name, ty)
870                }).collect();
871                let bound_refs: Vec<&dyn Ast> = bound_consts.iter().map(|d| d as &dyn Ast).collect();
872                Dynamic::from_ast(&z3::ast::exists_const(&bound_refs, &[], &body_encoded))
873            }
874
875            // ---- Bitvector operations ----
876
877            VerifyExpr::BitVecConst { width, value } => {
878                Dynamic::from_ast(&z3::ast::BV::from_u64(*value, *width))
879            }
880
881            VerifyExpr::BitVecBinary { op, left, right } => {
882                let l = self.encode(left);
883                let r = self.encode(right);
884                self.encode_bv_binary(op, l, r)
885            }
886
887            VerifyExpr::BitVecExtract { high, low, operand } => {
888                let bv = self.encode(operand);
889                if let Some(bv) = bv.as_bv() {
890                    Dynamic::from_ast(&bv.extract(*high, *low))
891                } else {
892                    bv
893                }
894            }
895
896            VerifyExpr::BitVecConcat(left, right) => {
897                let l = self.encode(left);
898                let r = self.encode(right);
899                if let (Some(lb), Some(rb)) = (l.as_bv(), r.as_bv()) {
900                    Dynamic::from_ast(&lb.concat(&rb))
901                } else {
902                    l
903                }
904            }
905
906            // ---- Array theory ----
907
908            VerifyExpr::Select { array, index } => {
909                let a = self.encode(array);
910                let i = self.encode(index);
911                if let Some(arr) = a.as_array() {
912                    Dynamic::from_ast(&arr.select(&i))
913                } else {
914                    a
915                }
916            }
917
918            VerifyExpr::Store { array, index, value } => {
919                let a = self.encode(array);
920                let i = self.encode(index);
921                let v = self.encode(value);
922                if let Some(arr) = a.as_array() {
923                    Dynamic::from_ast(&arr.store(&i, &v))
924                } else {
925                    a
926                }
927            }
928
929            // ---- Temporal (BMC) ----
930
931            VerifyExpr::AtState { state: _, expr } => {
932                // For now, just encode the expression (state context handled by variable naming)
933                self.encode(expr)
934            }
935
936            VerifyExpr::Transition { from, to } => {
937                // Encode as conjunction of from and to constraints
938                let f = self.encode(from);
939                let t = self.encode(to);
940                if let (Some(fb), Some(tb)) = (f.as_bool(), t.as_bool()) {
941                    Dynamic::from_ast(&Bool::and(&[&fb, &tb]))
942                } else {
943                    f
944                }
945            }
946
947            // ---- Biconditional ----
948
949            VerifyExpr::Iff(left, right) => {
950                let l = self.encode(left);
951                let r = self.encode(right);
952                if let (Some(lb), Some(rb)) = (l.as_bool(), r.as_bool()) {
953                    Dynamic::from_ast(&lb.iff(&rb))
954                } else {
955                    // Fallback: encode as (l → r) ∧ (r → l) at value level
956                    Dynamic::from_ast(&l.eq(&r))
957                }
958            }
959        }
960    }
961
962    fn type_to_sort(&self, ty: &VerifyType) -> z3::Sort {
963        match ty {
964            VerifyType::Int => z3::Sort::int(),
965            VerifyType::Bool => z3::Sort::bool(),
966            VerifyType::Object => z3::Sort::int(),
967            VerifyType::Real => z3::Sort::real(),
968            VerifyType::BitVector(width) => z3::Sort::bitvector(*width),
969            VerifyType::Array(idx, elem) => {
970                let idx_sort = self.type_to_sort(idx);
971                let elem_sort = self.type_to_sort(elem);
972                z3::Sort::array(&idx_sort, &elem_sort)
973            }
974        }
975    }
976
977    fn make_quantifier_var(&self, name: &str, ty: &VerifyType) -> Dynamic {
978        match ty {
979            VerifyType::Int => Dynamic::from_ast(&Int::new_const(name)),
980            VerifyType::Bool => Dynamic::from_ast(&Bool::new_const(name)),
981            VerifyType::BitVector(w) => Dynamic::from_ast(&z3::ast::BV::new_const(name, *w)),
982            VerifyType::Object => Dynamic::from_ast(&Int::new_const(name)),
983            VerifyType::Real => Dynamic::from_ast(&z3::ast::Real::new_const(name)),
984            VerifyType::Array(idx, elem) => {
985                let idx_sort = self.type_to_sort(idx);
986                let elem_sort = self.type_to_sort(elem);
987                Dynamic::from_ast(&z3::ast::Array::new_const(name, &idx_sort, &elem_sort))
988            }
989        }
990    }
991
992    fn encode_binary(&self, op: &VerifyOp, l: Dynamic, r: Dynamic) -> Dynamic {
993        match op {
994            // Arithmetic
995            VerifyOp::Add => {
996                if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
997                    Dynamic::from_ast(&(li + ri))
998                } else {
999                    l
1000                }
1001            }
1002            VerifyOp::Sub => {
1003                if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
1004                    Dynamic::from_ast(&(li - ri))
1005                } else {
1006                    l
1007                }
1008            }
1009            VerifyOp::Mul => {
1010                if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
1011                    Dynamic::from_ast(&(li * ri))
1012                } else {
1013                    l
1014                }
1015            }
1016            VerifyOp::Div => {
1017                if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
1018                    Dynamic::from_ast(&(li / ri))
1019                } else {
1020                    l
1021                }
1022            }
1023            // Floor division `a // b`: `to_int(to_real(a) / to_real(b))` — real division then the
1024            // floor (`Real::to_int` is floor), exact toward -inf for every sign.
1025            VerifyOp::FloorDiv => {
1026                if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
1027                    Dynamic::from_ast(&(li.to_real() / ri.to_real()).to_int())
1028                } else {
1029                    l
1030                }
1031            }
1032
1033            // Comparison
1034            VerifyOp::Gt => {
1035                if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
1036                    Dynamic::from_ast(&li.gt(&ri))
1037                } else {
1038                    Dynamic::from_ast(&Bool::from_bool(false))
1039                }
1040            }
1041            VerifyOp::Lt => {
1042                if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
1043                    Dynamic::from_ast(&li.lt(&ri))
1044                } else {
1045                    Dynamic::from_ast(&Bool::from_bool(false))
1046                }
1047            }
1048            VerifyOp::Gte => {
1049                if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
1050                    Dynamic::from_ast(&li.ge(&ri))
1051                } else {
1052                    Dynamic::from_ast(&Bool::from_bool(false))
1053                }
1054            }
1055            VerifyOp::Lte => {
1056                if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
1057                    Dynamic::from_ast(&li.le(&ri))
1058                } else {
1059                    Dynamic::from_ast(&Bool::from_bool(false))
1060                }
1061            }
1062
1063            // Equality
1064            VerifyOp::Eq => Dynamic::from_ast(&l.eq(&r)),
1065            VerifyOp::Neq => Dynamic::from_ast(&l.eq(&r).not()),
1066
1067            // Logic
1068            VerifyOp::And => {
1069                if let (Some(lb), Some(rb)) = (l.as_bool(), r.as_bool()) {
1070                    Dynamic::from_ast(&Bool::and(&[&lb, &rb]))
1071                } else {
1072                    Dynamic::from_ast(&Bool::from_bool(false))
1073                }
1074            }
1075            VerifyOp::Or => {
1076                if let (Some(lb), Some(rb)) = (l.as_bool(), r.as_bool()) {
1077                    Dynamic::from_ast(&Bool::or(&[&lb, &rb]))
1078                } else {
1079                    Dynamic::from_ast(&Bool::from_bool(false))
1080                }
1081            }
1082            VerifyOp::Implies => {
1083                if let (Some(lb), Some(rb)) = (l.as_bool(), r.as_bool()) {
1084                    Dynamic::from_ast(&lb.implies(&rb))
1085                } else {
1086                    Dynamic::from_ast(&Bool::from_bool(true))
1087                }
1088            }
1089        }
1090    }
1091
1092    fn encode_bv_binary(&self, op: &crate::ir::BitVecOp, l: Dynamic, r: Dynamic) -> Dynamic {
1093        use crate::ir::BitVecOp;
1094        if let (Some(lb), Some(rb)) = (l.as_bv(), r.as_bv()) {
1095            match op {
1096                BitVecOp::And => Dynamic::from_ast(&lb.bvand(&rb)),
1097                BitVecOp::Or => Dynamic::from_ast(&lb.bvor(&rb)),
1098                BitVecOp::Xor => Dynamic::from_ast(&lb.bvxor(&rb)),
1099                BitVecOp::Not => Dynamic::from_ast(&lb.bvnot()),
1100                BitVecOp::Shl => Dynamic::from_ast(&lb.bvshl(&rb)),
1101                BitVecOp::Shr => Dynamic::from_ast(&lb.bvlshr(&rb)),
1102                BitVecOp::AShr => Dynamic::from_ast(&lb.bvashr(&rb)),
1103                BitVecOp::Add => Dynamic::from_ast(&lb.bvadd(&rb)),
1104                BitVecOp::Sub => Dynamic::from_ast(&lb.bvsub(&rb)),
1105                BitVecOp::Mul => Dynamic::from_ast(&lb.bvmul(&rb)),
1106                BitVecOp::SDiv => Dynamic::from_ast(&lb.bvsdiv(&rb)),
1107                BitVecOp::SRem => Dynamic::from_ast(&lb.bvsrem(&rb)),
1108                BitVecOp::ULt => Dynamic::from_ast(&lb.bvult(&rb)),
1109                BitVecOp::SLt => Dynamic::from_ast(&lb.bvslt(&rb)),
1110                BitVecOp::ULe => Dynamic::from_ast(&lb.bvule(&rb)),
1111                BitVecOp::SLe => Dynamic::from_ast(&lb.bvsle(&rb)),
1112                BitVecOp::Eq => Dynamic::from_ast(&lb.eq(&rb)),
1113            }
1114        } else {
1115            l
1116        }
1117    }
1118
1119    fn encode_apply(&self, name: &str, args: &[VerifyExpr]) -> Dynamic {
1120        let int_sort = Sort::int();
1121        let domain: Vec<&Sort> = args.iter().map(|_| &int_sort).collect();
1122        let range = Sort::bool();
1123
1124        let func_decl = FuncDecl::new(name, &domain, &range);
1125
1126        let encoded_args: Vec<Dynamic> = args.iter().map(|a| self.encode(a)).collect();
1127        let arg_refs: Vec<&dyn Ast> = encoded_args.iter().map(|a| a as &dyn Ast).collect();
1128
1129        Dynamic::from_ast(&func_decl.apply(&arg_refs))
1130    }
1131}
1132
1133#[cfg(test)]
1134mod tests {
1135    use super::*;
1136
1137    #[test]
1138    fn test_tautology() {
1139        let verifier = Verifier::new();
1140        assert!(verifier.check_bool(true).is_ok());
1141    }
1142
1143    #[test]
1144    fn test_contradiction() {
1145        let verifier = Verifier::new();
1146        assert!(verifier.check_bool(false).is_err());
1147    }
1148
1149    #[test]
1150    fn test_int_greater_than_valid() {
1151        let verifier = Verifier::new();
1152        assert!(verifier.check_int_greater_than(10, 5).is_ok());
1153    }
1154
1155    #[test]
1156    fn test_int_greater_than_invalid() {
1157        let verifier = Verifier::new();
1158        assert!(verifier.check_int_greater_than(3, 5).is_err());
1159    }
1160
1161    #[test]
1162    fn test_int_equals_valid() {
1163        let verifier = Verifier::new();
1164        assert!(verifier.check_int_equals(42, 42).is_ok());
1165    }
1166
1167    #[test]
1168    fn test_int_equals_invalid() {
1169        let verifier = Verifier::new();
1170        assert!(verifier.check_int_equals(1, 2).is_err());
1171    }
1172
1173    #[test]
1174    fn test_context_api() {
1175        let verifier = Verifier::new();
1176        let vctx = verifier.context();
1177        let solver = vctx.solver();
1178
1179        // P ∨ ¬P is a tautology
1180        let p = vctx.bool_var("p");
1181        let tautology = Bool::or(&[&p, &p.not()]);
1182
1183        assert!(vctx.check_valid(&solver, &tautology).is_ok());
1184    }
1185
1186    #[test]
1187    fn test_context_contradiction() {
1188        let verifier = Verifier::new();
1189        let vctx = verifier.context();
1190        let solver = vctx.solver();
1191
1192        // P ∧ ¬P is a contradiction (not valid)
1193        let p = vctx.bool_var("p");
1194        let contradiction = Bool::and(&[&p, &p.not()]);
1195
1196        assert!(vctx.check_valid(&solver, &contradiction).is_err());
1197    }
1198
1199    // ============================================================
1200    // VerificationSession Tests
1201    // ============================================================
1202
1203    #[test]
1204    fn test_session_integer_bounds() {
1205        let mut session = VerificationSession::new();
1206
1207        // Declare x as Int
1208        session.declare("x", VerifyType::Int);
1209
1210        // Assume: x = 10
1211        session.assume(&VerifyExpr::eq(
1212            VerifyExpr::var("x"),
1213            VerifyExpr::int(10),
1214        ));
1215
1216        // Verify: x > 5 (should pass)
1217        let result = session.verify(&VerifyExpr::gt(
1218            VerifyExpr::var("x"),
1219            VerifyExpr::int(5),
1220        ));
1221        assert!(result.is_ok(), "10 > 5 should be provable");
1222    }
1223
1224    #[test]
1225    fn test_session_integer_contradiction() {
1226        let mut session = VerificationSession::new();
1227
1228        // Declare x as Int
1229        session.declare("x", VerifyType::Int);
1230
1231        // Assume: x = 10
1232        session.assume(&VerifyExpr::eq(
1233            VerifyExpr::var("x"),
1234            VerifyExpr::int(10),
1235        ));
1236
1237        // Verify: x < 5 (should FAIL)
1238        let result = session.verify(&VerifyExpr::lt(
1239            VerifyExpr::var("x"),
1240            VerifyExpr::int(5),
1241        ));
1242        assert!(result.is_err(), "10 < 5 should not be provable");
1243    }
1244
1245    #[test]
1246    fn test_session_uninterpreted_functions() {
1247        let mut session = VerificationSession::new();
1248
1249        // Declare x as Object
1250        session.declare("x", VerifyType::Object);
1251
1252        // Assume: Mortal(x) -> Human(x)
1253        session.assume(&VerifyExpr::implies(
1254            VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]),
1255            VerifyExpr::apply("Human", vec![VerifyExpr::var("x")]),
1256        ));
1257
1258        // Assume: Mortal(x)
1259        session.assume(&VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]));
1260
1261        // Verify: Human(x) - Z3 should deduce this structurally
1262        let result = session.verify(&VerifyExpr::apply("Human", vec![VerifyExpr::var("x")]));
1263        assert!(result.is_ok(), "Should deduce Human(x) from Mortal(x) and Mortal(x)->Human(x)");
1264    }
1265
1266    #[test]
1267    fn test_session_modal_structural_reasoning() {
1268        let mut session = VerificationSession::new();
1269
1270        // Declare A and B as Objects (representing propositions)
1271        session.declare("A", VerifyType::Object);
1272        session.declare("B", VerifyType::Object);
1273
1274        // Assume: Possible(A) -> Possible(B)
1275        session.assume(&VerifyExpr::implies(
1276            VerifyExpr::apply("Possible", vec![VerifyExpr::var("A")]),
1277            VerifyExpr::apply("Possible", vec![VerifyExpr::var("B")]),
1278        ));
1279
1280        // Assume: Possible(A)
1281        session.assume(&VerifyExpr::apply("Possible", vec![VerifyExpr::var("A")]));
1282
1283        // Verify: Possible(B)
1284        let result = session.verify(&VerifyExpr::apply("Possible", vec![VerifyExpr::var("B")]));
1285        assert!(result.is_ok(), "Should deduce Possible(B) from modus ponens");
1286    }
1287
1288    #[test]
1289    fn test_session_arithmetic() {
1290        let mut session = VerificationSession::new();
1291
1292        // Declare x and y
1293        session.declare("x", VerifyType::Int);
1294        session.declare("y", VerifyType::Int);
1295
1296        // Assume: x = 5, y = 3
1297        session.assume(&VerifyExpr::eq(VerifyExpr::var("x"), VerifyExpr::int(5)));
1298        session.assume(&VerifyExpr::eq(VerifyExpr::var("y"), VerifyExpr::int(3)));
1299
1300        // Verify: x + y > 7 (5 + 3 = 8 > 7)
1301        let sum = VerifyExpr::binary(
1302            VerifyOp::Add,
1303            VerifyExpr::var("x"),
1304            VerifyExpr::var("y"),
1305        );
1306        let result = session.verify(&VerifyExpr::gt(sum, VerifyExpr::int(7)));
1307        assert!(result.is_ok(), "5 + 3 > 7 should be provable");
1308    }
1309
1310    #[test]
1311    fn test_session_logic_and_or() {
1312        let mut session = VerificationSession::new();
1313
1314        // Declare p and q as Bool
1315        session.declare("p", VerifyType::Bool);
1316        session.declare("q", VerifyType::Bool);
1317
1318        // Assume: p = true, q = false
1319        session.assume(&VerifyExpr::eq(VerifyExpr::var("p"), VerifyExpr::bool(true)));
1320        session.assume(&VerifyExpr::eq(VerifyExpr::var("q"), VerifyExpr::bool(false)));
1321
1322        // Verify: p || q (true || false = true)
1323        let result = session.verify(&VerifyExpr::or(
1324            VerifyExpr::var("p"),
1325            VerifyExpr::var("q"),
1326        ));
1327        assert!(result.is_ok(), "true || false should be provable");
1328
1329        // Verify: !(p && q) (!(true && false) = true)
1330        let result = session.verify(&VerifyExpr::not(VerifyExpr::and(
1331            VerifyExpr::var("p"),
1332            VerifyExpr::var("q"),
1333        )));
1334        assert!(result.is_ok(), "!(true && false) should be provable");
1335    }
1336}
logicaffeine_verify/solver.rs

logicaffeine_verify/
solver.rs
