<commit_before>(********************************************************************)
(*                                                                  *)
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
(*                                                                  *)
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
(*  under the terms of the GNU Lesser General Public License        *)
(*  version 2.1.                                                    *)
(*                                                                  *)
(********************************************************************)

(* The compilation presented here was first defined in Garoche, Gurfinkel,
   Kahsai, HCSV'14.

   This is a modified version that handle reset
*)

open Format
open LustreSpec
open Corelang
open Machine_code

open Horn_backend_common
open Horn_backend_printers
open Horn_backend_collecting_sem

(*
TODO:
- gerer les traces. Ca merde pour l'instant dans le calcul des memoires sur les arrows

- gerer le reset --- DONE
- reconstruire les rechable states DONE
- reintroduire le cex/traces ... DONE
- traiter les types enum et les branchements sur ces types enum (en particulier les traitements des resets qui ont lieu dans certaines branches et pas dans d'autres )
*)

let main_print machines fmt =
if !Options.main_node <> "" then
  begin
    let node = !Options.main_node in
    let machine = get_machine machines node in
    collecting_semantics machines fmt node machine;
    check_prop machines fmt node machine;
    if !Options.horn_cex then(
      cex_computation machines fmt node machine;
      get_cex machines fmt node machine)
end

let print_type_definitions fmt =
  let cpt_type = ref 0 in
  Hashtbl.iter (fun typ decl ->
    match typ with
    | Tydec_const var ->
      (match decl.top_decl_desc with
      | TypeDef tdef -> (
	match tdef.tydef_desc with
	| Tydec_enum tl ->
	  incr cpt_type;
	  fprintf fmt "(declare-datatypes () ((%s %a));@.@."
	    var<commit_msg>solved bug: missing parenthesis in enum typedef<commit_after>(********************************************************************)
(*                                                                  *)
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
(*                                                                  *)
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
(*  under the terms of the GNU Lesser General Public License        *)
(*  version 2.1.                                                    *)
(*                                                                  *)
(********************************************************************)

(* The compilation presented here was first defined in Garoche, Gurfinkel,
   Kahsai, HCSV'14.

   This is a modified version that handle reset
*)

open Format
open LustreSpec
open Corelang
open Machine_code

open Horn_backend_common
open Horn_backend_printers
open Horn_backend_collecting_sem

(*
TODO:
- gerer les traces. Ca merde pour l'instant dans le calcul des memoires sur les arrows

- gerer le reset --- DONE
- reconstruire les rechable states DONE
- reintroduire le cex/traces ... DONE
- traiter les types enum et les branchements sur ces types enum (en particulier les traitements des resets qui ont lieu dans certaines branches et pas dans d'autres )
*)

let main_print machines fmt =
if !Options.main_node <> "" then
  begin
    let node = !Options.main_node in
    let machine = get_machine machines node in
    collecting_semantics machines fmt node machine;
    check_prop machines fmt node machine;
    if !Options.horn_cex then(
      cex_computation machines fmt node machine;
      get_cex machines fmt node machine)
end

let print_type_definitions fmt =
  let cpt_type = ref 0 in
  Hashtbl.iter (fun typ decl ->
    match typ with
    | Tydec_const var ->
      (match decl.top_decl_desc with
      | TypeDef tdef -> (
	match tdef.tydef_desc with
	| Tydec_enum tl ->
	  incr cpt_type;
	  fprintf fmt "(declare-datatypes () ((%s %a)));@.@."
	    var
{'fraction_non_alphanumeric': 0.12761949611490464, 'fraction_numerical': 0.004238285848834471, 'mean_word_length': 2.1963882618510158, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 13, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 18, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '908472', 'n_tokens_mistral': 1130, 'n_tokens_neox': 1075, 'n_words': 407}