encoding_decorate : ajout de goal, mono, inst mais assert false sur eux

bench : ajout d'un bench pour tester tous les provers sur des buts triviaux. Cela peut permettre de détecter un mauvais driver ou printer.

Makefile.in

@@ -476,13 +476,35 @@ bin/why3-cpulimit: src/tools/@CPULIMIT@.c
 clean::
 	rm -f bin/why3-cpulimit src/tools/*~
 
+#########
+# drivers
+#########
+#Only generated drivers
+DIR_DRIVERS := drivers/
+
+DRIVERS := z3_inst cvc3_inst
+DRIVERS := $(DRIVERS) $(addsuffix _def, $(DRIVERS)) \
+	$(addsuffix _goal, $(DRIVERS)) $(addsuffix _mono, $(DRIVERS))
+DRIVERS := $(DRIVERS) $(addsuffix _nbp, $(DRIVERS))
+DRIVERS := $(addsuffix .drv, $(DRIVERS))
+DRIVERS := $(addprefix $(DIR_DRIVERS), $(DRIVERS))
+
+#Not great for -j
+$(DRIVERS) : $(DIR_DRIVERS)z3.drv $(DIR_DRIVERS)cvc3.drv drivers/gen_drv.sh
+	drivers/gen_drv.sh
+
+byte opt: $(DRIVERS)
+
+clean::
+	rm -f $(DRIVERS)
+
 ########
 # bench
 ########
 
 .PHONY: bench test
 
-bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@
+bench:: bin/why.@OCAMLBEST@ bin/whyml.@OCAMLBEST@ $(TOOLS) $(DRIVERS)
 	sh bench/bench \
 	    "bin/why.@OCAMLBEST@" \
 	    "bin/whyml.@OCAMLBEST@"

bench/bench

@@ -88,6 +88,28 @@ valid_goals () {
     done
 }
 
+
+test_provers () {
+    for f in $1/*.mlw; do
+	echo -n "  "$f"... "
+	if $pgml -P alt-ergo $f | grep -q -v Valid; then
+	    echo "valid test $f failed!"
+	    exit 1
+       else 
+	    echo "ok"
+	fi
+    done
+}
+
+test_prover () {
+    if $pgm -t 1 -P $1 $2 | grep -q -v Valid; then
+	echo "  $1 fails!"
+    else
+        true
+    fi
+}
+
+
 # 1. Syntax
 echo "=== Parsing good files  ==="
 goods bench/typing/bad --parse-only
@@ -132,4 +154,33 @@ echo "=== Checking valid goals ==="
 valid_goals bench/valid
 echo ""
 
+echo "=== Checking provers ==="
+echo -n "Test provers on true..."
+provers=$($pgm --list-provers | cut -d " " -f 3 |grep -v "^$")
+good_provers=""
+bad_provers=""
+for prover in $(echo $provers); do 
+    if bin/why.opt -P $prover bench/true_goal.why | grep -q -v Valid; then
+        #echo "$i : Fail"
+        bad_provers="$bad_provers $prover"
+    else
+        #echo "$i : Ok"
+        good_provers="$good_provers $prover"
+    fi
+done
+echo "done"
+echo ""
+echo "On your installation the following provers can't prove \"true\":"
+echo "  $bad_provers"
+echo ""
+echo "So I will only test the following provers:"
+echo $good_provers
+echo ""
+echo "nb : If a prover can't prove a goal it's perhaps normal (ex: TPTP int)"
 
+for file in bench/valid/*.why; do
+    echo I test $file
+    for prover in $good_provers; do
+        test_prover $prover $file
+    done
+done
\ No newline at end of file

bench/true_goal.why

+theory True
+  goal True : true
+end
\ No newline at end of file

bench/valid/int.why

+theory Test
+  use import int.Int
+  goal G1 : 5 * 10 = 50
+  goal G2 : forall x:int. x + x - x + x  = 2 * x
+end

bench/valid/real.why

+theory Test
+  use import real.Real
+  goal G1 : 5.5 * 10. = 55. 
+  goal G2 : 9. / 3. = 3. 
+  goal G3 : inv(5.) = 0.2
+end

drivers/gen_drv.sh

+#!/bin/sh
+
+DIR=drivers/
+
+for prover in z3 cvc3; do
+    for what in "" _goal _mono _def; do
+        for complete in "" _nbp; do
+            cat ${DIR}${prover}.drv |sed -e "s/transformation \"encoding_decorate\"/transformation \"encoding_instantiate$what$complete\"/" > ${DIR}${prover}_inst${what}${complete}.drv
+        done
+    done
+done

drivers/z3.drv

@@ -23,7 +23,6 @@ transformation "simplify_trivial_quantification"
 transformation "encoding_decorate"
 (* transformation "encoding_decorate_every_simple" *)
 
-
 theory BuiltIn
   syntax type int "Int"
   syntax type real "Real"

drivers/z3_inst.drv

@@ -23,7 +23,6 @@ transformation "simplify_trivial_quantification"
 transformation "encoding_instantiate"
 (* transformation "encoding_decorate_every_simple" *)
 
-
 theory BuiltIn
   syntax type int "Int"
   syntax type real "Real"
@@ -73,7 +72,7 @@ theory real.Real
   syntax logic (_+_) "(+ %1 %2)"
   syntax logic (_-_) "(- %1 %2)"
   syntax logic (_*_) "(* %1 %2)"
-  syntax logic (_/_)  "(/ %1 %2)"
+  syntax logic (_/_) "(/ %1 %2)"
   syntax logic (-_)  "(- %1)"
   syntax logic inv  "(/ 1.0 %1)"
 

src/transform/encoding_decorate.ml

@@ -27,6 +27,7 @@ open Task
 open Decl
 
 let why_filename = ["transform" ; "encoding_decorate"]
+let kept_tag = "encoding_decorate : kept"
 
 (* From Encoding Polymorphism CADE07*)
 
@@ -128,7 +129,7 @@ let is_kept tenv ts =
         | None -> true (* every_simple *)
         | Some query ->
             let tags = Driver.query_tags query ts.ts_name in
-            Sstr.mem "encoding_decorate : kept" tags
+            Sstr.mem kept_tag tags
     end
 
 (* Translate a type to a term *)

src/transform/encoding_decorate.mli

@@ -23,3 +23,4 @@
     Jean-Francois Couchot et Stephane Lescuyer *)
 
 val why_filename : string list
+val kept_tag : string

src/transform/encoding_instantiate.ml

@@ -37,7 +37,6 @@ let ty_dumb = ty_var tv_dumb
 module OHTyl = OrderedHashList(Tty)
 module Mtyl = Map.Make(OHTyl)
 
-
 type tenv_aux = {
   deco : ty;
   undeco : ty;
@@ -46,13 +45,17 @@ type tenv_aux = {
 }
 
 type tenv =
-  | No_black_part
-  | Tenv of tenv_aux
+  | Tenv of tenv_aux (* The transformation decorates with tenv_aux.* *)
+  | No_black_part (* The environnement when the transformation isn't complete*)
 
+(* A type is projected on term or type depending 
+   of its color (green part,red part, black part) *)
 type tty =
   | Tyterm of term
   | Tyty of ty
 
+(* It can be backprojected to type, ty_dumb is like a bottom type it
+   never appear in final formulas *)
 let reduce_to_type = function
   | Tyty ty -> ty
   | Tyterm _ -> ty_dumb
@@ -69,6 +72,7 @@ let reduce_to_neg tenv = function
       | No_black_part -> assert false (* All is type in this mode *)
       | Tenv tenv -> tenv.deco
 
+(* The environnement of the transformation between two decl (* unmutable *) *)
 type env = {
   etenv : tenv;
   ekeep : Sty.t;
@@ -77,6 +81,8 @@ type env = {
   edefined_tsymbol : lsymbol Mtyl.t Mts.t;
 }
 
+(* The environnement of the transformation during 
+   the transformation of a formula *)
 type menv = {
   tenv : tenv;
   keep : Sty.t;
@@ -105,7 +111,7 @@ type tvar = {
 }
 
 let why_filename = Encoding_decorate.why_filename
-
+(* Useful function *)
 let rec logic_inst tl = function
   | None -> List.map reduce_to_type tl
   | Some ty -> (reduce_to_type ty) :: (logic_inst tl None)
@@ -212,7 +218,7 @@ let conv_vs_let menv tvar vsvar vs =
     | Tyterm _ -> Mvs.add vs (t_var vs') vsvar
     | Tyty _ -> Mvs.add vs (t_var vs') vsvar),vs'
 
-
+(* The convertion of term and formula *)
 let rec rewrite_term menv tvar vsvar t = 
   let fnT = rewrite_term menv tvar in
   let fnF = rewrite_fmla menv tvar in
@@ -265,7 +271,7 @@ and rewrite_fmla menv tvar vsvar f =
         f_let u t1' f2'
     | _ -> f_map (fnT vsvar) (fnF vsvar) f
 
-
+(* Generation of all the possible instantiation of a formula *)
 let gen_tvar env ts = 
   let aux tv tvarl = 
     let gen tvar ty = {tvar with tvar_ty = Mtv.add tv ty tvar.tvar_ty} in
@@ -318,6 +324,7 @@ let ty_quant =
     | _ -> ty_fold add_vs s ty in
   f_fold_ty add_vs Stv.empty
 
+(* The Core of the transformation *)
 let fold_map task_hd ((env:env),task) =
   match task_hd.task_decl with
     | Use _ | Clone _ -> env,add_tdecl task task_hd.task_decl
@@ -383,7 +390,7 @@ Perhaps you could use eliminate_definition"
       },
       List.fold_left conv_f task tvarl
 
-
+(* A Pre-transformation to work on monomorphic goal *)
 let on_goal fn =
   let fn task = match task with
     | Some {Task.task_decl = 
@@ -406,7 +413,9 @@ let monomorphise_goal =
       acc ltv in
     acc)
 
+let monomorphise_goal = Register.store (fun () -> monomorphise_goal)
 
+(* The prelude for the complete transformation *)
 let load_prelude env =
   let prelude = Env.find_theory env why_filename "Prelude" in
   let sort = Theory.ns_find_ls prelude.th_export ["sort"] in
@@ -420,11 +429,9 @@ let load_prelude env =
     sort = sort;
     ty = ty}
 
-
-let create_env_int_real env =
-  let task,tenv = load_prelude env in
-  let keep = List.fold_left (fun acc ty ->  Sty.add ty acc) 
-    Sty.empty [ty_int;ty_real] in
+(* Some general env creation function *) 
+let create_env task tenv sty =
+  let keep = sty in
   let projty = Sty.fold (fun ty tvar_ty -> Mty.add ty ty tvar_ty)
     keep Mty.empty in
   let task = Mty.fold (fun _ ty task -> 
@@ -432,45 +439,150 @@ let create_env_int_real env =
       | Tyapp (ts,[]) -> add_ty_decl task [ts,Tabstract]
       | _ -> assert false) projty task in
     task,{
-    etenv = Tenv tenv;
+    etenv = tenv;
     ekeep = keep;
     eprojty = projty;
     edefined_lsymbol = Mls.empty;
     edefined_tsymbol = Mts.empty
   }
 
-let create_env_int_real_no_black_part =
-  let keep = List.fold_left (fun acc ty ->  Sty.add ty acc) 
-    Sty.empty [ty_int;ty_real] in
-  let projty = Sty.fold (fun ty tvar_ty -> Mty.add ty ty tvar_ty)
-    keep Mty.empty in
-  let task = use_export None builtin_theory in
-  let task = Mty.fold (fun _ ty task -> 
-    match ty.ty_node with
-      | Tyapp (ts,[]) -> add_ty_decl task [ts,Tabstract]
-      | _ -> assert false) projty task in
-  task,{
-    etenv = No_black_part;
-    ekeep = keep;
-    eprojty = projty;
-    edefined_lsymbol = Mls.empty;
-    edefined_tsymbol = Mts.empty
-  }
 
+let create_env_complete env sty =
+  let task,tenv = load_prelude env in
+  create_env task (Tenv tenv) sty
 
-let t_all = Register.store_env 
-  (fun env -> 
-     let init_task,env = create_env_int_real env in
-     Trans.compose monomorphise_goal
-     (Trans.fold_map fold_map env init_task))
+let create_env_nbp sty =
+  let task = use_export None builtin_theory in
+  let tenv = No_black_part in
+  create_env task tenv sty
+
+let register_transform name create_env =
+  let t = Register.store_query
+    (fun query ->
+       Trans.store 
+         (fun task ->
+            let task = Register.apply monomorphise_goal task in
+            let drv = Driver.query_driver query in
+            let env = Driver.query_env query in
+            let init_task,env = create_env env drv task in
+            Trans.apply (Trans.fold_map fold_map env init_task) task)) in
+  Register.register_transform name t
+
+(* The most simple configuration takes only the tag keep into account *)
+let is_kept query ts = 
+  ts.ts_args = [] &&  
+    begin
+      ts_equal ts ts_int || ts_equal ts ts_real  (* for the constant *)
+      || let tags = Driver.query_tags query ts.ts_name in
+         Sstr.mem Encoding_decorate.kept_tag tags
+    end
+
+let fold_decl f = 
+  Trans.fold (fun task_hd acc ->
+    match task_hd.task_decl with
+      | Use _ | Clone _ -> acc
+      | Decl d -> f d acc)
+
+let look_for_keep query d sty =
+  match d.d_node with
+    | Dtype [ts,Tabstract] -> 
+        if is_kept query ts then Sty.add (ty_app ts []) sty else sty
+    | Dtype _ -> Register.unsupportedDecl 
+        d "encoding_decorate : I can work only on abstract\
+            type which are not in recursive bloc."
+    | _ -> sty
 
-let () = Register.register_transform "encoding_instantiate" t_all
+let look_for_keep =
+  Register.store_query
+    (fun query -> fold_decl (look_for_keep query) Sty.empty)
 
-let t_all = Register.store 
-  (fun () -> 
-     let init_task,env = create_env_int_real_no_black_part in
-     Trans.compose monomorphise_goal
-     (Trans.fold_map fold_map env init_task))
+let () = register_transform "encoding_instantiate"
+  (fun env drv task -> 
+     let sty = Register.apply_driver look_for_keep drv task in
+     create_env_complete env sty)
 
+let () = register_transform "encoding_instantiate_nbp"
+  (fun _ drv task -> 
+     let sty = Register.apply_driver look_for_keep drv task in
+     create_env_nbp sty)
 
-let () = Register.register_transform "encoding_instantiate_no_black_part" t_all
+(* This one take use the tag but also all the type which appear in the goal *)
+let is_ty_mono ~only_mono ty = 
+  try
+    let rec check () ty = match ty.ty_node with
+      | Tyvar _ -> raise Exit
+      | Tyapp _ -> ty_fold check () ty in
+    check () ty;
+    true
+  with Exit when not only_mono -> false
+
+let find_mono ~only_mono sty f = 
+  let add sty ty = if is_ty_mono ~only_mono ty then Sty.add ty sty else sty in
+  f_fold_ty add sty f
+
+let mono_in_goal d sty =
+  match d.d_node with
+    | Dprop (Pgoal,_,f) -> 
+        (try find_mono ~only_mono:true sty f
+         with Exit -> assert false) (*monomorphise goal should have been used*)
+    | _ -> sty
+
+let mono_in_goal =
+  Register.store (fun () -> fold_decl mono_in_goal Sty.empty)
+
+let () = register_transform "encoding_instantiate_goal"
+  (fun env drv task -> 
+     let sty1 = Register.apply_driver look_for_keep drv task in
+     let sty2 = Register.apply mono_in_goal task in
+     create_env_complete env (Sty.union sty1 sty2))
+
+let () = register_transform "encoding_instantiate_goal_nbp"
+  (fun _ drv task -> 
+     let sty1 = Register.apply_driver look_for_keep drv task in
+     let sty2 = Register.apply mono_in_goal task in
+     create_env_nbp (Sty.union sty1 sty2))
+
+(* This one use the tag and also all the type in all the definition *)
+let mono_in_def d sty =
+  match d.d_node with
+    | Dprop (_,_,f) -> find_mono ~only_mono:false sty f
+    | _ -> sty
+
+let mono_in_def =
+  Register.store (fun () -> fold_decl mono_in_def Sty.empty)
+
+let () = register_transform "encoding_instantiate_def"
+  (fun env drv task -> 
+     let sty1 = Register.apply_driver look_for_keep drv task in
+     let sty2 = Register.apply mono_in_def task in
+     create_env_complete env (Sty.union sty1 sty2))
+
+let () = register_transform "encoding_instantiate_def_nbp"
+  (fun _ drv task -> 
+     let sty1 = Register.apply_driver look_for_keep drv task in
+     let sty2 = Register.apply mono_in_def task in
+     create_env_nbp (Sty.union sty1 sty2))
+
+(* This one use the tag and also all ther type in all the 
+   monomorphic definition*)
+let mono_in_mono d sty =
+  match d.d_node with
+    | Dprop (_,_,f) -> 
+        (try find_mono ~only_mono:true sty f
+         with Exit -> sty)
+    | _ -> sty
+
+let mono_in_mono =
+  Register.store (fun () -> fold_decl mono_in_mono Sty.empty)
+
+let () = register_transform "encoding_instantiate_mono"
+  (fun env drv task -> 
+     let sty1 = Register.apply_driver look_for_keep drv task in
+     let sty2 = Register.apply mono_in_mono task in
+     create_env_complete env (Sty.union sty1 sty2))
+
+let () = register_transform "encoding_instantiate_mono_nbp"
+  (fun _ drv task -> 
+     let sty1 = Register.apply_driver look_for_keep drv task in
+     let sty2 = Register.apply mono_in_mono task in
+     create_env_nbp (Sty.union sty1 sty2))

why.conf

@@ -22,17 +22,6 @@ name = "Z3"
 command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
 driver = "drivers/z3.drv"
 
-
-[prover cvc3_inst]
-name = "CVC3"
-command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
-driver = "drivers/cvc3_inst.drv"
-
-[prover z3_inst]
-name = "Z3"
-command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
-driver = "drivers/z3_inst.drv"
-
 [prover spass]
 name = "spass"
 command = "why3-cpulimit 0 %m SPASS -TPTP -PGiven=0 -PProblem=0 -DocProof -TimeLimit=%t %f 2>&1"
@@ -52,3 +41,84 @@ driver = "drivers/simplify.drv"
 name = "Gappa"
 command = "why3-cpulimit %t %m gappa %f 2>&1"
 driver = "drivers/gappa.drv"
+
+[prover cvc3_inst]
+name = "CVC3"
+command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
+driver = "drivers/cvc3_inst.drv"
+
+[prover z3_inst]
+name = "Z3"
+command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
+driver = "drivers/z3_inst.drv"
+
+[prover cvc3_inst_nbp]
+name = "CVC3"
+command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
+driver = "drivers/cvc3_inst_nbp.drv"
+
+[prover z3_inst_nbp]
+name = "Z3"
+command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
+driver = "drivers/z3_inst_nbp.drv"
+
+[prover cvc3_inst_goal]
+name = "CVC3"
+command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
+driver = "drivers/cvc3_inst_goal.drv"
+
+[prover z3_inst_goal]
+name = "Z3"
+command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
+driver = "drivers/z3_inst_goal.drv"
+
+[prover cvc3_inst_goal_nbp]
+name = "CVC3"
+command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
+driver = "drivers/cvc3_inst_goal_nbp.drv"
+
+[prover z3_inst_goal_nbp]
+name = "Z3"
+command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
+driver = "drivers/z3_inst_goal_nbp.drv"
+
+[prover cvc3_inst_def]
+name = "CVC3"
+command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
+driver = "drivers/cvc3_inst_def.drv"
+
+[prover z3_inst_def]
+name = "Z3"
+command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
+driver = "drivers/z3_inst_def.drv"
+
+[prover cvc3_inst_def_nbp]
+name = "CVC3"
+command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
+driver = "drivers/cvc3_inst_def_nbp.drv"
+
+[prover z3_inst_def_nbp]
+name = "Z3"
+command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
+driver = "drivers/z3_inst_def_nbp.drv"
+
+
+[prover cvc3_inst_mono]
+name = "CVC3"
+command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
+driver = "drivers/cvc3_inst_mono.drv"
+
+[prover z3_inst_mono]
+name = "Z3"
+command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
+driver = "drivers/z3_inst_mono.drv"
+
+[prover cvc3_inst_mono_nbp]
+name = "CVC3"
+command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
+driver = "drivers/cvc3_inst_mono_nbp.drv"
+
+[prover z3_inst_mono_nbp]
+name = "Z3"
+command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
+driver = "drivers/z3_inst_mono_nbp.drv"