some cosmetic changes in drivers

drivers/alt_ergo.drv

-
 (* Why driver for Alt-Ergo *)
 
 prelude "(* this is a prelude for Alt-Ergo*)"
@@ -21,6 +20,7 @@ transformation "eliminate_inductive"
 transformation "eliminate_algebraic"
 transformation "eliminate_if"
 transformation "eliminate_let"
+
 transformation "simplify_formula"
 transformation "simplify_trivial_quantification_in_goal"
 
@@ -125,8 +125,8 @@ end
 *)
 
 (*
-Local Variables: 
+Local Variables:
 mode: why
 compile-command: "make -C .. bench"
-End: 
+End:
 *)

drivers/cvc3.drv

-
 (* Why driver for SMT syntax *)
 
 prelude ";;; this is a prelude for CVC3 "
@@ -10,13 +9,14 @@ valid "unsat"
 unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
 
 (* À discuter *)
-transformation "simplify_recursive_definition"      
+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"
 
@@ -31,9 +31,10 @@ end
 
 theory int.Int
 
-  prelude ";;; this is a prelude for CVC3, Arithmetic"
+  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)"
@@ -62,11 +63,13 @@ theory int.Int
 
 end
 
+
 theory real.Real
 
-  prelude ";;; this is a prelude for Z3, Arithmetic"
+  prelude ";;; this is a prelude for CVC3 real arithmetic"
 
-  syntax logic zero "0"
+  syntax logic zero "0.0"
+  syntax logic one  "1.0"
 
   syntax logic (+)  "(+ %1 %2)"
   syntax logic (-)  "(- %1 %2)"
@@ -107,14 +110,24 @@ theory bool.Bool
    syntax logic andb  "(and %1 %2)"
    syntax logic orb   "(or %1 %2)"
    syntax logic xorb  "(xor %1 %2)"
-   syntax logic notb  "(not %1)" 
+   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: 
+Local Variables:
 mode: why
-compile-command: "make -C ../.. bench"
-End: 
+compile-command: "unset LANG; make -C .. bench"
+End:
 *)

drivers/simplify.drv

-
 (* Why driver for Simplify *)
 
 prelude ";;; this is a prelude for Simplify"
@@ -9,7 +8,7 @@ filename "%f-%t-%g.sx"
 valid "\\bValid\\b"
 unknown "\\bInvalid\\b" "Unknown"
 
-transformation "simplify_recursive_definition"      
+transformation "simplify_recursive_definition"
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"
@@ -18,6 +17,7 @@ transformation "eliminate_inductive"
 transformation "eliminate_algebraic"
 transformation "eliminate_if"
 transformation "eliminate_let"
+
 transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
 
@@ -27,24 +27,18 @@ transformation "remove_triggers"
 trigger they can't appear since = can't appear *)
 (*transformation "filter_trigger_builtin"*)
 
-(* Add the projections for enumeration types*)
-transformation "encoding_enumeration"
-
-(* encode the polymorphism and sort *)
-(*transformation "encoding_decorate_mono"*)
-transformation "explicit_polymorphism"
+transformation "encoding_tptp"
 
 theory BuiltIn
-  syntax type int   "Int"
-  syntax type real  "Real"
   syntax logic (=)  "(EQ %1 %2)"
 end
 
 theory int.Int
 
-  prelude ";;; this is a prelude for Simplify, Arithmetic"
+  prelude ";;; this is a prelude for Simplify integer arithmetic"
 
   syntax logic zero "0"
+  syntax logic one  "1"
 
   syntax logic (+)  "(+ %1 %2)"
   syntax logic (-)  "(- %1 %2)"
@@ -68,11 +62,12 @@ theory int.Int
   remove prop Trans
   remove prop Antisymm
   remove prop Total
+
 end
 
 (*
-Local Variables: 
+Local Variables:
 mode: why
 compile-command: "make -C .. bench"
-End: 
+End:
 *)

drivers/tptp.drv

-
 (* Why driver for tptp first-order logic solvers *)
 
 prelude "% this is a why prelude for tptp solvers
-fof(two_constants, axiom, ~ ('0' = '1')).
-"
+fof(two_constants, axiom, ~ ('0' = '1'))."
 
 printer "tptp"
 filename "%f-%t-%g.p"
 
-valid "Proof found"
+valid   "Proof found"
 invalid "Completion found"
-fail "Failure" "Failure"
-unknown "No Proof Found" "Unknown"
-timeout "Resource limit exceeded"
 timeout "Ran out of time"
+timeout "Resource limit exceeded"
+unknown "No Proof Found"            "Unknown"
+fail    "Failure"                   "Failure"
 
 (* to be improved *)
 
@@ -27,13 +25,9 @@ transformation "eliminate_algebraic"
 transformation "eliminate_if"
 transformation "eliminate_let"
 
-(* Add the projections for enumeration types*)
-transformation "encoding_enumeration"
-transformation "explicit_polymorphism"
+transformation "encoding_tptp"
 
 theory BuiltIn
-  syntax type int   "Int"
-  syntax type real  "Real"
   syntax logic (=)  "(%1 = %2)"
 end
 
@@ -43,5 +37,3 @@ mode: why
 compile-command: "unset LANG; make -C .. bench"
 End:
 *)
