rustproof_libsmt/theories/
real_ints.rs

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

rustproof_libsmt/theories/
real_ints.rs
