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
29
30
31
32
33
34
35
36
37
38
39
40

//! Module that describes LIA logic.
//!
//! Note that the functions and structs that are defined.

use std::fmt;

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

define_sorts_for_logic!(LIA_Sorts,
                  Int -> integer::Sorts,
                  Core -> core::Sorts
                 );

define_fns_for_logic!(LIA_Fn,
                      IntOps -> integer::OpCodes,
                      CoreOps -> core::OpCodes
                     );

#[derive(Clone, Copy, Debug)]
pub struct LIA;

impl fmt::Display for LIA {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        write!(f, "{}", "LIA")
    }
}

impl Logic for LIA {
    type Fns = LIA_Fn;
    type Sorts = LIA_Sorts;

    fn free_var<T: AsRef<str>>(name: T, ty: LIA_Sorts) -> Self::Fns {
        let fv = match ty {
            LIA_Sorts::Int(_) => integer::OpCodes::FreeVar(name.as_ref().to_owned()),
            LIA_Sorts::Core(_) => unreachable!(),
        };
        LIA_Fn::IntOps(fv)
    }
}