Source file `formula_main.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
(**************************************************************************)
(*  This file is part of BINSEC.                                          *)
(*                                                                        *)
(*  Copyright (C) 2016-2026                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Formula_options

let transform ~filename =
  let cst = OptimAll.get () || OptimCst.get () in
  let itv = OptimAll.get () || OptimItv.get () in
  let prn = OptimAll.get () || OptimPrn.get () in
  let rbs = OptimAll.get () || OptimRbs.get () in
  let row = OptimAll.get () || OptimRow.get () in
  let ssa = OptimAll.get () || OptimSsa.get () in
  let lst =
    let i = OptimLst.get () in
    if i = 0 then None else Some i
  in
  let smt_script =
    Parse_utils.read_file ~parser:Smtlib.Lang.Parser.script
      ~lexer:Smtlib.Lang.Lexer.token ~filename
  in
  ( Smtlib_to_formula.script smt_script
    (* itv & keep are set to their default values *)
    |> Smtlib.Formula.Transformation.optimize
         ~is_controlled:(fun _ -> false)
         ~keep:Smtlib.Formula.VarSet.empty ?lst ~cst ~itv ~prn ~rbs ~row ~ssa
    |> Smtlib.Formula.To_smtlib.formula ~theory:(Smt_options.Theory.get ()),
    match lst with
    | None -> "smt_simpl_out.smt2"
    | Some n -> Printf.sprintf "smt_simpl_out_%08i.smt2" n )

let maybe_smt_transform_only () =
  if Formula_options.is_enabled () && Kernel_options.ExecFile.is_set () then
    let filename = Kernel_options.ExecFile.get () in
    if File_utils.has_suffix ~suffixes:[ ".smt"; ".smt2" ] filename then (
      transform ~filename |> fun (script, file) ->
      Smtlib.Lang.Printer.pp_tofile file script;
      exit 0)
    else (
      Logger.error "Bad filename extension: %s" filename;
      exit 1)

let _ = Cli.Boot.enlist ~name:"transform" ~f:maybe_smt_transform_only