Skip to content

why3
why3
Commit a6d89023 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

updated drivers with eliminate_literal

parent 02acc89f
Hide whitespace changes
Inline Side-by-side
Showing with 22 additions and 3 deletions
drivers/beagle.drv
View file @ a6d89023
......@@ -29,6 +29,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
(* currently, princess does not support $let and $ite *)
......@@ -318,4 +319,3 @@ end
theory tptp.RatToReal
syntax function to_real "$to_real(%1)"
end
drivers/gappa.drv
View file @ a6d89023
......@@ -17,6 +17,7 @@ transformation "inline_all"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
drivers/mathematica.drv
View file @ a6d89023
......@@ -19,6 +19,7 @@ transformation "eliminate_builtin"
(*transformation "eliminate_inductive"*)
(*transformation "eliminate_algebraic"*)
(*transformation "eliminate_algebraic_math"*)
transformation "eliminate_literal"
transformation "eliminate_epsilon"
(*transformation "eliminate_if"*)
transformation "eliminate_let"
......
drivers/mathsat.drv
View file @ a6d89023
......@@ -17,6 +17,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
drivers/metitarski.drv
View file @ a6d89023
......@@ -30,6 +30,7 @@ transformation "inline_all"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
drivers/polypaver.drv
View file @ a6d89023
......@@ -18,6 +18,7 @@ transformation "inline_all"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
drivers/princess.drv
View file @ a6d89023
......@@ -29,6 +29,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
(* currently, princess does not support $let and $ite *)
......@@ -315,4 +316,3 @@ end
theory tptp.RatToReal
syntax function to_real "$to_real(%1)"
end
drivers/psyche.drv
View file @ a6d89023
......@@ -15,6 +15,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
drivers/pvs-common.gen
View file @ a6d89023
......@@ -12,6 +12,7 @@ transformation "eliminate_mutual_recursion"
(* though we could do better, we only use recursion on one argument *)
transformation "eliminate_non_struct_recursion"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
(* PVS only has simple patterns *)
......
drivers/simplify.drv
View file @ a6d89023
......@@ -15,6 +15,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition" (*_func*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
drivers/spass_types.drv
View file @ a6d89023
......@@ -21,6 +21,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
drivers/tptp-tff0.drv
View file @ a6d89023
......@@ -28,6 +28,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "discriminate"
......
drivers/tptp-tff1.drv
View file @ a6d89023
......@@ -28,6 +28,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
theory BuiltIn
......
drivers/tptp.gen
View file @ a6d89023
......@@ -21,6 +21,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......@@ -34,4 +35,3 @@ theory BuiltIn
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
drivers/verit.drv
View file @ a6d89023
......@@ -21,6 +21,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
drivers/why3_tptp.drv
View file @ a6d89023
......@@ -9,6 +9,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
drivers/yices-smt2.drv
View file @ a6d89023
......@@ -19,6 +19,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
drivers/yices.drv
View file @ a6d89023
......@@ -16,6 +16,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
drivers/z3.drv
View file @ a6d89023
......@@ -14,6 +14,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
drivers/z3_smtv1.drv
View file @ a6d89023
......@@ -15,6 +15,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
......
drivers/zenon.drv
View file @ a6d89023
......@@ -17,6 +17,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
drivers/zenon_modulo.drv
View file @ a6d89023
......@@ -17,6 +17,7 @@ transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
......
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