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