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

//! Module that describes QF_BV (closed quatifier-free formulas built over
//! FixedSizeBitVector) logic.
//!
//! Note that the functions and structs that are defined.

use std::fmt;

use theories::{bitvec, core};
use backends::backend::{Logic, SMTNode};

define_sorts_for_logic!(QF_BV_Sorts,
                  BV -> bitvec::Sorts,
                  Core -> core::Sorts
                 );

define_fns_for_logic!(QF_BV_Fn,
                      BVOps -> bitvec::OpCodes,
                      CoreOps -> core::OpCodes
                     );

define_logic!(QF_BV,
              QF_BV_Fn,
              QF_BV_Sorts,
              map {
                  QF_BV_Sorts::BV(_) => bitvec::OpCodes::FreeVar
              }
             );