From ed4f9a61f3b62e74617b1c92c5a1c2af74dbfc53 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Wed, 16 Mar 2011 19:31:06 +0100 Subject: [PATCH] Elim_algebraic: generate indexing function only for SMT provers --- drivers/alt_ergo.drv | 2 +- drivers/cvc3.drv | 2 +- drivers/gappa.drv | 2 +- drivers/simplify.drv | 2 +- drivers/verit.drv | 2 +- drivers/why3_smt.drv | 2 +- drivers/why3_tptp.drv | 2 ++ drivers/yices.drv | 2 +- drivers/z3.drv | 2 +- drivers/z3_array.drv | 2 +- drivers/z3_smtv2.drv | 2 +- src/transform/eliminate_algebraic.ml | 18 +++++++++++++----- src/transform/eliminate_algebraic.mli | 4 ---- 13 files changed, 25 insertions(+), 19 deletions(-) diff --git a/drivers/alt_ergo.drv b/drivers/alt_ergo.drv index 68893e624..ab44ccb0d 100644 --- a/drivers/alt_ergo.drv +++ b/drivers/alt_ergo.drv @@ -19,7 +19,7 @@ transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_recursion" transformation "eliminate_inductive" -transformation "eliminate_algebraic" +transformation "eliminate_algebraic_smt" transformation "eliminate_if" transformation "eliminate_let" diff --git a/drivers/cvc3.drv b/drivers/cvc3.drv index 6ab1f91f5..6023d4d63 100644 --- a/drivers/cvc3.drv +++ b/drivers/cvc3.drv @@ -16,7 +16,7 @@ transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_definition" transformation "eliminate_inductive" -transformation "eliminate_algebraic" +transformation "eliminate_algebraic_smt" transformation "simplify_formula" (*transformation "simplify_trivial_quantification"*) diff --git a/drivers/gappa.drv b/drivers/gappa.drv index 74f925999..ce1a0a36b 100644 --- a/drivers/gappa.drv +++ b/drivers/gappa.drv @@ -17,7 +17,7 @@ transformation "eliminate_builtin" transformation "inline_all" transformation "eliminate_definition" transformation "eliminate_inductive" -transformation "eliminate_algebraic" +transformation "eliminate_algebraic_smt" transformation "eliminate_if" transformation "eliminate_let" transformation "simplify_formula" diff --git a/drivers/simplify.drv b/drivers/simplify.drv index 901fe4c9b..f406e4630 100644 --- a/drivers/simplify.drv +++ b/drivers/simplify.drv @@ -15,7 +15,7 @@ transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_definition" (*_func*) transformation "eliminate_inductive" -transformation "eliminate_algebraic" +transformation "eliminate_algebraic_smt" transformation "eliminate_if" transformation "eliminate_let" diff --git a/drivers/verit.drv b/drivers/verit.drv index 3c8e53c48..3a2cff3f2 100644 --- a/drivers/verit.drv +++ b/drivers/verit.drv @@ -16,7 +16,7 @@ transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_definition" transformation "eliminate_inductive" -transformation "eliminate_algebraic" +transformation "eliminate_algebraic_smt" transformation "simplify_formula" (*transformation "simplify_trivial_quantification"*) diff --git a/drivers/why3_smt.drv b/drivers/why3_smt.drv index afe708172..afcffdf2b 100644 --- a/drivers/why3_smt.drv +++ b/drivers/why3_smt.drv @@ -7,7 +7,7 @@ transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_definition" transformation "eliminate_inductive" -transformation "eliminate_algebraic" +transformation "eliminate_algebraic_smt" transformation "encoding_smt_array" transformation "encoding_sort" diff --git a/drivers/why3_tptp.drv b/drivers/why3_tptp.drv index bf6a5d78b..381f29cb6 100644 --- a/drivers/why3_tptp.drv +++ b/drivers/why3_tptp.drv @@ -7,6 +7,8 @@ transformation "eliminate_builtin" transformation "eliminate_definition" transformation "eliminate_inductive" transformation "eliminate_algebraic" +transformation "eliminate_if" +transformation "eliminate_let" transformation "encoding_tptp" diff --git a/drivers/yices.drv b/drivers/yices.drv index c362c19e2..8017a7a22 100644 --- a/drivers/yices.drv +++ b/drivers/yices.drv @@ -16,7 +16,7 @@ transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_definition" transformation "eliminate_inductive" -transformation "eliminate_algebraic" +transformation "eliminate_algebraic_smt" transformation "simplify_formula" (*transformation "simplify_trivial_quantification"*) diff --git a/drivers/z3.drv b/drivers/z3.drv index 5758fe5df..19c317005 100644 --- a/drivers/z3.drv +++ b/drivers/z3.drv @@ -17,7 +17,7 @@ transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_definition" transformation "eliminate_inductive" -transformation "eliminate_algebraic" +transformation "eliminate_algebraic_smt" transformation "simplify_formula" (*transformation "simplify_trivial_quantification"*) diff --git a/drivers/z3_array.drv b/drivers/z3_array.drv index 7e1ba8dfb..fd39d7e8c 100644 --- a/drivers/z3_array.drv +++ b/drivers/z3_array.drv @@ -17,7 +17,7 @@ transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_definition" transformation "eliminate_inductive" -transformation "eliminate_algebraic" +transformation "eliminate_algebraic_smt" transformation "simplify_formula" (*transformation "simplify_trivial_quantification"*) diff --git a/drivers/z3_smtv2.drv b/drivers/z3_smtv2.drv index 416011578..1eadac811 100644 --- a/drivers/z3_smtv2.drv +++ b/drivers/z3_smtv2.drv @@ -18,7 +18,7 @@ transformation "inline_trivial" transformation "eliminate_builtin" transformation "eliminate_definition" transformation "eliminate_inductive" -transformation "eliminate_algebraic" +transformation "eliminate_algebraic_smt" transformation "simplify_formula" (*transformation "simplify_trivial_quantification"*) diff --git a/src/transform/eliminate_algebraic.ml b/src/transform/eliminate_algebraic.ml index 0e59c3e0a..8e927b990 100644 --- a/src/transform/eliminate_algebraic.ml +++ b/src/transform/eliminate_algebraic.ml @@ -60,12 +60,14 @@ type state = { mt_map : lsymbol Mts.t; (* from type symbols to selector functions *) pj_map : lsymbol list Mls.t; (* from constructors to projections *) tp_map : (tysymbol * lsymbol list) Mid.t; (* skipped tuple symbols *) + in_smt : bool; (* generate indexing funcitons *) } -let empty_state = { +let empty_state smt = { mt_map = Mts.empty; pj_map = Mls.empty; tp_map = Mid.empty; + in_smt = smt; } let uncompiled = "eliminate_algebraic: compile_match required" @@ -211,6 +213,7 @@ let add_indexer (state,task) ts ty csl = let add_indexer (state,task) ts ty = function | [_] -> state, task + | _ when not state.in_smt -> state, task | csl -> add_indexer (state,task) ts ty csl let add_projections (state,task) _ts _ty csl = @@ -303,10 +306,15 @@ let comp t (state,task) = match t.task_decl.td_node with | _ -> comp t (state,task) -let eliminate_compiled_algebraic = Trans.fold_map comp empty_state None +let eliminate_algebraic_smt = Trans.compose compile_match + (Trans.fold_map comp (empty_state true) None) -let eliminate_algebraic = - Trans.compose compile_match eliminate_compiled_algebraic +let eliminate_algebraic = Trans.compose compile_match + (Trans.fold_map comp (empty_state false) None) -let () = Trans.register_transform "eliminate_algebraic" eliminate_algebraic +let () = + Trans.register_transform "eliminate_algebraic_smt" eliminate_algebraic_smt + +let () = + Trans.register_transform "eliminate_algebraic" eliminate_algebraic diff --git a/src/transform/eliminate_algebraic.mli b/src/transform/eliminate_algebraic.mli index f3c358f4d..620fb7c91 100644 --- a/src/transform/eliminate_algebraic.mli +++ b/src/transform/eliminate_algebraic.mli @@ -19,8 +19,4 @@ val compile_match : Task.task Trans.trans -val eliminate_compiled_algebraic : Task.task Trans.trans - -val eliminate_algebraic : Task.task Trans.trans - val meta_enum : Theory.meta -- GitLab