Project

General

Profile

« Previous | Next » 

Revision 4e809854

Added by Pierre-Loïc Garoche about 5 years ago

Cosmetic changes

View differences:

src/backends/Horn/horn_backend_printers.ml
245 245
    in
246 246
    pp_conj pp_branch fmt hl;
247 247
    reset_instances 
248

  
248
  | MComment _ -> []
249
     
249 250
and pp_machine_instrs machines reset_instances m fmt instrs = 
250 251
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
251 252
  match instrs with
......
296 297
  fprintf fmt "@]@ )"
297 298

  
298 299

  
299

  
300 300
(**************************************************************)
301 301

  
302 302
let is_stateless m = m.minstances = [] && m.mmemory = []
......
375 375
	    end
376 376
	  | assertsl -> 
377 377
	    begin
378
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
378
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in 
379 379
	      (* print_string pp_val; *)
380 380
	      fprintf fmt "; with Assertions @.";
381 381
	      
382 382
	      (*Rule for step*)
383 383
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
384 384
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
385
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
385
	      fprintf fmt "@. %a)" (pp_conj pp_val) assertsl;
386
	      fprintf fmt "(%a @[<v 0>%a)@]@]@.))@.@."
386 387
		pp_machine_step_name m.mname.node_id
387 388
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
388 389
	    end

Also available in: Unified diff