blob: bf0692f7dde0243019bd7ba9c902c26ed538fd61 (
plain)
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
|
; REQUIRES: symfpu
; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
; EXIT: 1
(set-logic FP)
(define-fun fp_plus_zero () Float16 (_ +zero 5 11))
(define-fun fp_minus_zero () Float16 (_ -zero 5 11))
(define-fun fp_plus_inf () Float16 (_ +oo 5 11))
(define-fun fp_minus_inf () Float16 (_ -oo 5 11))
(define-fun fp_nan () Float16 (_ NaN 5 11))
(synth-fun f ( (r RoundingMode) (x Float16) (y Float16)) Bool
(
(Start Bool (
(fp.isNaN FpOp)
(fp.isNegative FpOp)
(fp.isPositive FpOp)
(fp.isZero FpOp)
(fp.isSubnormal FpOp)
(fp.isNormal FpOp)
(and Start Start)
(or Start Start)
(not Start)
true
false
))
(FpOp Float16 (
(fp.abs FpOp)
(fp.neg FpOp)
(fp.add r FpOp FpOp)
(fp.sub r FpOp FpOp)
(fp.mul r FpOp FpOp)
(fp.div r FpOp FpOp)
(fp.sqrt r FpOp)
(fp.rem FpOp FpOp)
x
y
fp_plus_zero
fp_minus_zero
fp_plus_inf
fp_minus_inf
fp_nan
(ite Start FpOp FpOp)
))
))
(check-synth)
|
