Merge branch 'topic/526-kanig-unused' into 'master'

Remove unused constants in SPARK VCs

Issue: eng/spark/spark2014#526

See merge request eng/spark/why3!53

drivers/alt-ergo_gnatprove.drv

@@ -1,6 +1,6 @@
 import "alt_ergo_fp.drv"
 
-transformation "remove_unused_keep_constants"
+transformation "remove_unused"
 
 theory ieee_float.GenericFloat
  remove prop abs_special

drivers/colibri.drv

@@ -43,7 +43,7 @@ theory int.Int
   remove prop CompatOrderMult
 end
 
-transformation "remove_unused_keep_constants"
+transformation "remove_unused"
 (* Performed introductions depending on whether counterexamples are
    requested, as said by the meta "get_counterexmp". When this meta
    set, this transformation introduces the model variables that are

drivers/cvc5.drv

@@ -1,32 +1,4 @@
-(** Why3 driver for CVC5 1.0.0 *)
-
-prelude ";; produced by cvc5.drv ;;"
-prelude "(set-logic ALL)"
-prelude "(set-info :smt-lib-version 2.6)"
-
-unknown "^(error \"Can't get-info :reason-unknown when the last result wasn't unknown!\")$" "(not unknown!)"
-
-outofmemory "cvc5 suffered a segfault"
-outofmemory "cvc5::internal::Minisat::OutOfMemoryException"
-
-steps "resource::resourceUnitsUsed = \\([0-9]+\\)" 1
-
-theory BuiltIn
-  meta "supports_smt_get_info_unknown_reason" ""
-end
-
-import "smt-libv2.gen"
-filename "%f-%t-%g.smt2"
-printer "smtv2.6"
-import "smt-libv2-bv.gen"
-import "cvc4_bv.gen"
-import "smt-libv2-floats.gen"
-
-import "discrimination.gen"
-theory BuiltIn
-  meta "select_alginst_default" "local"
-  meta "eliminate_algebraic" "keep_mono"
-end
+import "cvc5.gen"
 
 (* Performed introductions depending on whether counterexamples are
    requested, as said by the meta "get_counterexmp". When this meta
@@ -57,49 +29,3 @@ transformation "discriminate_if_poly"
 transformation "eliminate_algebraic_if_poly"
 transformation "encoding_smt_if_poly"
 
-(** Error messages specific to CVC4 *)
-
-outofmemory "(error \".*out of memory\")"
-outofmemory "CVC4 suffered a segfault"
-outofmemory "CVC4::BVMinisat::OutOfMemoryException"
-outofmemory "std::bad_alloc"
-outofmemory "Cannot allocate memory"
-timeout "interrupted by timeout"
-steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
-(*
-specific output message when CVC4 reaches its resource limit
-*)
-steplimitexceeded "unknown (RESOURCEOUT)"
-
-theory real.Real
-  remove prop add_div
-  remove prop sub_div
-  remove prop neg_div
-  remove prop assoc_mul_div
-  remove prop assoc_div_mul
-  remove prop assoc_div_div
-  remove prop CompatOrderMult
-end
-
-(** Extra theories supported by CVC4 *)
-
-(* CVC4 division seems to be the Euclidean one, not the Computer one *)
-theory int.EuclideanDivision
-  syntax function div "(div %1 %2)"
-  syntax function mod "(mod %1 %2)"
-  remove prop Mod_bound
-  remove prop Div_mod
-  remove prop Mod_1
-  remove prop Div_1
-end
-
-(*
-theory int.ComputerDivision
-  syntax function div "(div %1 %2)"
-  syntax function mod "(mod %1 %2)"
-  remove prop Mod_bound
-  remove prop Div_mod
-  remove prop Mod_1
-  remove prop Div_1
-end
-*)

drivers/cvc5.gen

@@ -0,0 +1,76 @@
+(** Why3 driver for CVC5 1.0.0 *)
+
+prelude ";; produced by cvc5.drv ;;"
+prelude "(set-logic ALL)"
+prelude "(set-info :smt-lib-version 2.6)"
+
+unknown "^(error \"Can't get-info :reason-unknown when the last result wasn't unknown!\")$" "(not unknown!)"
+
+outofmemory "cvc5 suffered a segfault"
+outofmemory "cvc5::internal::Minisat::OutOfMemoryException"
+
+steps "resource::resourceUnitsUsed = \\([0-9]+\\)" 1
+
+theory BuiltIn
+  meta "supports_smt_get_info_unknown_reason" ""
+end
+
+import "smt-libv2.gen"
+filename "%f-%t-%g.smt2"
+printer "smtv2.6"
+import "smt-libv2-bv.gen"
+import "cvc4_bv.gen"
+import "smt-libv2-floats.gen"
+
+import "discrimination.gen"
+theory BuiltIn
+  meta "select_alginst_default" "local"
+  meta "eliminate_algebraic" "keep_mono"
+end
+
+(** Error messages specific to CVC4 *)
+
+outofmemory "(error \".*out of memory\")"
+outofmemory "CVC4 suffered a segfault"
+outofmemory "CVC4::BVMinisat::OutOfMemoryException"
+outofmemory "std::bad_alloc"
+outofmemory "Cannot allocate memory"
+timeout "interrupted by timeout"
+steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
+(*
+specific output message when CVC4 reaches its resource limit
+*)
+steplimitexceeded "unknown (RESOURCEOUT)"
+
+theory real.Real
+  remove prop add_div
+  remove prop sub_div
+  remove prop neg_div
+  remove prop assoc_mul_div
+  remove prop assoc_div_mul
+  remove prop assoc_div_div
+  remove prop CompatOrderMult
+end
+
+(** Extra theories supported by CVC4 *)
+
+(* CVC4 division seems to be the Euclidean one, not the Computer one *)
+theory int.EuclideanDivision
+  syntax function div "(div %1 %2)"
+  syntax function mod "(mod %1 %2)"
+  remove prop Mod_bound
+  remove prop Div_mod
+  remove prop Mod_1
+  remove prop Div_1
+end
+
+(*
+theory int.ComputerDivision
+  syntax function div "(div %1 %2)"
+  syntax function mod "(mod %1 %2)"
+  remove prop Mod_bound
+  remove prop Div_mod
+  remove prop Mod_1
+  remove prop Div_1
+end
+*)

drivers/cvc5_gnatprove.drv

@@ -1,10 +1,39 @@
-import "cvc5.drv"
+import "cvc5.gen"
 import "smt-libv2-gnatprove.gen"
 import "smt-libv2-floats-gnatprove.gen"
 import "smt-libv2-floats-int_via_real.gen"
 
 steps "resource::resourceUnitsUsed = \\([0-9]+.?[0-9]*\\)" 1
 
+(* Performed introductions depending on whether counterexamples are
+   requested, as said by the meta "get_counterexmp". When this meta
+   set, this transformation introduces the model variables that are
+   still embedded in the goal. When it is not set, it removes all
+   these unused-ce-related variables, even in the context.  *)
+transformation "counterexamples_dependent_intros"
+
+transformation "inline_trivial"
+transformation "eliminate_builtin"
+transformation "remove_unused"
+transformation "detect_polymorphism"
+transformation "eliminate_definition_conditionally"
+transformation "eliminate_inductive"
+transformation "eliminate_gnatprove_guard_epsilon"
+transformation "eliminate_epsilon"
+transformation "eliminate_literal"
+transformation "simplify_formula"
+
+(* Prepare for counter-example query: get rid of some quantifiers
+   (makes it possible to query model values of the variables in
+   premises) and introduce counter-example projections.  Note: does
+   nothing if meta get_counterexmp is not set *)
+transformation "prepare_for_counterexmp"
+
+transformation "eliminate_projections_sums"
+transformation "discriminate_if_poly"
+transformation "eliminate_algebraic_if_poly"
+transformation "encoding_smt_if_poly"
+
 theory int.Abs
   syntax function abs "(abs %1)"
 

drivers/z3_gnatprove.drv

@@ -23,7 +23,7 @@ model_parser "smtv2"
 
 transformation "inline_trivial"
 transformation "eliminate_builtin"
-transformation "remove_unused_keep_constants"
+transformation "remove_unused"
 transformation "detect_polymorphism"
 transformation "eliminate_inductive"
 transformation "eliminate_algebraic_if_poly"