Move every file to src root and create logic.ml

formalsec · Dec 6, 2024 · 3d872d2 · 3d872d2
1 parent 7f25a33
commit 3d872d2
Show file tree

Hide file tree

Showing 53 changed files with 116 additions and 150 deletions.
diff --git a/src/ast/ast.ml → src/ast.ml b/src/ast/ast.ml → src/ast.ml
@@ -22,7 +22,7 @@ type t =
   | Reset
   | Reset_assertions
   | Set_info of Expr.t
-  | Set_logic of Ty.logic
+  | Set_logic of Logic.t
   | Set_option of Expr.t
 
 type script = t list
@@ -51,7 +51,7 @@ let pp fmt (instr : t) =
   | Reset -> Fmt.string fmt "(reset)"
   | Reset_assertions -> Fmt.string fmt "(reset-assertions)"
   | Set_info info -> Fmt.pf fmt "(set-info %a)" Expr.pp info
-  | Set_logic logic -> Fmt.pf fmt "(set-logic %a)" Ty.pp_logic logic
+  | Set_logic logic -> Fmt.pf fmt "(set-logic %a)" Logic.pp logic
   | Set_option opt -> Fmt.pf fmt "(set-option %a)" Expr.pp opt
 
 let to_string (instr : t) : string = Fmt.str "%a" pp instr
diff --git a/src/ast/ast.mli → src/ast.mli b/src/ast/ast.mli → src/ast.mli
@@ -22,7 +22,7 @@ type t =
   | Reset
   | Reset_assertions
   | Set_info of Expr.t
-  | Set_logic of Ty.logic
+  | Set_logic of Logic.t
   | Set_option of Expr.t
 
 type script = t list

diff --git a/src/axioms/axioms.ml → src/axioms.ml b/src/axioms/axioms.ml → src/axioms.ml
diff --git a/src/utils/cache.ml → src/cache.ml b/src/utils/cache.ml → src/cache.ml
diff --git a/src/utils/cache.mli → src/cache.mli b/src/utils/cache.mli → src/cache.mli
diff --git a/src/utils/cache_intf.ml → src/cache_intf.ml b/src/utils/cache_intf.ml → src/cache_intf.ml
diff --git a/src/ast/compile.ml → src/compile.ml b/src/ast/compile.ml → src/compile.ml
diff --git a/src/ast/constructors_intf.ml → src/constructors_intf.ml b/src/ast/constructors_intf.ml → src/constructors_intf.ml
diff --git a/src/dune b/src/dune
@@ -1,24 +1,29 @@
-(include_subdirs unqualified)
-
 (library
  (name smtml_prelude)
  (public_name smtml.prelude)
  (modules smtml_prelude)
  (libraries prelude))
 
