rz3 0.1.3

Deterministic, exact-rational SMT solver in pure Rust (DPLL(T)/CDCL) with an exact linear-arithmetic core. Zero C dependencies, WASM-deployable, reproducible run-to-run.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

pub mod array;
pub mod bv;
pub mod euf;
pub mod fp;
pub mod lra;
pub mod nla;
pub mod quantifier;
pub mod string;

pub use crate::ast::fp::{FloatSort, FloatValue, RoundingMode};
pub use array::ArraySolver;
pub use bv::BitBlaster;
pub use euf::EufSolver;
pub use lra::LraSolver;
pub use nla::NlaSolver;
pub use quantifier::QuantifierSolver;
pub use string::StringSolver;

use crate::ast::{Expr, ModelValue};

/// Interfaz fundamental para Solvers de Teoría (Theory Solvers).
/// Permite al núcleo SAT delegar la verificación de restricciones no booleanas.
pub trait TheorySolver {
    /// Añade una restricción a la teoría actual.
    fn assert(&mut self, expr: &Expr);
    /// Verifica si el conjunto actual de restricciones es consistente (Satisfiable).
    fn check(&mut self) -> bool;
    /// En caso de conflicto (Unsat), devuelve el subconjunto de expresiones que lo causan.
    fn explain(&self) -> Vec<Expr>;
    /// Obtiene el valor asignado a una expresión en el modelo actual.
    fn get_model_value(&self, expr: &Expr) -> Option<ModelValue>;
}

#[derive(Debug, Clone)]
pub struct Bound {
    pub val: num_rational::BigRational,
    pub is_strict: bool,
}