Rename Cnf into Translate

OCamlPro · Oct 8, 2024 · b92fe5b · b92fe5b
1 parent 2b1f718
commit b92fe5b
Show file tree

Hide file tree

Showing 7 changed files with 9 additions and 18 deletions.
diff --git a/rsc/extra/subgraphs.dot b/rsc/extra/subgraphs.dot
@@ -202,10 +202,7 @@ subgraph cluster_lib {
                 style=filled;
                 color=lightblue;
                 "Frontend";
-                "Cnf";
-                "Typechecker";
-                "Parsed_interface";
-                "Input";
+                "Translate";
                 "Parse_command"
         }
 

diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
@@ -349,7 +349,7 @@ let process_source ?selector_inst ~print_status src =
       ~size_limit ~response_file
     |> Parser.init
     |> Typer.init
-      ~additional_builtins:Cnf.builtins
+      ~additional_builtins:Translate.builtins
       ~extension_builtins:[Typer.Ext.bv2nat]
     |> Typer_Pipe.init ~type_check
   in
@@ -512,7 +512,7 @@ let process_source ?selector_inst ~print_status src =
         { Typer_Pipe.id; contents; loc; attrs = []; implicit = false }
       in
       let cnf =
-        Cnf.make (State.get State.logic_file st).loc
+        Translate.make (State.get State.logic_file st).loc
           (State.get solver_ctx_key st).ctx stmt
       in
       State.set solver_ctx_key (
@@ -628,7 +628,7 @@ let process_source ?selector_inst ~print_status src =
       Expr.mk_term
         (Sy.name name)
         []
-        (Cnf.dty_to_ty term.DStd.Expr.term_ty)
+        (Translate.dty_to_ty term.DStd.Expr.term_ty)
     in
     match get_value simple_form with
     | Some v -> Fmt.to_to_string Expr.print v
@@ -705,7 +705,7 @@ let process_source ?selector_inst ~print_status src =
         in
         let stmt = { Typer_Pipe.id; contents; loc ; attrs; implicit } in
         let cnf, is_thm =
-          match Cnf.make (State.get State.logic_file st).loc l stmt with
+          match Translate.make (State.get State.logic_file st).loc l stmt with
           | { Commands.st_decl = Query (_, _, kind); _ } as cnf :: hyps ->
             let is_thm =
               match kind with Ty.Thm | Sat -> true | _ -> false
@@ -827,7 +827,7 @@ let process_source ?selector_inst ~print_status src =
              unsupported statement is encountered.
         *)
         let cnf =
-          Cnf.make (State.get State.logic_file st).loc
+          Translate.make (State.get State.logic_file st).loc
             (State.get solver_ctx_key st).ctx td
         in
         State.set solver_ctx_key (

diff --git a/src/lib/dune b/src/lib/dune
@@ -46,7 +46,7 @@
   ; modules that make up the lib
   (modules
     ; frontend
-    Cnf D_loop D_state_option Frontend Parsed_interface Models
+    Translate D_loop D_state_option Frontend Parsed_interface Models
     ; reasoners
     Ac Arith Arrays_rel Bitv Ccx Shostak Relation
     Fun_sat Fun_sat_frontend Inequalities Bitv_rel Th_util Adt Adt_rel

diff --git a/src/lib/frontend/cnf.ml → src/lib/frontend/translate.ml b/src/lib/frontend/cnf.ml → src/lib/frontend/translate.ml
diff --git a/src/lib/frontend/cnf.mli → src/lib/frontend/translate.mli b/src/lib/frontend/cnf.mli → src/lib/frontend/translate.mli
diff --git a/src/lib/index.mld b/src/lib/index.mld
@@ -78,11 +78,8 @@ Finally, the native input method is defined in the {!module:AltErgoLib.Parsed_in
 and {!module:AltErgoLib.Typechecker} modules.
 
 {!modules:
-AltErgoLib.Cnf
+AltErgoLib.Translate
 AltErgoLib.Frontend
-AltErgoLib.Input
-AltErgoLib.Parsed_interface
-AltErgoLib.Typechecker
 }
 
 
@@ -117,10 +114,7 @@ AltErgoLib.Matching_types
 AltErgoLib.Shostak
 AltErgoLib.Ac
 AltErgoLib.Arith
-AltErgoLib.Arrays
 AltErgoLib.Bitv
-AltErgoLib.Enum
-AltErgoLib.Ite
 AltErgoLib.Polynome
 AltErgoLib.Records
 AltErgoLib.Sig

diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
@@ -2346,7 +2346,7 @@ module Triggers = struct
           let content = TMap.fold (fun t _ acc -> t :: acc) res [] in
           let content = List.stable_sort pat_weight content in
           if Options.get_verbose () then
-            Printer.print_dbg ~module_name:"Cnf"
+            Printer.print_dbg ~module_name:"Translate"
               ~function_name:"clean_trigger"
               "AXIOM: %s@ \
                from multi-trig of sz %d : %a@ \