Elim_algebraic: generate indexing function only for SMT provers

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"
 

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"*)

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"

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"
 

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"*)

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"

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"
 

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"*)

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"*)

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"*)

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"*)

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
 

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