Parsing a model returned by the solver - added possibility to specify the...

Parsing a model returned by the solver -  added possibility to specify the parser of model in the driver.

Makefile.in

@@ -142,7 +142,7 @@ LIB_UTIL = config bigInt util opt lists strings \
 	   cmdline warning sysutil rc plugin bigInt number pqueue
 
 LIB_CORE = ident ty term pattern decl theory \
-	   task pretty dterm env trans printer
+	   task pretty dterm env trans printer model_parser
 
 LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 	     whyconf autodetection

src/core/model_parser.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  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.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+open Stdlib
+
+
+type model_parser = string -> (string * string) list
+
+type reg_model_parser = Pp.formatted * model_parser
+
+let model_parsers : reg_model_parser Hstr.t = Hstr.create 17
+
+exception KnownModelParser of string
+exception UnknownModelParser of string
+
+let register_model_parser ~desc s p =
+  if Hstr.mem model_parsers s then raise (KnownModelParser s);
+  Hstr.replace model_parsers s (desc, p)
+
+let lookup_model_parser s =
+  try snd (Hstr.find model_parsers s)
+  with Not_found -> raise (UnknownModelParser s)
+
+let list_model_parsers () =
+  Hstr.fold (fun k (desc,_) acc -> (k,desc)::acc) model_parsers []
+
+let () = register_model_parser
+  ~desc:"Model@ parser@ with@ no@ output@ (used@ if@ the@ solver@ does@ not@ support@ models." "no_model"
+  (fun _ -> [])

src/core/model_parser.mli

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  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.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+type model_parser = string -> (string * string) list
+
+val register_model_parser : desc:Pp.formatted -> string -> model_parser -> unit
+
+val lookup_model_parser : string -> model_parser
+
+val list_model_parsers : unit -> (string * Pp.formatted) list

src/driver/call_provers.ml

@@ -97,6 +97,7 @@ type prover_result = {
   pr_output : string;
   pr_time   : float;
   pr_steps  : int;		(* -1 if unknown *)
+  pr_model  : (string * string) list;
 }
 
 type prover_result_parser = {
@@ -104,6 +105,7 @@ type prover_result_parser = {
   prp_timeregexps : timeregexp list;
   prp_stepsregexp : stepsregexp list;
   prp_exitcodes   : (int * prover_answer) list;
+  prp_model_parser : Model_parser.model_parser;
 }
 
 let print_prover_answer fmt = function
@@ -153,6 +155,22 @@ type pre_prover_call = unit -> prover_call
 
 let save f = f ^ ".save"
 
+let rec debug_print_model model =
+  match model with
+  | [] -> ()
+  | (term, value)::t -> begin
+    Debug.dprintf debug "Call_provers: model %s = %s@." term value;
+    debug_print_model t;
+  end
+
+let rec add_model str model =
+  match model with
+  | [] -> str
+  | (term, value)::t -> begin
+    let n_str = str ^ term ^ " = " ^ value ^ "\n" in
+    add_model n_str t
+  end
+
 let parse_prover_run res_parser time out ret on_timelimit timelimit =
   let ans = match ret with
     | Unix.WSTOPPED n ->
@@ -174,11 +192,17 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit =
       && time >= (0.9 *. float timelimit) -> Timeout
     | _ -> ans
   in
+  let model = res_parser.prp_model_parser out in
+  let out_with_model = add_model (out^"\nModel:\n") model
+  in
+  Debug.dprintf debug "Call_provers: model:@.";
+  debug_print_model model;
   { pr_answer = ans;
     pr_status = ret;
-    pr_output = out;
+    pr_output = out_with_model;
     pr_time   = time;
     pr_steps  = steps;
+    pr_model  = model;
   }
 
 let actualcommand command timelimit memlimit stepslimit file =

src/driver/call_provers.mli

@@ -39,6 +39,8 @@ type prover_result = {
   (** The time taken by the prover *)
   pr_steps  : int;
   (** The number of steps taken by the prover (-1 if not available) *)
+  (** The model produced by a the solver (pairs of term value) *)
+  pr_model  : (string * string) list;
 }
 
 val print_prover_answer : Format.formatter -> prover_answer -> unit
@@ -73,6 +75,8 @@ type prover_result_parser = {
   prp_timeregexps : timeregexp list;
   prp_stepsregexp : stepsregexp list;
   prp_exitcodes   : (int * prover_answer) list;
+  (* The parser for a model returned by the solver. *)
+  prp_model_parser : Model_parser.model_parser;
 }
 
 type prover_call

src/driver/driver.ml

@@ -73,6 +73,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
   let exitcodes = ref [] in
   let filename  = ref None in
   let printer   = ref None in
+  let model_parser = ref "no_model" in
   let transform = ref [] in
   let timeregexps = ref [] in
   let stepsregexps = ref [] in
@@ -101,6 +102,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
     | ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
     | Filename s -> set_or_raise loc filename s "filename"
     | Printer s -> set_or_raise loc printer s "printer"
+    | ModelParser s -> model_parser := s
     | Transform s -> add_to_list transform s
     | Plugin files -> load_plugin (Filename.dirname file) files
     | Blacklist sl -> List.iter (fun s -> Queue.add s blacklist) sl
@@ -201,6 +203,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
       prp_timeregexps = List.rev !timeregexps;
       prp_stepsregexp = List.rev !stepsregexps;
       prp_exitcodes   = List.rev !exitcodes;
+      prp_model_parser = Model_parser.lookup_model_parser !model_parser
     };
     drv_tag         = !driver_tag;
   }

