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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
open Options
module E = Expr
module Ex = Explanation
module EX2 = struct
type t = E.t * E.t
let compare (s1, s2) (t1, t2) =
let c = E.compare s1 t1 in
if c <> 0 then c else E.compare s2 t2
end
module ME2 = Map.Make(EX2)
module SE2 = Set.Make(EX2)
module ME = Expr.Map
module TB =
Map.Make
(struct
type t = E.t * bool
let compare (a1, b1) (a2, b2) =
let c = E.compare a1 a2 in
if c <> 0 then c else Stdlib.compare b1 b2
end)
type t =
{ pending_deds : Ex.t ME2.t;
guarded_pos_deds : SE2.t ME.t;
guarded_neg_deds : SE2.t ME.t;
assumed_pos_preds : Ex.t ME.t;
assumed_neg_preds : Ex.t ME.t;
}
let empty _ =
{ pending_deds = ME2.empty;
guarded_pos_deds = ME.empty;
guarded_neg_deds = ME.empty;
assumed_pos_preds = ME.empty;
assumed_neg_preds = ME.empty;
}
let is_ite =
let ite = Symbols.Op Symbols.Tite in
fun t ->
match E.term_view t with
| E.Not_a_term _ -> assert false
| E.Term { E.f ; xs = [p;t1;t2]; _ } when Symbols.equal f ite ->
Some (p, t1, t2)
| _ ->
None
let add_to_guarded p s t mp =
let st = try ME.find p mp with Not_found -> SE2.empty in
ME.add p (SE2.add (s, t) st) mp
let add_aux env t =
if Options.get_disable_ites () then env
else
match is_ite t with
| None -> env
| Some (p, t1, t2) ->
if get_debug_ite () then
Printer.print_dbg
~module_name:"Ite_rel" ~function_name:"add_aux"
"(if %a then %a else %a)"
E.print p E.print t1 E.print t2;
try
let ex = ME.find p env.assumed_pos_preds in
{env with pending_deds = ME2.add (t, t1) ex env.pending_deds}
with Not_found ->
try
let ex = ME.find p env.assumed_neg_preds in
{env with pending_deds = ME2.add (t, t2) ex env.pending_deds}
with Not_found ->
let guarded_pos_deds = add_to_guarded p t t1 env.guarded_pos_deds in
let guarded_neg_deds = add_to_guarded p t t2 env.guarded_neg_deds in
{env with guarded_pos_deds; guarded_neg_deds}
let add env _ _ t =
add_aux env t, []
let env la =
List.fold_left
(fun acc (_ra, root, expl, _orig) ->
match root with
| None -> acc
| Some a ->
match E.lit_view a with
| E.Pred (t, is_neg)
when not (ME.mem t env.assumed_pos_preds) &&
not (ME.mem t env.assumed_neg_preds) ->
if get_debug_ite () then
Printer.print_dbg
~module_name:"Ite_rel" ~function_name:"assume"
"%a" E.print a;
TB.add (t, is_neg) expl acc
| _ -> acc
)TB.empty la
let env =
let l =
ME2.fold
(fun (s, t) ex acc ->
let a = E.mk_eq ~iff:false s t
[@ocaml.ppwarning "TODO: build IFF instead ?"]
in
if get_debug_ite () then
Printer.print_dbg
~module_name:"Ite_rel" ~function_name:"assume"
"deduce that %a with expl %a"
E.print a Ex.print ex;
(Sig_rel.LTerm a, ex, Th_util.Other) :: acc)
env.pending_deds []
in
{env with pending_deds = ME2.empty}, l
let assume env _ la =
if Options.get_disable_ites () then env, { Sig_rel.assume = []; remove = [] }
else
let env =
TB.fold
(fun (t, is_neg) ex env ->
if is_neg then
let assumed_neg_preds = ME.add t ex env.assumed_neg_preds in
let deds =
try ME.find t env.guarded_neg_deds
with Not_found -> SE2.empty
in
let pending_deds =
SE2.fold (fun e acc -> ME2.add e ex acc) deds env.pending_deds
in
{env with assumed_neg_preds; pending_deds}
else
let assumed_pos_preds = ME.add t ex env.assumed_pos_preds in
let deds =
try ME.find t env.guarded_pos_deds
with Not_found -> SE2.empty
in
let pending_deds =
SE2.fold (fun e acc -> ME2.add e ex acc) deds env.pending_deds
in
{env with assumed_pos_preds; pending_deds}
)(extract_preds env la) env
in
let env, deds = extract_pending_deductions env in
env, { Sig_rel.assume = deds; remove = [] }
let assume env uf la =
if Options.get_timers() then
try
Timers.exec_timer_start Timers.M_Arrays Timers.F_assume;
let res =assume env uf la in
Timers.exec_timer_pause Timers.M_Arrays Timers.F_assume;
res
with e ->
Timers.exec_timer_pause Timers.M_Arrays Timers.F_assume;
raise e
else assume env uf la
let case_split _ _ ~for_model:_ = []
let query _ _ _ = None
let print_model _ _ _ = ()
let new_terms _ = E.Set.empty
let instantiate ~do_syntactic_matching:_ _ env _ _ = env, []
let assume_th_elt t _ _ = t