rz3 0.1.2

Deterministic, exact-rational SMT solver in pure Rust (DPLL(T)/CDCL) with a complete 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

use crate::sat::Literal;
use std::fs::File;
use std::io::Write;

pub struct DratGenerator {
    file: File,
}

impl DratGenerator {
    pub fn new(path: &str) -> std::io::Result<Self> {
        let file = File::create(path)?;
        Ok(Self { file })
    }

    pub fn log_clause(&mut self, lits: &[Literal]) -> std::io::Result<()> {
        for lit in lits {
            write!(self.file, "{} ", lit)?;
        }
        writeln!(self.file, "0")?;
        Ok(())
    }
}