Add parameter to encoding_arrays and split it into distinction and select

Makefile.in

@@ -126,11 +126,12 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
 		inlining split_goal \
 		eliminate_definition eliminate_algebraic \
 		eliminate_inductive eliminate_let eliminate_if \
+		encoding_distinction \
 		encoding_enumeration encoding encoding_decorate_mono \
-		libencoding encoding_decorate encoding_bridge \
+		libencoding encoding_select \
+		encoding_decorate encoding_bridge \
 		encoding_explicit encoding_guard encoding_sort \
 		encoding_instantiate simplify_array filter_trigger \
-		encoding_arrays \
 		introduction abstraction close_epsilon lift_epsilon
 
 LIB_PRINTER = print_real alt_ergo why3 smt smt2 coq tptp simplify gappa cvc3

drivers/cvc3.drv

-(* Why driver for SMT syntax *)
-
-prelude "%%% this is a prelude for CVC3 "
-
-printer "cvc3"
-filename "%f-%t-%g.cvc"
-
-valid "Valid."
-unknown "Unknown." ""
-time "why3cpulimit time : %s s"
-
-(* À discuter *)
-transformation "simplify_recursive_definition"
-transformation "inline_trivial"
-
-transformation "eliminate_builtin"
-transformation "eliminate_definition"
-transformation "eliminate_inductive"
-transformation "eliminate_algebraic_smt"
-
-transformation "simplify_formula"
-(*transformation "simplify_trivial_quantification"*)
-
-transformation "select_array_symbol_in_goal"
-transformation "instantiate_lsymbol"
-transformation "encoding_smt"
+import "cvc3.gen"
 
 theory BuiltIn
