Passing traceability information from printer to the parser of the output of the solver.

Conflicts:
	src/driver/call_provers.ml
	src/printer/smtv2.ml
	src/session/session_scheduler.ml

src/core/model_parser.ml

@@ -12,7 +12,7 @@
 open Stdlib
 
 
-type model_parser = string -> (string * string) list
+type model_parser =  string -> Printer.printer_mapping -> (string * string) list
 
 type reg_model_parser = Pp.formatted * model_parser
 
@@ -34,4 +34,4 @@ let list_model_parsers () =
 
 let () = register_model_parser
   ~desc:"Model@ parser@ with@ no@ output@ (used@ if@ the@ solver@ does@ not@ support@ models." "no_model"
-  (fun _ -> [])
+  (fun _ _ -> [])

src/core/model_parser.mli

@@ -9,7 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
-type model_parser = string -> (string * string) list
+type model_parser = string ->  Printer.printer_mapping -> (string * string) list
 
 val register_model_parser : desc:Pp.formatted -> string -> model_parser -> unit
 

src/core/printer.ml

@@ -28,11 +28,17 @@ type blacklist = string list
 
 type 'a pp = Pp.formatter -> 'a -> unit
 
+type printer_mapping = {
+  lsymbol_m     : string -> Term.lsymbol;
+  queried_terms : Term.term list;
+}
+
 type printer_args = {
   env        : Env.env;
   prelude    : prelude;
   th_prelude : prelude_map;
   blacklist  : blacklist;
+  mutable printer_mapping : printer_mapping; 
 }
 
 type printer = printer_args -> ?old:in_channel -> task pp
@@ -44,6 +50,11 @@ let printers : reg_printer Hstr.t = Hstr.create 17
 exception KnownPrinter of string
 exception UnknownPrinter of string
 
+let get_default_printer_mapping = {
+  lsymbol_m = (function _ -> raise Not_found);
+  queried_terms = [];
+}
+
 let register_printer ~desc s p =
   if Hstr.mem printers s then raise (KnownPrinter s);
   Hstr.replace printers s (desc, p)

src/core/printer.mli

@@ -24,15 +24,25 @@ type blacklist = string list
 
 type 'a pp = Format.formatter -> 'a -> unit
 
+(* Makes it possible to estabilish traceability from names
+in the output of the printer to elements of AST in its input. *)
+type printer_mapping = {
+  lsymbol_m     : string -> Term.lsymbol;
+  queried_terms : Term.term list;
+}
+
 type printer_args = {
   env        : Env.env;
   prelude    : prelude;
   th_prelude : prelude_map;
   blacklist  : blacklist;
+  mutable printer_mapping : printer_mapping;
 }
 
 type printer = printer_args -> ?old:in_channel -> task pp
 
+val get_default_printer_mapping : printer_mapping
+
 val register_printer : desc:Pp.formatted -> string -> printer -> unit
 
 val lookup_printer : string -> printer

src/driver/call_provers.ml

@@ -185,7 +185,6 @@ let parse_prover_run res_parser time out ret on_timelimit timelimit ~printer_map
     | _ -> ans
   in
   let model = res_parser.prp_model_parser out printer_mapping 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;

src/driver/call_provers.mli

@@ -94,6 +94,7 @@ val call_on_file :
   ?memlimit   : int ->
   ?stepslimit : int ->
   res_parser  : prover_result_parser ->
+  printer_mapping : Printer.printer_mapping ->
   ?cleanup    : bool ->
   ?inplace    : bool ->
   ?redirect   : bool ->
@@ -106,6 +107,7 @@ val call_on_buffer :
   ?stepslimit : int ->
   res_parser  : prover_result_parser ->
   filename    : string ->
