rustproof_libsmt/theories/
real.rs

1//! Defines basic operations defined under Real 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    Const(f64),
19    FreeVar(String),
20}
21
22impl fmt::Display for OpCodes {
23    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
24        let s = match *self {
25            OpCodes::Neg => "-".to_owned(),
26            OpCodes::Sub => "-".to_owned(),
27            OpCodes::Add => "+".to_owned(),
28            OpCodes::Mul => "*".to_owned(),
29            OpCodes::Div => "/".to_owned(),
30            OpCodes::Lte => "<=".to_owned(),
31            OpCodes::Lt => "<".to_owned(),
32            OpCodes::Gte => ">=".to_owned(),
33            OpCodes::Gt => ">".to_owned(),
34            OpCodes::Const(ref val) => format!("{}", val),
35            OpCodes::FreeVar(ref name) => format!("{}", name),
36        };
37        write!(f, "{}", s)
38    }
39}
40
41impl_smt_node!(OpCodes, define vars [OpCodes::FreeVar(_)], define consts [OpCodes::Const(_)]);
42
43#[derive(Clone,Debug)]
44pub enum Sorts {
45    Real
46}
47
48impl fmt::Display for Sorts {
49    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
50        write!(f, "{}", "Real")
51    }
52}
rustproof_libsmt/theories/real.rs

rustproof_libsmt/theories/
real.rs
