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