alt_ergo_worker.ml 2.6 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12 13 14
open Format
open Worker_proto

15
module Worker = Js_of_ocaml.Worker
16
module SAT = (val (Sat_solver.get_current ()) : Sat_solver_sig.S)
17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
module FE = Frontend.Make (SAT)

let print_status fmt _d status steps =
  match status with
  | FE.Unsat _dep ->
    fprintf fmt "Proved (%Ld steps)" steps
  | FE.Inconsistent -> ()
    (* fprintf fmt "Inconsistent assumption" *)
  | FE.Unknown _t | FE.Sat _t ->
      fprintf fmt "Unknown (%Ld steps)@." steps


let report_status report _d status _steps =
  match status with
  | FE.Unsat _dep -> report Valid
  | FE.Inconsistent -> ()
  | FE.Unknown _t | FE.Sat _t -> report (Unknown "unknown")

let run_alt_ergo_on_task text =
  let lb = Lexing.from_string text in
(* from Alt-Ergo, src/main/frontend.ml *)
38
  let a = Why_parser.file_parser Why_lexer.parse_token lb in
39
  Parsing.clear_parser ();
40 41
  let ltd, _typ_env = Typechecker.file false Typechecker.empty_env a in
  match Typechecker.split_goals ltd with
42 43
  | [d] ->
    let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
44
    SAT.reset_refs ();
45 46 47 48 49 50 51 52
    let stat = ref (Invalid "no answer from Alt-Ergo") in
    let f s = stat := s in
    begin
      try
        let _x = Queue.fold (FE.process_decl (report_status f))
          (SAT.empty (), true, Explanation.empty) d
        in
        !stat
53
      with Fun_sat.StepsLimitReached -> Unknown "steps limit reached"
54 55 56 57 58 59 60 61
    end
  | _ -> Invalid "zero or more than 1 goal to solve"




let () =
  Options.set_steps_bound 100;
62
  Options.set_is_gui false;
63
  Worker.set_onmessage (fun msg ->
64
			match unmarshal msg with
65 66 67
			  Goal (id, text, steps) ->
			  let old_steps = Options.steps_bound () in
			  if steps > 0 then Options.set_steps_bound steps;
68
			  let result = run_alt_ergo_on_task text in
69
			  Options.set_steps_bound old_steps;
70 71
			  Worker.post_message (marshal (id,result))
			| OptionSteps i -> Options.set_steps_bound i)
72 73 74 75 76 77

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. trywhy3"
End:
*)