Revision 7a19992d
Added by Pierre-Loïc Garoche almost 11 years ago
src/basic_library.ml | ||
---|---|---|
169 | 169 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
170 | 170 |
| _ -> assert false |
171 | 171 |
|
172 |
let pp_horn i pp_val fmt vl = |
|
173 |
match i, vl with |
|
174 |
| "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 |
|
175 |
| "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v |
|
176 |
| "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v |
|
177 |
| "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 |
|
178 |
| "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 |
|
179 |
| "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 |
|
180 |
| _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 |
|
181 |
| _ -> assert false |
|
182 |
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
|
183 |
| "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2 |
|
184 |
| "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 |
|
185 |
*) |
|
172 | 186 |
|
173 | 187 |
(* Local Variables: *) |
174 | 188 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff
In the middle of the coding process. Just pushing thinks
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@143 041b043f-8d7c-46b2-b46e-ef0dd855326e