rustproof-libsmt 0.1.0

Rust bindings for z3 as utilized by RustProof.
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

//! Crate that allows rust programs to interact with SMT (Satisfiability Modulo Theory) solvers.

extern crate petgraph;
extern crate regex;

pub mod theories {
    #[macro_use] pub mod utils;
    #[macro_use] pub mod bitvec;
    pub mod integer;
    pub mod core;
    pub mod array_ex;
    pub mod real;
    pub mod real_ints;
}

pub mod logics {
    #[macro_use] pub mod utils;
    pub mod qf_bv;
    pub mod qf_aufbv;
    pub mod qf_abv;
    pub mod lia;
}

pub mod backends {
    pub mod backend;
    pub mod smtlib2;
    pub mod z3;
}