+  printer_mapping : Printer.printer_mapping ->
   ?inplace    : bool ->
   Buffer.t -> pre_prover_call
 (** Call a prover on the task printed in the {!type: Buffer.t} given.

src/driver/driver.ml

@@ -240,10 +240,10 @@ let file_of_task drv input_file theory_name task =
 let file_of_theory drv input_file th =
   get_filename drv input_file th.th_name.Ident.id_string "null"
 
-let call_on_buffer ~command ?timelimit ?memlimit ?stepslimit ?inplace ~filename drv buffer =
+let call_on_buffer ~command ?timelimit ?memlimit ?stepslimit ?inplace ~filename ~printer_mapping drv buffer =
   Call_provers.call_on_buffer
     ~command ?timelimit ?memlimit ?stepslimit ~res_parser:drv.drv_res_parser
-    ~filename ?inplace buffer
+    ~filename ~printer_mapping ?inplace buffer
 
 
 (** print'n'prove *)
@@ -283,16 +283,20 @@ let print_task_prepared ?old drv fmt task =
     | None -> raise NoPrinter
     | Some p -> p
   in
-  let printer = lookup_printer p
-    { Printer.env = drv.drv_env;
+  let printer_args = { Printer.env = drv.drv_env;
       prelude     = drv.drv_prelude;
       th_prelude  = drv.drv_thprelude;
-      blacklist   = drv.drv_blacklist } in
-  fprintf fmt "@[%a@]@?" (printer ?old) task
+      blacklist   = drv.drv_blacklist;
+      printer_mapping = get_default_printer_mapping;
+    } in
+  let printer = lookup_printer p printer_args in
+  fprintf fmt "@[%a@]@?" (printer ?old) task;
+  printer_args.printer_mapping
 
 let print_task ?old drv fmt task =
   let task = prepare_task drv task in
-  print_task_prepared ?old drv fmt task
+  print_task_prepared ?old drv fmt task;
+  ()
 
 let print_theory ?old drv fmt th =
   let task = Task.use_export None th in
@@ -303,7 +307,8 @@ let prove_task_prepared
   let buf = Buffer.create 1024 in
   let fmt = formatter_of_buffer buf in
   let old_channel = Opt.map open_in old in
-  print_task_prepared ?old:old_channel drv fmt task; pp_print_flush fmt ();
+  let printer_mapping = print_task_prepared ?old:old_channel drv fmt task in
+  pp_print_flush fmt ();
   Opt.iter close_in old_channel;
   let filename = match old, inplace with
     | Some fn, Some true -> fn
@@ -316,7 +321,7 @@ let prove_task_prepared
         get_filename drv fn "T" pr.pr_name.id_string
   in
   let res =
-    call_on_buffer ~command ?timelimit ?memlimit ?stepslimit ?inplace ~filename drv buf in
+    call_on_buffer ~command ?timelimit ?memlimit ?stepslimit ?inplace ~filename ~printer_mapping drv buf in
   Buffer.reset buf;
   res
 

src/driver/driver.mli

@@ -41,6 +41,7 @@ val call_on_buffer :
   ?stepslimit : int ->
   ?inplace   : bool ->
   filename   : string ->
+  printer_mapping : Printer.printer_mapping ->
   driver -> Buffer.t -> Call_provers.pre_prover_call
 
 
@@ -67,7 +68,7 @@ val prepare_task : driver -> Task.task -> Task.task
 
 val print_task_prepared :
   ?old       : in_channel ->
-  driver -> Format.formatter -> Task.task -> unit
+  driver -> Format.formatter -> Task.task -> Printer.printer_mapping
 
 val prove_task_prepared :
   command    : string ->

src/driver/parse_cvc4_z3_model.ml

@@ -11,6 +11,10 @@
 
 (* Parses the model returned by CVC4 and Z3. *)
 
+open Printer
+open Ident
+open Term
+
 exception EndOfStringExc;;
 
 let add_chr str chr num_opened =
@@ -103,18 +107,48 @@ let rec parse_pairs str pos list =
 let _ = parse_pairs "((s(s)) 1) (x 1))" 0 []
 let _ = parse_pairs "((= (+ (+ (+ (+ (+ (+ (+ x1 x2) x3) x4) x5) x6) x7) x8) 2) false))" 0 []
 
+let rec extract_term_string labels raw_string regexp =
+  match labels with
+  | [] -> raw_string
+  | label::labels_tail ->
+    let l_string = label.lab_string in
+    begin 
+      try 
+	    ignore(Str.search_forward regexp l_string 0);
+	    let end_pos = Str.match_end () in
+	    String.sub l_string end_pos ((String.length l_string) - end_pos)
+      with Not_found -> extract_term_string labels_tail raw_string regexp
+    end
+    
+
+let get_term_string term raw_string  =
+  let labels = Slab.elements term.t_label in
+  let regexp = Str.regexp "model_trace:" in
+  extract_term_string labels raw_string regexp
+  
+
+let rec get_terms_values_strings raw_strings terms collected_strings =
+  match raw_strings with
+  | [] -> collected_strings
+  | (raw_term_string, value)::raw_strings_tail ->
+    let (term_string, terms_tail) = match terms with
+      | [] -> (raw_term_string, [])
+      | term::t_tail -> ((get_term_string term raw_term_string), t_tail) in
+    get_terms_values_strings raw_strings_tail terms_tail (collected_strings @ [(term_string, value)])
+
 (* Parses the model returned by CVC4 or Z3.
 Assumes that the model has the following form "model: (pairs)"
 Returns the list of pairs term - value *)
-let parse model =
+let parse model printer_mapping =
   try
     let r = Str.regexp "unknown\\|sat" in
     let start_m = Str.search_forward r model 0 in
     let start = find_first_open_bracket model start_m in
-    snd(parse_pairs model (start+1) []);
+    let raw_terms_values_strings = snd(parse_pairs model (start+1) []) in
+    get_terms_values_strings raw_terms_values_strings printer_mapping.queried_terms []
   with Not_found -> [] 
 
-let _ = parse "dasfdfd dafsd ( dasfdf ) dfa unknown ((x 1))"
+let _ = parse "dasfdfd dafsd ( dasfdf ) dfa unknown ((x 1))" Printer.get_default_printer_mapping
 
 let () = Model_parser.register_model_parser "cvc4_z3" parse
   ~desc:"Parser@ for@ the@ model@ of@ cv4@ and@ z3."

src/printer/smtv2.ml

@@ -287,7 +287,7 @@ let print_logic_decl info fmt (ls,def) =
     (print_expr info) expr;
   List.iter forget_var vsl
 
-let print_prop_decl info fmt k pr f = match k with
+let print_prop_decl args info fmt k pr f = match k with
   | Paxiom ->
       fprintf fmt "@[<hov 2>;; %s@\n(assert@ %a)@]@\n@\n"
         pr.pr_name.id_string (* FIXME? collisions *)
@@ -314,10 +314,13 @@ let print_prop_decl info fmt k pr f = match k with
           fprintf fmt "@\n;; %s@\n%s" s s;
           ) model_list;
 	  fprintf fmt "))@]@\n";
