Added src directory, moved some files around

2025-12-11 13:38:43 -05:00 · 2016-07-07 15:48:50 +02:00 · 2016-07-07 15:48:50 +02:00 · bbbc29948d
commit bbbc29948d
parent 599a59dda9
72 changed files with 48 additions and 41 deletions
--- a/2
+++ b/2
@ -37,7 +37,7 @@ log:
 clean:
 	$(COMP) -clean

-TO_INSTALL=META $(addprefix _build/,$(LIB) $(NAME).a $(NAME).cmi)
+TO_INSTALL=META $(addprefix _build/src/,$(LIB) $(NAME).a $(NAME).cmi)

 install: lib
 	ocamlfind install msat $(TO_INSTALL)
--- a/29
+++ b/29
@ -5,22 +5,23 @@ true: color(always)
 true: optimize(3), unbox_closures, unbox_closures_factor(20)

 # Include paths
-<sat>: include
-<smt>: include
-<solver>: include
-<backend>: include
-<util>: include
-<util/smtlib>: include
+<src>: include
+<src/core>: include
+<src/solver>: include
+<src/backend>: include
+<src/example>: include
+<src/util>: include
+<src/util/smtlib>: include

 # Pack options
-<util/*.cmx>: for-pack(Msat)
-<smt/*.cmx>: for-pack(Msat)
-<sat/*.cmx>: for-pack(Msat)
-<solver/*.cmx>: for-pack(Msat)
-<backend/*.cmx>: for-pack(Msat)
+<src/core/*.cmx>: for-pack(Msat)
+<src/solver/*.cmx>: for-pack(Msat)
+<src/backend/*.cmx>: for-pack(Msat)
+<src/util/*.cmx>: for-pack(Msat)
+<src/example/*.cmx>: for-pack(Msat)

 # more warnings
-<**/*.ml>: warn_K, warn_Y, warn_X
-<**/*.ml>: short_paths, safe_string, strict_sequence
-<**/*.cm*>: debug
+<src/**/*.ml>: warn_K, warn_Y, warn_X
+<src/**/*.ml>: short_paths, safe_string, strict_sequence
+<src/**/*.cm*>: debug

