flux_infer/
fixpoint_qualifiers.rs

1use std::sync::LazyLock;
2
3use liquid_fixpoint::{BinOp, BinRel, Sort};
4
5use crate::fixpoint_encoding::fixpoint::{
6    LocalVar, Var,
7    fixpoint_generated::{Expr, Qualifier},
8};
9pub(crate) static FIXPOINT_QUALIFIERS: LazyLock<[Qualifier; 13]> = LazyLock::new(|| {
10    // UNARY
11    let eqtrue = Qualifier {
12        name: String::from("EqTrue"),
13        args: vec![(Var::Local(LocalVar::from(0u32)), Sort::Bool)],
14        body: Expr::Var(Var::Local(LocalVar::from(0u32))),
15    };
16    let eqfalse = Qualifier {
17        name: String::from("EqFalse"),
18        args: vec![(Var::Local(LocalVar::from(0u32)), Sort::Bool)],
19        body: Expr::Neg(Box::new(Expr::Var(Var::Local(LocalVar::from(0u32))))),
20    };
21    let eqzero = Qualifier {
22        name: String::from("EqZero"),
23        args: vec![(Var::Local(LocalVar::from(0u32)), Sort::Int)],
24        body: Expr::Atom(
25            BinRel::Eq,
26            Box::new([Expr::Var(Var::Local(LocalVar::from(0u32))), Expr::int(0)]),
27        ),
28    };
29    let gtzero = Qualifier {
30        name: String::from("GtZero"),
31        args: vec![(Var::Local(LocalVar::from(0u32)), Sort::Int)],
32        body: Expr::Atom(
33            BinRel::Gt,
34            Box::new([Expr::Var(Var::Local(LocalVar::from(0u32))), Expr::int(0)]),
35        ),
36    };
37    let gezero = Qualifier {
38        name: String::from("GeZero"),
39        args: vec![(Var::Local(LocalVar::from(0u32)), Sort::Int)],
40        body: Expr::Atom(
41            BinRel::Ge,
42            Box::new([Expr::Var(Var::Local(LocalVar::from(0u32))), Expr::int(0)]),
43        ),
44    };
45    let ltzero = Qualifier {
46        name: String::from("LtZero"),
47        args: vec![(Var::Local(LocalVar::from(0u32)), Sort::Int)],
48        body: Expr::Atom(
49            BinRel::Lt,
50            Box::new([Expr::Var(Var::Local(LocalVar::from(0u32))), Expr::int(0)]),
51        ),
52    };
53    let lezero = Qualifier {
54        name: String::from("LeZero"),
55        args: vec![(Var::Local(LocalVar::from(0u32)), Sort::Int)],
56        body: Expr::Atom(
57            BinRel::Le,
58            Box::new([Expr::Var(Var::Local(LocalVar::from(0u32))), Expr::int(0)]),
59        ),
60    };
61
62    // BINARY
63    let eq = Qualifier {
64        name: String::from("Eq"),
65        args: vec![
66            (Var::Local(LocalVar::from(0u32)), Sort::Int),
67            (Var::Local(LocalVar::from(1u32)), Sort::Int),
68        ],
69        body: Expr::Atom(
70            BinRel::Eq,
71            Box::new([
72                Expr::Var(Var::Local(LocalVar::from(0u32))),
73                Expr::Var(Var::Local(LocalVar::from(1u32))),
74            ]),
75        ),
76    };
77    let gt = Qualifier {
78        name: String::from("Gt"),
79        args: vec![
80            (Var::Local(LocalVar::from(0u32)), Sort::Int),
81            (Var::Local(LocalVar::from(1u32)), Sort::Int),
82        ],
83        body: Expr::Atom(
84            BinRel::Gt,
85            Box::new([
86                Expr::Var(Var::Local(LocalVar::from(0u32))),
87                Expr::Var(Var::Local(LocalVar::from(1u32))),
88            ]),
89        ),
90    };
91    let ge: liquid_fixpoint::Qualifier<crate::fixpoint_encoding::fixpoint::FixpointTypes> =
92        Qualifier {
93            name: String::from("Ge"),
94            args: vec![
95                (Var::Local(LocalVar::from(0u32)), Sort::Int),
96                (Var::Local(LocalVar::from(1u32)), Sort::Int),
97            ],
98            body: Expr::Atom(
99                BinRel::Ge,
100                Box::new([
101                    Expr::Var(Var::Local(LocalVar::from(0u32))),
102                    Expr::Var(Var::Local(LocalVar::from(1u32))),
103                ]),
104            ),
105        };
106    let lt = Qualifier {
107        name: String::from("Lt"),
108        args: vec![
109            (Var::Local(LocalVar::from(0u32)), Sort::Int),
110            (Var::Local(LocalVar::from(1u32)), Sort::Int),
111        ],
112        body: Expr::Atom(
113            BinRel::Lt,
114            Box::new([
115                Expr::Var(Var::Local(LocalVar::from(0u32))),
116                Expr::Var(Var::Local(LocalVar::from(1u32))),
117            ]),
118        ),
119    };
120    let le = Qualifier {
121        name: String::from("Le"),
122        args: vec![
123            (Var::Local(LocalVar::from(0u32)), Sort::Int),
124            (Var::Local(LocalVar::from(1u32)), Sort::Int),
125        ],
126        body: Expr::Atom(
127            BinRel::Le,
128            Box::new([
129                Expr::Var(Var::Local(LocalVar::from(0u32))),
130                Expr::Var(Var::Local(LocalVar::from(1u32))),
131            ]),
132        ),
133    };
134    let le1 = Qualifier {
135        name: String::from("Le1"),
136        args: vec![
137            (Var::Local(LocalVar::from(0u32)), Sort::Int),
138            (Var::Local(LocalVar::from(1u32)), Sort::Int),
139        ],
140        body: Expr::Atom(
141            BinRel::Le,
142            Box::new([
143                Expr::Var(Var::Local(LocalVar::from(0u32))),
144                Expr::BinaryOp(
145                    BinOp::Sub,
146                    Box::new([Expr::Var(Var::Local(LocalVar::from(1u32))), Expr::int(1)]),
147                ),
148            ]),
149        ),
150    };
151    [eqtrue, eqfalse, eqzero, gtzero, gezero, ltzero, lezero, eq, gt, ge, lt, le, le1]
152});
flux_infer/fixpoint_qualifiers.rs

flux_infer/
fixpoint_qualifiers.rs
