Project

General

Profile

Revision 212d6eff

View differences:

src/backends/Horn/horn_backend_printers.ml
430 430
	    (Utils.fprintf_list ~sep:" " pp_type)
431 431
	    (List.map (fun v -> v.var_type) (inout_vars machines m));
432 432

  
433
	  (* Rule for single predicate *)
434
	  fprintf fmt "@[<v 2>(rule (=> @ ";
435
	  ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
436
	  fprintf fmt "@ (%a %a)@]@.))@.@."
437
	    pp_machine_stateless_name m.mname.node_id
438
	    (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
433
          match m.mstep.step_asserts with
434
	  | [] ->
435
	     begin
436

  
437
	       (* Rule for single predicate *)
438
	       fprintf fmt "; Stateless step rule @.";
439
	       fprintf fmt "@[<v 2>(rule (=> @ ";
440
	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
441
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
442
		 pp_machine_stateless_name m.mname.node_id
443
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
444
	     end
445
	  | assertsl ->
446
	     begin
447
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
448
	       
449
	       fprintf fmt "; Stateless step rule with Assertions @.";
450
	       (*Rule for step*)
451
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
452
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
453
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
454
		 pp_machine_stateless_name m.mname.node_id
455
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
456
	  
457
	     end
458
	       
439 459
	end
440 460
      else
441 461
	begin
......
460 480

  
461 481
          match m.mstep.step_asserts with
462 482
	  | [] ->
463
	    begin
464

  
465
	      (* Rule for step*)
466
	      fprintf fmt "@[<v 2>(rule (=> @ ";
467
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
468
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
469
		pp_machine_step_name m.mname.node_id
470
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
471
	    end
483
	     begin
484
	       fprintf fmt "; Step rule @.";
485
	       (* Rule for step*)
486
	       fprintf fmt "@[<v 2>(rule (=> @ ";
487
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
488
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
489
		 pp_machine_step_name m.mname.node_id
490
		 (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
491
	     end
472 492
	  | assertsl -> 
473
	    begin
474
	      let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
475
	      (* print_string pp_val; *)
476
	      fprintf fmt "; with Assertions @.";
477
	      
478
	      (*Rule for step*)
479
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
480
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
481
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
482
		pp_machine_step_name m.mname.node_id
483
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
484
	    end
485
	      
486
	      
493
	     begin
494
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
495
	       (* print_string pp_val; *)
496
	       fprintf fmt "; Step rule with Assertions @.";
497
	       
498
	       (*Rule for step*)
499
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
500
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
501
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
502
		 pp_machine_step_name m.mname.node_id
503
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
504
	     end
505
	       
506
	       
487 507
	end
488 508
    end
489 509

  

Also available in: Unified diff