--- a/msat.odocl
+++ b/msat.odocl
@ -1,26 +0,0 @@
-util/Log
-
-solver/Formula_intf
-solver/Theory_intf
-solver/Plugin_intf
-solver/Expr_intf
-solver/Tseitin_intf
-solver/Res_intf
-solver/Solver_types_intf
-solver/Solver_intf
-
-solver/Internal
-solver/External
-solver/Solver
-solver/Mcsolver
-solver/Solver_types
-
-solver/Res
-solver/Tseitin
-
-backend/Dot
-backend/Dedukti
-backend/Backend_intf
-
-sat/Sat
-
--- a/src/backend/backend_intf.ml
+++ b/src/backend/backend_intf.ml
--- a/src/backend/dedukti.ml
+++ b/src/backend/dedukti.ml
--- a/src/backend/dedukti.mli
+++ b/src/backend/dedukti.mli
--- a/src/backend/dot.ml
+++ b/src/backend/dot.ml
--- a/src/backend/dot.mli
+++ b/src/backend/dot.mli
--- a/src/core/expr_intf.ml
+++ b/src/core/expr_intf.ml
--- a/src/core/external.ml
+++ b/src/core/external.ml
--- a/src/core/external.mli
+++ b/src/core/external.mli
--- a/src/core/formula_intf.ml
+++ b/src/core/formula_intf.ml
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
--- a/src/core/internal.mli
+++ b/src/core/internal.mli
--- a/src/core/plugin_intf.ml
+++ b/src/core/plugin_intf.ml
--- a/src/core/res.ml
+++ b/src/core/res.ml
--- a/src/core/res.mli
+++ b/src/core/res.mli
--- a/src/core/res_intf.ml
+++ b/src/core/res_intf.ml
--- a/src/core/solver_intf.ml
+++ b/src/core/solver_intf.ml
--- a/src/core/solver_types.ml
+++ b/src/core/solver_types.ml
--- a/src/core/solver_types.mli
+++ b/src/core/solver_types.mli
--- a/src/core/solver_types_intf.ml
+++ b/src/core/solver_types_intf.ml
--- a/src/core/theory_intf.ml
+++ b/src/core/theory_intf.ml
--- a/src/example/cc.ml
+++ b/src/example/cc.ml
--- a/src/example/cc.mli
+++ b/src/example/cc.mli
--- a/src/example/cnf.ml
+++ b/src/example/cnf.ml
--- a/src/example/cnf.mli
+++ b/src/example/cnf.mli
--- a/src/example/expr.ml
+++ b/src/example/expr.ml
--- a/src/example/expr.mli
+++ b/src/example/expr.mli
--- a/src/example/mcsat.ml
+++ b/src/example/mcsat.ml
--- a/src/example/sat.ml
+++ b/src/example/sat.ml
--- a/src/example/sat.mli
+++ b/src/example/sat.mli
--- a/src/example/sig.mli
+++ b/src/example/sig.mli
--- a/src/example/smt.ml
+++ b/src/example/smt.ml
--- a/src/example/smt.mli
+++ b/src/example/smt.mli
--- a/src/example/unionfind.ml
+++ b/src/example/unionfind.ml
--- a/src/example/unionfind.mli
+++ b/src/example/unionfind.mli
--- a/src/main.ml
+++ b/src/main.ml
--- a/src/msat.mlpack
+++ b/src/msat.mlpack
--- a/src/msat.odocl
+++ b/src/msat.odocl
@ -0,0 +1,32 @@
+# Log utilities
+util/Log
+
+# Interfaces
+core/Formula_intf
+core/Theory_intf
+core/Plugin_intf
+core/Expr_intf
+core/Res_intf
+core/Solver_types_intf
+core/Solver_intf
+solver/Tseitin_intf
+
+# Main modules
+core/Res
+core/Internal
+core/External
+core/Solver_types
+
+solver/Solver
+solver/Mcsolver
+solver/Tseitin
+
+# Backends
+backend/Dot
+backend/Dedukti
+backend/Backend_intf
+
+# Examples
+example/Sat
+example/Smt
+
--- a/src/solver/mcsolver.ml
+++ b/src/solver/mcsolver.ml
--- a/src/solver/mcsolver.mli
+++ b/src/solver/mcsolver.mli
--- a/src/solver/solver.ml
+++ b/src/solver/solver.ml
--- a/src/solver/solver.mli
+++ b/src/solver/solver.mli
--- a/src/solver/tseitin.ml
+++ b/src/solver/tseitin.ml
--- a/src/solver/tseitin.mli
+++ b/src/solver/tseitin.mli
--- a/src/solver/tseitin_intf.ml
+++ b/src/solver/tseitin_intf.ml
--- a/src/util/.merlin
+++ b/src/util/.merlin
--- a/src/util/either.ml
+++ b/src/util/either.ml
--- a/src/util/either.mli
+++ b/src/util/either.mli
--- a/src/util/iheap.ml
+++ b/src/util/iheap.ml
--- a/src/util/iheap.mli
+++ b/src/util/iheap.mli
--- a/src/util/log.ml
+++ b/src/util/log.ml
--- a/src/util/log.mli
+++ b/src/util/log.mli
--- a/src/util/log_dummy.ml
+++ b/src/util/log_dummy.ml
--- a/src/util/log_real.ml
+++ b/src/util/log_real.ml
--- a/src/util/parsedimacs.ml
+++ b/src/util/parsedimacs.ml
--- a/src/util/parsedimacs.mli
+++ b/src/util/parsedimacs.mli
--- a/src/util/smtlib/.merlin
+++ b/src/util/smtlib/.merlin
--- a/src/util/smtlib/lexsmtlib.mli
+++ b/src/util/smtlib/lexsmtlib.mli
--- a/src/util/smtlib/lexsmtlib.mll
+++ b/src/util/smtlib/lexsmtlib.mll
--- a/src/util/smtlib/parsesmtlib.mly
+++ b/src/util/smtlib/parsesmtlib.mly
--- a/src/util/smtlib/smtlib.ml
+++ b/src/util/smtlib/smtlib.ml
--- a/src/util/smtlib/smtlib.mli
+++ b/src/util/smtlib/smtlib.mli
--- a/src/util/smtlib/smtlib_syntax.ml
+++ b/src/util/smtlib/smtlib_syntax.ml
--- a/src/util/smtlib/smtlib_syntax.mli
+++ b/src/util/smtlib/smtlib_syntax.mli
--- a/src/util/smtlib/smtlib_util.ml
+++ b/src/util/smtlib/smtlib_util.ml
--- a/src/util/smtlib/smtlib_util.mli
+++ b/src/util/smtlib/smtlib_util.mli
--- a/src/util/sparse_vec.ml
+++ b/src/util/sparse_vec.ml
--- a/src/util/sparse_vec.mli
+++ b/src/util/sparse_vec.mli
--- a/src/util/vec.ml
+++ b/src/util/vec.ml
--- a/src/util/vec.mli
+++ b/src/util/vec.mli