xmt-lib 0.1.1

A grounder for SMT solvers
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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

// Copyright Pierre Carbonnelle, 2025.

pub mod ast;
pub mod error;
pub mod grammar;
pub mod solver;
mod private;

use std::fs;
use std::path::PathBuf;
use std::ffi::CStr;
use z3_sys::{Z3_get_full_version};

use clap::Parser;

use crate::solver::Solver;

/// A high-level language for interacting with SMT solvers
#[derive(Parser)]
#[command(author, version, about, long_about = None)]
struct Cli {
    /// Path to the script file containing XMT-Lib commands.
    file_path: PathBuf,
}

fn main() {
    unsafe {
        let version_cstr = CStr::from_ptr(Z3_get_full_version());
        println!("Z3 version: {}", version_cstr.to_string_lossy());
    }
    let args = Cli::parse();

    if args.file_path.exists() {
        let source = fs::read_to_string(args.file_path).unwrap();
        let mut solver = Solver::new(None);
        let results = solver.parse_and_execute(&source);
        for result in results {
            print!("{}", result);
        }
    } else {
        eprintln!("Error: File '{:?}' does not exist.", args.file_path);
        std::process::exit(1);
    }
}


#[cfg(test)]
mod tests {
    use std::fs::File;

    use simplelog::*;
    use crate::solver::Solver;

    fn tester(source: &str, output: &str) {
        let mut solver = Solver::new(None);
        let results = solver.parse_and_execute(source);
        assert_eq!(results.into_iter().collect::<Vec<_>>().join(""), output);
    }

    #[test]
    fn sandbox() {
        let config = ConfigBuilder::new()
            .set_time_level(LevelFilter::Off)
            .build();
        let _ = WriteLogger::init(LevelFilter::Trace, config, File::create("xmtlib.log").unwrap());

        tester( "(assert false)
            (check-sat)",

        "unsat\n"
        );
    }
}