improved support of provers

drivers/cvc3.drv

 
 (* Why driver for SMT syntax *)
 
-prelude "(* this is a prelude for smtlib*)"
+prelude ";;; this is a prelude for CVC3 "
 
 printer "smtv1"
 filename "%f-%t-%g.smt"
@@ -32,7 +32,7 @@ end
 
 theory int.Int
 
-  prelude "(* this is a prelude for Alt-Ergo arithmetic *)"
+  prelude ";;; this is a prelude for CVC3, Arithmetic"
 
   syntax logic zero "0"
 

drivers/z3.drv

@@ -7,7 +7,7 @@ printer "smtv1"
 filename "%f-%t-%g.smt"
 
 valid "unsat"
-unknown "unknown\\|sat|Fail" "Unknown"
+unknown "unknown\\|sat\\|Fail" "Unknown"
 
 (* À discuter *)
 transformations

src/manager/db.ml

@@ -1260,24 +1260,16 @@ let string_from_result = function
 
 exception AlreadyAttempted
 
-let try_prover ~timelimit ?memlimit ~prover:_prover ~command ~driver 
+let try_prover ~debug ~timelimit ~memlimit ~prover:_prover ~command ~driver 
     (g : goal) : unit -> unit =
   (* TODO: check if attempt already present *)
   (* TODO: add attempt as "Running" *)
-  begin
-    match memlimit with None -> ()
-      | Some _ -> Format.eprintf "Db.try_prover warning: memlimit is ignored@."
-  end;
-  Format.eprintf "Task : %a@." Why.Pretty.print_task g.task;
+  if debug then Format.eprintf "Task : %a@." Why.Pretty.print_task g.task;
   let task = match Why.Driver.apply_transforms driver g.task with
     | [t] -> t
     | _ -> assert false
   in
-  Format.eprintf "Task for prover: %a@." (Why.Driver.print_task driver) task;
-(*
-  let callback = Why.Driver.call_prover_ext ~debug:true ~timeout:timelimit d g.task
-  in 
-*)
+  if debug then Format.eprintf "Task for prover: %a@." (Why.Driver.print_task driver) task;
   let callback = 
     let dest =
       Why.Driver.file_of_task driver "" "" task
@@ -1286,12 +1278,12 @@ let try_prover ~timelimit ?memlimit ~prover:_prover ~command ~driver
       Format.fprintf fmt "@[%a@]@?" (Why.Driver.print_task driver) task
     in
     let regexps = Why.Driver.get_regexps driver in
-    Why.Call_provers.call_on_formatter ~debug:true ~suffix:dest
-      ~command ~timelimit ~memlimit:0 ~regexps print_task
+    Why.Call_provers.call_on_formatter ~debug ~suffix:dest
+      ~command ~timelimit ~memlimit ~regexps print_task
   in
   fun () ->
     let r = callback () in
-    Format.eprintf "prover result: %a@." Why.Call_provers.print_prover_result r;
+    if debug then Format.eprintf "prover result: %a@." Why.Call_provers.print_prover_result r;
     (* TODO : update attempt depending on r = Valid *)
     ()
       

src/manager/db.mli

@@ -159,8 +159,8 @@ val root_goals : unit -> goal list
 exception AlreadyAttempted
 
 val try_prover : 
-  timelimit:int -> ?memlimit:int -> prover:prover -> command:string -> 
-  driver:Why.Driver.driver -> goal -> (unit -> unit)
+  debug:bool -> timelimit:int -> memlimit:int -> prover:prover -> 
+  command:string -> driver:Why.Driver.driver -> goal -> (unit -> unit)
   (** attempts to prove goal with the given prover.  This function
       prepares the goal for that prover, adds it as an new
       external_proof attempt, setting its current status to Running,

src/manager/test.ml

@@ -33,7 +33,7 @@ let autodetection () =
   let config = {
     conf_file = "why.conf";
     loadpath  = ["theories"];
-    timelimit = Some 10;
+    timelimit = Some 2;
     memlimit  = None;
     provers   = provers }
   in
@@ -88,6 +88,10 @@ let provers_data =
   l
    
 
+let timelimit = 
+match config.timelimit with
+| None -> 2
+| Some n -> n
 
 let () = 
   printf "previously known goals:@\n";
@@ -203,7 +207,10 @@ let goal_menu g =
          let i = int_of_string s in
          if i=0 then raise Exit; 
          let p = List.assoc i menu in
-         let call = Db.try_prover ~timelimit:config.timelimit ~prover:p.prover ~command:p.command ~driver:p.driver g in
+         let call = 
+	   Db.try_prover ~debug:true ~timelimit ~memlimit:0 
+~prover:p.prover ~command:p.command ~driver:p.driver g 
+	 in
          call ()
        with Not_found | Failure _ -> 
          printf "unknown choice@.");

why.conf

@@ -4,7 +4,7 @@ timelimit = 2
 
 [prover alt-ergo]
 name = "Alt-Ergo"
-command = "alt-ergo %f"
+command = "why-cpulimit %t alt-ergo %f 2>&1"
 driver = "drivers/alt_ergo.drv"
 
 [prover coq]
@@ -14,11 +14,11 @@ driver = "drivers/coq.drv"
 
 [prover cvc3]
 name = "CVC3"
-command = "cvc3 -lang smt"
+command = "why-cpulimit %t cvc3 -lang smt %f 2>&1"
 driver = "drivers/cvc3.drv"
 
 [prover z3]
 name = "Z3"
-command = "why-cpulimit %t z3 -smt %f"
+command = "why-cpulimit %t z3 -smt %f 2>&1"
 driver = "drivers/z3.drv"