-  syntax type int   "INT"
-  syntax type real  "REAL"
-  syntax logic (=)  "(%1 = %2)"
-
-  meta "encoding : kept" type int
-end
-
-theory int.Int
-
-  prelude "%%% this is a prelude for CVC3 integer arithmetic"
-
-  syntax logic zero "0"
-  syntax logic one  "1"
-
-  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
-  remove prop NonTrivialRing
-  remove prop CompatOrderAdd
-
-end
-
-
-theory real.Real
-
-  prelude "%%% this is a prelude for CVC3 real arithmetic"
-
-  syntax logic zero "0"
-  syntax logic one  "1"
-
-
-  syntax logic (+)  "(%1 + %2)"
-  syntax logic (-)  "(%1 - %2)"
-  syntax logic (*)  "(%1 * %2)"
-  syntax logic (/)  "(%1 / %2)"
-  syntax logic (-_) "(- %1)"
-  syntax logic inv  "(1 / %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
-  remove prop NonTrivialRing
-  remove prop CompatOrderAdd
-
-  meta "encoding : kept" type real
-
-end
-
-(*
-(* L'encodage des types sommes bloquent cette théorie builtin *)
-theory bool.Bool
-   syntax type bool   "BITVECTOR(1)"
-   syntax logic True  "0bin1"
-   syntax logic False "0bin0"
-   syntax logic andb  "(%1 & %2)"
-   syntax logic orb   "(%1 | %2)"
-   syntax logic xorb  "(BVXOR(%1,%2))"
-   syntax logic notb  "(~ %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
-*)
-
-
-theory array.Array
-  syntax type t "(ARRAY %1 OF %2)"
-  meta "encoding : lskept" logic get
-  meta "encoding : lskept" logic set
-
-  meta "smt_dist_syntax" logic get, "(%1[%2])"
-  meta "smt_dist_syntax" logic set, "(%1 WITH [%2] := %3)"
+  meta "select_inst" "nothing"
+  meta "select_kept" "nothing"
+  meta "select_lskept" "nothing"
+  meta "completion_mode" "nothing"
 end
 
 (*

drivers/cvc3.gen

+(* Why driver for SMT syntax *)
+
+prelude "%%% this is a prelude for CVC3 "
+
+printer "cvc3"
+filename "%f-%t-%g.cvc"
+
+valid "Valid."
+unknown "Unknown." ""
+time "why3cpulimit time : %s s"
+
+(* À discuter *)
+transformation "simplify_recursive_definition"
+transformation "inline_trivial"
+
+transformation "eliminate_builtin"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic_smt"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "encoding_smt"
+
+theory BuiltIn
+  syntax type int   "INT"
+  syntax type real  "REAL"
+  syntax logic (=)  "(%1 = %2)"
+
+  meta "encoding : kept" type int
+end
+
+theory int.Int
+
+  prelude "%%% this is a prelude for CVC3 integer arithmetic"
+
+  syntax logic zero "0"
+  syntax logic one  "1"
+
+  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
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+
+end
+
+
+theory real.Real
+
+  prelude "%%% this is a prelude for CVC3 real arithmetic"
+
+  syntax logic zero "0"
+  syntax logic one  "1"
+
+
+  syntax logic (+)  "(%1 + %2)"
+  syntax logic (-)  "(%1 - %2)"
+  syntax logic (*)  "(%1 * %2)"
+  syntax logic (/)  "(%1 / %2)"
+  syntax logic (-_) "(- %1)"
+  syntax logic inv  "(1 / %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
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+
+  meta "encoding : kept" type real
+
+end
+
+(*
+(* L'encodage des types sommes bloquent cette théorie builtin *)
+theory bool.Bool
+   syntax type bool   "BITVECTOR(1)"
+   syntax logic True  "0bin1"
+   syntax logic False "0bin0"
+   syntax logic andb  "(%1 & %2)"
+   syntax logic orb   "(%1 | %2)"
+   syntax logic xorb  "(BVXOR(%1,%2))"
+   syntax logic notb  "(~ %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
+*)
+
+
+theory array.Array
+  syntax type t "(ARRAY %1 OF %2)"
+  meta "encoding : lskept" logic get
+  meta "encoding : lskept" logic set
+
+  meta "smt_dist_syntax" logic get, "(%1[%2])"
+  meta "smt_dist_syntax" logic set, "(%1 WITH [%2] := %3)"
+end
+
+(*
+Local Variables:
+mode: why
+compile-command: "unset LANG; make -C .. bench"
+End:
+*)

drivers/cvc3_all_type.drv

+import "cvc3.gen"
+
+theory BuiltIn
+  meta "select_inst" "nothing"
+  meta "select_kept" "goal"
+  meta "select_lskept" "nothing"
+  meta "completion_mode" "only_kept"
+end
+
+(*
+Local Variables:
+mode: why
+compile-command: "unset LANG; make -C .. bench"
+End:
+*)

drivers/cvc3_array.drv

+import "cvc3.gen"
+
+theory BuiltIn
+  meta "select_inst" "goal"
+  meta "select_kept" "goal"
+  meta "select_lskept" "nothing"
+  meta "completion_mode" "only_kept"
+end
+
+(*
+Local Variables:
+mode: why
+compile-command: "unset LANG; make -C .. bench"
+End:
+*)

drivers/cvc3_array_array.drv

+import "cvc3.gen"
+
+theory BuiltIn
+  meta "select_inst" "nothing"
+  meta "select_kept" "nothing"
+  meta "select_lskept" "goal"
+  meta "completion_mode" "only_kept"
+end
+
+(*
+Local Variables:
+mode: why
+compile-command: "unset LANG; make -C .. bench"
+End:
+*)

drivers/why3_smt.drv

@@ -9,8 +9,7 @@ transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "eliminate_algebraic_smt"
 
-transformation "encoding_smt_array"
-transformation "encoding_sort"
+transformation "encoding_smt"
 
 theory BuiltIn
   syntax type  int  "int"
@@ -19,4 +18,10 @@ theory BuiltIn
 
   meta "encoding : kept" type int
   meta "encoding : kept" type real
+
+
+  meta "select_inst" "goal"
+  meta "select_kept" "goal"
+  meta "select_lskept" "nothing"
+  meta "completion_mode" "only_kept"
 end

drivers/z3.drv

@@ -131,14 +131,6 @@ theory int.EuclideanDivision
    remove prop Div_1
 end
 
-theory transform.array.Array
-  syntax cloned logic get "(select %1 %2)"
-  syntax cloned logic set "(store %1 %2 %3)"
-  remove cloned prop Select_eq
-  remove cloned prop Select_neq
-
-end
-
 (*
 Local Variables:
 mode: why

drivers/z3_array.drv → drivers/z3_smtv1.drv

 (* Why driver for SMT syntax *)
 
 prelude ";;; this is a prelude for Z3"
+prelude "(set-logic AUFNIRA)"
 
-printer "smtv1"
+printer "smtv2"
 filename "%f-%t-%g.smt"
 
 valid "^unsat"
@@ -22,15 +23,12 @@ transformation "eliminate_algebraic_smt"
 transformation "simplify_formula"
 (*transformation "simplify_trivial_quantification"*)
 
-transformation "encoding_smt_array"
-transformation "encoding_sort"
+transformation "encoding_smt"
 
 theory BuiltIn
   syntax type int   "Int"
   syntax type real  "Real"
   syntax logic (=)  "(= %1 %2)"
-
-  meta "encoding : kept" type int
 end
 
 theory int.Int
@@ -65,6 +63,8 @@ theory int.Int
   remove prop NonTrivialRing
   remove prop CompatOrderAdd
 
+  meta "encoding : kept" type int
+
 end
 
 
@@ -131,12 +131,33 @@ theory int.EuclideanDivision
    remove prop Div_1
 end
 
-theory transform.array.Array
-  syntax cloned logic get "(select %1 %2)"
-  syntax cloned logic set "(store %1 %2 %3)"
-  remove cloned prop Select_eq
-  remove cloned prop Select_neq
+(*
+theory real.FromInt
+  syntax logic from_int "(from_int %1)"
+  remove prop Add
+  remove prop Sub
+  remove prop Mul
+  remove prop Neg
+end
+*)
+
+(*
+theory real.Truncate
+  syntax logic floor "(to_int %1)"
+  remove prop Floor_down
+  remove prop Floor_monotonic
+end
+*)
+
+theory array.Array
+  syntax type t "(Array %1 %2)"
+  meta "encoding : lskept" logic get
+  meta "encoding : lskept" logic set
+  meta "encoding : lskept" logic create_const
 
+  meta "smt_dist_syntax" logic get, "(select %1 %2)"
+  meta "smt_dist_syntax" logic set, "(store %1 %2 %3)"
+  meta "smt_dist_syntax" logic create_const, "(const[%t0] %1)"
 end
 
 (*

drivers/z3_smtv2.drv

 import "z3_smtv2.gen"
 
-transformation "encoding_smt"
-transformation "encoding_sort"
+theory BuiltIn
+  meta "select_inst" "nothing"
+  meta "select_kept" "nothing"
+  meta "select_lskept" "nothing"
+  meta "completion_mode" "nothing"
+end
 
 (*
 Local Variables:

drivers/z3_smtv2.gen

@@ -22,6 +22,7 @@ transformation "eliminate_algebraic_smt"
 
 transformation "simplify_formula"
 (*transformation "simplify_trivial_quantification"*)
+transformation "encoding_smt"
 
 theory BuiltIn
   syntax type int   "Int"
@@ -129,14 +130,6 @@ theory int.EuclideanDivision
    remove prop Div_1
 end
 
-theory transform.array.Array
-  syntax cloned logic get "(select %1 %2)"
-  syntax cloned logic set "(store %1 %2 %3)"
-  remove cloned prop Select_eq
-  remove cloned prop Select_neq
-
-end
-
 (*
 theory real.FromInt
   syntax logic from_int "(from_int %1)"

drivers/z3_smtv2_all_type.drv

+import "z3_smtv2.gen"
+
+theory BuiltIn
+  meta "select_inst" "nothing"
+  meta "select_kept" "goal"
+  meta "select_lskept" "nothing"
+  meta "completion_mode" "only_kept"
+end
+
+(*
+Local Variables:
+mode: why
+compile-command: "unset LANG; make -C .. bench"
+End:
+*)

drivers/z3_smtv2_array.drv

 import "z3_smtv2.gen"
 
-transformation "select_array_symbol_in_goal"
-transformation "instantiate_lsymbol"
-transformation "encoding_smt"
+theory BuiltIn
+  meta "select_inst" "goal"
+  meta "select_kept" "goal"
+  meta "select_lskept" "nothing"
+  meta "completion_mode" "only_kept"
+end
 
 (*
 Local Variables:

share/provers-detection-data.conf.in

@@ -38,7 +38,7 @@ version_regexp = "This is CVC3 version \\([^ \n]+\\)"
 version_ok = "2.2"
 version_old = "2.1"
 command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -timeout %t %f"
-driver = "drivers/cvc3.drv"
+driver = "drivers/cvc3_array.drv"
 
 [ATP yices]
 name = "Yices"
@@ -112,18 +112,6 @@ version_regexp = "Version: \\([^ \n\r]+\\)"
 command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
 driver = "drivers/verit.drv"
 
-[ATP z3_smtv1]
-name = "Z3_smtv1"
-exec = "z3"
-exec = "z3-2.2"
-version_switch = "-version"
-version_regexp = "Z3 version \\([^ \n\r]+\\)"
-version_old = "2.2"
-version_old = "2.1"
-version_old = "1.3"
-command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt %f"
-driver = "drivers/z3.drv"
-
 [ATP z3]
 name = "Z3"
 exec = "z3"
@@ -133,9 +121,24 @@ version_ok = "2.19"
 version_old = "2.18"
 version_old = "2.17"
 version_old = "2.16"
+version_bad = "2.2"
+version_bad = "2.1"
+version_bad = "1.3"
 command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt2 %f"
 driver = "drivers/z3_smtv2_array.drv"
 
+[ATP z3]
+name = "Z3 smtv1 no arrays"
+exec = "z3"
+exec = "z3-2.2"
+version_switch = "-version"
+version_regexp = "Z3 version \\([^ \n\r]+\\)"
+version_old = "2.2"
+version_old = "2.1"
+version_old = "1.3"
+command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt %f"
+driver = "drivers/z3.drv"
+
 [ITP coq]
 name = "Coq"
 exec = "coqc"

src/core/env.ml

@@ -138,7 +138,7 @@ let () = Exn_printer.register