Commit b71623a7 authored by Andrei Paskevich's avatar Andrei Paskevich

rename files in drivers/

parent 9fb83919
......@@ -7,21 +7,21 @@ timelimit = 60
[prover z3]
command = "../../bin/why3-cpulimit %t %m -s z3 -smt2 %f"
driver = "../../share/drivers/z3_smtv2.drv"
driver = "../../share/drivers/z3_bare.drv"
editor = ""
name = "Z3"
version = "..."
[prover yices]
command = "../../bin/why3-cpulimit %t %m -s yices -smt %f"
driver = "../../share/drivers/yices.drv"
driver = "../../share/drivers/yices_bare.drv"
editor = ""
name = "Yices"
version = "..."
[prover cvc3]
command = "../../bin/why3-cpulimit 0 %m -s cvc3 -timeout %t %f"
driver = "../../share/drivers/cvc3.drv"
driver = "../../share/drivers/cvc3_bare.drv"
editor = ""
name = "CVC3"
version = "..."
(* 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
import "alt_ergo.drv"
theory map.Map
syntax type map "(%1,%2) farray"
syntax type map "(%1,%2) farray"
syntax logic get "(%1[%2])"
syntax logic set "(%1[%2 <- %3])"
end
(*
Local Variables:
mode: why
......
import "cvc3.gen"
import "cvc3_bare.drv"
import "discrimination.gen"
(*
Local Variables:
......
import "cvc3.gen"
theory BuiltIn
meta "select_inst" "nothing"
meta "select_kept" "goal"
meta "select_lskept" "nothing"
meta "completion_mode" "only_kept"
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
import "cvc3.gen"
theory BuiltIn
meta "select_inst" "nothing"
meta "select_kept" "nothing"
meta "select_lskept" "goal"
meta "completion_mode" "only_kept"
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
import "cvc3.gen"
theory BuiltIn
meta "select_inst" "goal"
meta "select_kept" "goal"
......@@ -7,9 +5,3 @@ theory BuiltIn
meta "completion_mode" "only_kept"
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
......@@ -118,7 +118,7 @@ theory real.Real
meta "inline : no" logic (<=)
meta "inline : no" logic (>=)
meta "inline : no" logic (>)
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
remove prop CommutativeGroup.Unit_def
......
......@@ -18,10 +18,6 @@ theory BuiltIn
meta "encoding : kept" type int
meta "encoding : kept" type real
meta "select_inst" "goal"
meta "select_kept" "goal"
meta "select_lskept" "nothing"
meta "completion_mode" "only_kept"
end
import "discrimination.gen"
(* Why driver for SMT syntax *)
prelude ";;; this is a prelude for Yices "
printer "smtv1"
filename "%f-%t-%g.smt"
valid "\\bunsat\\b"
unknown "\\bunknown\\b\\|\\bsat\\b\\|feature not supported: non linear problem" "Unknown"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "simplify_recursive_definition"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "encoding_smt"
transformation "encoding_sort"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (=) "(= %1 %2)"
meta "encoding : kept" type int
end
theory int.Int
prelude ";;; this is a prelude for Yices 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 Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
end
theory real.Real
prelude ";;; this is a prelude for Yices 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 Inverse
remove prop Assoc.Assoc
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
meta "encoding : kept" type real
end
(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
syntax type bool "bool"
syntax logic True "true"
syntax logic False "false"
syntax logic andb "(and %1 %2)"
syntax logic orb "(or %1 %2)"
syntax logic xorb "(xor %1 %2)"
syntax logic notb "(not %1)"
meta cloned "encoding_decorate : kept" type bool
end
*)
import "yices_bare.drv"
import "discrimination.gen"
(*
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:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
(* Why driver for SMT syntax *)
prelude ";;; this is a prelude for Yices "
printer "smtv1"
filename "%f-%t-%g.smt"
valid "\\bunsat\\b"
unknown "\\bunknown\\b\\|\\bsat\\b\\|feature not supported: non linear problem" "Unknown"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "simplify_recursive_definition"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "encoding_smt"
transformation "encoding_sort"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (=) "(= %1 %2)"
meta "encoding : kept" type int
end
theory int.Int
prelude ";;; this is a prelude for Yices 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 Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
end
theory real.Real
prelude ";;; this is a prelude for Yices 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 Inverse
remove prop Assoc.Assoc
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
meta "encoding : kept" type real
end
(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
syntax type bool "bool"
syntax logic True "true"
syntax logic False "false"
syntax logic andb "(and %1 %2)"
syntax logic orb "(or %1 %2)"
syntax logic xorb "(xor %1 %2)"
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:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
(* Why driver for SMT syntax *)
prelude ";;; this is a prelude for Z3"
printer "smtv1"
filename "%f-%t-%g.smt"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "simplify_recursive_definition"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "encoding_smt"
transformation "encoding_sort"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (=) "(= %1 %2)"
meta "encoding : kept" type int
end
theory int.Int
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)"
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 Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
end
theory real.Real
prelude ";;; this is a prelude for Z3 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 Inverse
remove prop Assoc.Assoc
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
meta "encoding : kept" type real
end
(*
(* L'encodage des types sommes bloquent cette théorie builtin *)
theory bool.Bool
syntax type bool "bool"
syntax logic True "true"
syntax logic False "false"
syntax logic andb "(and %1 %2)"
syntax logic orb "(or %1 %2)"
syntax logic xorb "(xor %1 %2)"
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
import "z3_bare.drv"
import "discrimination.gen"
(*
Local Variables:
......