Commit ca87ca91 authored by Andrei Paskevich's avatar Andrei Paskevich

change z3 and cvc3 prover identifiers, accept alt-ergo 0.93

parent c0be075f
(* Why driver for Alt-Ergo *)
import "alt_ergo_bare.drv"
prelude "(* this is a prelude for Alt-Ergo*)"
theory map.Map
syntax type map "(%1,%2) farray"
printer "alt-ergo"
filename "%f-%t-%g.why"
valid "Valid"
invalid "Invalid"
unknown "I don't know" "Unknown"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (%s)"
time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "split_premise"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax predicate (=) "(%1 = %2)"
end
theory int.Int
prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (-_) "(-%1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%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 Total
remove prop Antisymm
remove prop NonTrivialRing
remove prop CompatOrderAdd
end
theory int.EuclideanDivision
syntax function div "(%1 / %2)"
syntax function mod "(%1 % %2)"
end
theory real.Real
prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (/) "(%1 / %2)"
syntax function (-_) "(-%1)"
syntax function inv "(1.0 / %1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%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 Total
remove prop Antisymm
remove prop Inverse
remove prop NonTrivialRing
remove prop CompatOrderAdd
end
theory real.RealInfix
syntax function (+.) "(%1 + %2)"
syntax function (-.) "(%1 - %2)"
syntax function ( *.) "(%1 * %2)"
syntax function (/.) "(%1 / %2)"
syntax function (-._) "(-%1)"
syntax predicate (<=.) "(%1 <= %2)"
syntax predicate (<.) "(%1 < %2)"
syntax predicate (>=.) "(%1 >= %2)"
syntax predicate (>.) "(%1 > %2)"
end
theory bool.Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
end
theory Tuple0
syntax type tuple0 "unit"
syntax function Tuple0 "void"
end
theory algebra.AC
meta cloned AC function op
remove cloned prop Comm.Comm
remove cloned prop Assoc.Assoc
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
end
(*
......
(* Why driver for Alt-Ergo *)
prelude "(* this is a prelude for Alt-Ergo*)"
printer "alt-ergo"
filename "%f-%t-%g.why"
valid "Valid"
invalid "Invalid"
unknown "I don't know" "Unknown"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
time "Valid (%s)"
time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "split_premise"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax predicate (=) "(%1 = %2)"
end
theory int.Int
prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (-_) "(-%1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%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 Total
remove prop Antisymm
remove prop NonTrivialRing
remove prop CompatOrderAdd
end
theory int.EuclideanDivision
syntax function div "(%1 / %2)"
syntax function mod "(%1 % %2)"
end
theory real.Real
prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
syntax function zero "0.0"
syntax function one "1.0"
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (/) "(%1 / %2)"
syntax function (-_) "(-%1)"
syntax function inv "(1.0 / %1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%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 Total
remove prop Antisymm
remove prop Inverse
remove prop NonTrivialRing
remove prop CompatOrderAdd
end
theory real.RealInfix
syntax function (+.) "(%1 + %2)"
syntax function (-.) "(%1 - %2)"
syntax function ( *.) "(%1 * %2)"
syntax function (/.) "(%1 / %2)"
syntax function (-._) "(-%1)"
syntax predicate (<=.) "(%1 <= %2)"
syntax predicate (<.) "(%1 < %2)"
syntax predicate (>=.) "(%1 >= %2)"
syntax predicate (>.) "(%1 > %2)"
end
theory bool.Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
end
theory Tuple0
syntax type tuple0 "unit"
syntax function Tuple0 "void"
end
theory algebra.AC
meta cloned AC function op
remove cloned prop Comm.Comm
remove cloned prop Assoc.Assoc
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
import "alt_ergo.drv"
theory map.Map
syntax type map "(%1,%2) farray"
syntax function get "(%1[%2])"
syntax function set "(%1[%2 <- %3])"
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
......@@ -5,7 +5,7 @@
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
version="0.94"/>
<prover
id="alt-ergo-0.93.1"
name="Alt-Ergo"
......@@ -15,7 +15,7 @@
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
......@@ -51,7 +51,7 @@
name="Yices"
version="1.0.25"/>
<prover
id="z3"
id="z3-2"
name="Z3"
version="2.19"/>
<prover
......@@ -68,30 +68,30 @@
expanded="true">
<goal
name="toto"
sum="59cafced2f6bc3b8459444b6a68d53c8"
sum="165013fe8031c756d7de7572f7f8946f"
proved="true"
expanded="true"
shape="ainfix <V0ainfix +aroundaUpV0c1.F">
<proof
prover="cvc3"
prover="z3-2"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
prover="cvc3-2.2"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
prover="alt-ergo"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="gappa"
......
......@@ -11,7 +11,7 @@
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
......@@ -43,7 +43,7 @@
name="Yices"
version="1.0.25"/>
<prover
id="z3"
id="z3-2"
name="Z3"
version="2.19"/>
<file
......
......@@ -11,7 +11,7 @@
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
......@@ -43,7 +43,7 @@
name="Yices"
version="1.0.25"/>
<prover
id="z3"
id="z3-2"
name="Z3"
version="2.19"/>
<file
......@@ -61,7 +61,7 @@
expanded="true"
shape="ainfix =afV0V1afV1V0F">
<proof
prover="cvc3"
prover="cvc3-2.2"
timelimit="10"
edited=""
obsolete="false">
......@@ -75,7 +75,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="z3"
prover="z3-2"
timelimit="10"
edited=""
obsolete="false">
......@@ -96,7 +96,7 @@
expanded="true"
shape="ainfix =afafV0V1V2afV0afV1V2F">
<proof
prover="cvc3"
prover="cvc3-2.2"
timelimit="10"
edited=""
obsolete="false">
......@@ -110,7 +110,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
prover="z3-2"
timelimit="10"
edited=""
obsolete="false">
......
......@@ -5,15 +5,23 @@
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
version="0.94"/>
<prover
id="alt-ergo-0.93.1"
name="Alt-Ergo"
version="0.93.1"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
......@@ -43,9 +51,13 @@
name="Yices"
version="1.0.25"/>
<prover
id="z3"
id="z3-2"
name="Z3"
version="2.19"/>
<prover
id="z3-3"
name="Z3"
version="3.2"/>
<file
name="../array.why"
verified="true"
......@@ -56,26 +68,26 @@
expanded="true">
<goal
name="G1"
sum="bacc88b1086b3ebd586dbbaca50d4fee"
sum="589d57410c730650567c090856fb4f1f"
proved="true"
expanded="true"
shape="ainfix =agetasetV2V1V0V1V0FF">
<proof
prover="cvc3"
prover="z3-2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="cvc3-2.2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
......@@ -91,26 +103,26 @@
</goal>
<goal
name="G2"
sum="d0b4373dd121cec555de03978775b663"
sum="310823a6ed0f7beadc64c708369dd65b"
proved="true"
expanded="true"
shape="ainfix =agetasetV5V0V4V3V1Iainfix =agetV5V3V1Iainfix =V3V0NFF">
<proof
prover="cvc3"
prover="z3-2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="alt-ergo"
prover="cvc3-2.2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
......@@ -121,31 +133,31 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="G3"
sum="6ae604e4f05d34cfca040accc5548015"
sum="810f5223114ce85ada728907bee101ff"
proved="true"
expanded="true"
shape="ainfix =agetasetV2c1V1c0V0Iainfix =agetV2c0V0FF">
<proof
prover="cvc3"
prover="z3-2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="cvc3-2.2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
......@@ -156,31 +168,31 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.15"/>
<result status="valid" time="0.14"/>
</proof>
</goal>
<goal
name="G4"
sum="4b8d214718d344bac7b206bb433df5ea"
sum="ce6d85ded5b6a4dfe2bd82631dec3a7b"
proved="true"
expanded="true"
shape="ainfix =agetasetasetV2c1V1c0V0c1V1FF">
<proof
prover="cvc3"
prover="z3-2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="alt-ergo"
prover="cvc3-2.2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
......@@ -191,7 +203,7 @@
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.19"/>
<result status="valid" time="0.22"/>
</proof>
</goal>
</theory>
......
......@@ -11,7 +11,7 @@
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
......@@ -43,7 +43,7 @@
name="Yices"
version="1.0.25"/>
<prover
id="z3"
id="z3-2"
name="Z3"
version="2.19"/>
<file
......@@ -61,7 +61,7 @@
expanded="true"
shape="ainfix =aTrueaFalseN">
<proof
prover="cvc3"
prover="cvc3-2.2"
timelimit="10"
edited=""
obsolete="false">
......@@ -75,7 +75,7 @@
<result status="valid" time="0.00"/>
</proof>
<proof
prover="z3"
prover="z3-2"
timelimit="10"
edited=""
obsolete="false">
......@@ -96,7 +96,7 @@
expanded="true"
shape="ainfix =V0aFalseOainfix =V0aTrueF">
<proof
prover="cvc3"
prover="cvc3-2.2"
timelimit="10"
edited=""
obsolete="false">
......@@ -110,7 +110,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="z3"
prover="z3-2"
timelimit="10"
edited=""
obsolete="false">
......@@ -131,7 +131,7 @@
expanded="true"
shape="fIainfix =V2V0NAainfix =V1V2NAainfix =V0V1NF">
<proof
prover="cvc3"
prover="cvc3-2.2"
timelimit="10"
edited=""
obsolete="false">
......@@ -145,7 +145,7 @@
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="z3"
prover="z3-2"
timelimit="10"
edited=""
obsolete="false">
......
......@@ -5,15 +5,23 @@
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
version="0.94"/>
<prover
id="alt-ergo-0.93.1"
name="Alt-Ergo"
version="0.93.1"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
id="cvc3-2.4"