+(ocamllex
+ (modules lexer))
+
+(menhir
+ (modules parser)
+ (flags --table))
+
 (library
  (name smtml)
  (public_name smtml)
  (modules
-  ast
   altergo_mappings
-  bitwuzla_mappings
+  ast
   ;axioms
+  bitwuzla_mappings
   cache
   cache_intf
+  colibri2_mappings
   compile
   constructors_intf
-  colibri2_mappings
   cvc5_mappings
   dolmenexpr_to_expr
   eval
@@ -27,25 +32,26 @@
   interpret_intf
   lexer
   log
+  logic
   mappings
   mappings_intf
   model
   num
   op_intf
   optimizer
   optimizer_intf
-  parser
   params
   parse
+  parser
   rewrite
+  smtlib
   solver
+  solver_dispatcher
   solver_intf
   solver_mode
   solver_type
-  solver_dispatcher
-  smtlib
-  symbol
   statistics
+  symbol
   ty
   utils
   value

diff --git a/src/interpret/eval.ml → src/eval.ml b/src/interpret/eval.ml → src/eval.ml
diff --git a/src/interpret/eval.mli → src/eval.mli b/src/interpret/eval.mli → src/eval.mli
diff --git a/src/ast/expr.ml → src/expr.ml b/src/ast/expr.ml → src/expr.ml
diff --git a/src/ast/expr.mli → src/expr.mli b/src/ast/expr.mli → src/expr.mli
diff --git a/src/interpret/interpret.ml → src/interpret.ml b/src/interpret/interpret.ml → src/interpret.ml
diff --git a/src/interpret/interpret.mli → src/interpret.mli b/src/interpret/interpret.mli → src/interpret.mli
diff --git a/src/interpret/interpret_intf.ml → src/interpret_intf.ml b/src/interpret/interpret_intf.ml → src/interpret_intf.ml
diff --git a/src/parser/lexer.mll → src/lexer.mll b/src/parser/lexer.mll → src/lexer.mll
diff --git a/src/logic.ml b/src/logic.ml
@@ -0,0 +1,88 @@
+type t =
+  | ALL
+  | AUFLIA
+  | AUFLIRA
+  | AUFNIRA
+  | LIA
+  | LRA
+  | QF_ABV
+  | QF_AUFBV
+  | QF_AUFLIA
+  | QF_AX
+  | QF_BV
+  | QF_BVFP
+  | QF_IDL
+  | QF_LIA
+  | QF_LRA
+  | QF_NIA
+  | QF_NRA
+  | QF_RDL
+  | QF_S
+  | QF_UF
+  | QF_UFBV
+  | QF_UFIDL
+  | QF_UFLIA
+  | QF_UFLRA
+  | QF_UFNRA
+  | UFLRA
+  | UFNIA
+
+let pp fmt = function
+  | ALL -> Fmt.string fmt "ALL"
+  | AUFLIA -> Fmt.string fmt "AUFLIA"
+  | AUFLIRA -> Fmt.string fmt "AUFLIRA"
+  | AUFNIRA -> Fmt.string fmt "AUFNIRA"
+  | LIA -> Fmt.string fmt "LIA"
+  | LRA -> Fmt.string fmt "LRA"
+  | QF_ABV -> Fmt.string fmt "QF_ABV"
+  | QF_AUFBV -> Fmt.string fmt "QF_AUFBV"
+  | QF_AUFLIA -> Fmt.string fmt "QF_AUFLIA"
+  | QF_AX -> Fmt.string fmt "QF_AX"
+  | QF_BV -> Fmt.string fmt "QF_BV"
+  | QF_BVFP -> Fmt.string fmt "QF_BVFP"
+  | QF_IDL -> Fmt.string fmt "QF_IDL"
+  | QF_LIA -> Fmt.string fmt "QF_LIA"
+  | QF_LRA -> Fmt.string fmt "QF_LRA"
+  | QF_NIA -> Fmt.string fmt "QF_NIA"
+  | QF_NRA -> Fmt.string fmt "QF_NRA"
+  | QF_RDL -> Fmt.string fmt "QF_RDL"
+  | QF_S -> Fmt.string fmt "QF_S"
+  | QF_UF -> Fmt.string fmt "QF_UF"
+  | QF_UFBV -> Fmt.string fmt "QF_UFBV"
+  | QF_UFIDL -> Fmt.string fmt "QF_UFIDL"
+  | QF_UFLIA -> Fmt.string fmt "QF_UFLIA"
+  | QF_UFLRA -> Fmt.string fmt "QF_UFLRA"
+  | QF_UFNRA -> Fmt.string fmt "QF_UFNRA"
+  | UFLRA -> Fmt.string fmt "UFLRA"
+  | UFNIA -> Fmt.string fmt "UFNIA"
+
+let of_string logic =
+  match logic with
+  | "ALL" -> Ok ALL
+  | "AUFLIA" -> Ok AUFLIA
+  | "AUFLIRA" -> Ok AUFLIRA
+  | "AUFNIRA" -> Ok AUFNIRA
+  | "LIA" -> Ok LIA
+  | "LRA" -> Ok LRA
+  | "QF_ABV" -> Ok QF_ABV
+  | "QF_AUFBV" -> Ok QF_AUFBV
+  | "QF_AUFLIA" -> Ok QF_AUFLIA
+  | "QF_AX" -> Ok QF_AX
+  | "QF_BV" -> Ok QF_BV
+  | "QF_BVFP" -> Ok QF_BVFP
+  | "QF_IDL" -> Ok QF_IDL
+  | "QF_LIA" -> Ok QF_LIA
+  | "QF_LRA" -> Ok QF_LRA
+  | "QF_NIA" -> Ok QF_NIA
+  | "QF_NRA" -> Ok QF_NRA
+  | "QF_RDL" -> Ok QF_RDL
+  | "QF_S" -> Ok QF_S
+  | "QF_UF" -> Ok QF_UF
+  | "QF_UFBV" -> Ok QF_UFBV
+  | "QF_UFIDL" -> Ok QF_UFIDL
+  | "QF_UFLIA" -> Ok QF_UFLIA
+  | "QF_UFLRA" -> Ok QF_UFLRA
+  | "QF_UFNRA" -> Ok QF_UFNRA
+  | "UFLRA" -> Ok UFLRA
+  | "UFNIA" -> Ok UFNIA
+  | _ -> Error (`Msg (Fmt.str "unknown logic %s" logic))
diff --git a/src/mappings_intf.ml b/src/mappings_intf.ml
@@ -344,7 +344,7 @@ module type M = sig
   end
 
   module Solver : sig
-    val make : ?params:Params.t -> ?logic:Ty.logic -> unit -> solver
+    val make : ?params:Params.t -> ?logic:Logic.t -> unit -> solver
 
     val clone : solver -> solver
 
@@ -396,7 +396,7 @@ module type M = sig
   module Smtlib : sig
     val pp :
          ?name:string
-      -> ?logic:Ty.logic
+      -> ?logic:Logic.t
       -> ?status:satisfiability
       -> term list Fmt.t
   end
@@ -428,13 +428,13 @@ module type S = sig
   module Smtlib : sig
     val pp :
          ?name:string
-      -> ?logic:Ty.logic
+      -> ?logic:Logic.t
       -> ?status:satisfiability
       -> Expr.t list Fmt.t
   end
 
   module Solver : sig
-    val make : ?params:Params.t -> ?logic:Ty.logic -> unit -> solver
+    val make : ?params:Params.t -> ?logic:Logic.t -> unit -> solver
 
     val add_simplifier : solver -> solver
 

diff --git a/src/solvers/model.ml → src/model.ml b/src/solvers/model.ml → src/model.ml
diff --git a/src/solvers/model.mli → src/model.mli b/src/solvers/model.mli → src/model.mli
diff --git a/src/ast/num.ml → src/num.ml b/src/ast/num.ml → src/num.ml
diff --git a/src/ast/num.mli → src/num.mli b/src/ast/num.mli → src/num.mli
diff --git a/src/solvers/optimizer.ml → src/optimizer.ml b/src/solvers/optimizer.ml → src/optimizer.ml
diff --git a/src/solvers/optimizer.mli → src/optimizer.mli b/src/solvers/optimizer.mli → src/optimizer.mli
diff --git a/src/solvers/optimizer_intf.ml → src/optimizer_intf.ml b/src/solvers/optimizer_intf.ml → src/optimizer_intf.ml
diff --git a/src/solvers/params.ml → src/params.ml b/src/solvers/params.ml → src/params.ml
diff --git a/src/solvers/params.mli → src/params.mli b/src/solvers/params.mli → src/params.mli
diff --git a/src/parser/parse.ml → src/parse.ml b/src/parser/parse.ml → src/parse.ml
diff --git a/src/parser/parse.mli → src/parse.mli b/src/parser/parse.mli → src/parse.mli
diff --git a/src/parser/parser.mly → src/parser.mly b/src/parser/parser.mly → src/parser.mly
@@ -36,7 +36,7 @@ let get_bind x = Hashtbl.find varmap x
 %token <Ty.t * Ty.cvtop> CVTOP
 %token <Ty.t * Ty.naryop> NARY
 %token <Ty.t> TYPE
-%token <Ty.logic> LOGIC
+%token <Logic.t> LOGIC
 
 %start <Ast.t list> script
 %%

diff --git a/src/parser/dune b/src/parser/dune
diff --git a/src/ast/rewrite.ml → src/rewrite.ml b/src/ast/rewrite.ml → src/rewrite.ml
diff --git a/src/parser/smtlib.ml → src/smtlib.ml b/src/parser/smtlib.ml → src/smtlib.ml
@@ -356,8 +356,8 @@ module Statement = struct
     let logic =
       Log.on_error ~level:Logs.Debug
         ~pp:(fun fmt (`Msg err) -> Fmt.pf fmt "%a%s. Using: ALL" pp_loc loc err)
-        ~use:(fun _ -> Ty.ALL)
-        (Ty.logic_of_string logic)
+        ~use:(fun _ -> Logic.ALL)
+        (Logic.of_string logic)
     in
     Set_logic logic
 end

diff --git a/src/solvers/solver.ml → src/solver.ml b/src/solvers/solver.ml → src/solver.ml
diff --git a/src/solvers/solver.mli → src/solver.mli b/src/solvers/solver.mli → src/solver.mli
diff --git a/src/solvers/solver_dispatcher.ml → src/solver_dispatcher.ml b/src/solvers/solver_dispatcher.ml → src/solver_dispatcher.ml
diff --git a/src/solvers/solver_dispatcher.mli → src/solver_dispatcher.mli b/src/solvers/solver_dispatcher.mli → src/solver_dispatcher.mli
diff --git a/src/solvers/solver_intf.ml → src/solver_intf.ml b/src/solvers/solver_intf.ml → src/solver_intf.ml
@@ -27,7 +27,7 @@ module type S = sig
       assertions used. When knowing what the underlying theory is going to be,
       setting this parameter can help the SMT solver be more performant. The
       default logic is {e unknown_theory}. *)
