Commit d95ebb61 authored by François Bobot's avatar François Bobot

alt-ergo : use polymorph array for the trunk version

parent f05fb27f
(* 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 "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (=) "(%1 = %2)"
end
theory int.Int
prelude "(* this is a prelude for Alt-Ergo 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 Total
remove prop Antisymm
remove prop NonTrivialRing
remove prop CompatOrderAdd
end
theory int.EuclideanDivision
syntax logic div "(%1 / %2)"
syntax logic mod "(%1 % %2)"
end
theory real.Real
prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
syntax logic zero "0.0"
syntax logic one "1.0"
syntax logic (+) "(%1 + %2)"
syntax logic (-) "(%1 - %2)"
syntax logic (*) "(%1 * %2)"
syntax logic (/) "(%1 / %2)"
syntax logic (-_) "(-%1)"
syntax logic inv "(1.0 / %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 Total
remove prop Antisymm
remove prop Inverse
remove prop NonTrivialRing
remove prop CompatOrderAdd
end
theory real.RealInfix
syntax logic (+.) "(%1 + %2)"
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)"
end
theory bool.Bool
syntax type bool "bool"
syntax logic True "true"
syntax logic False "false"
end
theory Tuple0
syntax type tuple0 "unit"
syntax logic Tuple0 "void"
end
theory algebra.AC
meta cloned AC logic op
remove cloned prop Comm.Comm
remove cloned prop Assoc.Assoc
end
theory array.Array
syntax type t "(%1,%2) farray"
syntax logic get "(%1[%2])"
syntax logic set "(%1[%2 <- %3])"
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
......@@ -14,6 +14,18 @@ version_old = "0.8"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo.drv"
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "ergo"
exec = "alt-ergo"
exec = "alt-ergo-0.91"
version_switch = "-version"
version_regexp = ".*Ergo \\([^ \n]*\\)"
version_ok = "0.92.3"
command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/alt_ergo_trunk.drv"
[ATP cvc3]
name = "CVC3"
exec = "cvc3"
......@@ -89,7 +101,7 @@ command = "@LOCALBIN@why3-cpulimit %t %m -s %e %f"
driver = "drivers/verit.drv"
[ATP z3_smtv1]
name = "Z3"
name = "Z3_smtv1"
exec = "z3"
exec = "z3-2.2"
version_switch = "-version"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment