fixed drivers for division

drivers/alt_ergo.drv

@@ -7,14 +7,36 @@ theory BuiltIn
   meta "eliminate_algebraic" "keep_recs"
 end
 
-(* 
+
 theory int.EuclideanDivision
 
-  syntax function div "(%1 / %2)"
-  syntax function mod "(%1 % %2)"
+  (* protection against wrongs semantics for negative arguments *)
+
+  prelude "logic safe_div: int, int -> int"
+  prelude "axiom safe_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_div(x,y) = x / y"
+
+  prelude "logic safe_mod: int, int -> int"
+  prelude "axiom safe_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_mod(x,y) = x % y"
+
+  syntax function div "safe_div(%1,%2)"
+  syntax function mod "safe_mod(%1,%2)"
+
+end
+
+theory int.ComputerDivision
+
+  (* protection against wrongs semantics for negative arguments *)
+
+  prelude "logic safe_div: int, int -> int"
+  prelude "axiom safe_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_div(x,y) = x / y"
+
+  prelude "logic safe_mod: int, int -> int"
+  prelude "axiom safe_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_mod(x,y) = x % y"
+
+  syntax function div "safe_div(%1,%2)"
+  syntax function mod "safe_mod(%1,%2)"
 
 end
-*)
 
 theory map.Map
   syntax type  map "(%1,%2) farray"

drivers/alt_ergo_0.94.drv

@@ -10,18 +10,36 @@ theory BuiltIn
   meta "eliminate_algebraic" "keep_recs"
 end
 
