nicer smt output

src/coq-plugin/test.v

@@ -30,8 +30,10 @@ Qed.
 Definition eq (A:Set) (x y : A) := x=y.
 
 Goal eq nat O O.
+why "z3".
+ae.
 (*
-why "z3".  (* BUG transformation ici ? *)
+why "z3".  (* BUG encoding decorate ici ? *)
 Qed.
 *)
 Admitted.

src/driver/prover.ml

@@ -56,11 +56,18 @@ let print_task drv fmt task =
   let printer = try lookup_printer p with
     Not_found -> errorm "unknown printer %s" p
   in
-  let lookup t = try lookup_transform t with
+  let lookup t = try t, lookup_transform t with
     Not_found -> errorm "unknown transformation %s" t
   in
   let transl = List.map lookup (get_transform drv) in
-  let apply task tr = Register.apply_driver tr drv task in
+  let apply task (s, tr) = 
+    try
+      Register.apply_driver tr drv task 
+    with e ->
+      Format.eprintf "failure in transformation %s: %s@." 
+	s (Printexc.to_string e);
+      raise e
+  in
   let task = List.fold_left apply task transl in
   let printer = printer (driver_query drv task) in
   fprintf fmt "@[%a@]@?" printer task

src/printer/smt.ml

@@ -70,7 +70,7 @@ let rec print_term drv fmt t = match t.t_node with
       | Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
       | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
           | [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
-          | _ -> fprintf fmt "@[(%a %a)@]" 
+          | _ -> fprintf fmt "@[(%a@ %a)@]" 
 	      print_ident ls.ls_name (print_list space (print_term drv)) tl
         end end
   | Tlet (t1, tb) ->
@@ -93,7 +93,7 @@ and print_fmla drv fmt f = match f.f_node with
       | Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
       | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
           | [] -> fprintf fmt "%a" print_ident ls.ls_name
-          | _ -> fprintf fmt "(%a %a)" 
+          | _ -> fprintf fmt "(%a@ %a)" 
 	      print_ident ls.ls_name (print_list space (print_term drv)) tl 
         end end
   | Fquant (q, fq) ->
@@ -109,14 +109,14 @@ and print_fmla drv fmt f = match f.f_node with
       forall fmt vl;
       List.iter forget_var vl
   | Fbinop (Fand, f1, f2) ->
-      fprintf fmt "@[(and@ %a %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
+      fprintf fmt "@[(and@ %a@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
   | Fbinop (For, f1, f2) ->
-      fprintf fmt "@[(or@ %a %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
+      fprintf fmt "@[(or@ %a@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
   | Fbinop (Fimplies, f1, f2) ->
-      fprintf fmt "@[(implies@ %a %a)@]" 
+      fprintf fmt "@[(implies@ %a@ %a)@]" 
         (print_fmla drv) f1 (print_fmla drv) f2
   | Fbinop (Fiff, f1, f2) ->
-      fprintf fmt "@[(iff@ %a %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
+      fprintf fmt "@[(iff@ %a@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
   | Fnot f ->
       fprintf fmt "@[(not@ %a)@]" (print_fmla drv) f
   | Ftrue ->
@@ -192,7 +192,7 @@ let print_decl drv fmt d = match d.d_node with
 let print_decl drv fmt = catch_unsupportedDecl (print_decl drv fmt)
 
 let print_task drv fmt task = 
-  fprintf fmt "(benchmark toto@\n" 
+  fprintf fmt "(benchmark why3@\n" 
     (*print_ident (Task.task_goal task).pr_name*);
   fprintf fmt "  :status unknown@\n";
   Driver.print_full_prelude drv task fmt;

src/util/pp.ml

@@ -73,7 +73,7 @@ let comma fmt () = fprintf fmt ",@ "
 let simple_comma fmt () = fprintf fmt ", "
 let underscore fmt () = fprintf fmt "_"
 let semi fmt () = fprintf fmt ";@ "
-let space fmt () = fprintf fmt " "
+let space fmt () = fprintf fmt "@ "
 let alt fmt () = fprintf fmt "|@ "
 let equal fmt () = fprintf fmt "@ =@ "
 let newline fmt () = fprintf fmt "@\n"

tests/test-bobot.why

 
 (* test file *)
 
+theory Test_inline_trivial
+  type t
+  logic c : t
+  logic eq(x:'a, y:'a) = x=y
+  goal G : eq(c,c)
+end
+
 theory Test_encoding
   use import int.Int
   logic id(x: int) : int = x