From 7f3bc56bb6b11d99afaa5824f7a4e1828c2cbfdc Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 8 Jun 2022 13:36:14 +0200
Subject: [PATCH] Remove old standalone version.
---
standalone/config.ml | 216 ----------------------
standalone/config.mli | 28 ---
standalone/dune | 15 --
standalone/engine.ml | 328 ---------------------------------
standalone/engine.mli | 11 --
standalone/main.ml | 206 ---------------------
standalone/marabou.ml | 156 ----------------
standalone/marabou.mli | 7 -
standalone/model.ml | 199 --------------------
standalone/model.mli | 39 ----
standalone/property.ml | 229 -----------------------
standalone/property.mli | 55 ------
standalone/property_lexer.mll | 81 --------
standalone/property_parser.mly | 110 -----------
standalone/property_types.mli | 35 ----
standalone/pyrat.ml | 56 ------
standalone/pyrat.mli | 7 -
standalone/solver.ml | 42 -----
standalone/solver.mli | 63 -------
standalone/utils.ml | 14 --
standalone/utils.mli | 9 -
21 files changed, 1906 deletions(-)
delete mode 100644 standalone/config.ml
delete mode 100644 standalone/config.mli
delete mode 100644 standalone/dune
delete mode 100644 standalone/engine.ml
delete mode 100644 standalone/engine.mli
delete mode 100644 standalone/main.ml
delete mode 100644 standalone/marabou.ml
delete mode 100644 standalone/marabou.mli
delete mode 100644 standalone/model.ml
delete mode 100644 standalone/model.mli
delete mode 100644 standalone/property.ml
delete mode 100644 standalone/property.mli
delete mode 100644 standalone/property_lexer.mll
delete mode 100644 standalone/property_parser.mly
delete mode 100644 standalone/property_types.mli
delete mode 100644 standalone/pyrat.ml
delete mode 100644 standalone/pyrat.mli
delete mode 100644 standalone/solver.ml
delete mode 100644 standalone/solver.mli
delete mode 100644 standalone/utils.ml
delete mode 100644 standalone/utils.mli
diff --git a/standalone/config.ml b/standalone/config.ml
deleted file mode 100644
index 56a8b53..0000000
--- a/standalone/config.ml
+++ /dev/null
@@ -1,216 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-open Base
-
-module Format = Caml.Format
-module Sys = Caml.Sys
-module Filename = Caml.Filename
-
-type version =
- | Unknown
- | Version of string
-[@@deriving show { with_path = false }, yojson]
-
-type t = {
- name: string;
- exe: string;
- version: version;
-}
-[@@deriving yojson, show]
-
-type full_config = t list [@@deriving yojson, show]
-
-let exe_path_of_solver solver =
- let module S = (val solver: Solver.S) in
- (* We want the complete path of [exe] in $PATH: we use `command -v [exe]'
- and retrieve the result, if any. *)
- let tmp = Filename.temp_file S.name "command" in
- let _retcode =
- Sys.command
- (Filename.quote_command
- ~stdout:tmp ~stderr:tmp
- "command" ["-v"; S.exe_name])
- in
- let in_channel = Stdlib.open_in tmp in
- let found, exe =
- try true, Stdlib.input_line in_channel
- with End_of_file -> false, S.exe_name
- in
- Stdlib.close_in in_channel;
- Utils.remove_on_normal_mode tmp;
- if found
- then Ok exe
- else begin
- match Sys.getenv_opt "DIR" with
- | None ->
- Error (Format.asprintf "Cannot find the executable of `%s'." S.name)
- | Some dir ->
- (* The env variable should already provide the path to the executable: we
- first check that the path exists, refers to a directory and it is
- absolute, then we concatenate the [exe] name to it. *)
- if not (Sys.file_exists dir && Sys.is_directory dir)
- then
- Error (Format.sprintf "`%s' not exist or is not a directory." dir)
- else
- if Filename.is_relative dir
- then
- Error
- (Format.sprintf
- "`%s' is a relative path. An absolute path is required for DIR."
- dir)
- else
- let exe =
- if Filename.check_suffix dir Filename.dir_sep
- then dir ^ exe
- else Format.sprintf "%s%s%s" dir Filename.dir_sep exe
- in
- Ok exe
- end
-
-let version_of_solver solver s =
- let module S = (val solver: Solver.S) in
- try
- (* We suppose that the first occurrence that matches [re_version] is indeed
- the version of the concercend [solver]. *)
- ignore (Str.search_forward S.re_version s 0);
- Version (Str.matched_string s)
- with Stdlib.Not_found ->
- Logs.debug (fun m -> m "No recognizable version found.");
- Unknown
-
-let default_config_file =
- let filename = ".caisar.conf" in
- match Sys.getenv_opt "HOME" with
- | None -> filename
- | Some p -> p ^ "/.caisar.conf"
-
-let retrieve_full_config file =
- let open Result in
- match full_config_of_yojson (Yojson.Safe.from_file file) with
- | Error _ | exception _ ->
- []
- | Ok full_config ->
- begin
- Logs.debug (fun m ->
- m "Configuration in file `%s':@ %a"
- file
- pp_full_config full_config);
- full_config
- end
-
-let retrieve ~file solver =
- let open Result in
- let module S = (val solver: Solver.S) in
- Logs.info (fun m ->
- m "Reading configuration file `%s' for solver `%s'." file S.name);
- if not (Sys.file_exists file)
- then Error (Format.sprintf "Configuration file `%s' not exist." file)
- else begin
- (* Read all solver configs present in the given configuration file. *)
- let full_config = retrieve_full_config file in
- (* Search for a [config] with [solver]. *)
- match List.find ~f:(fun cs -> String.equal cs.name S.name) full_config with
- | None ->
- Error
- (Format.asprintf
- "No solver `%s' found in configuration file `%s'."
- S.name file)
- | Some ({ name; version; _ } as config) ->
- begin
- Logs.info (fun m -> m "Found `%s' `%s'." name (show_version version));
- Ok config
- end
- end
-
-(* All solver instances. *)
-let default_solvers =
- [ (module Pyrat: Solver.S); (module Marabou: Solver.S) ]
-
-let detect_default_solvers () =
- try
- let config =
- List.filter_map
- ~f:(fun solver ->
- match exe_path_of_solver solver with
- | Error msg ->
- Logs.info (fun m -> m "%s" msg);
- None
- | Ok exe ->
- (* We detect whether solver is available in $PATH, or in the
- provided path via env variable, by executing `solver
- --version' command. *)
- let module S = (val solver: Solver.S) in
- let tmp = Filename.temp_file S.name "detect" in
- let cmd =
- Filename.quote_command
- ~stdout:tmp ~stderr:tmp
- exe
- [S.exe_default_option]
- in
- Logs.debug (fun m ->
- m "Executing command `%s' to detect `%s'."
- cmd S.name);
- let retcode = Sys.command cmd in
- let cmd_output =
- let in_channel = Stdlib.open_in tmp in
- let buf = Buffer.create 512 in
- try
- while true do
- Stdlib.Buffer.add_channel buf in_channel 512;
- done;
- assert false
- with End_of_file ->
- Stdlib.close_in in_channel;
- Buffer.contents buf
- in
- if retcode <> 0
- then begin
- Logs.info (fun m -> m "No solver `%s' found." S.name);
- None
- end
- else begin
- Utils.remove_on_normal_mode tmp;
- (* If available, we save a [config] for solver. *)
- let version = version_of_solver solver cmd_output in
- let config = { name = S.name; exe; version; } in
- Logs.app (fun m ->
- m "Found solver `%s' `%a' (%s)."
- S.name
- pp_version version
- exe);
- Some config
- end)
- default_solvers
- in
- Ok config
- with _ ->
- Error "Unexpected failure."
-
-let detect ~file =
- let open Result in
- (* Detect default supported solvers in $PATH or $DIR. *)
- detect_default_solvers () >>= fun default_full_config ->
- (* Retrieve the current configuration from [file]. *)
- let current_full_config = retrieve_full_config file in
- (* Create new configuration file. *)
- Logs.debug (fun m -> m "Creating new configuration file `%s'." file);
- let out_channel = Stdlib.open_out file in
- (* Build [full_config] by first appending [default_full_config] to
- [current_full_config], and then deduping the result. *)
- let full_config =
- (* TODO: This comparison is not optimal but sufficient as long as we register
- solver as simply as done in [detect_default_solvers]. *)
- let compare cs1 cs2 = String.compare cs1.name cs2.name in
- List.dedup_and_sort
- ~compare
- (List.append current_full_config default_full_config)
- in
- (* We write all solver configs in the configuration file, as JSON data. *)
- let full_config_json = full_config_to_yojson full_config in
- Yojson.Safe.pretty_to_channel out_channel full_config_json;
- Stdlib.close_out out_channel;
- Ok ()
diff --git a/standalone/config.mli b/standalone/config.mli
deleted file mode 100644
index cfb1caa..0000000
--- a/standalone/config.mli
+++ /dev/null
@@ -1,28 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-type version =
- | Unknown
- | Version of string
-
-type t = private {
- name: string;
- exe: string;
- version: version;
-}
-
-(** Path to default configuration file. *)
-val default_config_file: string
-
-(** The list of supported solvers by default. *)
-val default_solvers: Solver.instance list
-
-(** [detect ~file] searches for solvers in $PATH, or in the path provided in env
- variable $DIR, and save the configurations in [file]. *)
-val detect: file:string -> (unit, string) Result.t
-
-(** @return the [solver] configuration, if any, from the given [file]. *)
-val retrieve: file:string -> Solver.instance -> (t, string) Result.t
diff --git a/standalone/dune b/standalone/dune
deleted file mode 100644
index 7eea482..0000000
--- a/standalone/dune
+++ /dev/null
@@ -1,15 +0,0 @@
-(ocamllex
- (modules property_lexer))
-
-(menhir
- (modules property_parser)
- (flags --table))
-
-(executable
- (name main)
- (public_name caisar-standalone)
- (modules_without_implementation property_types)
- (libraries menhirLib yojson cmdliner logs logs.cli logs.fmt fmt.tty base unix str ppx_deriving_yojson.runtime)
- (preprocess (pps ppx_deriving_yojson ppx_deriving.show ppx_deriving.ord ppx_deriving.eq))
- (package caisar)
-)
diff --git a/standalone/engine.ml b/standalone/engine.ml
deleted file mode 100644
index 129235d..0000000
--- a/standalone/engine.ml
+++ /dev/null
@@ -1,328 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-open Base
-open Property_types
-
-module Format = Caml.Format
-module Sys = Caml.Sys
-module Filename = Caml.Filename
-
-(* Verification task submitted to a solver. *)
-type task = {
- (* Identifier. *)
- id: string;
- (* Original goal name. *)
- goalname: string;
- (* Subgoal identifier.
- Typically a goal is translated to multiple subgoals by a solver.
- [None] means the goal has no subgoals. *)
- subgoal: int option;
- (* The formula to verify. *)
- formula: string;
- (* Verification result.
- [None] means no verification yet. *)
- result: (task_result, string) Result.t option;
-}
-(* Result of a well-terminated task. *)
-and task_result = {
- (* Solver result. *)
- solver_result: Solver.Result.t;
- (* Time elapsed to compute the result. *)
- elapsed_time: float;
-}
-
-let check_availability solver config =
- let module S = (val solver: Solver.S) in
- Logs.debug (fun m -> m "Checking actual availability of `%s'." S.name);
- try
- (* Execute command `solver --version' to check actual availability. *)
- let tmp = Filename.temp_file S.name "avail" in
- let cmd =
- Filename.quote_command
- ~stdout:tmp ~stderr:tmp
- config.Config.exe
- [S.exe_default_option]
- in
- Logs.debug (fun m ->
- m "Executing command `%s' to check `%s' availability." cmd S.name);
- let retcode = Sys.command cmd in
- let in_channel = Stdlib.open_in tmp in
- Stdlib.close_in in_channel;
- if retcode = 0
- then begin
- Utils.remove_on_normal_mode tmp;
- Ok ()
- end
- else
- Error
- (Format.sprintf
- "Command `%s' failed. \
- Try to launch the configuration process again."
- cmd)
- with Stdlib.Not_found | End_of_file | Failure _ | Sys_error _ ->
- Error "Unexpected failure."
-
-let check_compatibility solver model =
- let module S = (val solver: Solver.S) in
- if S.is_model_format_supported model.Model.format
- then Ok ()
- else
- Error
- (Format.asprintf
- "No support yet for `%s' and model format `%s'."
- S.name
- (Model.show_format model.format))
-
-let tasks_of_property solver { axioms; goals } =
- let module S = (val solver: Solver.S) in
- let make_task goalname subgoal formula =
- let id =
- Format.sprintf "%s%s"
- goalname
- (Option.value_map subgoal
- ~default:""
- ~f:(fun idx -> Format.sprintf ".%d" idx))
- in
- { id;
- goalname;
- subgoal;
- formula = Format.asprintf "%a" S.pretty formula;
- result = None; }
- in
- let hypothesis =
- match axioms with
- | [] ->
- (* Axioms are non-empty lists. *)
- assert false
- | [ { formula; _ } ] ->
- formula
- | a :: aa ->
- List.fold_left aa ~init:a.formula ~f:(fun acc a -> And (acc, a.formula))
- in
- let table = Hashtbl.create (module String) in
- List.iter
- goals
- ~f:(fun { name; formula; } ->
- let elts = S.(repr (translate ~hypothesis ~goal:formula)) in
- let tasks =
- if List.length elts = 1
- then [ make_task name None (List.hd_exn elts) ]
- else List.mapi elts ~f:(fun idx elt -> make_task name (Some idx) elt)
- in
- Hashtbl.set table ~key:name ~data:tasks);
- table
-
-let build_command ~raw_options solver config model task =
- let open Result in
- let module S = (val solver: Solver.S) in
- (* Write property to temporary file. *)
- begin
- try
- let tmp = Filename.temp_file "prop" S.name in
- let out_channel = Stdlib.open_out tmp in
- let fmt = Format.formatter_of_out_channel out_channel in
- Format.fprintf fmt "%s@?" task.formula;
- Stdlib.close_out out_channel;
- Ok tmp
- with Sys_error e ->
- Error (Format.sprintf "Unexpected failure:@ %s." e)
- end >>= fun property ->
- (* Build actual command-line. *)
- try
- let log = Filename.temp_file "log" S.name in
- let output = Filename.temp_file "output" S.name in
- let options = S.options ~model:model.Model.filename ~property ~output in
- let command =
- let args = options @ raw_options in
- Filename.quote_command ~stdout:log ~stderr:log config.Config.exe args
- in
- Ok (command, property, log, output)
- with Failure e ->
- Error (Format.sprintf "Unexpected failure:@ %s." e)
-
-let extract_solver_result solver ~log ~output =
- let module S = (val solver: Solver.S) in
- Logs.info (fun m -> m "Extracting result of verification.");
- let output =
- let content file =
- let in_channel = Stdlib.open_in file in
- let buf = Buffer.create 512 in
- try
- while true do
- Stdlib.Buffer.add_channel buf in_channel 512;
- done;
- assert false
- with End_of_file ->
- Stdlib.close_in in_channel;
- buf
- in
- let output = content output in
- if Buffer.length output > 0
- then output
- else content log
- in
- let output = Buffer.contents output in
- let results = [ Solver.Result.Valid; Invalid; Timeout; Unknown ] in
- List.fold
- results
- ~init:Solver.Result.Failure
- ~f:(fun acc result ->
- let regexp = S.re_of_result result in
- let found =
- try Str.search_forward regexp output 0 >= 0
- with Stdlib.Not_found -> false
- in
- if found
- then result
- else acc)
-
-let exec_tasks ~raw_options solver config model tasks_htbl =
- let module S = (val solver: Solver.S) in
- let open Result in
- Logs.app (fun m -> m "Launching verification with `%s'." S.name);
- (* Run one task at a time and modify its status. *)
- Hashtbl.map_inplace
- tasks_htbl
- ~f:(fun tasks ->
- List.map
- tasks
- ~f:(fun task ->
- Logs.app (fun m ->
- m "Verifying goal `%s'%s."
- task.goalname
- (Option.value_map task.subgoal
- ~default:""
- ~f:(fun subgoal ->
- Format.sprintf ", subgoal %d (%s)"
- subgoal task.id)));
- let task_result =
- (* Build the required command-line. *)
- build_command ~raw_options solver config model task
- >>= fun (cmd, prop, log, output) ->
- (* Execute the command. *)
- Logs.info (fun m -> m "Executing command `%s'." cmd);
- try
- let start_time = Unix.gettimeofday () in
- let retcode = Sys.command cmd in
- let elapsed_time = Unix.gettimeofday () -. start_time in
- (* We extract the solver result first before looking at
- [retcode] as the solver may crash after having produced a
- result. *)
- let solver_result =
- extract_solver_result solver ~log ~output
- in
- if retcode <> 0
- && Solver.Result.equal solver_result Solver.Result.Failure
- then
- Error (Format.sprintf "Command `%s' has failed." cmd)
- else begin
- Logs.app
- (fun m -> m "Result of `%s': %a (%.3fs)."
- task.id
- Solver.Result.pretty solver_result
- elapsed_time);
- if Solver.Result.equal solver_result Solver.Result.Failure
- then
- Logs.app (fun m ->
- m "See error messages in `%s' for more information."
- log)
- else begin
- Utils.remove_on_normal_mode log;
- Utils.remove_on_normal_mode prop;
- Utils.remove_on_normal_mode output;
- end;
- Ok { solver_result; elapsed_time; }
- end
- with _ ->
- Error "Unexpected failure."
- in
- { task with result = Some task_result; }));
- tasks_htbl
-
-let consolidate_task_results solver tasks_htbl =
- let module S = (val solver: Solver.S) in
- Hashtbl.map
- tasks_htbl
- ~f:(fun tasks ->
- let consolidated_task_result =
- List.fold
- ~init:None
- ~f:(fun accum { result; _ } ->
- let task_result =
- match result with
- | None ->
- None
- | Some Ok result ->
- Some (result.solver_result, result.elapsed_time)
- | Some Error _ ->
- Some (Failure, 0.)
- in
- match accum, task_result with
- | _, None ->
- accum
- | None, result ->
- result
- | Some (r1, t1), Some (r2, t2) ->
- Some (S.consolidate r1 r2, t1 +. t2))
- tasks
- in
- consolidated_task_result, tasks)
-
-let pretty_summary tasks_htbl =
- let pretty_task_status fmt { id; result; _ } =
- let result = Option.value_exn result in
- let result_string =
- match result with
- | Ok r ->
- Format.asprintf "%a (%.3fs)"
- Solver.Result.pretty r.solver_result
- r.elapsed_time
- | Error msg ->
- msg
- in
- Format.fprintf fmt "@[-- %s: @[<hov>%s@]@]" id result_string
- in
- let pretty_tasks _fmt = function
- | [] | [ _ ] ->
- (* We don't print task details: the consolidated goal result is enough. *)
- ()
- | tasks ->
- Format.printf "@ %a"
- (Format.pp_print_list ~pp_sep:Format.pp_print_space pretty_task_status)
- tasks
- in
- let pretty_goal_tasks fmt (goalname, (consolidated_task_result, tasks)) =
- let consolidated_result, consolidated_time =
- Option.value_exn consolidated_task_result
- in
- Format.fprintf fmt "@[<v 2>- %s: @[%a (%.3fs)@]%a@]"
- goalname
- Solver.Result.pretty consolidated_result
- consolidated_time
- pretty_tasks tasks
- in
- Logs.app (fun m ->
- m "@[<v 2>Summary:@ %a@]"
- (Format.pp_print_list ~pp_sep:Format.pp_print_space pretty_goal_tasks)
- (Hashtbl.to_alist tasks_htbl))
-
-let exec ~raw_options solver config model property =
- let open Result in
- let module S = (val solver: Solver.S) in
- (* Check solver availability. *)
- check_availability solver config >>= fun () ->
- (* Check solver and model compatibility. *)
- check_compatibility solver model >>= fun () ->
- (* Translate property into tasks. *)
- tasks_of_property solver property |>
- (* Run verification process. *)
- exec_tasks ~raw_options solver config model |>
- (* Consolidate task results for every goal. *)
- consolidate_task_results solver |>
- (* Pretty print a summary on results. *)
- pretty_summary |> fun () ->
- Ok ()
diff --git a/standalone/engine.mli b/standalone/engine.mli
deleted file mode 100644
index ad36710..0000000
--- a/standalone/engine.mli
+++ /dev/null
@@ -1,11 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-(** [exec ~raw_options config model property] runs a solver wrt the given
- [config] on [property] for [model] with the provided [raw_options]. *)
-val exec:
- raw_options:string list ->
- Solver.instance -> Config.t -> Model.t -> Property.t -> (unit, string) Result.t
diff --git a/standalone/main.ml b/standalone/main.ml
deleted file mode 100644
index 425cc9d..0000000
--- a/standalone/main.ml
+++ /dev/null
@@ -1,206 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-open Base
-open Cmdliner
-
-module Format = Caml.Format
-
-let caisar = "caisar"
-
-
-(* Logs. *)
-
-let pp_header =
- let x = match Array.length Caml.Sys.argv with
- | 0 -> Caml.(Filename.basename Sys.executable_name)
- | _ -> Caml.(Filename.basename Sys.argv.(0))
- in
- let pp_h ppf style h =
- Fmt.pf ppf "[%s][%a] " x Fmt.(styled style string) h in
- fun ppf (l, h) ->
- (let open Logs_fmt in
- match l with
- | Logs.App ->
- Fmt.pf ppf "[%a] " Fmt.(styled app_style string) x
- | Logs.Error ->
- pp_h ppf err_style (match h with None -> "ERROR" | Some h -> h)
- | Logs.Warning ->
- pp_h ppf warn_style (match h with None -> "WARNING" | Some h -> h)
- | Logs.Info ->
- pp_h ppf info_style (match h with None -> "INFO" | Some h -> h)
- | Logs.Debug ->
- pp_h ppf debug_style (match h with None -> "DEBUG" | Some h -> h))
-
-let setup_logs =
- let setup_log level =
- Fmt_tty.setup_std_outputs ~style_renderer:`Ansi_tty ();
- Logs.set_level level;
- Logs.set_reporter (Logs_fmt.reporter ~pp_header ())
- in
- Term.(const setup_log $ Logs_cli.level ())
-
-
-(* Commands. *)
-
-let config cmd detect file () =
- Logs.debug
- (fun m -> m "Command `%s' with configuration file `%s'." cmd file);
- if detect
- then begin
- match Config.detect ~file with
- | Ok () -> Logs.app (fun m -> m "Configuration saved in `%s'." file)
- | Error e -> Logs.err (fun m -> m "%s" e)
- end
-
-let verify cmd raw_options config_file model property solver () =
- let module S = (val solver: Solver.S) in
- Logs.debug
- (fun m ->
- m "Command `%s' with@ model `%s',@ property `%s' and@ solver `%s' \
- (using configuration file `%s')."
- cmd model property S.name config_file);
- let do_verify () =
- let open Result in
- Model.build ~filename:model >>= fun model ->
- Property.build ~filename:property >>= fun property ->
- Config.retrieve ~file:config_file solver >>= fun config ->
- Engine.exec ~raw_options solver config model property
- in
- match do_verify () with
- | Ok () -> Logs.app (fun m -> m "Done.")
- | Error e -> Logs.err (fun m -> m "%s" e)
-
-
-(* Command line. *)
-
-let config_cmd =
- let cmdname = "config" in
- let dirvar = "DIR" in
- let envs =
- [ Term.env_info
- ~doc:"Absolute path to the directory containing the executable \
- of a solver."
- dirvar ]
- in
- let detect =
- let doc =
- Format.sprintf "Detect solvers in \\$PATH (or \\$%s, if specified)." dirvar
- in
- Arg.(value & flag & info ["d"; "detect"] ~doc)
- in
- let filename =
- let docv_filename = "FILE" in
- let doc =
- Format.sprintf "$(b,FILE) to write the %s configuration to." caisar
- in
- Arg.(value & pos 0 string Config.default_config_file
- & info [] ~docv:docv_filename ~doc)
- in
- let doc = Format.sprintf "%s configuration." caisar in
- let exits = Term.default_exits in
- let man = [
- `S Manpage.s_description;
- `P (Format.sprintf "Handle the configuration of %s." caisar); ]
- in
- Term.(ret
- (const (fun cmdname detect filename _ ->
- if not detect
- then `Help (`Pager, Some "config")
- else
- (* TODO: Do not only check for [detect], and enable it by
- default, as soon as other options are available. *)
- `Ok (config cmdname true filename ()))
- $ const cmdname $ detect $ filename $ setup_logs)),
- Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man
-
-let verify_cmd =
- let cmdname = "verify" in
- let docv_solver = "SOLVER" in
- let solver =
- let solver_names =
- List.map
- Config.default_solvers
- ~f:(fun solver ->
- let module S = (val solver: Solver.S) in
- String.lowercase S.name)
- in
- let doc =
- Format.asprintf
- "The solver to use for verification. \
- $(docv) must be chosen among: %a."
- (Format.pp_print_list
- ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ", ")
- Format.pp_print_string)
- solver_names
- in
- let solvers =
- Arg.enum
- (List.map
- Config.default_solvers
- ~f:(fun solver ->
- let module S = (val solver: Solver.S) in
- String.lowercase S.name, solver))
- in
- Arg.(required
- & pos 2 (some solvers) (Some (module Pyrat: Solver.S))
- & info [] ~docv:docv_solver ~doc)
- in
- let docv_model = "MODEL" in
- let model =
- let doc = "$(b,FILE) of a neural network model." in
- Arg.(required & pos 0 (some file) None & info [] ~docv:docv_model ~doc)
- in
- let docv_property = "PROPERTY" in
- let property =
- let doc = "$(b,FILE) of a property to verify." in
- Arg.(required & pos 1 (some file) None & info [] ~docv:docv_property ~doc)
- in
- let solver_raw_options =
- let doc = "Additional options provided to the solver." in
- Arg.(value & opt (list ~sep:' ' string) []
- & info ["raw"; "raw-options"] ~doc)
- in
- let config_filename =
- let doc = "$(b,FILE) to read the configuration from." in
- Arg.(value & opt file Config.default_config_file
- & info ["c"; "config"] ~doc)
- in
- let doc = "Property verification of neural networks." in
- let exits = Term.default_exits in
- let man = [
- `S Manpage.s_description;
- `P (Format.sprintf
- "Verify $(i,%s) on $(i,%s) by using $(i,%s)."
- docv_property docv_model docv_solver); ]
- in
- Term.(const verify
- $ const cmdname
- $ solver_raw_options
- $ config_filename
- $ model $ property $ solver
- $ setup_logs),
- Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man
-
-let default_cmd =
- let doc = "Framework for neural networks property verification and more." in
- let sdocs = Manpage.s_common_options in
- let man =
- [ `S Manpage.s_common_options;
- `P "These options are common to all commands.";
- `S "MORE HELP";
- `P "Use `$(mname) $(i,COMMAND) --help' for help on a single command.";
- `S Manpage.s_bugs;
- `P "Email bug reports to <...>" ]
- in
- let version = "0.0" in
- Term.(ret (const (fun _ -> `Help (`Pager, None)) $ const ())),
- Term.info caisar ~version ~doc ~sdocs ~exits:Term.default_exits ~man
-
-let () =
- match Term.(eval_choice default_cmd [ verify_cmd; config_cmd ]) with
- | `Error _ -> Caml.exit 1
- | _ -> Caml.exit (if Logs.err_count () > 0 then 1 else 0)
diff --git a/standalone/marabou.ml b/standalone/marabou.ml
deleted file mode 100644
index 205fcc1..0000000
--- a/standalone/marabou.ml
+++ /dev/null
@@ -1,156 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-open Property_types
-
-type t = Property.disjunct Property.nform
-
-let name = "Marabou"
-let exe_name = "Marabou"
-let exe_default_option = "--version"
-let re_version = Str.regexp "[0-9]\\(\\.[0-9]\\)*\\(\\.?[A-Za-z-+]\\)*"
-
-let re_of_result result =
- Str.regexp
- (match result with
- | Solver.Result.Valid ->
- (* The original formula is valid iff [result], computed on the negation
- of the original formula as typical in SAT/SMT, is unsat. *)
- "^\\(u\\|U\\)nsat\\|UNSAT"
- | Invalid ->
- (* The original formula is invalid iff [result], computed on the negation
- of the original formula as typical in SAT/SMT, is sat. *)
- "^\\(s\\|S\\)at\\|SAT"
- | Timeout -> "\\(t\\|T\\)imeout\\|TIMEOUT"
- | Unknown -> "\\(u\\|U\\)nknown\\|UNKNOWN"
- | Failure -> assert false)
-
-let is_model_format_supported = function
- | Model.Nnet _ -> true
- | Onnx -> false
-
-let options ~model ~property ~output =
- let verbosity_level =
- match Logs.level () with
- | None | Some (App | Error | Warning) -> 0
- | Some Info -> 1
- | Some Debug -> 2
- in
- [ "--property"; property;
- "--input"; model;
- "--verbosity"; Int.to_string verbosity_level;
- "--summary-file"; output ]
-
-(* Recall that Marabou is a SAT/SMT-like solver that supports conjunctive
- formulae only, meaning that disjunctive formulae need to be split into
- multiple files. If consolidation of formulae is needed, then the original
- formula, ie before taking the negation as typical in SAT/SMT, was a
- conjunctive formula: we consolidate wrt logical and-operator semantics. *)
-let consolidate r1 r2=
- match r1, r2 with
- | result, Solver.Result.Valid | Solver.Result.Valid, result -> result
- | Invalid, _ | _, Invalid -> Invalid
- | Failure, _ | _, Failure -> Failure
- | Timeout, _ | _, Timeout -> Timeout
- | Unknown, Unknown -> Unknown
-
-(* Transform [k_y_0 + ky_1 + ... + ky_n cop ky_n+1] into [ky_n+1 + k_y_0 +
- ky_1 + ... + ky_n cop 0], taking care of the sign. *)
-let rec constant_rhs formula =
- match formula with
- | Constraint (terms, cop, General (sign_opt, cst_opt, var)) ->
- let terms =
- match sign_opt, cst_opt with
- | _, Some Int i when i = 0 -> terms
- | _, Some Float f when Base.Float.(=) f 0. -> terms
- | (None | Some Plus), None ->
- General (Some Minus, None, var) :: terms
- | (None | Some Plus), Some cst ->
- let negcst =
- match cst with
- | Int i -> Int (~- i)
- | Float f -> Float (~-. f)
- in
- General (Some Plus, Some negcst, var) :: terms
- | Some Minus, _ ->
- General (Some Plus, cst_opt, var) :: terms
- in
- Constraint (terms, cop, Constant (Int 0))
- | Constraint (_, _, Constant _) ->
- formula
- | And (p1, p2) ->
- And (constant_rhs p1, constant_rhs p2)
- | Or (p1, p2) ->
- Or (constant_rhs p1, constant_rhs p2)
-
-(* Marabou does not support greater-than (ie Gt) and less-than (ie Lt)
- comparison operators. Then, transform these into their non-strict versions by
- adding (Gt) or subtracting (Lt) an [epsilon]. For example, [k_y_0 > c] iff
- [k_y_0 >= c + epsilon]. *)
-let rec epsilon_rhs ~epsilon formula =
- match formula with
- | Constraint (terms, Gt, Constant cst) ->
- let fcst =
- (match cst with
- | Int i -> Float.of_int i
- | Float f -> f)
- +. epsilon
- in
- Constraint (terms, Ge, Constant (Float fcst))
- | Constraint (terms, Lt, Constant cst) ->
- let fcst =
- (match cst with
- | Int i -> Float.of_int i
- | Float f -> f)
- -. epsilon
- in
- Constraint (terms, Le, Constant (Float fcst))
- | Constraint _ ->
- formula
- | And (p1, p2) ->
- And (epsilon_rhs ~epsilon p1, epsilon_rhs ~epsilon p2)
- | Or (p1, p2) ->
- Or (epsilon_rhs ~epsilon p1, epsilon_rhs ~epsilon p2)
-
-let translate ~hypothesis ~goal =
- let goal = Property.negation goal in
- let goal = constant_rhs goal in
- let goal = epsilon_rhs ~epsilon:0.00001 goal in
- Property.dnf_of_formula (And (hypothesis, goal))
-
-let repr = Property.get_disjuncts
-
-let pretty fmt t =
- let pp_terms fmt terms =
- match terms with
- | [] ->
- assert false (* Terms are non-empty lists by construction. *)
- | [ t ] ->
- Property.pretty_term fmt t
- | t :: tt ->
- let pp_term = Property.pretty_term ~pp_sign:true in
- Format.fprintf fmt "@[%a %a@]"
- pp_term t
- (Format.pp_print_list
- ~pp_sep:(fun fmt () -> Format.pp_print_char fmt ' ')
- pp_term) tt
- in
- let rec pp_formula fmt formula =
- match formula with
- | Constraint (terms, cop, term) ->
- Format.fprintf fmt "%a %a %a"
- pp_terms terms
- Property.pretty_cop cop
- (Property.pretty_term ~pp_sign:true) term
- | And (p1, p2) ->
- Format.fprintf fmt "%a@\n%a" pp_formula p1 pp_formula p2
- | Or _ ->
- (* Marabou does not handle Or connectives directly. Anyway, it should
- not happen as in [translate] we convert the original goal into a
- dnf-like form where we retrieve only the final conjuncts. *)
- assert false
- in
- Format.fprintf fmt "@[%a@]" pp_formula t
diff --git a/standalone/marabou.mli b/standalone/marabou.mli
deleted file mode 100644
index 8cf7a73..0000000
--- a/standalone/marabou.mli
+++ /dev/null
@@ -1,7 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-include Solver.S
diff --git a/standalone/model.ml b/standalone/model.ml
deleted file mode 100644
index f95352d..0000000
--- a/standalone/model.ml
+++ /dev/null
@@ -1,199 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-open Base
-
-module Format = Caml.Format
-module Sys = Caml.Sys
-module Filename = Caml.Filename
-
-type nnet = {
- n_layers : int;
- n_inputs: int;
- n_outputs: int;
- max_layer_size: int;
- layer_sizes: int list;
- min_input_values: float list;
- max_input_values: float list;
- mean_values: float list * float;
- range_values: float list * float;
-} [@@deriving show { with_path = false }]
-
-type format = Onnx | Nnet of nnet [@@deriving show { with_path = false}]
-
-type t = {
- format: format;
- filename: string;
-}
-
-
-(* Nnet format handling. *)
-
-let nnet_format_error s =
- Error (Format.sprintf "Nnet format error: %s condition not satisfied." s)
-
-let nnet_delimiter = Str.regexp ","
-
-(* Parse a single Nnet format line: split line using [nnet_delimiter] as
- delimiter, and convert each string into a number by means of converter [f]. *)
-let handle_nnet_line ~f line =
- List.filter_map
- ~f:(fun s -> try Some (f (String.strip s)) with _ -> None)
- (Str.split nnet_delimiter line)
-
-(* Skip the header part, ie comments, of the Nnet format. *)
-let handle_nnet_header filename in_channel =
- let exception End_of_header in
- let pos_in = ref (Stdlib.pos_in in_channel) in
- try
- while true do
- let line = Stdlib.input_line in_channel in
- if not (Str.string_match (Str.regexp "//") line 0)
- then raise End_of_header
- else pos_in := Stdlib.pos_in in_channel
- done;
- assert false
- with
- | End_of_header ->
- (* At this point we have read one line past the header part: seek back. *)
- Stdlib.seek_in in_channel !pos_in;
- Ok ()
- | End_of_file ->
- Error (Format.sprintf "Nnet model not found in file `%s'." filename)
-
-(* Retrieve number of layers, inputs, outputs and maximum layer size. *)
-let handle_nnet_basic_info in_channel =
- try
- let line = Stdlib.input_line in_channel in
- match handle_nnet_line ~f:Stdlib.int_of_string line with
- | [ n_layers; n_inputs; n_outputs; max_layer_size ] ->
- Ok (n_layers, n_inputs, n_outputs, max_layer_size)
- | _ ->
- nnet_format_error "second"
- with End_of_file ->
- nnet_format_error "second"
-
-(* Retrieve size of each layer, including inputs and outputs. *)
-let handle_nnet_layer_sizes n_layers in_channel =
- try
- let line = Stdlib.input_line in_channel in
- let layer_sizes = handle_nnet_line ~f:Stdlib.int_of_string line in
- if List.length layer_sizes = (n_layers + 1)
- then Ok layer_sizes
- else nnet_format_error "third"
- with End_of_file ->
- nnet_format_error "third"
-
-(* Skip unused flag. *)
-let handle_nnet_unused_flag in_channel =
- try
- let _ = Stdlib.input_line in_channel in
- Ok ()
- with End_of_file ->
- nnet_format_error "forth"
-
-(* Retrive minimum values of inputs. *)
-let handle_nnet_min_input_values n_inputs in_channel =
- try
- let line = Stdlib.input_line in_channel in
- let min_input_values = handle_nnet_line ~f:Stdlib.float_of_string line in
- if List.length min_input_values = n_inputs
- then Ok min_input_values
- else nnet_format_error "fifth"
- with End_of_file ->
- nnet_format_error "fifth"
-
-(* Retrive maximum values of inputs. *)
-let handle_nnet_max_input_values n_inputs in_channel =
- try
- let line = Stdlib.input_line in_channel in
- let max_input_values = handle_nnet_line ~f:Stdlib.float_of_string line in
- if List.length max_input_values = n_inputs
- then Ok max_input_values
- else nnet_format_error "sixth"
- with End_of_file ->
- nnet_format_error "sixth"
-
-(* Retrieve mean values of inputs and one value for all outputs. *)
-let handle_nnet_mean_values n_inputs in_channel =
- try
- let line = Stdlib.input_line in_channel in
- let mean_values = handle_nnet_line ~f:Stdlib.float_of_string line in
- if List.length mean_values = (n_inputs + 1)
- then
- let mean_input_values, mean_output_value =
- List.split_n mean_values n_inputs
- in
- Ok (mean_input_values, List.hd_exn mean_output_value)
- else
- nnet_format_error "seventh"
- with End_of_file ->
- nnet_format_error "seventh"
-
-(* Retrieve range values of inputs and one value for all outputs. *)
-let handle_nnet_range_values n_inputs in_channel =
- try
- let line = Stdlib.input_line in_channel in
- let range_values = handle_nnet_line ~f:Stdlib.float_of_string line in
- if List.length range_values = (n_inputs + 1)
- then
- let range_input_values, range_output_value =
- List.split_n range_values n_inputs
- in
- Ok (range_input_values, List.hd_exn range_output_value)
- else
- nnet_format_error "eighth"
- with End_of_file ->
- nnet_format_error "eighth"
-
-(* Retrieves [filename] Nnet model metadata wrt Nnet format specification (see
- https://github.com/sisl/NNet for details.) *)
-let retrieve_nnet_metadata filename =
- let open Result in
- let in_channel = Stdlib.open_in filename in
- try
- handle_nnet_header filename in_channel >>= fun () ->
- handle_nnet_basic_info in_channel >>= fun (n_ls, n_is, n_os, max_l_size) ->
- handle_nnet_layer_sizes n_ls in_channel >>= fun layer_sizes ->
- handle_nnet_unused_flag in_channel >>= fun () ->
- handle_nnet_min_input_values n_is in_channel >>= fun min_input_values ->
- handle_nnet_max_input_values n_is in_channel >>= fun max_input_values ->
- handle_nnet_mean_values n_is in_channel >>= fun mean_values ->
- handle_nnet_range_values n_is in_channel >>= fun range_values ->
- Stdlib.close_in in_channel;
- Ok
- { n_layers = n_ls;
- n_inputs = n_is;
- n_outputs = n_os;
- max_layer_size = max_l_size;
- layer_sizes;
- min_input_values;
- max_input_values;
- mean_values;
- range_values; }
- with Failure msg ->
- Error (Format.sprintf "Unexpected error: %s." msg)
-
-(* Generic model. *)
-
-let build ~filename =
- let open Result in
- Logs.info (fun m -> m "Checking format of model file `%s'." filename);
- if Sys.file_exists filename
- then
- begin
- if Filename.check_suffix filename "onnx"
- then Ok Onnx
- else
- retrieve_nnet_metadata filename >>= fun nnet ->
- Ok (Nnet nnet)
- end >>= fun format ->
- Logs.info (fun m ->
- m "Model format recognized as `%s'."
- (match format with Onnx -> "ONNX" | Nnet _ -> "NNet"));
- Ok { format; filename }
- else
- Error (Format.sprintf "No such file `%s'." filename)
diff --git a/standalone/model.mli b/standalone/model.mli
deleted file mode 100644
index fdc61c7..0000000
--- a/standalone/model.mli
+++ /dev/null
@@ -1,39 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-(** Nnet model metadata. *)
-type nnet = private {
- (** Number of layers. *)
- n_layers : int;
- (** Number of inputs. *)
- n_inputs: int;
- (** Number of outputs. *)
- n_outputs: int;
- (** Maximum layer size. *)
- max_layer_size: int;
- (** Size of each layer. *)
- layer_sizes: int list;
- (** Minimum values of inputs. *)
- min_input_values: float list;
- (** Maximum values of inputs. *)
- max_input_values: float list;
- (** Mean values of inputs and one value for all outputs. *)
- mean_values: float list * float;
- (** Range values of inputs and one value for all outputs. *)
- range_values: float list * float;
-} [@@deriving show { with_path = false }]
-
-type format = Onnx | Nnet of nnet [@@deriving show { with_path = false }]
-
-type t = private {
- format: format;
- filename: string;
-}
-
-(** Builds a model out of the given [filename], if possible. The model is
- inferred from the [filename] extension for the Onnx case, while Nnet models
- are parsed for metadata retrieval and conformity checks. *)
-val build: filename:string -> (t, string) Result.t
diff --git a/standalone/property.ml b/standalone/property.ml
deleted file mode 100644
index b440ac4..0000000
--- a/standalone/property.ml
+++ /dev/null
@@ -1,229 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-open Base
-open Property_types
-
-module Format = Caml.Format
-module Sys = Caml.Sys
-module Lexer = Property_lexer
-module Parser = Property_parser
-module MI = Parser.MenhirInterpreter
-module ER = MenhirLib.ErrorReports
-module LU = MenhirLib.LexerUtil
-
-type t = Property_types.t
-type 'a printer = Caml.Format.formatter -> 'a -> unit
-
-(* [show text (pos1, pos2)] displays a range of the input text [text]
- delimited by the positions [pos1] and [pos2]. *)
-let show text positions =
- ER.extract text positions
- |> ER.sanitize
- |> ER.compress
- |> ER.shorten 20 (* max width 43 *)
-
-(* The parser has succeeded and produced a property. *)
-let succeed (property: t) =
- Ok property
-
-(* The parser has encountered a syntax error. *)
-let fail text buffer (_ : t MI.checkpoint) =
- (* Indicate where in the input file the error occurred. *)
- let location = LU.range (ER.last buffer) in
- (* Show the tokens just before and just after the error. *)
- let indication =
- Format.sprintf "Syntax error %s." (ER.show (show text) buffer)
- in
- (* Show these three components. *)
- Error (Format.sprintf "%s%s" location indication)
-
-let build ~filename =
- (* Read the file; allocate and initialize a lexing buffer. *)
- let text, lexbuf = LU.read filename in
- (* Wrap the lexer and lexbuf together into a supplier, that is, a
- function of type [unit -> token * position * position]. *)
- let supplier = MI.lexer_lexbuf_to_supplier Lexer.token lexbuf in
- (* Equip the supplier with a two-place buffer that records the positions
- of the last two tokens. This is useful when a syntax error occurs, as
- these are the token just before and just after the error. *)
- let buffer, supplier = ER.wrap_supplier supplier in
- (* Fetch the parser's initial checkpoint. *)
- let checkpoint = Parser.Incremental.main lexbuf.lex_curr_p in
- (* Run the parser. *)
- try MI.loop_handle succeed (fail text buffer) supplier checkpoint
- with
- | Property_lexer.Error msg ->
- Error (Format.sprintf "%s" msg)
-
-
-(* Printing. *)
-
-let pretty_cop fmt cop =
- let string_of_cop = function
- | Eq -> "="
- | Ge -> ">="
- | Le -> "<="
- | Gt -> ">"
- | Lt -> "<"
- in
- Format.pp_print_string fmt (string_of_cop cop)
-
-let pretty_var fmt = function
- | Input s | Output s -> Format.pp_print_string fmt s
-
-let pretty_cst fmt = function
- | Int i -> Format.fprintf fmt "%d" i
- | Float f -> Format.fprintf fmt "%f" f
-
-let pretty_term ?(pp_sign=false) fmt = function
- | Constant cst ->
- pretty_cst fmt cst
- | General (sign_opt, cst_opt, var) ->
- begin match sign_opt, cst_opt with
- | _, Some Int i when i = 0 -> ()
- | _, Some Float f when Float.(=) f 0. -> ()
- | (None | Some Plus), None ->
- Format.fprintf fmt "@[%s%a@]"
- (if not pp_sign then "" else "+")
- pretty_var var
- | (None | Some Plus), Some cst ->
- let is_cst_negative =
- match cst with
- | Int i -> Int.is_negative i
- | Float f -> Float.is_negative f
- in
- Format.fprintf fmt "@[%s%a%a@]"
- (if not pp_sign || is_cst_negative then "" else "+")
- pretty_cst cst
- pretty_var var
- | Some Minus, None ->
- Format.fprintf fmt "@[-%a@]" pretty_var var
- | Some Minus, Some cst ->
- let negcst, is_negcst_negative =
- match cst with
- | Int i -> Int (~- i), i > 0
- | Float f -> Float (~-. f), Float.(>) f 0.
- in
- Format.fprintf fmt "@[%s%a%a@]"
- (if not pp_sign || is_negcst_negative then "" else "+")
- pretty_cst negcst
- pretty_var var
- end
-
-let pretty_terms pp_term fmt terms =
- match terms with
- | [] ->
- assert false (* Terms are non-empty lists by construction. *)
- | [ t ] ->
- pp_term fmt t
- | t :: tt ->
- Format.fprintf fmt "@[%a %a@]"
- pp_term t
- (Format.pp_print_list
- ~pp_sep:(fun fmt () -> Format.pp_print_char fmt ' ')
- pp_term) tt
-
-let rec pretty_formula fmt formula =
- match formula with
- | Constraint ([], _, _) ->
- (* Non-empty list by construction. *)
- assert false
- | Constraint (terms, cop, term) ->
- Format.fprintf fmt "@[%a %a %a@]"
- (pretty_terms pretty_term) terms
- pretty_cop cop
- (pretty_term ~pp_sign:false) term
- | And (p1, p2) ->
- Format.fprintf fmt "@[%a@ &&@ %a@]" pretty_formula p1 pretty_formula p2
- | Or (p1, p2) ->
- Format.fprintf fmt "@[%a@ ||@ %a@]" pretty_formula p1 pretty_formula p2
-
-let pretty_goal fmt goal =
- Format.fprintf fmt "@[<v 2>goal %s:@ @[<hov>%a@]@]"
- goal.name
- pretty_formula goal.formula
-
-let pretty_axiom fmt axiom =
- Format.fprintf fmt "@[<v 2>axiom %s:@ @[<hov>%a@]@]"
- axiom.name
- pretty_formula axiom.formula
-
-let pretty fmt t =
- Format.fprintf fmt "@[%a@]@\n@[<v>%a@]"
- (Format.pp_print_list pretty_axiom) t.axioms
- (Format.pp_print_list pretty_goal) t.goals
-
-
-(* Transformations and normal forms. *)
-
-let rec negation f =
- let negate_cop = function
- | Eq -> assert false (* We do not support Neq for the moment. *)
- | Ge -> Lt
- | Le -> Gt
- | Lt -> Ge
- | Gt -> Le
- in
- match f with
- | Constraint (tt, cop, t) ->
- let ncop = negate_cop cop in
- Constraint (tt, ncop, t)
- | And (f1, f2) ->
- let nf1 = negation f1 in
- let nf2 = negation f2 in
- Or (nf1, nf2)
- | Or (f1, f2) ->
- let nf1 = negation f1 in
- let nf2 = negation f2 in
- And (nf1, nf2)
-
-type conjunct = formula
-type disjunct = formula
-type 'a nform = formula list
-
-let combine ~f f1 f2 =
- if List.is_empty f1 || List.is_empty f2
- then assert false
- else begin
- let rec loop (l1: formula list) l2 acc =
- match l1 with
- | [] ->
- acc
- | t :: tt ->
- loop tt l2 List.(rev_append (map ~f:(fun x -> f t x) l2) acc)
- in
- List.rev (loop f1 f2 [])
- end
-
-let rec convert_to_nf ~and_ ~or_ formula =
- match formula with
- | Constraint _ ->
- [ formula ]
- | And (p1, p2) ->
- and_ (convert_to_nf ~and_ ~or_ p1) (convert_to_nf ~and_ ~or_ p2)
- | Or (p1, p2) ->
- or_ (convert_to_nf ~and_ ~or_ p1) (convert_to_nf ~and_ ~or_ p2)
-
-let cnf_of_formula (formula: formula) =
- let and_ = function
- | [] -> assert false
- | [ _ ] as f -> f
- | t :: tt -> [ List.fold tt ~init:t ~f:(fun acc f -> And (acc, f)) ]
- in
- convert_to_nf
- ~and_:(fun l1 l2 -> and_ (List.append l1 l2))
- ~or_:(combine ~f:(fun x y -> Or (x, y)))
- formula
-
-let dnf_of_formula (formula: formula) =
- convert_to_nf
- ~and_:(combine ~f:(fun x y -> And (x, y)))
- ~or_:List.append
- formula
-
-let get_conjuncts = Fn.id
-let get_disjuncts = Fn.id
diff --git a/standalone/property.mli b/standalone/property.mli
deleted file mode 100644
index 28c6eb5..0000000
--- a/standalone/property.mli
+++ /dev/null
@@ -1,55 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-open Base
-open Property_types
-
-type t = Property_types.t
-
-(** Builds a property out of the content of the given [filename], if possible. *)
-val build: filename:string -> (t, string) Result.t
-
-
-(** {2 Pretty printing.} *)
-
-type 'a printer = Caml.Format.formatter -> 'a -> unit
-
-(** Comparison operator pretty printer. *)
-val pretty_cop: cop printer
-
-(** Variable pretty printer. *)
-val pretty_var: var printer
-
-(** Constant pretty printer. *)
-val pretty_cst: constant printer
-
-(** Term pretty printer.
- @param pp_sign determines whether the printer should print the sign also
- for monomial terms.
-*)
-val pretty_term: ?pp_sign:bool -> term printer
-
-(** Term list pretty printer given one for a term. *)
-val pretty_terms: term printer -> term list printer
-
-(** [pretty property] pretty prints [property]. *)
-val pretty: Caml.Format.formatter -> t -> unit
-
-
-(** {2 Transformations and normal forms.} *)
-
-val negation: formula -> formula
-
-
-type conjunct
-type disjunct
-type 'a nform
-
-val cnf_of_formula: formula -> conjunct nform
-val dnf_of_formula: formula -> disjunct nform
-
-val get_conjuncts: conjunct nform -> formula list
-val get_disjuncts: disjunct nform -> formula list
diff --git a/standalone/property_lexer.mll b/standalone/property_lexer.mll
deleted file mode 100644
index 8647c71..0000000
--- a/standalone/property_lexer.mll
+++ /dev/null
@@ -1,81 +0,0 @@
-{
- open Property_parser
-
- exception Error of string
-}
-
-(* Identifiers for input and output variable regexps: an input variable starts
- with 'x' followed by a number, while an output variable starts with 'y'
- followed by a number. *)
-
-let input = 'x'['0'-'9']+
-let output = 'y'['0'-'9']+
-
-(* Keywords. *)
-
-let goal = "goal"
-let axiom = "axiom"
-
-(* Macros. *)
-
-let space = [' ' '\t' '\r']
-
-let dec = ['0'-'9']
-let dec_sep = ['0'-'9' '_']
-
-let lalpha = ['a'-'z']
-let ualpha = ['A'-'Z']
-let alpha = (lalpha | ualpha)
-
-let suffix = (alpha | dec_sep)*
-let ident = alpha suffix
-
-
-(* This rule analyzes multiple lines until eof and turns them into a stream of
- tokens. *)
-
-rule token = parse
-| [' ' '\t' '\r']
- { token lexbuf }
-| '\n'
- { MenhirLib.LexerUtil.newline lexbuf; token lexbuf }
-| input as i
- { INPUT i }
-| output as o
- { OUTPUT o }
-| axiom
- { AXIOM }
-| goal
- { GOAL }
-| (ident as gid) space* ":"
- { ID gid }
-| ('-'|'+')?['0'-'9']+'.'['0'-'9']+ as f
- { FLOAT (float_of_string f) }
-| ('-'|'+')?['0'-'9']+ as i
- { INT (int_of_string i) }
-| "+"
- { PLUS }
-| "-"
- { MINUS }
-| "="
- { EQ }
-| ">"
- { GT }
-| "<"
- { LT }
-| ">="
- { GE }
-| "<="
- { LE }
-| "&&"
- { AND }
-| "||"
- { OR }
-| '('
- { LPAREN }
-| ')'
- { RPAREN }
-| eof
- { EOF }
-| _
- { raise (Error (Format.sprintf "Property lexer at offset %d: unexpected character." (Lexing.lexeme_start lexbuf))) }
diff --git a/standalone/property_parser.mly b/standalone/property_parser.mly
deleted file mode 100644
index 2b8b351..0000000
--- a/standalone/property_parser.mly
+++ /dev/null
@@ -1,110 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-(* Tokens. *)
-
-%token <int> INT
-%token <float> FLOAT
-%token <string> INPUT OUTPUT ID
-%token EQ GT LT GE LE
-%token PLUS MINUS
-%token AND OR
-%token LPAREN RPAREN
-%token AXIOM GOAL
-%token EOF
-
-(* Starting rule. *)
-
-%start <Property_types.t> main
-%{ open Property_types %}
-
-%%
-
-(* -------------------------------------------------------------------------- *)
-
-(* We parse a property given by
- a non-empty list of axioms
- a non-empty list of goals
- followed by an end-of-file. *)
-
-let main :=
- axioms = nonempty_list(axiom); goals = nonempty_list(goal); EOF; { { axioms; goals; } }
-
-(* An axiom is a conjunctive formula over constraints. *)
-
-let axiom ==
- AXIOM; name = ID; formula = and_formula(constraint_); { { name; formula; } }
-
-(* A goal has a name and a formula. *)
-
-let goal :=
- GOAL; name = ID; ~ = formula; { { name; formula; } }
-
-(* A formula is given by disjunctions of conjuctions of (delimited) formulae. *)
-
-let formula ==
- or_formula(and_formula(delimited_formula))
-
-(* A disjunctive formula is a left-associative list of formulae, separated by OR
- (i.e. ||) connective. *)
-
-let or_formula(elem) :=
- | elem
- | ors = or_formula(elem); OR; ~ = elem; { Or (ors, elem) }
-
-(* A conjunctive formula is a left-associative list of formulae, separated by
- AND (i.e. &&) connective. *)
-
-let and_formula(elem) :=
- | elem
- | ands = and_formula(elem); AND; ~ = elem; { And (ands, elem) }
-
-(* A delimited formula is
- either a constraint
- or a parenthesized formula. *)
-
-let delimited_formula :=
- | constraint_
- | delimited(LPAREN, formula, RPAREN)
-
-(* A constraint is the application of a comparison operator to a non-empty list
- of terms and a constant or a term. *)
-
-let constraint_ :=
- | terms = nonempty_list(term); ~ = cop; ~ = constant; { Constraint (terms, cop, Constant constant) }
- | terms = nonempty_list(term); ~ = cop; ~ = term; { Constraint (terms, cop, term) }
-
-(* A term is a constant coupled with a variable, possibly with a sign. *)
-
-let term :=
- s = ioption(sign); c = ioption(constant); ~ = variable; { General (s, c, variable) }
-
-(* A constant is an integer or float value. *)
-
-let constant :=
- | ~ = INT; <Int>
- | ~ = FLOAT; <Float>
-
-(* A variable is either input or output. *)
-
-let variable :=
- | ~ = INPUT; <Input>
- | ~ = OUTPUT; <Output>
-
-(* Signs. *)
-
-let sign ==
- | PLUS; { Plus }
- | MINUS; { Minus }
-
-(* Comparison operators. *)
-
-let cop ==
- | EQ; { Eq }
- | GE; { Ge }
- | LE; { Le }
- | GT; { Gt }
- | LT; { Lt }
diff --git a/standalone/property_types.mli b/standalone/property_types.mli
deleted file mode 100644
index 9b9c048..0000000
--- a/standalone/property_types.mli
+++ /dev/null
@@ -1,35 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-type cop = Eq | Ge | Le | Gt | Lt
-type sign = Plus | Minus
-
-type constant =
- | Int of int
- | Float of float
-
-type var =
- | Input of string
- | Output of string
-
-type term =
- | Constant of constant
- | General of sign option * constant option * var
-
-type formula =
- | Constraint of term list * cop * term
- | And of formula * formula
- | Or of formula * formula
-
-type named_formula = {
- name: string;
- formula: formula;
-}
-
-type t = {
- axioms: named_formula list;
- goals: named_formula list;
-}
diff --git a/standalone/pyrat.ml b/standalone/pyrat.ml
deleted file mode 100644
index b2fdd49..0000000
--- a/standalone/pyrat.ml
+++ /dev/null
@@ -1,56 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-open Property_types
-
-type t = Property.conjunct Property.nform
-
-let name = "PyRAT"
-let exe_name = "pyrat.py"
-let exe_default_option = "-v"
-let re_version = Str.regexp "[0-9]\\(\\.[0-9]\\)*\\(\\.?[A-Za-z-+]\\)*"
-
-let re_of_result result =
- Str.regexp
- ("^Result: " ^
- match result with
- | Solver.Result.Valid -> "True"
- | Invalid -> "False"
- | Timeout -> "Timeout"
- | Unknown -> "Unknown"
- | Failure -> assert false)
-
-let is_model_format_supported = function
- | Model.Nnet _ -> true
- | Onnx -> false
-
-let options ~model ~property ~output:_ =
- model :: property ::
- match Logs.level () with
- | None | Some (App | Error | Warning) -> []
- | Some (Info | Debug) -> [ "--verbose" ]
-
-let consolidate _r1 _r2 = assert false
-
-let translate ~hypothesis ~goal =
- Property.cnf_of_formula (And (hypothesis, goal))
-
-let repr = Property.get_conjuncts
-
-let pretty fmt t =
- let rec pp_formula fmt formula =
- match formula with
- | Constraint (terms, cop, term) ->
- Format.fprintf fmt "%a %a %a"
- Property.(pretty_terms (pretty_term ~pp_sign:false)) terms
- Property.pretty_cop cop
- (Property.pretty_term ~pp_sign:false) term
- | And (p1, p2) ->
- Format.fprintf fmt "%a@\n%a" pp_formula p1 pp_formula p2
- | Or (p1, p2) ->
- Format.fprintf fmt "%a or %a" pp_formula p1 pp_formula p2
- in
- Format.fprintf fmt "@[%a@]" pp_formula t
diff --git a/standalone/pyrat.mli b/standalone/pyrat.mli
deleted file mode 100644
index 8cf7a73..0000000
--- a/standalone/pyrat.mli
+++ /dev/null
@@ -1,7 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-include Solver.S
diff --git a/standalone/solver.ml b/standalone/solver.ml
deleted file mode 100644
index 6b7dc37..0000000
--- a/standalone/solver.ml
+++ /dev/null
@@ -1,42 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-open Base
-open Property_types
-
-module Format = Caml.Format
-
-module Result = struct
- type t =
- | Valid
- | Invalid
- | Timeout
- | Unknown
- | Failure
- [@@deriving show { with_path = false }, eq]
-
- let pretty fmt t =
- Format.fprintf fmt "%s" (String.uppercase (show t))
-end
-
-(* Solver instances. *)
-
-module type S = sig
- type t
- val name: string
- val exe_name: string
- val exe_default_option: string
- val re_version: Str.regexp
- val re_of_result: Result.t -> Str.regexp
- val is_model_format_supported: Model.format -> bool
- val options: model:string -> property:string -> output:string -> string list
- val consolidate: Result.t -> Result.t -> Result.t
- val translate: hypothesis:formula -> goal:formula -> t
- val repr: t -> formula list
- val pretty: Caml.Format.formatter -> formula -> unit
-end
-
-type instance = (module S)
diff --git a/standalone/solver.mli b/standalone/solver.mli
deleted file mode 100644
index 6934a70..0000000
--- a/standalone/solver.mli
+++ /dev/null
@@ -1,63 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-open Property_types
-
-(** Solver possible results. *)
-module Result: sig
- type t =
- | Valid
- | Invalid
- | Timeout
- | Unknown
- | Failure
- [@@deriving show, eq]
-
- val pretty: Caml.Format.formatter -> t -> unit
-end
-
-(** Solvers common interface. *)
-module type S = sig
- type t
-
- (** The name of the solver. *)
- val name: string
-
- (** The executable name. *)
- val exe_name: string
-
- (** The default option of the executable. Typically, `--version'. *)
- val exe_default_option: string
-
- (** Regexp for extracting the solver version when running the solver on the
- default option. *)
- val re_version: Str.regexp
-
- (** @return regexp for extracting the given result from the solver output. *)
- val re_of_result: Result.t -> Str.regexp
-
- (** @return whether the given model format is supported by the solver. *)
- val is_model_format_supported: Model.format -> bool
-
- (** @return solver options to execute the solver on the given [model] and
- [property] files, while using [output] as file to store the result. *)
- val options: model:string -> property:string -> output:string -> string list
-
- (** @return consolidated result of the given ones. *)
- val consolidate: Result.t -> Result.t -> Result.t
-
- (** Encodes the given formulae into the solver internal representation. *)
- val translate: hypothesis:formula -> goal:formula -> t
-
- (** Decodes the internal representation into formulae. *)
- val repr: t -> formula list
-
- (** Solver pretty-printing of formulae. *)
- val pretty: Caml.Format.formatter -> formula -> unit
-end
-
-(** An actual instance of solver interface [S]. *)
-type instance = (module S)
diff --git a/standalone/utils.ml b/standalone/utils.ml
deleted file mode 100644
index d39033e..0000000
--- a/standalone/utils.ml
+++ /dev/null
@@ -1,14 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-let remove_on_normal_mode filename =
- let verbose =
- match Logs.level () with
- | Some Info | Some Debug -> true
- | _ -> false
- in
- if not verbose
- then Sys.remove filename
diff --git a/standalone/utils.mli b/standalone/utils.mli
deleted file mode 100644
index c2851d9..0000000
--- a/standalone/utils.mli
+++ /dev/null
@@ -1,9 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Caisar. *)
-(* *)
-(**************************************************************************)
-
-(** [remove_on_normal_mode filename] removes the given file from the file system
- when caisar is run without any active verbosity. *)
-val remove_on_normal_mode: string -> unit
--
GitLab