Revision 79614a15 src/basic_library.ml
src/basic_library.ml | ||
---|---|---|
127 | 127 |
| "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2 |
128 | 128 |
| "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2 |
129 | 129 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
130 |
| _ -> failwith i
|
|
130 |
| _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false)
|
|
131 | 131 |
|
132 | 132 |
let pp_java i pp_val fmt vl = |
133 | 133 |
match i, vl with |
... | ... | |
140 | 140 |
| "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 |
141 | 141 |
| "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 |
142 | 142 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
143 |
| _ -> assert false
|
|
143 |
| _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false)
|
|
144 | 144 |
|
145 | 145 |
let pp_horn i pp_val fmt vl = |
146 | 146 |
match i, vl with |
... | ... | |
158 | 158 |
| "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 |
159 | 159 |
| "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2 |
160 | 160 |
| _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 |
161 |
| _ -> assert false
|
|
161 |
| _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
|
|
162 | 162 |
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
163 | 163 |
|
164 | 164 |
*) |
Also available in: Unified diff