-  val create : ?params:Params.t -> ?logic:Ty.logic -> unit -> t
+  val create : ?params:Params.t -> ?logic:Logic.t -> unit -> t
 
   (** Interrupt solver. *)
   val interrupt : t -> unit

diff --git a/src/solvers/solver_mode.ml → src/solver_mode.ml b/src/solvers/solver_mode.ml → src/solver_mode.ml
diff --git a/src/solvers/solver_mode.mli → src/solver_mode.mli b/src/solvers/solver_mode.mli → src/solver_mode.mli
diff --git a/src/solvers/solver_type.ml → src/solver_type.ml b/src/solvers/solver_type.ml → src/solver_type.ml
diff --git a/src/solvers/solver_type.mli → src/solver_type.mli b/src/solvers/solver_type.mli → src/solver_type.mli
diff --git a/src/solvers/statistics.ml → src/statistics.ml b/src/solvers/statistics.ml → src/statistics.ml
diff --git a/src/solvers/statistics.mli → src/statistics.mli b/src/solvers/statistics.mli → src/statistics.mli
diff --git a/src/ast/symbol.ml → src/symbol.ml b/src/ast/symbol.ml → src/symbol.ml
diff --git a/src/ast/symbol.mli → src/symbol.mli b/src/ast/symbol.mli → src/symbol.mli
diff --git a/src/ast/ty.ml → src/ty.ml b/src/ast/ty.ml → src/ty.ml
@@ -267,35 +267,6 @@ let naryop_equal op1 op2 =
     true
   | (Logand | Logor | Concat | Regexp_union), _ -> false
 
