diff --git a/src/ast/ast.ml b/src/ast.ml similarity index 94% rename from src/ast/ast.ml rename to src/ast.ml index 1c8d04cb..f1760de7 100644 --- a/src/ast/ast.ml +++ b/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 b/src/ast.mli similarity index 95% rename from src/ast/ast.mli rename to src/ast.mli index e21237d4..04661e0b 100644 --- a/src/ast/ast.mli +++ b/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 b/src/axioms.ml similarity index 100% rename from src/axioms/axioms.ml rename to src/axioms.ml diff --git a/src/utils/cache.ml b/src/cache.ml similarity index 100% rename from src/utils/cache.ml rename to src/cache.ml diff --git a/src/utils/cache.mli b/src/cache.mli similarity index 100% rename from src/utils/cache.mli rename to src/cache.mli diff --git a/src/utils/cache_intf.ml b/src/cache_intf.ml similarity index 100% rename from src/utils/cache_intf.ml rename to src/cache_intf.ml diff --git a/src/ast/compile.ml b/src/compile.ml similarity index 100% rename from src/ast/compile.ml rename to src/compile.ml diff --git a/src/ast/constructors_intf.ml b/src/constructors_intf.ml similarity index 100% rename from src/ast/constructors_intf.ml rename to src/constructors_intf.ml diff --git a/src/dune b/src/dune index 065d6a9e..95ce1eec 100644 --- 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,6 +32,7 @@ interpret_intf lexer log + logic mappings mappings_intf model @@ -34,18 +40,18 @@ 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 b/src/eval.ml similarity index 100% rename from src/interpret/eval.ml rename to src/eval.ml diff --git a/src/interpret/eval.mli b/src/eval.mli similarity index 100% rename from src/interpret/eval.mli rename to src/eval.mli diff --git a/src/ast/expr.ml b/src/expr.ml similarity index 100% rename from src/ast/expr.ml rename to src/expr.ml diff --git a/src/ast/expr.mli b/src/expr.mli similarity index 100% rename from src/ast/expr.mli rename to src/expr.mli diff --git a/src/interpret/interpret.ml b/src/interpret.ml similarity index 100% rename from src/interpret/interpret.ml rename to src/interpret.ml diff --git a/src/interpret/interpret.mli b/src/interpret.mli similarity index 100% rename from src/interpret/interpret.mli rename to src/interpret.mli diff --git a/src/interpret/interpret_intf.ml b/src/interpret_intf.ml similarity index 100% rename from src/interpret/interpret_intf.ml rename to src/interpret_intf.ml diff --git a/src/parser/lexer.mll b/src/lexer.mll similarity index 100% rename from src/parser/lexer.mll rename to src/lexer.mll diff --git a/src/logic.ml b/src/logic.ml new file mode 100644 index 00000000..ec9b2d65 --- /dev/null +++ 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 index 32cd9fb7..cd599aa9 100644 --- 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 b/src/model.ml similarity index 100% rename from src/solvers/model.ml rename to src/model.ml diff --git a/src/solvers/model.mli b/src/model.mli similarity index 100% rename from src/solvers/model.mli rename to src/model.mli diff --git a/src/ast/num.ml b/src/num.ml similarity index 100% rename from src/ast/num.ml rename to src/num.ml diff --git a/src/ast/num.mli b/src/num.mli similarity index 100% rename from src/ast/num.mli rename to src/num.mli diff --git a/src/solvers/optimizer.ml b/src/optimizer.ml similarity index 100% rename from src/solvers/optimizer.ml rename to src/optimizer.ml diff --git a/src/solvers/optimizer.mli b/src/optimizer.mli similarity index 100% rename from src/solvers/optimizer.mli rename to src/optimizer.mli diff --git a/src/solvers/optimizer_intf.ml b/src/optimizer_intf.ml similarity index 100% rename from src/solvers/optimizer_intf.ml rename to src/optimizer_intf.ml diff --git a/src/solvers/params.ml b/src/params.ml similarity index 100% rename from src/solvers/params.ml rename to src/params.ml diff --git a/src/solvers/params.mli b/src/params.mli similarity index 100% rename from src/solvers/params.mli rename to src/params.mli diff --git a/src/parser/parse.ml b/src/parse.ml similarity index 100% rename from src/parser/parse.ml rename to src/parse.ml diff --git a/src/parser/parse.mli b/src/parse.mli similarity index 100% rename from src/parser/parse.mli rename to src/parse.mli diff --git a/src/parser/parser.mly b/src/parser.mly similarity index 99% rename from src/parser/parser.mly rename to src/parser.mly index b7e340d1..49dd2e82 100644 --- a/src/parser/parser.mly +++ b/src/parser.mly @@ -36,7 +36,7 @@ let get_bind x = Hashtbl.find varmap x %token CVTOP %token NARY %token TYPE -%token LOGIC +%token LOGIC %start script %% diff --git a/src/parser/dune b/src/parser/dune deleted file mode 100644 index 283d31f6..00000000 --- a/src/parser/dune +++ /dev/null @@ -1,6 +0,0 @@ -(ocamllex - (modules lexer)) - -(menhir - (modules parser) - (flags --table)) diff --git a/src/ast/rewrite.ml b/src/rewrite.ml similarity index 100% rename from src/ast/rewrite.ml rename to src/rewrite.ml diff --git a/src/parser/smtlib.ml b/src/smtlib.ml similarity index 99% rename from src/parser/smtlib.ml rename to src/smtlib.ml index 138879b7..e0fceb45 100644 --- a/src/parser/smtlib.ml +++ b/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 b/src/solver.ml similarity index 100% rename from src/solvers/solver.ml rename to src/solver.ml diff --git a/src/solvers/solver.mli b/src/solver.mli similarity index 100% rename from src/solvers/solver.mli rename to src/solver.mli diff --git a/src/solvers/solver_dispatcher.ml b/src/solver_dispatcher.ml similarity index 100% rename from src/solvers/solver_dispatcher.ml rename to src/solver_dispatcher.ml diff --git a/src/solvers/solver_dispatcher.mli b/src/solver_dispatcher.mli similarity index 100% rename from src/solvers/solver_dispatcher.mli rename to src/solver_dispatcher.mli diff --git a/src/solvers/solver_intf.ml b/src/solver_intf.ml similarity index 98% rename from src/solvers/solver_intf.ml rename to src/solver_intf.ml index d3534bc9..e0deaa90 100644 --- a/src/solvers/solver_intf.ml +++ b/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 b/src/solver_mode.ml similarity index 100% rename from src/solvers/solver_mode.ml rename to src/solver_mode.ml diff --git a/src/solvers/solver_mode.mli b/src/solver_mode.mli similarity index 100% rename from src/solvers/solver_mode.mli rename to src/solver_mode.mli diff --git a/src/solvers/solver_type.ml b/src/solver_type.ml similarity index 100% rename from src/solvers/solver_type.ml rename to src/solver_type.ml diff --git a/src/solvers/solver_type.mli b/src/solver_type.mli similarity index 100% rename from src/solvers/solver_type.mli rename to src/solver_type.mli diff --git a/src/solvers/statistics.ml b/src/statistics.ml similarity index 100% rename from src/solvers/statistics.ml rename to src/statistics.ml diff --git a/src/solvers/statistics.mli b/src/statistics.mli similarity index 100% rename from src/solvers/statistics.mli rename to src/statistics.mli diff --git a/src/ast/symbol.ml b/src/symbol.ml similarity index 100% rename from src/ast/symbol.ml rename to src/symbol.ml diff --git a/src/ast/symbol.mli b/src/symbol.mli similarity index 100% rename from src/ast/symbol.mli rename to src/symbol.mli diff --git a/src/ast/ty.ml b/src/ty.ml similarity index 83% rename from src/ast/ty.ml rename to src/ty.ml index c148d76d..c2a29418 100644 --- a/src/ast/ty.ml +++ b/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 diff --git a/src/ast/ty.mli b/src/ty.mli similarity index 86% rename from src/ast/ty.mli rename to src/ty.mli index 20fb2cf1..12a6b1f9 100644 --- a/src/ast/ty.mli +++ b/src/ty.mli @@ -131,35 +131,6 @@ type naryop = | Concat | Regexp_union -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 - val compare : t -> t -> int val unop_equal : unop -> unop -> bool @@ -176,8 +147,6 @@ val naryop_equal : naryop -> naryop -> bool val equal : t -> t -> bool -val logic_of_string : string -> (logic, [> `Msg of string ]) result - val pp_unop : unop Fmt.t val pp_binop : binop Fmt.t @@ -192,8 +161,6 @@ val pp_naryop : naryop Fmt.t val pp : t Fmt.t -val pp_logic : logic Fmt.t - val string_of_type : t -> string val of_string : string -> (t, string) Result.t diff --git a/src/utils/utils.ml b/src/utils.ml similarity index 100% rename from src/utils/utils.ml rename to src/utils.ml diff --git a/src/ast/value.ml b/src/value.ml similarity index 100% rename from src/ast/value.ml rename to src/value.ml diff --git a/src/ast/value.mli b/src/value.mli similarity index 100% rename from src/ast/value.mli rename to src/value.mli diff --git a/src/z3_mappings.default.ml b/src/z3_mappings.default.ml index 6ca2ffd6..6777e094 100644 --- a/src/z3_mappings.default.ml +++ b/src/z3_mappings.default.ml @@ -444,7 +444,7 @@ module M = struct Option.iter set_params params; let logic = Option.map - (fun l -> Fmt.kstr (Z3.Symbol.mk_string ctx) "%a" Ty.pp_logic l) + (fun l -> Fmt.kstr (Z3.Symbol.mk_string ctx) "%a" Logic.pp l) logic in Z3.Solver.mk_solver ctx logic @@ -521,7 +521,7 @@ module M = struct let name = Option.value name ~default:"" in let logic = Fmt.str "%a" - (Fmt.option ~none:(fun fmt () -> Fmt.string fmt "ALL") Ty.pp_logic) + (Fmt.option ~none:(fun fmt () -> Fmt.string fmt "ALL") Logic.pp) logic in let status =