-	end
+	end;
+      args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
+			       queried_terms = info.info_model; }
+	  
   | Plemma| Pskip -> assert false
 
-let print_decl info fmt d = match d.d_node with
+let print_decl args info fmt d = match d.d_node with
   | Dtype ts ->
       print_type_decl info fmt ts
   | Ddata _ -> unsupportedDecl d
@@ -331,27 +334,18 @@ let print_decl info fmt d = match d.d_node with
       "smtv2 : inductive definition are not supported"
   | Dprop (k,pr,f) ->
       if Mid.mem pr.pr_name info.info_syn then () else
-      print_prop_decl info fmt k pr f
+      print_prop_decl args info fmt k pr f
 
-let print_decls =
+let print_decls args =
   let print_decl (sm, cm, model) fmt d =
     try let info = {info_syn = sm; info_converters = cm; info_model = model} in
-        print_decl info fmt d; (sm, cm, info.info_model), []
+        print_decl args info fmt d; (sm, cm, info.info_model), []
     with Unsupported s -> raise (UnsupportedDecl (d,s)) in
   let print_decl = Printer.sprint_decl print_decl in
   let print_decl task acc = print_decl task.Task.task_decl acc in
   Discriminate.on_syntax_map (fun sm ->
   Printer.on_converter_map (fun cm ->
       Trans.fold print_decl ((sm, cm, []),[])))
-(*
-  let print_decl (sm,model) fmt d =
-    try let info = {info_syn = sm; info_model = model} in
-        print_decl info fmt d; (sm, info.info_model), []
-    with Unsupported s -> raise (UnsupportedDecl (d,s)) in
-  let print_decl = Printer.sprint_decl print_decl in
-  let print_decl task acc = print_decl task.Task.task_decl acc in
-  Discriminate.on_syntax_map (fun sm -> Trans.fold print_decl ((sm,[]),[]))
-  Preliminary support for model from CVC4 *)
 
 let print_task args ?old:_ fmt task =
   (* In trans-based p-printing [forget_all] is a no-no *)
@@ -361,7 +355,7 @@ let print_task args ?old:_ fmt task =
   let rec print = function
     | x :: r -> print r; Pp.string fmt x
     | [] -> () in
-  print (snd (Trans.apply print_decls task));
+  print (snd (Trans.apply (print_decls args) task));
   pp_print_flush fmt ()
 
 let () = register_printer "smtv2" print_task

src/session/session_scheduler.ml

@@ -294,10 +294,10 @@ 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 _ -> [] 
+      Call_provers.prp_model_parser = fun _ _ -> [] 
     } in
   let precall =
-    Call_provers.call_on_file ~command ~res_parser ~redirect:false filename in
+    Call_provers.call_on_file ~command ~res_parser ~redirect:false filename ~printer_mapping:Printer.get_default_printer_mapping in
   callback Running;
   t.running_proofs <- (Check_prover(callback, precall ())) :: t.running_proofs;
   run_timeout_handler t