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

use crate::ast::Expr;

// REF: [Stump et al., 2008] "StarExec: A Benchmark Management System for the SMT Community"
//      Note: Reference to LFSC (Logical Framework with Side Conditions) commonly used for SMT proofs.

#[derive(Debug, Clone)]
pub enum ProofStep {
    Assume(Expr),
    TheoryLemma(Vec<Expr>, String), // The conflict clause and the theory name
    Resolution(usize, usize),       // Reference to two previous steps
}

pub struct Proof {
    pub steps: Vec<ProofStep>,
}

impl Default for Proof {
    fn default() -> Self {
        Self::new()
    }
}

impl Proof {
    pub fn new() -> Self {
        Self { steps: Vec::new() }
    }

    pub fn add_step(&mut self, step: ProofStep) -> usize {
        let id = self.steps.len();
        self.steps.push(step);
        id
    }
}

pub mod drat;