rustproof_libsmt/theories/
core.rs

1//! Defines basic operation defined under Core theory in SMTLIB2.
2
3use std::fmt;
4
5use backends::backend::SMTNode;
6
7#[derive(Clone, Debug)]
8pub enum OpCodes {
9    Not,
10    Imply,
11    And,
12    Or,
13    Xor,
14    Cmp,
15    Distinct,
16    ITE,
17    Const(bool),
18    FreeVar(String)
19}
20
21impl fmt::Display for OpCodes {
22    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
23        let s = match *self {
24            OpCodes::Not => "not".to_owned(),
25            OpCodes::Imply => "=>".to_owned(),
26            OpCodes::And => "and".to_owned(),
27            OpCodes::Or => "or".to_owned(),
28            OpCodes::Xor => "xor".to_owned(),
29            OpCodes::Cmp => "=".to_owned(),
30            OpCodes::Distinct => "distinct".to_owned(),
31            OpCodes::ITE => "ite".to_owned(),
32            OpCodes::Const(val) => format!("{}", val),
33            OpCodes::FreeVar(ref s) => s.clone(),
34        };
35        write!(f, "{}", s)
36    }
37}
38
39impl_smt_node!(OpCodes, define vars [OpCodes::FreeVar(_)], define consts [OpCodes::Const(_)]);
40
41#[derive(Clone, Copy, Debug, PartialEq)]
42pub enum Sorts {
43    Bool
44}
45
46impl fmt::Display for Sorts {
47    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
48        write!(f, "{}", "bool")
49    }
50}
rustproof_libsmt/theories/core.rs

rustproof_libsmt/theories/
core.rs
