blob: 3172fd6951fe382ca073c36a0168a7d6ff2db1e4 (
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
|
; COMMAND-LINE: --fmf-fun --no-check-models --lang=smt2.5
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
(define-fun BoolToString ((b Bool)) String (ite b "true" "false") )
(declare-datatypes () (
(Color (red) (white) (blue))
) )
(define-fun ColorToString ((c Color)) String (ite (is-red c) "red" (ite (is-white c) "white" "blue")) )
(declare-datatypes () (
(CP (cp (b Bool) (c Color)))
) )
(define-fun-rec CPToString ((cp CP)) String (str.++ "cp(" (BoolToString (b cp)) "," (ColorToString (c cp)) ")"))
(declare-fun CPFromString (String) CP)
(assert (forall ((cp1 CP)) (= cp1 (CPFromString (CPToString cp1)))))
(declare-fun cpx() CP)
(assert (= cpx (CPFromString "cp(true,white)")))
(check-sat)
|
