formalsec / smtml

A frontend for multiple SMT solvers in OCaml
https://formalsec.github.io/smtml/smtml/
MIT License
26 stars 7 forks source link

Restructure lib directory to organise source files #6

Closed filipeom closed 1 year ago

filipeom commented 1 year ago

Is your feature request related to a problem? Please describe. Although the files in lib are correctly named, it would help having them organised into sub-directories that aggregate related code. This feature would reduce mental effort in locating desired source files.

Describe the solution you'd like For example, files related with the abstract syntax (e.g., intOp.ml or floatOp.ml) should be place in a directory titled syntax.

Describe alternatives you've considered Alternatives have yet to be considered.

Additional context No additional context.

filipeom commented 1 year ago

Proposed directory structure (so far):

  1. solvers: Contains OCaml modules related to solver implementations, such as batch.ml for batch solver operations, and incremental.ml for incremental solver operations;
  2. syntax: Contains OCaml modules related to syntax and expression manipulation, such as types.ml for defining types, expression.ml for defining expressions, num.ml for numeric operations;
  3. exec: Contains OCaml modules related to execution and evaluation, such as eval_numeric.ml for numeric evaluation.
  4. operators: Contains OCaml modules related to operator implementations, such as bvOp.ml for bit vector operations, strOp.ml for string operations, intOp.ml for integer operations, floatOp.ml for floating-point operations, and boolOp.ml for boolean operations;
  5. optimizer: Contains OCaml modules related to optimization, such as optimizer.ml for optimization operations;
  6. axioms: Contains OCaml module(s) related to axioms used in the project, such as axioms.ml for defining axioms;
  7. constructors: Contains OCaml module(s) related to constructor implementations, such as bitVector.ml for bit vector constructors, integer.ml for integer constructors, strings.ml for string constructors, and real.ml for real number constructors;
  8. mappings: Contains OCaml modules related to mappings for different SMT solvers, such as z3_mappings.ml for internal mappings of Z3 solver, and potentially other modules for other SMT solvers in the future.
  9. utils: Contains OCaml modules related to utility functions or helper modules that can be used across different parts of the project.
  10. common: Contains OCaml module(s) with common utility functions or helper modules that can be used across different parts of the project, but not specific to any particular solver or SMT operations.