only one transformation for encoding instantiate

.gitignore

@@ -58,24 +58,6 @@
 /doc/*.hind
 /doc/*.htoc
 
-# /drivers/
-/drivers/cvc3_inst.drv
-/drivers/cvc3_inst_nbp.drv
-/drivers/cvc3_inst_def.drv
-/drivers/cvc3_inst_def_nbp.drv
-/drivers/cvc3_inst_goal.drv
-/drivers/cvc3_inst_goal_nbp.drv
-/drivers/cvc3_inst_mono.drv
-/drivers/cvc3_inst_mono_nbp.drv
-/drivers/z3_inst.drv
-/drivers/z3_inst_nbp.drv
-/drivers/z3_inst_def.drv
-/drivers/z3_inst_def_nbp.drv
-/drivers/z3_inst_goal.drv
-/drivers/z3_inst_goal_nbp.drv
-/drivers/z3_inst_mono.drv
-/drivers/z3_inst_mono_nbp.drv
-
 # /share/
 /share/*.cm*
 /share/*.annot

Makefile.in

@@ -470,10 +470,8 @@ install::
 #Only generated drivers
 DIR_DRIVERS := drivers/
 
-DRIVERS := z3_inst cvc3_inst
-DRIVERS := $(DRIVERS) $(addsuffix _all, $(DRIVERS)) \
-	$(addsuffix _goal, $(DRIVERS)) $(addsuffix _mono, $(DRIVERS))
-DRIVERS := $(DRIVERS) $(addsuffix _incomplete, $(DRIVERS))
+DRIVERS := z3_inst cvc3_inst z3_simple cvc3_simple
+
 DRIVERS := $(addsuffix .drv, $(DRIVERS))
 DRIVERS := $(addprefix $(DIR_DRIVERS), $(DRIVERS))
 

drivers/cvc3_simple.drv

-
-(* Why driver for SMT syntax *)
-
-prelude ";;; this is a prelude for CVC3 "
-
-printer "smtv1"
-filename "%f-%t-%g.smt"
-
-valid "unsat"
-unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
-
-(* À discuter *)
-transformation "simplify_recursive_definition"
-transformation "inline_trivial"
-
-transformation "eliminate_builtin"
-transformation "eliminate_definition"
-transformation "eliminate_inductive"
-transformation "eliminate_algebraic"
-transformation "simplify_formula"
-transformation "simplify_trivial_quantification"
-
-transformation "encoding_enumeration"
-transformation "explicit_polymorphism"
-transformation "encoding_simple_kept"
-
-theory BuiltIn
-  syntax type int   "Int"
-  syntax type real  "Real"
-  syntax logic (=)  "(= %1 %2)"
-  syntax logic (<>) "(not (= %1 %2))"
-end
-
-theory int.Int
-
-  prelude ";;; this is a prelude for CVC3, Arithmetic"
-
-  syntax logic zero "0"
-
-  syntax logic (+)  "(+ %1 %2)"
-  syntax logic (-)  "(- %1 %2)"
-  syntax logic (*)  "(* %1 %2)"
-  syntax logic (-_) "(- %1)"
-
-  syntax logic (<=) "(<= %1 %2)"
-  syntax logic (<)  "(< %1 %2)"
-  syntax logic (>=) "(>= %1 %2)"
-  syntax logic (>)  "(> %1 %2)"
-
-  remove prop CommutativeGroup.Comm.Comm
-  remove prop CommutativeGroup.Assoc.Assoc
-  remove prop CommutativeGroup.Unit_def
-  remove prop CommutativeGroup.Inv_def
-  remove prop Assoc.Assoc
-  remove prop Mul_distr
-  remove prop Comm.Comm
-  remove prop Unitary
-  remove prop Refl
-  remove prop Trans
-  remove prop Antisymm
-  remove prop Total
-end
-
-theory real.Real
-
-  prelude ";;; this is a prelude for Z3, Arithmetic"
-
-  syntax logic zero "0"
-
-  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)"
-
-  syntax logic (<=) "(<= %1 %2)"
-  syntax logic (<)  "(< %1 %2)"
-  syntax logic (>=) "(>= %1 %2)"
-  syntax logic (>)  "(> %1 %2)"
-
-  remove prop CommutativeGroup.Comm.Comm
-  remove prop CommutativeGroup.Assoc.Assoc
-  remove prop CommutativeGroup.Unit_def
-  remove prop CommutativeGroup.Inv_def
-  remove prop Inverse
-  remove prop Assoc.Assoc
-  remove prop Mul_distr
-  remove prop Comm.Comm
-  remove prop Unitary
-  remove prop Refl
-  remove prop Trans
-  remove prop Antisymm
-  remove prop Total
-
-end
-
-(*
-(* L'encodage des types sommes bloquent cette théorie builtin *)
-theory bool.Bool
-   syntax type bool   "bool"
-   syntax logic True  "true"
-   syntax logic False "false"
-   syntax logic andb  "(and %1 %2)"
-   syntax logic orb   "(or %1 %2)"
-   syntax logic xorb  "(xor %1 %2)"
-   syntax logic notb  "(not %1)"
-   meta cloned "encoding_decorate : kept" type bool
-end
-*)
-
-(*
-Local Variables:
-mode: why
-compile-command: "make -C ../.. bench"
-End:
-*)

drivers/gen_drv.sh

@@ -2,10 +2,21 @@
 
 DIR=drivers/
 
+
+
+replace (){
+ prover=$1;
+ suffix=$2;
+ src=$3
+ dst=$4
+ cat ${DIR}${prover}.drv |sed -e "s/${src}/${dst}/" > ${DIR}${prover}_${suffix}.drv
+}
+
+for prover in z3 cvc3; do
+    replace $prover "inst" transformation\ \"encoding_decorate\" transformation\ \"encoding_instantiate\"
+done
+
 for prover in z3 cvc3; do
-    for what in "" _goal _mono _all; do
-        for complete in "" _incomplete; do
-            cat ${DIR}${prover}.drv |sed -e "s/transformation \"encoding_decorate\"/transformation \"encoding_instantiate$what$complete\"/" > ${DIR}${prover}_inst${what}${complete}.drv
-        done
-    done
+    replace $prover "simple" transformation\ \"encoding_decorate\" \
+"transformation \"encoding_enumeration\"\ntransformation \"explicit_polymorphism\"\ntransformation \"encoding_simple_kept\""
 done

drivers/z3_simple.drv

-
-(* Why driver for SMT syntax *)
-
-prelude ";;; this is a prelude for Z3"
-
-printer "smtv1"
-filename "%f-%t-%g.smt"
-
-valid "^unsat"
-unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
-
-(* À discuter *)
-transformation "simplify_recursive_definition"
-transformation "inline_trivial"
-
-transformation "eliminate_builtin"
-transformation "eliminate_definition"
-transformation "eliminate_inductive"
-transformation "eliminate_algebraic"
-transformation "simplify_formula"
-transformation "simplify_trivial_quantification"
-
-transformation "encoding_enumeration"
-transformation "explicit_polymorphism"
-transformation "encoding_simple_kept"
-
-theory BuiltIn
-  syntax type int   "Int"
-  syntax type real  "Real"
-  syntax logic (=)  "(= %1 %2)"
-  syntax logic (<>) "(not (= %1 %2))"
-end
-
-
-theory int.Int
-
-  prelude ";;; this is a prelude for Z3, Arithmetic"
-
-  syntax logic zero "0"
-
-  syntax logic (+)  "(+ %1 %2)"
-  syntax logic (-)  "(- %1 %2)"
-  syntax logic (*)  "(* %1 %2)"
-  syntax logic (-_) "(- %1)"
-
-  syntax logic (<=) "(<= %1 %2)"
-  syntax logic (<)  "(< %1 %2)"
-  syntax logic (>=) "(>= %1 %2)"
-  syntax logic (>)  "(> %1 %2)"
-
-  remove prop CommutativeGroup.Comm.Comm
-  remove prop CommutativeGroup.Assoc.Assoc
-  remove prop CommutativeGroup.Unit_def
-  remove prop CommutativeGroup.Inv_def
-  remove prop Assoc.Assoc
-  remove prop Mul_distr
-  remove prop Comm.Comm
-  remove prop Unitary
-  remove prop Refl
-  remove prop Trans
-  remove prop Antisymm
-  remove prop Total
-
-end
-
-
-theory real.Real
-
-  prelude ";;; this is a prelude for Z3, Arithmetic"
-
-  syntax logic zero "0"
-
-  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)"
-
-  syntax logic (<=) "(<= %1 %2)"
-  syntax logic (<)  "(< %1 %2)"
-  syntax logic (>=) "(>= %1 %2)"
-  syntax logic (>)  "(> %1 %2)"
-
-  remove prop CommutativeGroup.Comm.Comm
-  remove prop CommutativeGroup.Assoc.Assoc
-  remove prop CommutativeGroup.Unit_def
-  remove prop CommutativeGroup.Inv_def
-  remove prop Inverse
-  remove prop Assoc.Assoc
-  remove prop Mul_distr
-  remove prop Comm.Comm
-  remove prop Unitary
-  remove prop Refl
-  remove prop Trans
-  remove prop Antisymm
-  remove prop Total
-
-end
-
-(*
-(* L'encodage des types sommes bloquent cette théorie builtin *)
-theory bool.Bool
-   syntax type bool   "bool"
-   syntax logic True  "true"
-   syntax logic False "false"
-   syntax logic andb  "(and %1 %2)"
-   syntax logic orb   "(or %1 %2)"
-   syntax logic xorb  "(xor %1 %2)"
-   syntax logic notb  "(not %1)"
-   meta cloned "encoding_decorate : kept" type bool
-end
-*)
-
-
-theory int.EuclideanDivision
-   syntax logic div "(div %1 %2)"
-   syntax logic mod "(mod %1 %2)"
-   remove prop Mod_bound
-   remove prop Div_mod
-   remove prop Mod_1
-   remove prop Div_1
-end
-
-(*
-Local Variables:
-mode: why
-compile-command: "unset LANG; make -C .. bench"
-End:
-*)

share/zsh/_why3

@@ -74,7 +74,7 @@ case $state in
         ;;
     metas)
         _message "<metas>"
-        compadd "$($cmd --list-metas | egrep -E "^  [a-z]" | sed "s/^[ ]*\(.*\)$/\1/")";
+        compadd "$($cmd --list-metas | egrep -E "^  [a-z]" | sed "s/^[ ]*\(.*\)$/'\1'/")";
         return 0
         ;;
     theories)

src/core/task.ml

@@ -247,7 +247,7 @@ exception NotExclusiveMeta of string
 let get_meta_exc t tds =
   if not (is_meta_excl t) then raise (NotExclusiveMeta t);
   Stdecl.fold (fun td _ -> match td.td_node with
-    | Meta (s,_) when s = t -> Some td
+    | Meta (s,arg) when s = t -> Some arg
     | _ -> assert false) tds.tds_set None
 
 (* Exception reporting *)

src/core/task.mli

@@ -107,7 +107,7 @@ val find_tagged_pr : string -> tdecl_set -> Spr.t -> Spr.t
 
 exception NotExclusiveMeta of string
 
-val get_meta_exc : string -> tdecl_set -> tdecl option
+val get_meta_exc : string -> tdecl_set -> meta_arg list option
 
 (* exceptions *)
 

src/transform/encoding_instantiate.ml

@@ -28,8 +28,12 @@ open Task
 open Decl
 
 
-let meta_kept = register_meta "encoding_instantiate : kept" [MTtysymbol]
-let meta_level = register_meta_excl "encoding_instantiate : level" [MTstring]
+let meta_kept = register_meta
+  "encoding_instantiate : kept" [MTtysymbol]
+let meta_level = register_meta_excl 
+  "encoding_instantiate : level" [MTstring]
+let meta_complete = register_meta_excl 
+  "encoding_instantiate : complete" [MTstring]
 
 
 (* Ce type est utiliser pour indiquer un alpha *)
@@ -420,10 +424,10 @@ let load_prelude env =
   let undeco = ty_app (Theory.ns_find_ts prelude.th_export ["undeco"]) [] in
   let task = None in
   let task = Task.use_export task prelude in
-  task,{ deco = deco;
-    undeco = undeco;
-    sort = sort;
-    ty = ty}
+  task,Tenv { deco = deco;
+              undeco = undeco;
+              sort = sort;
+              ty = ty}
 
 
 let collect_green_part tds =
@@ -467,28 +471,6 @@ let create_env task tenv tds =
     edefined_tsymbol = Mts.empty
   }
 
-let create_trans_complete env tds =
-  let task,tenv = load_prelude env in
-  let init_task,env = create_env task (Tenv tenv) tds in
-  Trans.fold_map fold_map env init_task
-
-let create_trans_incomplete tds =
-  let task = use_export None builtin_theory in
-  let tenv = No_black_part in
-  let init_task,env = create_env task tenv tds in
-  Trans.fold_map fold_map env init_task
-
-let encoding_gen get_kept env =
-  Trans.compose monomorphise_goal (
-    Trans.compose get_kept
-      (Trans.on_meta meta_kept (create_trans_complete env)))
-
-
-let encoding_gen_incomplete get_kept = 
-  Trans.compose monomorphise_goal
-    (Trans.compose get_kept
-       (Trans.on_meta meta_kept create_trans_incomplete))
-
 (* This one take use the tag but also all the type which appear in the goal *)
 let is_ty_mono ~only_mono ty =
   try
@@ -539,19 +521,33 @@ let mono_in_mono d =
 
 let mono_in_mono = Trans.tdecl mono_in_mono None
 
-let () =
-  List.iter (fun (name,get_kept) -> 
-    Trans.register_env_transform name (encoding_gen get_kept))
-    ["encoding_instantiate",Trans.identity;
-     "encoding_instantiate_goal", mono_in_goal;
-     "encoding_instantiate_all", mono_in_def;
-     "encoding_instantiate_mono", mono_in_mono]
-
-
-let () =
-  List.iter (fun (name,get_kept) -> 
-    Trans.register_transform name (encoding_gen_incomplete get_kept))
-    ["encoding_instantiate_incomplete",Trans.identity;
-     "encoding_instantiate_goal_incomplete", mono_in_goal;
-     "encoding_instantiate_all_incomplete", mono_in_def;
-     "encoding_instantiate_mono_incomplete", mono_in_mono]
+
+let get_kept =
+  Trans.on_meta meta_level (fun tds ->
+    match get_meta_exc meta_level tds with
+      | None | Some [MAstr "goal"] -> mono_in_goal
+      | Some [MAstr "kept"] -> Trans.identity
+      | Some [MAstr "all"] -> mono_in_def
+      | Some [MAstr "mono"] -> mono_in_mono
+      | _ -> failwith "instantiate level wrong argument")
+
+
+let create_trans_complete env metas =
+  let tds_kept = Mstr.find meta_kept metas in
+  let complete = get_meta_exc meta_complete (Mstr.find meta_complete metas) in
+  let task, tenv = match complete with
+    | None | Some [MAstr "yes"] -> load_prelude env
+    | Some [MAstr "no"] ->  
+      let task = use_export None builtin_theory in
+      let tenv = No_black_part in
+      task, tenv
+    | _ -> failwith "instantiate complete wrong argument" in
+  let init_task,env = create_env task tenv tds_kept in
+  Trans.fold_map fold_map env init_task
+
+let encoding env =
+  Trans.compose monomorphise_goal (
+    Trans.compose get_kept
+      (Trans.on_metas [meta_kept;meta_complete] (create_trans_complete env)))
+
+let () = Trans.register_env_transform "encoding_instantiate" encoding

why.conf

@@ -22,6 +22,11 @@ name = "CVC3_simple"
 command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
 driver = "drivers/cvc3_simple.drv"
 
+[prover cvc3_inst]
+name = "CVC3 (inst)"
+command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
+driver = "drivers/cvc3_inst.drv"
+
 [prover z3]
 name = "Z3"
 command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
@@ -32,6 +37,11 @@ name = "Z3_simple"
 command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
 driver = "drivers/z3_simple.drv"
 
+[prover z3_inst]
+name = "Z3 (inst)"
+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"
@@ -61,84 +71,3 @@ driver = "drivers/simplify.drv"
 name = "Gappa"
 command = "why3-cpulimit %t %m gappa %f 2>&1"
 driver = "drivers/gappa.drv"
-
-[prover cvc3_inst]
-name = "CVC3 (inst)"
-command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
-driver = "drivers/cvc3_inst.drv"
-
-[prover z3_inst]
-name = "Z3 (inst)"
-command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
-driver = "drivers/z3_inst.drv"
-
-[prover cvc3_inst_incomplete]
-name = "CVC3 (inst+incomplete)"
-command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
-driver = "drivers/cvc3_inst_incomplete.drv"
-
-[prover z3_inst_incomplete]
-name = "Z3 (inst+incomplete)"
-command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
-driver = "drivers/z3_inst_incomplete.drv"
-
-[prover cvc3_inst_goal]
-name = "CVC3 (inst+goal)"
-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 (inst+goal)"
-command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
-driver = "drivers/z3_inst_goal.drv"
-
-[prover cvc3_inst_goal_incomplete]
-name = "CVC3 (inst+goal+incomplete)"
-command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
-driver = "drivers/cvc3_inst_goal_incomplete.drv"
-
-[prover z3_inst_goal_incomplete]
-name = "Z3 (inst+goal+incomplete)"
-command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
-driver = "drivers/z3_inst_goal_incomplete.drv"
-
-[prover cvc3_inst_all]
-name = "CVC3 (inst+def)"
-command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
-driver = "drivers/cvc3_inst_all.drv"
-
-[prover z3_inst_all]
-name = "Z3 (inst+def)"
-command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
-driver = "drivers/z3_inst_all.drv"
-
-[prover cvc3_inst_all_incomplete]
-name = "CVC3 (inst+def+incomplete)"
-command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
-driver = "drivers/cvc3_inst_all_incomplete.drv"
-
-[prover z3_inst_all_incomplete]
-name = "Z3 (inst+def+incomplete)"
-command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
-driver = "drivers/z3_inst_all_incomplete.drv"
-
-
-[prover cvc3_inst_mono]
-name = "CVC3 (inst+mono)"
-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 (inst+mono)"
-command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
-driver = "drivers/z3_inst_mono.drv"
-
-[prover cvc3_inst_mono_incomplete]
-name = "CVC3 (inst+mono+incomplete)"
-command = "why3-cpulimit 0 %m cvc3 -timeout %t -lang smt %f 2>&1"
-driver = "drivers/cvc3_inst_mono_incomplete.drv"
-
-[prover z3_inst_mono_incomplete]
-name = "Z3 (inst+mono+incomplete)"
-command = "why3-cpulimit %t %m z3 -smt %f 2>&1"
-driver = "drivers/z3_inst_mono_incomplete.drv"