blob: cca2487d4ea2e9eaed82570cd7fff5126b854a9d (
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
|
; 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
; 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)) Float16
(
(Start Float16 (
(fp.abs Start)
(fp.neg Start)
(fp.add r Start Start)
(fp.sub r Start Start)
(fp.mul r Start Start)
(fp.div r Start Start)
(fp.sqrt r Start)
(fp.rem Start Start)
x
y
fp_plus_zero
fp_minus_zero
fp_plus_inf
fp_minus_inf
fp_nan
))
))
(check-synth)
|
