forked from batchenRothenberg/SMTSampler
-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathtest_model.cpp
138 lines (136 loc) · 4.16 KB
/
test_model.cpp
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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
//
// Created by batchen on 06/02/2022.
//
#include "z3++.h"
#include "model.h"
int main()
{
Model new_m = Model();
z3::context c;
bool res;
std::pair<int,bool> p;
z3::expr e1(c);
p = new_m.evalArrayVar("a",0);
assert(!p.second);
assert(p.first == -1);
res = new_m.addArrayAssignment("a",0,3);
assert(res);
p = new_m.evalArrayVar("a",0);
assert(p.second);
assert(p.first == 3);
res = new_m.addArrayAssignment("a",1,5);
assert(res);
p = new_m.evalArrayVar("a",1);
assert(p.second);
assert(p.first == 5);
res = new_m.addArrayAssignment("a",1,5);
assert(!res);
res = new_m.addArrayAssignment("a",2,-6);
assert(res);
res = new_m.addArrayAssignment("b",0,3);
assert(res);
res = new_m.addArrayAssignment("b",2,50);
assert(res);
p = new_m.evalArrayVar("b",2);
assert(p.second);
assert(p.first == 50);
res = new_m.addArrayAssignment("a",1,5);
assert(!res);
res = new_m.addArrayAssignment("a",1,-8);
assert(!res);
p = new_m.evalArrayVar("a",1);
assert(p.second);
assert(p.first == 5);
p = new_m.evalIntVar("x");
assert(!p.second);
assert(p.first == -1);
res = new_m.addIntAssignment("x",3);
assert(res);
p = new_m.evalIntVar("x");
assert(p.second);
assert(p.first == 3);
res = new_m.addIntAssignment("x",30);
assert(!res);
p = new_m.evalIntVar("x");
assert(p.second);
assert(p.first == 3);
res = new_m.addIntAssignment("y",3);
assert(res);
p = new_m.evalIntVar("y");
assert(p.second);
assert(p.first == 3);
res = new_m.addIntAssignment("x",3);
assert(!res);
res = new_m.addIntAssignment("y",-93);
assert(!res);
p = new_m.evalIntVar("y");
assert(p.second);
assert(p.first == 3);
p = new_m.evalArrayVar("b",2);
assert(p.second);
assert(p.first == 50);
p = new_m.evalArrayVar("c",2);
assert(!p.second);
assert(p.first == -1);
std::cout << new_m.toString() << "\n";
e1 = c.int_const("x");
p = new_m.evalIntExpr(e1, true);
assert(p.second);
assert(p.first == 3);
e1 = c.int_const("z");
p = new_m.evalIntExpr(e1, true);
assert(!p.second);
assert(p.first == -1);
e1 = z3::select(c.constant("a",c.array_sort(c.int_sort(), c.int_sort())), 0);
p = new_m.evalIntExpr(e1, true);
assert(p.second);
assert(p.first == 3);
e1 = z3::select(c.constant("a",c.array_sort(c.int_sort(), c.int_sort())), -1);
p = new_m.evalIntExpr(e1, true);
assert(!p.second);
assert(p.first == -1);
e1 = c.int_val(8);
p = new_m.evalIntExpr(e1, true);
assert(p.second);
assert(p.first == 8);
e1 = c.int_val(8) + z3::select(c.constant("a",c.array_sort(c.int_sort(), c.int_sort())), 0);
p = new_m.evalIntExpr(e1, true);
assert(p.second);
assert(p.first == 11);
e1 = c.int_const("x") - z3::select(c.constant("b",c.array_sort(c.int_sort(), c.int_sort())), 2);
p = new_m.evalIntExpr(e1, true);
assert(p.second);
assert(p.first == -47);
e1 = -(c.int_const("x") * z3::select(c.constant("b",c.array_sort(c.int_sort(), c.int_sort())), 2));
p = new_m.evalIntExpr(e1, true);
assert(p.second);
assert(p.first == -150);
z3::expr e2 = (e1 + e1);
p = new_m.evalIntExpr(e2, true);
assert(p.second);
assert(p.first == -300);
p = new_m.evalIntExpr(4*e2, true);
assert(p.second);
assert(p.first == -1200);
p = new_m.evalIntExpr(c.int_const("w"), true);
assert(!p.second);
p = new_m.evalIntExpr(c.int_const("w"), true, true);
assert(p.second);
int w_val = p.first;
p = new_m.evalIntVar("w");
assert(p.second);
assert(p.first == w_val);
e1 = c.int_val(8) + z3::select(c.constant("a",c.array_sort(c.int_sort(), c.int_sort())), 8);
p = new_m.evalIntExpr(e1, true);
assert(!p.second);
p = new_m.evalIntExpr(e1, true, true);
assert(p.second);
int e1_val = p.first;
p = new_m.evalIntExpr(e1, true, true);
assert(p.second);
assert(e1_val == p.first);
e1 = z3::select(c.constant("a",c.array_sort(c.int_sort(), c.int_sort())), 80);
p = new_m.evalIntExpr(e1, true, true);
assert(p.second);
std::cout << "TEST SUCCESSFUL\n";
}