blob: 6c1c633a9c0172614293dfddbdeb8efdd17410d2 (
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
|
; COMMAND-LINE: --incremental --fmf-fun-rlv --no-check-models
(set-logic ALL_SUPPORTED)
(declare-datatypes ((Color 0)) (
((red) (white) (blue))
))
(define-fun ColorToString ((c Color)) String (ite ((_ is red) c) "red" (ite ((_ is white) c) "white" "blue")) )
(declare-fun ColorFromString (String) Color)
(assert (forall ((c Color)) (= c (ColorFromString (ColorToString c)))))
(declare-datatypes ((CP 0)) (
((cp (c1 Color) (c2 Color)))
))
(define-fun-rec CPToString ((cp CP)) String (str.++ "cp(" (ColorToString (c1 cp)) "," (ColorToString (c2 cp)) ")"))
(declare-fun CPFromString (String) CP)
(assert (forall ((cp1 CP)) (= cp1 (CPFromString (CPToString cp1)))))
(declare-fun cpx() CP)
(assert (= cpx (CPFromString "cp(white,red)")))
; EXPECT: sat
(check-sat)
(declare-fun cpy() CP)
(assert (= cpy (CPFromString "cp(red,blue)")))
; EXPECT: sat
(check-sat)
|