-type logic =
-  | ALL
-  | AUFLIA
-  | AUFLIRA
-  | AUFNIRA
-  | LIA
-  | LRA
-  | QF_ABV
-  | QF_AUFBV
-  | QF_AUFLIA
-  | QF_AX
-  | QF_BV
-  | QF_BVFP
-  | QF_IDL
-  | QF_LIA
-  | QF_LRA
-  | QF_NIA
-  | QF_NRA
-  | QF_RDL
-  | QF_S
-  | QF_UF
-  | QF_UFBV
-  | QF_UFIDL
-  | QF_UFLIA
-  | QF_UFLRA
-  | QF_UFNRA
-  | UFLRA
-  | UFNIA
-
 let pp_unop fmt (op : unop) =
   match op with
   | Neg -> Fmt.string fmt "neg"
@@ -448,66 +419,6 @@ let of_string = function
     end
     else Error (Fmt.str "can not parse type %s" s)
 
-let pp_logic fmt = function
-  | ALL -> Fmt.string fmt "ALL"
-  | AUFLIA -> Fmt.string fmt "AUFLIA"
-  | AUFLIRA -> Fmt.string fmt "AUFLIRA"
-  | AUFNIRA -> Fmt.string fmt "AUFNIRA"
-  | LIA -> Fmt.string fmt "LIA"
-  | LRA -> Fmt.string fmt "LRA"
-  | QF_ABV -> Fmt.string fmt "QF_ABV"
-  | QF_AUFBV -> Fmt.string fmt "QF_AUFBV"
-  | QF_AUFLIA -> Fmt.string fmt "QF_AUFLIA"
-  | QF_AX -> Fmt.string fmt "QF_AX"
-  | QF_BV -> Fmt.string fmt "QF_BV"
-  | QF_BVFP -> Fmt.string fmt "QF_BVFP"
-  | QF_IDL -> Fmt.string fmt "QF_IDL"
-  | QF_LIA -> Fmt.string fmt "QF_LIA"
-  | QF_LRA -> Fmt.string fmt "QF_LRA"
-  | QF_NIA -> Fmt.string fmt "QF_NIA"
-  | QF_NRA -> Fmt.string fmt "QF_NRA"
-  | QF_RDL -> Fmt.string fmt "QF_RDL"
-  | QF_S -> Fmt.string fmt "QF_S"
-  | QF_UF -> Fmt.string fmt "QF_UF"
-  | QF_UFBV -> Fmt.string fmt "QF_UFBV"
-  | QF_UFIDL -> Fmt.string fmt "QF_UFIDL"
-  | QF_UFLIA -> Fmt.string fmt "QF_UFLIA"
-  | QF_UFLRA -> Fmt.string fmt "QF_UFLRA"
-  | QF_UFNRA -> Fmt.string fmt "QF_UFNRA"
-  | UFLRA -> Fmt.string fmt "UFLRA"
-  | UFNIA -> Fmt.string fmt "UFNIA"
-
-let logic_of_string logic =
-  match logic with
-  | "ALL" -> Ok ALL
-  | "AUFLIA" -> Ok AUFLIA
-  | "AUFLIRA" -> Ok AUFLIRA
-  | "AUFNIRA" -> Ok AUFNIRA
-  | "LIA" -> Ok LIA
-  | "LRA" -> Ok LRA
-  | "QF_ABV" -> Ok QF_ABV
-  | "QF_AUFBV" -> Ok QF_AUFBV
-  | "QF_AUFLIA" -> Ok QF_AUFLIA
-  | "QF_AX" -> Ok QF_AX
-  | "QF_BV" -> Ok QF_BV
-  | "QF_BVFP" -> Ok QF_BVFP
-  | "QF_IDL" -> Ok QF_IDL
-  | "QF_LIA" -> Ok QF_LIA
-  | "QF_LRA" -> Ok QF_LRA
-  | "QF_NIA" -> Ok QF_NIA
-  | "QF_NRA" -> Ok QF_NRA
-  | "QF_RDL" -> Ok QF_RDL
-  | "QF_S" -> Ok QF_S
-  | "QF_UF" -> Ok QF_UF
-  | "QF_UFBV" -> Ok QF_UFBV
-  | "QF_UFIDL" -> Ok QF_UFIDL
-  | "QF_UFLIA" -> Ok QF_UFLIA
-  | "QF_UFLRA" -> Ok QF_UFLRA
-  | "QF_UFNRA" -> Ok QF_UFNRA
-  | "UFLRA" -> Ok UFLRA
-  | "UFNIA" -> Ok UFNIA
-  | _ -> Error (`Msg (Fmt.str "unknown logic %s" logic))
-
 let discr = function
   | Ty_app -> 0
   | Ty_bool -> 1