code wiki / _hdl_build / _cegis_clamp.nx
_cegis_clamp.nx source
↩ module page · 46 lines · 1583 B
1// CONVERGED BY THE NISHI TEAM CEGIS LOOP (_cegis_authored): counterexample-guided,
2// zero disagreements with the oracle on the full probe domain. NOT retrieved.
3import "nx_syscalls.nx"
4func _c_le(a: i64, b: i64) -> i64 { if a <= b { return 1 } return 0 }
5func _c_and(a: i64, b: i64) -> i64 { return a & b }
6func _c_shr(a: i64, b: i64) -> i64 { return a >> (b & 63) }
7func _c_min(a: i64, b: i64) -> i64 { if a < b { return a } return b }
8func _c_max(a: i64, b: i64) -> i64 { if a > b { return a } return b }
9func _c_add(a: i64, b: i64) -> i64 { return a + b }
10func _c_sub(a: i64, b: i64) -> i64 { return a - b }
11func _c_mul(a: i64, b: i64) -> i64 { return a * b }
12func _c_shl(a: i64, b: i64) -> i64 { return a << (b & 63) }
13func _c_div(a: i64, b: i64) -> i64 { if b == 0 { return 0 } return a / b }
14func _c_mod(a: i64, b: i64) -> i64 { if b == 0 { return 0 } return a % b }
15func _c_abs(a: i64) -> i64 { if a < 0 { return 0 - a } return a }
16func resynth(a: i64, b: i64) -> i64 { return _c_min(b, _c_max(a, 0)) }
17func main() -> i64 {
18 let ka: *i64 = sys_mmap(256) as *i64
19 let kb: *i64 = sys_mmap(256) as *i64
20 let kx: *i64 = sys_mmap(256) as *i64
21 ka[0] = 0
22 kb[0] = 0
23 kx[0] = 0
24 ka[1] = 1
25 kb[1] = 1
26 kx[1] = 1
27 ka[2] = 16
28 kb[2] = 8
29 kx[2] = 8
30 ka[3] = 100
31 kb[3] = 50
32 kx[3] = 50
33 ka[4] = 0 - 60
34 kb[4] = 1
35 kx[4] = 0
36 ka[5] = 0 - 60
37 kb[5] = 0 - 59
38 kx[5] = 0 - 59
39 var i: i64 = 0
40 while i < 6 {
41 if resynth(ka[i], kb[i]) != kx[i] { sys_exit(1) }
42 i = i + 1
43 }
44 sys_exit(0)
45 return 0
46}