-(* vim:syntax=ocaml
-*)

drivers/tptp_simple.drv

-
-(* Why driver for tptp first-order logic solvers *)
-
-prelude "% this is a why prelude for tptp solvers
-fof(two_constants, axiom, ~ ('0' = '1')).
-"
-
-printer "tptp"
-filename "%f-%t-%g.p"
-
-valid "Proof found"
-invalid "Completion found"
-fail "Failure" "Failure"
-unknown "No Proof Found" "Unknown"
-timeout "Resource limit exceeded"
-timeout "Ran out of time"
-
-(* to be improved *)
-
-transformation "simplify_recursive_definition"
-transformation "inline_trivial"
-
-transformation "eliminate_builtin"
-transformation "eliminate_definition"
-transformation "eliminate_inductive"
-transformation "eliminate_algebraic"
-transformation "eliminate_if"
-transformation "eliminate_let"
-
-(* Add the projections for enumeration types*)
-transformation "encoding_enumeration"
-transformation "explicit_polymorphism"
-transformation "encoding_simple"
-
-theory BuiltIn
-  syntax type int   "Int"
-  syntax type real  "Real"
-  syntax logic (=)  "(%1 = %2)"
-end
-
-(*
-Local Variables:
-mode: why
-compile-command: "unset LANG; make -C .. bench"
-End:
-*)
-(* vim:syntax=ocaml
-*)

drivers/why3.drv

+(* Why driver for Why3 syntax *)
+
 printer "why3"
 filename "%f-%t-%g.why"
 

drivers/why3_inline_all.drv

-printer "why3"
-filename "%f-%t-%g.why"
-
-(* À discuter *)
-transformation "simplify_recursive_definition"      
-transformation "inline_all"
-
-theory BuiltIn
-  syntax type  int  "int"
-  syntax type  real "real"
-  syntax logic (=)  "(%1 = %2)"
-end

drivers/why3_encoding_decorate.drv → drivers/why3_smt.drv

+(* Why driver for Why3 syntax *)
+
 printer "why3"
 filename "%f-%t-%g.why"
 
@@ -5,8 +7,6 @@ transformation "eliminate_builtin"
 transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "eliminate_algebraic"
-transformation "eliminate_if"
-transformation "eliminate_let"
 
 transformation "encoding_smt"
 
@@ -14,4 +14,7 @@ theory BuiltIn
   syntax type  int  "int"
   syntax type  real "real"
   syntax logic (=)  "(%1 = %2)"
+
+  meta "encoding : kept" type int
+  meta "encoding : kept" type real
 end

drivers/why3_total_elimination.drv → drivers/why3_tptp.drv

+(* Why driver for Why3 syntax *)
+
 printer "why3"
 filename "%f-%t-%g.why"
 
@@ -5,13 +7,9 @@ transformation "eliminate_builtin"
 transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "eliminate_algebraic"
-transformation "eliminate_if"
-transformation "eliminate_let"
-transformation "simplify_formula"
-transformation "simplify_trivial_quantification"
+
+transformation "encoding_tptp"
 
 theory BuiltIn
-  syntax type  int  "int"
-  syntax type  real "real"
   syntax logic (=)  "(%1 = %2)"
 end

drivers/z3.drv

-
 (* Why driver for SMT syntax *)
 
 prelude ";;; this is a prelude for Z3"
@@ -10,19 +9,19 @@ valid "^unsat"
 unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
 
 (* À discuter *)
-transformation "simplify_recursive_definition"      
+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_smt"
 transformation "encoding_simple2"
-(* transformation "encoding_decorate_every_simple" *)
 
 theory BuiltIn
   syntax type int   "Int"
@@ -30,12 +29,12 @@ theory BuiltIn
   syntax logic (=)  "(= %1 %2)"
 end
 
-
 theory int.Int
 
-  prelude ";;; this is a prelude for Z3, Arithmetic"
-  
+  prelude ";;; this is a prelude for Z3 integer arithmetic"
+
   syntax logic zero "0"
+  syntax logic one  "1"
 
   syntax logic (+)  "(+ %1 %2)"
   syntax logic (-)  "(- %1 %2)"
@@ -67,9 +66,10 @@ end
 
 theory real.Real
 
-  prelude ";;; this is a prelude for Z3, Arithmetic"
+  prelude ";;; this is a prelude for Z3 real arithmetic"
 
-  syntax logic zero "0"
+  syntax logic zero "0.0"
+  syntax logic one  "1.0"
 
   syntax logic (+)  "(+ %1 %2)"
   syntax logic (-)  "(- %1 %2)"
@@ -110,7 +110,7 @@ theory bool.Bool
    syntax logic andb  "(and %1 %2)"
    syntax logic orb   "(or %1 %2)"
    syntax logic xorb  "(xor %1 %2)"
-   syntax logic notb  "(not %1)" 
+   syntax logic notb  "(not %1)"
    meta cloned "encoding_decorate : kept" type bool
 end
 *)
@@ -126,8 +126,8 @@ theory int.EuclideanDivision
 end
 
 (*
-Local Variables: 
+Local Variables:
 mode: why
 compile-command: "unset LANG; make -C .. bench"
-End: 
+End:
 *)