blob: 69271636dbd35711a605daec6ea0a77dcdc354ff (
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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
; EXPECT: unsat
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: unsat
; EXPECT: unsat
;;;;; iteEvalThen(true)
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(assert a)
(assert b)
(assert (not (ite a b c)))
(check-sat)
(reset)
;;;;; iteEvalThen(false)
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(assert a)
(assert (not b))
(assert (or (ite a b c) d))
(check-sat)
(reset)
;;;;; iteEvalElse(true)
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(assert (not a))
(assert c)
(assert (not (ite a b c)))
(check-sat)
(reset)
;;;;; iteEvalElse(false)
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(assert (not a))
(assert (not c))
(assert (or (ite a b c) d))
(check-sat)
(reset)
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(assert a)
(assert b)
(assert (=> a c))
(assert (=> b (not c)))
(check-sat)
(reset)
(set-logic ALL)
(assert false)
(check-sat)
(reset)
(set-logic ALL)
(declare-fun x () Bool)
(declare-fun z () Bool)
(assert (= x z))
(assert (not x))
(assert z)
(check-sat)
(reset)
(set-logic ALL)
(declare-fun x3 () Bool)
(declare-fun x9 () Bool)
(assert (not x3))
(assert (or x3 (and x9 x3)))
(check-sat)
|
