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
39
40
41
42
43
44

//! Tipos canónicos de punto flotante IEEE-754 para valores de modelo.
//!
//! Viven en `ast` (capa baja) para que `theory::fp` los consuma SIN invertir
//! capas (ast NO debe depender de theory). `ModelValue::Float` usa `FloatValue`.
//! Estos tipos son el CONTRATO compartido: `theory::fp` debe `use crate::ast::fp::*`
//! en vez de definirlos localmente. [coordinación Claude/codex 2026-06-08]

use num_bigint::BigUint;
use num_rational::BigRational;
use serde::{Deserialize, Serialize};

/// Modos de redondeo IEEE-754.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
pub enum RoundingMode {
    NearestTiesToEven,
    TowardZero,
    TowardPositive,
    TowardNegative,
}

/// Formato del float: anchura de exponente y de significando.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
pub struct FloatSort {
    pub exponent_bits: u16,
    pub significand_bits: u16,
}

/// Clase de valor IEEE-754 con representación EXACTA (sin floats nativos/aproximación).
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum FloatClass {
    QuietNaN { payload: BigUint },
    PositiveInfinity,
    NegativeInfinity,
    PositiveZero,
    NegativeZero,
    Finite { negative: bool, value: BigRational },
}

/// Valor de modelo FP completo: formato + clase.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct FloatValue {
    pub sort: FloatSort,
    pub class: FloatClass,
}