mikino_api 0.1.0

A simple induction and BMC engine
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
74
75
76
77
78
79

//! Mikino's macros.

/// Imports mikino's prelude.
#[macro_export]
macro_rules! prelude {
    {} => { use $crate::prelude::*; };
    { pub } => { pub use $crate::prelude::*; };
}

/// Convenience macro, provides a DSL for writing expressions.
///
/// - identifiers must be written as `(var_name: var_typ)`, without any quotes.
#[macro_export]
macro_rules! build_expr {
    (true) => ( $crate::expr::PExpr::from(true) );
    (false) => ( $crate::expr::PExpr::from(false) );

    ( ($var:ident : $typ:ident) ) => (
        $crate::expr::PExpr::new_var(
            $crate::expr::Var::new(stringify!($var), $crate::build_typ!($typ))
        )
    );
    ( ($var:ident @ 0 : $typ:ident) ) => (
        $crate::expr::PExpr::new_var(
            $crate::expr::SVar::new_curr(
                $crate::expr::Var::new(stringify!($var), $crate::build_typ!($typ))
            )
        )
    );
    ( ($var:ident @ 1 : $typ:ident) ) => (
        $crate::expr::PExpr::new_var(
            $crate::expr::SVar::new_next(
                $crate::expr::Var::new(stringify!($var), $crate::build_typ!($typ))
            )
        )
    );

    ( ($op:tt $($args:tt)*) ) => (
        $crate::expr::PExpr::from((
            $crate::build_expr!(@op $op),
            vec![ $($crate::build_expr!($args)),* ],

        ))
    );

    ($cst:expr) => ( $crate::expr::PExpr::from($cst) );

    (@op ite) => ( $crate::expr::Op::Ite );
    (@op +) => ( $crate::expr::Op::Add );
    (@op -) => ( $crate::expr::Op::Sub );
    (@op *) => ( $crate::expr::Op::Mul );
    (@op /) => ( $crate::expr::Op::Div );
    (@op %) => ( $crate::expr::Op::Mod );
    (@op >=) => ( $crate::expr::Op::Ge );
    (@op <=) => ( $crate::expr::Op::Le );
    (@op >) => ( $crate::expr::Op::Gt );
    (@op <) => ( $crate::expr::Op::Lt );
    (@op =) => ( $crate::expr::Op::Eq );
    (@op not) => ( $crate::expr::Op::Not );
    (@op and) => ( $crate::expr::Op::And );
    (@op or) => ( $crate::expr::Op::Or );
    (@op !) => ( $crate::expr::Op::Not );
    (@op &&) => ( $crate::expr::Op::And );
    (@op ||) => ( $crate::expr::Op::Or );
}

/// Builds a type.
#[macro_export]
macro_rules! build_typ {
    (bool) => {
        $crate::expr::Typ::Bool
    };
    (int) => {
        $crate::expr::Typ::Int
    };
    (rat) => {
        $crate::expr::Typ::Rat
    };
}