blob: d243e0ce717fa168e95896606352a59fc5fdb0cb (
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
|
; COMMAND-LINE: --fmf-fun --no-check-models
; EXPECT: sat
(set-logic UFDTSLIA)
(set-option :produce-models true)
(declare-datatypes ((Conditional_Int 0) (Conditional_T_titleType 0) (Conditional_boolean 0) (Conditional_string 0) (Double 0) (List_T_titleType 0) (List_boolean 0) (List_string 0) (T_titleType 0)) (
((Conditional_Int$CAbsent_Int) (Conditional_Int$CPresent_Int (Conditional_Int$CPresent_Int$value Int)))
((Conditional_T_titleType$CAbsent_T_titleType) (Conditional_T_titleType$CPresent_T_titleType (Conditional_T_titleType$CPresent_T_titleType$value T_titleType)))
((Conditional_boolean$CAbsent_boolean) (Conditional_boolean$CPresent_boolean (Conditional_boolean$CPresent_boolean$value Bool)))
((Conditional_string$CAbsent_string) (Conditional_string$CPresent_string (Conditional_string$CPresent_string$value String)))
((Double$CINF) (Double$CNINF) (Double$CNaN) (Double$CValue (Double$CValue$value Int)))
((List_T_titleType$CNil_T_titleType) (List_T_titleType$Cstr_T_titleType (List_T_titleType$Cstr_T_titleType$head T_titleType) (List_T_titleType$Cstr_T_titleType$tail List_T_titleType)))
((List_boolean$CNil_boolean) (List_boolean$Cstr_boolean (List_boolean$Cstr_boolean$head Bool) (List_boolean$Cstr_boolean$tail List_boolean)))
((List_string$CNil_string) (List_string$Cstr_string (List_string$Cstr_string$head String) (List_string$Cstr_string$tail List_string)))
((T_titleType$C_T_titleType (T_titleType$C_T_titleType$base String)))
))
(define-fun f1361$isValid_string((x String)) Bool true)
(define-fun f5131$isValid_T_titleType((x T_titleType)) Bool (and (f1361$isValid_string (T_titleType$C_T_titleType$base x)) (<= (str.len (T_titleType$C_T_titleType$base x)) 80)))
(define-funs-rec
(
(f5242$isValidElementsList_T_titleType((x List_T_titleType)) Bool)
)
(
(=> ((_ is List_T_titleType$Cstr_T_titleType) x) (and (f5131$isValid_T_titleType (List_T_titleType$Cstr_T_titleType$head x)) (f5242$isValidElementsList_T_titleType (List_T_titleType$Cstr_T_titleType$tail x))))
)
)
(define-fun f1348$isValid_boolean((x Bool)) Bool true)
(define-funs-rec
(
(f4169$isValidElementsList_boolean((x List_boolean)) Bool)
)
(
(=> ((_ is List_boolean$Cstr_boolean) x) (and (f1348$isValid_boolean (List_boolean$Cstr_boolean$head x)) (f4169$isValidElementsList_boolean (List_boolean$Cstr_boolean$tail x))))
)
)
(declare-const title T_titleType)
(check-sat)
|
