rustproof_libsmt/theories/
integer.rs

1//! Defines basic operations defined under Int theory in SMTLIB2.
2
3use std::fmt;
4
5use backends::backend::SMTNode;
6
7#[derive(Clone, Debug)]
8pub enum OpCodes {
9    Cmp,
10    Lt,
11    Gt,
12    Lte,
13    Gte,
14    Mod,
15    Div,
16    Abs,
17    Mul,
18    Add,
19    Sub,
20    Neg,
21    Const(u64),
22    FreeVar(String),
23}
24
25
26impl fmt::Display for OpCodes {
27    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
28        let s = match *self {
29            OpCodes::Cmp => "=".to_owned(),
30            OpCodes::Lt => "<".to_owned(),
31            OpCodes::Gt => ">".to_owned(),
32            OpCodes::Lte => "<=".to_owned(),
33            OpCodes::Gte => ">=".to_owned(),
34            OpCodes::Mod => "mod".to_owned(),
35            OpCodes::Div => "div".to_owned(),
36            OpCodes::Abs => "abs".to_owned(),
37            OpCodes::Mul => "*".to_owned(),
38            OpCodes::Add => "+".to_owned(),
39            OpCodes::Sub => "-".to_owned(),
40            OpCodes::Neg => "-".to_owned(),
41            OpCodes::Const(ref val) => format!("{}", val),
42            OpCodes::FreeVar(ref name) => format!("{}", name),
43        };
44        write!(f, "{}", s)
45    }
46}
47
48impl_smt_node!(OpCodes, define vars [OpCodes::FreeVar(_)], define consts [OpCodes::Const(_)]);
49
50#[derive(Clone, Debug)]
51pub enum Sorts {
52    Int
53}
54
55impl fmt::Display for Sorts {
56    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
57        write!(f, "{}", "Int")
58    }
59}
rustproof_libsmt/theories/integer.rs

rustproof_libsmt/theories/
integer.rs
