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

//! Common imports throughout this project.

pub use std::{
    collections::{BTreeMap as Map, BTreeSet as Set},
    fmt,
    io::Write,
    ops::{Deref, DerefMut},
};

pub use error_chain::bail;
pub use num::{bigint::Sign, BigInt as Int, BigRational as Rat, Zero};
pub use rsmt2::SmtRes;

pub use crate::{check, expr, parse, trans};

/// Step index.
///
/// In the context of a stateful expression, this is the index of the *current step*. If this index
/// is `7` for instance, then state variable `v` in the current step will be `v_7` and will be `v_8`
/// in the next step.
pub type Unroll = usize;

error_chain::error_chain! {
    types {
        Error, ErrorKind, ResExt, Res;
    }

    links {
        Smt2(rsmt2::errors::Error, rsmt2::errors::ErrorKind)
        /// An error from the `rsmt2` crate.
        ;
    }

    foreign_links {
        Io(std::io::Error)
        /// I/O error.
        ;
    }

    errors {
        /// A parse error.
        ///
        /// **NB**: `row` and `col` start at zero.
        ParseErr(row: usize, col: usize, line: String, msg: String) {
            description("parse error")
            display("error @{}:{}: `{}`, {}", row, col, line, msg)
        }
    }
}