rustproof_libsmt/theories/
array_ex.rs

1//! Module that describes the ArrayEx Theory
2
3use std::fmt;
4
5use backends::backend::SMTNode;
6
7#[derive(Clone, Debug)]
8pub enum OpCodes<X, Y, Z>
9    where X: fmt::Debug + fmt::Display + Clone,
10          Y: fmt::Debug + fmt::Display + Clone,
11          Z: fmt::Debug + fmt::Display + Clone
12{
13    Select,
14    Store,
15    FreeVar(String),
16    Const(Sorts<X, Y>, Box<Z>),
17}
18
19impl<X, Y, Z> fmt::Display for OpCodes<X, Y, Z>
20where X: fmt::Debug + fmt::Display + Clone,
21      Y: fmt::Debug + fmt::Display + Clone,
22      Z: fmt::Debug + fmt::Display + Clone {
23    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
24        let s = match *self {
25            OpCodes::Select => "select".to_owned(),
26            OpCodes::Store => "store".to_owned(),
27            OpCodes::FreeVar(ref s) => s.clone(),
28            OpCodes::Const(ref arr, ref val) => format!("((as const {}) {})", arr, val),
29        };
30        write!(f, "{}", s)
31    }
32}
33
34impl<X, Y, Z> SMTNode for OpCodes<X, Y, Z>
35where X: fmt::Debug + fmt::Display + Clone,
36      Z: fmt::Debug + fmt::Display + Clone,
37      Y: fmt::Debug + fmt::Display + Clone {
38
39    fn is_var(&self) -> bool {
40        if let OpCodes::FreeVar(_) = *self {
41            true
42        } else {
43            false
44        }
45    }
46
47    fn is_const(&self) -> bool {
48        match *self {
49            OpCodes::Const(_, _) => true,
50            _ => false,
51        }
52    }
53}
54
55#[derive(Clone, Debug)]
56pub enum Sorts<X, Y>
57    where X: fmt::Display + fmt::Debug + Clone,
58          Y: fmt::Display + fmt::Debug + Clone
59{
60    Array(Box<X>, Box<Y>),
61}
62
63impl<X, Y> fmt::Display for Sorts<X, Y>
64    where X: fmt::Display + fmt::Debug + Clone,
65          Y: fmt::Display + fmt::Debug + Clone {
66    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
67        let s = match *self {
68            Sorts::Array(ref x, ref y) => format!("(Array {} {})", x, y),
69        };
70        write!(f, "{}", s)
71    }
72}
73
74impl<X, Y> Sorts<X, Y>
75where X: fmt::Debug + fmt::Display + Clone,
76      Y: fmt::Debug + fmt::Display + Clone
77{
78    pub fn new(idx: X, ty: Y) -> Sorts<X, Y> {
79        Sorts::Array(Box::new(idx), Box::new(ty))
80    }
81}
rustproof_libsmt/theories/array_ex.rs

rustproof_libsmt/theories/
array_ex.rs
