Project

General

Profile

« Previous | Next » 

Revision 7a19992d

Added by Pierre-Loïc Garoche almost 11 years ago

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

View differences:

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