Commit 1ffa7c32 authored by Francois Bobot's avatar Francois Bobot
Browse files

Since its already incorrect no encoding for simplify, and also no trigger...

Since its already incorrect no encoding for simplify, and also no trigger because its buggy inside simplify
parent ff662df6
...@@ -13,7 +13,7 @@ transformation "simplify_recursive_definition" ...@@ -13,7 +13,7 @@ transformation "simplify_recursive_definition"
transformation "inline_trivial" transformation "inline_trivial"
transformation "eliminate_builtin" transformation "eliminate_builtin"
transformation "eliminate_definition" transformation "eliminate_definition"(*_func"*)
transformation "eliminate_inductive" transformation "eliminate_inductive"
transformation "eliminate_algebraic" transformation "eliminate_algebraic"
transformation "eliminate_if" transformation "eliminate_if"
...@@ -21,12 +21,13 @@ transformation "eliminate_let" ...@@ -21,12 +21,13 @@ transformation "eliminate_let"
transformation "simplify_formula" transformation "simplify_formula"
transformation "simplify_trivial_quantification" transformation "simplify_trivial_quantification"
transformation "filter_trigger_no_predicate" transformation "remove_triggers"
(*transformation "filter_trigger_no_predicate"*)
(* predicate are *currently* translated to P(\x) = true, thus in a (* predicate are *currently* translated to P(\x) = true, thus in a
trigger they can't appear since = can't appear *) trigger they can't appear since = can't appear *)
(*transformation "filter_trigger_builtin"*) (*transformation "filter_trigger_builtin"*)
transformation "encoding_decorate_mono" (*transformation "encoding_decorate_mono"*)
theory BuiltIn theory BuiltIn
syntax type int "Int" syntax type int "Int"
......
...@@ -27,7 +27,7 @@ open Task ...@@ -27,7 +27,7 @@ open Task
open Printer open Printer
let ident_printer = let ident_printer =
let bls = [] in let bls = ["select";"store"] in
let san = sanitizer char_to_alpha char_to_alnumus in let san = sanitizer char_to_alpha char_to_alnumus in
create_ident_printer bls ~sanitizer:san create_ident_printer bls ~sanitizer:san
......
...@@ -35,6 +35,18 @@ let make_rt_rf keep = ...@@ -35,6 +35,18 @@ let make_rt_rf keep =
rt,rf rt,rf
let keep_no_trigger _ = false
let remove_triggers =
let rt,rf = make_rt_rf keep_no_trigger in
Trans.rewrite rt rf None
let () = Trans.register_transform "remove_triggers"
(fun _ -> remove_triggers)
let keep_no_predicate = function let keep_no_predicate = function
| Term _ -> true | Term _ -> true
| _ -> false | _ -> false
......
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