src/driver/driver_ast.ml

@@ -53,6 +53,7 @@ type module_rules = {
 type global =
   | Prelude of string
   | Printer of string
+  | ModelParser of string
   | RegexpValid of string
   | RegexpInvalid of string
   | RegexpTimeout of string

src/driver/driver_lexer.mll

 (********************************************************************)
 (*                                                                  *)
 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
-(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
+(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
 (*                                                                  *)
 (*  This software is distributed under the terms of the GNU Lesser  *)
 (*  General Public License version 2.1, with the special exception  *)
@@ -32,6 +32,7 @@
         "prelude", PRELUDE;
         "printer", PRINTER;
 	"steps", STEPS;
+	"model_parser", MODEL_PARSER;
         "valid", VALID;
         "invalid", INVALID;
         "timeout", TIMEOUT;

src/driver/driver_parser.mly

 (********************************************************************)
 (*                                                                  *)
 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
-(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
+(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
 (*                                                                  *)
 (*  This software is distributed under the terms of the GNU Lesser  *)
 (*  General Public License version 2.1, with the special exception  *)
@@ -22,7 +22,7 @@
 %token <string> STRING
 %token <string> OPERATOR
 %token <string> INPUT (* never reaches the parser *)
-%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER
+%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER MODEL_PARSER
 %token VALID INVALID TIMEOUT OUTOFMEMORY UNKNOWN FAIL TIME STEPS
 %token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF
 %token BLACKLIST
@@ -51,6 +51,7 @@ list0_global_theory:
 global:
 | PRELUDE STRING { Prelude $2 }
 | PRINTER STRING { Printer $2 }
+| MODEL_PARSER STRING { ModelParser $2 }
 | VALID STRING { RegexpValid $2 }
 | INVALID STRING { RegexpInvalid $2 }
 | TIMEOUT STRING { RegexpTimeout $2 }
@@ -114,6 +115,7 @@ ident:
 | BLACKLIST    { "blacklist" }
 | PRINTER      { "printer" }
 | STEPS        { "steps" }
+| MODEL_PARSER { "model_parser" }
 | VALID        { "valid" }
 | INVALID      { "invalid" }
 | TIMEOUT      { "timeout" }

src/session/session.ml

@@ -1195,7 +1195,8 @@ let load_result r =
           Call_provers.pr_time = time;
           Call_provers.pr_output = "";
           Call_provers.pr_status = Unix.WEXITED 0;
-	  Call_provers.pr_steps = steps
+	  Call_provers.pr_steps = steps;
+	  Call_provers.pr_model = []
         }
     | "undone" -> Interrupted
     | "unedited" -> Unedited

src/session/session_scheduler.ml

@@ -294,6 +294,7 @@ let schedule_edition t command filename callback =
       Call_provers.prp_regexps = [];
       Call_provers.prp_timeregexps = [];
       Call_provers.prp_stepsregexp = [];
+      Call_provers.prp_model_parser = fun _ -> [] 
     } in
   let precall =
     Call_provers.call_on_file ~command ~res_parser ~redirect:false filename in