-
Notifications
You must be signed in to change notification settings - Fork 0
/
reason.h
149 lines (118 loc) · 3.69 KB
/
reason.h
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
139
140
141
142
143
144
145
146
147
148
149
#ifndef REASON_H
#define REASON_H
#include <z3.h>
#include <gmpxx.h>
#include "common.h"
/*
* We can create a numeral in Z3 in a number of ways. This allows us to make the
* choce depending on the type of our domain.
*/
template <typename T>
Z3_ast MkNumeral(Z3_context context, const T &num);
template <>
Z3_ast MkNumeral(Z3_context context, const int &num) {
return Z3_mk_int(context, num, Z3_mk_int_sort(context));
}
template <>
Z3_ast MkNumeral(Z3_context context, const long long &num) {
return Z3_mk_int64(context, num, Z3_mk_int_sort(context));
}
template <>
Z3_ast MkNumeral(Z3_context context, const mpz_class &num) {
return Z3_mk_numeral(context, num.get_str().c_str(), Z3_mk_int_sort(context));
}
template <>
Z3_ast MkNumeral(Z3_context context, const mpq_class &num) {
return Z3_mk_numeral(context, num.get_str().c_str(),
Z3_mk_real_sort(context));
}
/*
* Reason for adding some edge
*/
class Reason {
public:
virtual Z3_ast MkAst(Z3_context, std::unordered_map<VarId, Z3_ast> &id_to_ast,
Z3_func_decl utvpi, Z3_func_decl svpi, Z3_ast minus, Z3_ast plus) const = 0;
virtual std::ostream& Print(std::ostream& out) const = 0;
};
typedef typename std::shared_ptr<Reason> ReasonPtr;
std::ostream& operator<<(std::ostream& out, const Reason &s) {
s.Print(out);
return out;
}
Z3_ast SignToArg2(Z3_ast minus, Z3_ast plus, Sign sign) {
if (sign == Pos)
return plus;
return minus;
}
class Equality : public Reason {
public:
Equality(VarId x, VarId y) : x_(x), y_(y) { }
Z3_ast MkAst(Z3_context context, std::unordered_map<VarId, Z3_ast> &id_to_ast,
Z3_func_decl utvpi, Z3_func_decl svpi, Z3_ast minus, Z3_ast plus) const {
Z3_ast ast_x = id_to_ast[x_];
Z3_ast ast_y = id_to_ast[y_];
return Z3_mk_eq(context, ast_x, ast_y);
}
std::ostream& Print(std::ostream &out) const {
out << x_ << " = " << y_;
return out;
}
private:
VarId x_;
VarId y_;
};
template <typename T>
class Inequality1 : public Reason {
public:
Inequality1(Sign a, VarId x, T c) : a_(a), x_(x), c_(c) { }
Z3_ast MkAst(Z3_context context, std::unordered_map<VarId, Z3_ast> &id_to_ast,
Z3_func_decl utvpi, Z3_func_decl svpi, Z3_ast minus, Z3_ast plus) const {
Z3_ast args[] = { SignToArg2(minus, plus, a_)
, id_to_ast[x_]
, MkNumeral(context, c_)
};
Z3_ast ast = Z3_mk_app(context, svpi, 3, args);
#ifdef DEBUG
std::cout << "Created: " << Z3_ast_to_string(context, ast) << std::endl;
#endif
return ast;
}
std::ostream& Print(std::ostream &out) const {
out << a_ << x_ << " <= " << c_;
return out;
}
private:
Sign a_;
VarId x_;
T c_;
};
template <typename T>
class Inequality2 : public Reason {
public:
Inequality2(Sign a, VarId x, Sign b, VarId y, T c)
: a_(a), b_(b), x_(x), y_(y), c_(c) { }
Z3_ast MkAst(Z3_context context, std::unordered_map<VarId, Z3_ast> &id_to_ast,
Z3_func_decl utvpi, Z3_func_decl svpi, Z3_ast minus, Z3_ast plus) const {
Z3_ast args[] = { SignToArg2(minus, plus, a_)
, id_to_ast[x_]
, SignToArg2(minus, plus, b_)
, id_to_ast[y_]
, MkNumeral(context, c_)
};
Z3_ast ast = Z3_mk_app(context, utvpi, 5, args);
#ifdef DEBUG
std::cout << "Created: " << Z3_ast_to_string(context, ast) << std::endl;
#endif
return ast;
}
std::ostream& Print(std::ostream &out) const {
out << a_ << x_ << " + " << b_ << y_ << " <= " << c_;
return out;
}
private:
Sign a_, b_;
VarId x_, y_;
T c_;
};
#endif /* REASON_H */