encoding_simple2 -> encoding_sort

Makefile.in

@@ -128,7 +128,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
 		eliminate_inductive eliminate_let eliminate_if \
 		encoding_enumeration encoding encoding_decorate_mono \
 		libencoding encoding_decorate encoding_bridge \
-		encoding_explicit encoding_simple2 \
+		encoding_explicit encoding_sort \
 		encoding_instantiate simplify_array filter_trigger \
 		introduction abstraction close_epsilon lift_epsilon
 

drivers/cvc3.drv

@@ -21,7 +21,7 @@ transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
 
 transformation "encoding_smt"
-transformation "encoding_simple2"
+transformation "encoding_sort"
 
 theory BuiltIn
   syntax type int   "Int"

drivers/verit.drv

@@ -21,7 +21,7 @@ transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
 
 transformation "encoding_smt"
-transformation "encoding_simple2"
+transformation "encoding_sort"
 
 theory BuiltIn
   syntax type int   "Int"

drivers/yices.drv

@@ -21,7 +21,7 @@ transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
 
 transformation "encoding_smt"
-transformation "encoding_simple2"
+transformation "encoding_sort"
 
 theory BuiltIn
   syntax type int   "Int"

drivers/z3.drv

@@ -21,7 +21,7 @@ transformation "simplify_formula"
 transformation "simplify_trivial_quantification"
 
 transformation "encoding_smt"
-transformation "encoding_simple2"
+transformation "encoding_sort"
 
 theory BuiltIn
   syntax type int   "Int"

src/transform/encoding_simple2.ml → src/transform/encoding_sort.ml

@@ -158,5 +158,5 @@ let t =
   let tenv = init_tenv in
   Trans.decl (decl tenv) None
 
-let () = Trans.register_transform "encoding_simple2" t
+let () = Trans.register_transform "encoding_sort" t