Project

General

Profile

« Previous | Next » 

Revision 9c4624e4

Added by Teme Kahsai about 9 years ago

do not use lusi for horn, and some logging for horn

View differences:

src/backends/Horn/horn_backend.ml
328 328
       Format.pp_print_newline fmt ();
329 329

  
330 330
       (* Rule for init *)
331
       (* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *)
332
       (*   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs *)
333
       (*   pp_machine_init_name m.mname.node_id *)
334
       (*   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); *)
335

  
336
       (* (\* Rule for step *\) *)
337
       (* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *)
338
       (*   (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs *)
339
       (*   pp_machine_step_name m.mname.node_id *)
340
       (*   (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); *)
341

  
331
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
332
	 (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
333
	 pp_machine_init_name m.mname.node_id
334
	 (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
342 335

  
343 336
      (* Adding assertions *)
344 337
       (match m.mstep.step_asserts with
......
373 366
                           (pp_conj pp_val) assertsl
374 367
                           pp_machine_step_name m.mname.node_id
375 368
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
376
	    (* Format.fprintf fmt " @[<v 2>%a@]@ @.@.@." *)
377
            (*                 (pp_conj pp_val) assertsl; *)
378

  
379 369
          end
380 370
       );
381

  
382

  
383 371
     end
384 372
    end
385 373

  
......
445 433
    (pp_conj pp_var) main_output
446 434
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
447 435
    ;
448
   Format.fprintf fmt "(query ERR)@."
436
   if !Options.horn_query then Format.fprintf fmt "(query ERR)@."
449 437

  
450 438

  
451 439
let cex_computation machines fmt node machine =
......
534 522

  
535 523

  
536 524
let translate fmt basename prog machines =
525
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification");
537 526
  List.iter (print_machine machines fmt) (List.rev machines);
538 527
  main_print machines fmt
539 528

  
540 529

  
541 530
let traces_file fmt basename prog machines =
542
  (* Format.fprintf fmt *)
543
  (*   "; Horn code traceability generated by %s@.; SVN version number %s@.@." *)
544
  (*   (Filename.basename Sys.executable_name) *)
545
  (*   Version.number; *)
546 531

  
547 532
  Format.fprintf fmt
548 533
  "<?xml version=\"1.0\"?>\n<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">\n";
......
622 607
	memories_old
623 608
    in
624 609

  
625
    let pp_prefix_rev fmt prefix =
626
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
627
    in
610
    (* let pp_prefix_rev fmt prefix = *)
611
    (*   Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) *)
612
    (* in *)
628 613

  
629
  let pp_prefix_rev fmt prefix =
614
    let pp_prefix_rev fmt prefix =
630 615
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
631 616
    in
632 617

  
......
663 648
  ) (List.rev machines);
664 649
  Format.fprintf fmt "</Traces>@.";
665 650

  
651
          (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)
652
   (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" *)
653
   (*                                  pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old); *)
654

  
666 655
(* Local Variables: *)
667 656
(* compile-command:"make -C ../.." *)
668 657
(* End: *)

Also available in: Unified diff