-(*
-
 theory int.EuclideanDivision
 
-  (* workaround for the "-1 % 32 = -1" bug *)
-  prelude "logic safe_modulo: int, int -> int"
-  prelude "axiom safe_modulo_def: forall x, y:int. x >= 0 and y > 0 -> safe_modulo(x,y) = x % y"
-  syntax function div "(%1 / %2)"
-  syntax function mod "safe_modulo(%1,%2)"
+  (* protection against wrongs semantics for negative arguments *)
+
+  prelude "logic safe_div: int, int -> int"
+  prelude "axiom safe_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_div(x,y) = x / y"
+
+  prelude "logic safe_mod: int, int -> int"
+  prelude "axiom safe_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_mod(x,y) = x % y"
+
+  syntax function div "safe_div(%1,%2)"
+  syntax function mod "safe_mod(%1,%2)"
 
 end
-*)
+
+theory int.ComputerDivision
+
+  (* protection against wrongs semantics for negative arguments *)
+
+  prelude "logic safe_div: int, int -> int"
+  prelude "axiom safe_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_div(x,y) = x / y"
+
+  prelude "logic safe_mod: int, int -> int"
+  prelude "axiom safe_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_mod(x,y) = x % y"
+
+  syntax function div "safe_div(%1,%2)"
+  syntax function mod "safe_mod(%1,%2)"
+
+end
+
 
 (*
 Local Variables:

drivers/alt_ergo_smt2.drv

@@ -69,13 +69,6 @@ theory int.Int
 
 end
 
-theory int.EuclideanDivision
-
-  syntax function div "(div %1 %2)"
-  syntax function mod "(mod %1 %2)"
-
-end
-
 theory real.Real
 
   prelude ";;; this is a prelude for Alt-Ergo real arithmetic"

drivers/cvc3_bare.drv

@@ -146,17 +146,6 @@ theory bool.Bool
    syntax function notb  "(~ %1)"
 end
 
-(*
-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 map.Map
   syntax type map "(ARRAY %1 OF %2)"

drivers/cvc4_bare.drv

@@ -152,7 +152,9 @@ theory bool.Bool
 end
 *)
 
-(* CVC4 division does not seem to be the Euclidean one
+(* CVC4 division seems to be neither the Euclidean one,
+nor the Computer one *)
+(*
 theory int.EuclideanDivision
    syntax function div "(div %1 %2)"
    syntax function mod "(mod %1 %2)"
@@ -161,8 +163,18 @@ theory int.EuclideanDivision
    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
 *)
 
+
 (*
 theory real.Truncate
   syntax function floor "(to_int %1)"

drivers/verit.drv

@@ -129,17 +129,6 @@ theory bool.Bool
 end
 
 
-(* needs to checked
-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
-*)
-
 (*
 Local Variables:
 mode: why

drivers/yices_bare.drv

@@ -133,18 +133,6 @@ theory bool.Bool
 end
 
 
-(* needs to be checked
-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 map.Map
   syntax type map "(-> %1 %2)"
   meta "encoding : lskept" function get

drivers/z3_bare.drv

@@ -132,7 +132,7 @@ theory bool.Bool
    syntax function implb "(=> %1 %2)"
 end
 
-(* needs to be checked
+(* div/mod of Z3 seems to be Euclidean Division *)
 theory int.EuclideanDivision
    syntax function div "(div %1 %2)"
    syntax function mod "(mod %1 %2)"
@@ -141,7 +141,6 @@ theory int.EuclideanDivision
    remove prop Mod_1
    remove prop Div_1
 end
-*)
 
 theory real.FromInt
   syntax function from_int "(to_real %1)"

drivers/z3_smtv1.drv

@@ -132,17 +132,6 @@ end
 *)
 
 
-(* needs to be checked
-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
-*)
-
 (*
 Local Variables:
 mode: why

examples/bitvectors/neg_as_xor/why3session.xml

@@ -7,33 +7,37 @@
   version="0.94"/>
  <prover
   id="1"
+  name="Alt-Ergo"
+  version="0.95"/>
+ <prover
+  id="2"
   name="Coq"
   version="8.3pl4"/>
  <prover
-  id="2"
+  id="3"
   name="Z3"
   version="2.19"/>
  <prover
-  id="3"
+  id="4"
   name="Z3"
   version="3.2"/>
  <file
   name="../neg_as_xor.why"
-  verified="false"
-  expanded="false">
+  verified="true"
+  expanded="true">
   <theory
    name="TestNegAsXOR"
    locfile="../neg_as_xor.why"
    loclnum="2" loccnumb="7" loccnume="19"
-   verified="false"
+   verified="true"
    expanded="true">
    <goal
     name="Nth_j"
     locfile="../neg_as_xor.why"
     loclnum="13" loccnumb="8" loccnume="13"
     sum="ffa7aadc98c7c81aa8afa142b455755d"
-    proved="false"
-    expanded="false"
+    proved="true"
+    expanded="true"
     shape="ainfix =anthajV0aFalseIainfix &lt;=V0c62Aainfix &lt;=c0V0F">
     <proof
      prover="0"
@@ -43,6 +47,14 @@
      archived="false">
      <result status="timeout" time="5.03"/>
     </proof>
+    <proof
+     prover="1"
+     timelimit="3"
+     memlimit="1000"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.83"/>
+    </proof>
    </goal>
    <goal
     name="sign_of_j"
@@ -78,7 +90,7 @@
      <result status="valid" time="0.06"/>
     </proof>
     <proof
-     prover="2"
+     prover="3"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -86,7 +98,7 @@
      <result status="valid" time="0.69"/>
     </proof>
     <proof
-     prover="3"
+     prover="4"
      timelimit="10"
      memlimit="1000"
      obsolete="false"
@@ -111,7 +123,7 @@
      <result status="valid" time="0.07"/>
     </proof>
     <proof
-     prover="2"
+     prover="3"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -119,7 +131,7 @@
      <result status="valid" time="0.71"/>
     </proof>
     <proof
-     prover="3"
+     prover="4"
      timelimit="11"
      memlimit="1000"
      obsolete="false"
@@ -144,7 +156,7 @@
      <result status="valid" time="0.04"/>
     </proof>
     <proof
-     prover="2"
+     prover="3"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -152,7 +164,7 @@
      <result status="valid" time="0.11"/>
     </proof>
     <proof
-     prover="3"
+     prover="4"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -211,7 +223,7 @@
      <result status="valid" time="0.03"/>
     </proof>
     <proof
-     prover="2"
+     prover="3"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -219,7 +231,7 @@
      <result status="valid" time="0.00"/>
     </proof>
     <proof
-     prover="3"
+     prover="4"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -244,7 +256,7 @@
      <result status="valid" time="0.92"/>
     </proof>
     <proof
-     prover="2"
+     prover="3"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -252,7 +264,7 @@
      <result status="valid" time="0.71"/>
     </proof>
     <proof
-     prover="3"
+     prover="4"
      timelimit="10"
      memlimit="1000"
      obsolete="false"
@@ -277,7 +289,7 @@
      <result status="valid" time="0.58"/>
     </proof>
     <proof
-     prover="2"
+     prover="3"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -285,7 +297,7 @@
      <result status="valid" time="0.72"/>
     </proof>
     <proof
-     prover="3"
+     prover="4"
      timelimit="10"
      memlimit="1000"
      obsolete="false"
@@ -310,7 +322,7 @@
      <result status="valid" time="1.77"/>
     </proof>
     <proof
-     prover="2"
+     prover="3"
      timelimit="5"
      memlimit="1000"
      obsolete="false"
@@ -318,7 +330,7 @@
      <result status="valid" time="0.97"/>
     </proof>
     <proof
-     prover="3"
+     prover="4"
      timelimit="10"
      memlimit="1000"
      obsolete="false"
@@ -352,7 +364,7 @@
     expanded="true"
     shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix &lt;aexpV0c2047Aainfix &lt;c0aexpV0F">
     <proof
-     prover="1"
+     prover="2"
      timelimit="5"
      memlimit="1000"
      edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"