lib/accy/src/choir/shape/fact.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

 1 const expression = @import("expression.zig");
 2 
 3 pub const Bounds = struct {
 4     min: ?u64 = null,
 5     opt: ?u64 = null,
 6     max: ?u64 = null,
 7 
 8     pub fn valid(self: Bounds) bool {
 9         if (self.min == null and self.opt == null and self.max == null) return false;
10         if (self.min) |min| {
11             if (self.opt) |opt| {
12                 if (min > opt) return false;
13             }
14             if (self.max) |max| {
15                 if (min > max) return false;
16             }
17         }
18         if (self.opt) |opt| {
19             if (self.max) |max| {
20                 if (opt > max) return false;
21             }
22         }
23         return true;
24     }
25 };
26 
27 pub const Equality = struct {
28     lhs: expression.Expression,
29     rhs: expression.Expression,
30 };
31 
32 pub const Bound = struct {
33     value: expression.Expression,
34     bounds: Bounds,
35 };
36 
37 pub const Divisibility = struct {
38     value: expression.Expression,
39     divisor: u64,
40 };
41 
42 pub const Predicate = union(enum) {
43     equal: Equality,
44     bound: Bound,
45     divisible: Divisibility,
46 };
47 
48 pub const Mode = enum {
49     assume,
50     assert,
51 };
52 
53 pub const Fact = struct {
54     mode: Mode,
55     predicate: Predicate,
56 };