Skip to content

why3
why3
Commit 54cd6e48 authored by François Bobot's avatar François Bobot
Browse files
Options

driver : comment simplify trivial quantification which can grow monstruously the size of th goal

parent bfff13fa
Hide whitespace changes
Inline Side-by-side
Showing with 8 additions and 8 deletions
drivers/alt_ergo.drv
View file @ 54cd6e48
......@@ -24,7 +24,7 @@ transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_trivial_quantification_in_goal"
(*transformation "simplify_trivial_quantification_in_goal"*)
theory BuiltIn
syntax type int "int"
......
drivers/coq.drv
View file @ 54cd6e48
......@@ -20,7 +20,7 @@ transformation "eliminate_recursion"
transformation "eliminate_if"
transformation "simplify_formula"
transformation "simplify_trivial_quantification_in_goal"
(*transformation "simplify_trivial_quantification_in_goal"*)
theory BuiltIn
......
drivers/cvc3.drv
View file @ 54cd6e48
......@@ -19,7 +19,7 @@ transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
(*transformation "simplify_trivial_quantification"*)
transformation "encoding_smt"
transformation "encoding_sort"
......
drivers/gappa.drv
View file @ 54cd6e48
......@@ -21,7 +21,7 @@ transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
(*transformation "simplify_trivial_quantification"*)
transformation "introduce_premises"
theory BuiltIn
......
drivers/simplify.drv
View file @ 54cd6e48
......@@ -20,7 +20,7 @@ transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
(*transformation "simplify_trivial_quantification"*)
transformation "remove_triggers"
(*transformation "filter_trigger_no_predicate"*)
......
drivers/verit.drv
View file @ 54cd6e48
......@@ -19,7 +19,7 @@ transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
(*transformation "simplify_trivial_quantification"*)
transformation "encoding_smt"
transformation "encoding_sort"
......
drivers/yices.drv
View file @ 54cd6e48
......@@ -19,7 +19,7 @@ transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
(*transformation "simplify_trivial_quantification"*)
transformation "encoding_smt"
transformation "encoding_sort"
......
drivers/z3.drv
View file @ 54cd6e48
......@@ -20,7 +20,7 @@ transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
(*transformation "simplify_trivial_quantification"*)
(* transformation "encoding_array" *)
......
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