Project

General

Profile

Revision 3cdd2147 src/backends/Horn/horn_backend.ml

View differences:

src/backends/Horn/horn_backend.ml
302 302
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
303 303

  
304 304
       (* Rule for single predicate *)
305
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
306
	 (pp_conj (pp_instr
307
		     true (* In this case, the boolean init can be set to true or false.
305

  
306
       (match m.mstep.step_asserts with
307
        | [] ->
308
           begin
309
             (*No assertions *)
310
             Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
311
	                    (pp_conj (pp_instr
312
		                        true (* In this case, the boolean init can be set to true or false.
308 313
			     The node is stateless. *)
309
		     m.mname.node_id)
310
	 )
311
	 m.mstep.step_instrs
312
	 pp_machine_stateless_name m.mname.node_id
313
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
314
		                        m.mname.node_id)
315
	                    )
316
	                    m.mstep.step_instrs
317
	                  pp_machine_stateless_name m.mname.node_id
318
	                  (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
319
           end
320
       | assertsl ->
321
          begin
322
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
323
            let instrs_concat = m.mstep.step_instrs in
324
            Format.fprintf fmt "; with Assertions @.";
325
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
326
                           (pp_conj (pp_instr true m.mname.node_id)) instrs_concat
327
                           (pp_conj pp_val) assertsl
328
	                   pp_machine_stateless_name m.mname.node_id
329
	                   (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
330
          end
331
       )
314 332
     end
315 333
   else
316 334
     begin

Also available in: Unified diff