From bbbc29948d239a1695613567586c184b837c45a8 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 7 Jul 2016 15:48:50 +0200 Subject: [PATCH] Added src directory, moved some files around --- Makefile | 2 +- _tags | 29 ++++++++++--------- msat.odocl | 26 ----------------- {backend => src/backend}/backend_intf.ml | 0 {backend => src/backend}/dedukti.ml | 0 {backend => src/backend}/dedukti.mli | 0 {backend => src/backend}/dot.ml | 0 {backend => src/backend}/dot.mli | 0 {solver => src/core}/expr_intf.ml | 0 {solver => src/core}/external.ml | 0 {solver => src/core}/external.mli | 0 {solver => src/core}/formula_intf.ml | 0 {solver => src/core}/internal.ml | 0 {solver => src/core}/internal.mli | 0 {solver => src/core}/plugin_intf.ml | 0 {solver => src/core}/res.ml | 0 {solver => src/core}/res.mli | 0 {solver => src/core}/res_intf.ml | 0 {solver => src/core}/solver_intf.ml | 0 {solver => src/core}/solver_types.ml | 0 {solver => src/core}/solver_types.mli | 0 {solver => src/core}/solver_types_intf.ml | 0 {solver => src/core}/theory_intf.ml | 0 {smt => src/example}/cc.ml | 0 {smt => src/example}/cc.mli | 0 {smt => src/example}/cnf.ml | 0 {smt => src/example}/cnf.mli | 0 {smt => src/example}/expr.ml | 0 {smt => src/example}/expr.mli | 0 {smt => src/example}/mcsat.ml | 0 {sat => src/example}/sat.ml | 0 {sat => src/example}/sat.mli | 0 {smt => src/example}/sig.mli | 0 {smt => src/example}/smt.ml | 0 {smt => src/example}/smt.mli | 0 {smt => src/example}/unionfind.ml | 0 {smt => src/example}/unionfind.mli | 0 main.ml => src/main.ml | 0 msat.mlpack => src/msat.mlpack | 0 src/msat.odocl | 32 +++++++++++++++++++++ {solver => src/solver}/mcsolver.ml | 0 {solver => src/solver}/mcsolver.mli | 0 {solver => src/solver}/solver.ml | 0 {solver => src/solver}/solver.mli | 0 {solver => src/solver}/tseitin.ml | 0 {solver => src/solver}/tseitin.mli | 0 {solver => src/solver}/tseitin_intf.ml | 0 {util => src/util}/.merlin | 0 {util => src/util}/either.ml | 0 {util => src/util}/either.mli | 0 {util => src/util}/iheap.ml | 0 {util => src/util}/iheap.mli | 0 {util => src/util}/log.ml | 0 {util => src/util}/log.mli | 0 {util => src/util}/log_dummy.ml | 0 {util => src/util}/log_real.ml | 0 {util => src/util}/parsedimacs.ml | 0 {util => src/util}/parsedimacs.mli | 0 {util => src/util}/smtlib/.merlin | 0 {util => src/util}/smtlib/lexsmtlib.mli | 0 {util => src/util}/smtlib/lexsmtlib.mll | 0 {util => src/util}/smtlib/parsesmtlib.mly | 0 {util => src/util}/smtlib/smtlib.ml | 0 {util => src/util}/smtlib/smtlib.mli | 0 {util => src/util}/smtlib/smtlib_syntax.ml | 0 {util => src/util}/smtlib/smtlib_syntax.mli | 0 {util => src/util}/smtlib/smtlib_util.ml | 0 {util => src/util}/smtlib/smtlib_util.mli | 0 {util => src/util}/sparse_vec.ml | 0 {util => src/util}/sparse_vec.mli | 0 {util => src/util}/vec.ml | 0 {util => src/util}/vec.mli | 0 72 files changed, 48 insertions(+), 41 deletions(-) delete mode 100644 msat.odocl rename {backend => src/backend}/backend_intf.ml (100%) rename {backend => src/backend}/dedukti.ml (100%) rename {backend => src/backend}/dedukti.mli (100%) rename {backend => src/backend}/dot.ml (100%) rename {backend => src/backend}/dot.mli (100%) rename {solver => src/core}/expr_intf.ml (100%) rename {solver => src/core}/external.ml (100%) rename {solver => src/core}/external.mli (100%) rename {solver => src/core}/formula_intf.ml (100%) rename {solver => src/core}/internal.ml (100%) rename {solver => src/core}/internal.mli (100%) rename {solver => src/core}/plugin_intf.ml (100%) rename {solver => src/core}/res.ml (100%) rename {solver => src/core}/res.mli (100%) rename {solver => src/core}/res_intf.ml (100%) rename {solver => src/core}/solver_intf.ml (100%) rename {solver => src/core}/solver_types.ml (100%) rename {solver => src/core}/solver_types.mli (100%) rename {solver => src/core}/solver_types_intf.ml (100%) rename {solver => src/core}/theory_intf.ml (100%) rename {smt => src/example}/cc.ml (100%) rename {smt => src/example}/cc.mli (100%) rename {smt => src/example}/cnf.ml (100%) rename {smt => src/example}/cnf.mli (100%) rename {smt => src/example}/expr.ml (100%) rename {smt => src/example}/expr.mli (100%) rename {smt => src/example}/mcsat.ml (100%) rename {sat => src/example}/sat.ml (100%) rename {sat => src/example}/sat.mli (100%) rename {smt => src/example}/sig.mli (100%) rename {smt => src/example}/smt.ml (100%) rename {smt => src/example}/smt.mli (100%) rename {smt => src/example}/unionfind.ml (100%) rename {smt => src/example}/unionfind.mli (100%) rename main.ml => src/main.ml (100%) rename msat.mlpack => src/msat.mlpack (100%) create mode 100644 src/msat.odocl rename {solver => src/solver}/mcsolver.ml (100%) rename {solver => src/solver}/mcsolver.mli (100%) rename {solver => src/solver}/solver.ml (100%) rename {solver => src/solver}/solver.mli (100%) rename {solver => src/solver}/tseitin.ml (100%) rename {solver => src/solver}/tseitin.mli (100%) rename {solver => src/solver}/tseitin_intf.ml (100%) rename {util => src/util}/.merlin (100%) rename {util => src/util}/either.ml (100%) rename {util => src/util}/either.mli (100%) rename {util => src/util}/iheap.ml (100%) rename {util => src/util}/iheap.mli (100%) rename {util => src/util}/log.ml (100%) rename {util => src/util}/log.mli (100%) rename {util => src/util}/log_dummy.ml (100%) rename {util => src/util}/log_real.ml (100%) rename {util => src/util}/parsedimacs.ml (100%) rename {util => src/util}/parsedimacs.mli (100%) rename {util => src/util}/smtlib/.merlin (100%) rename {util => src/util}/smtlib/lexsmtlib.mli (100%) rename {util => src/util}/smtlib/lexsmtlib.mll (100%) rename {util => src/util}/smtlib/parsesmtlib.mly (100%) rename {util => src/util}/smtlib/smtlib.ml (100%) rename {util => src/util}/smtlib/smtlib.mli (100%) rename {util => src/util}/smtlib/smtlib_syntax.ml (100%) rename {util => src/util}/smtlib/smtlib_syntax.mli (100%) rename {util => src/util}/smtlib/smtlib_util.ml (100%) rename {util => src/util}/smtlib/smtlib_util.mli (100%) rename {util => src/util}/sparse_vec.ml (100%) rename {util => src/util}/sparse_vec.mli (100%) rename {util => src/util}/vec.ml (100%) rename {util => src/util}/vec.mli (100%) diff --git a/Makefile b/Makefile index 9745db2b..ffd07fd8 100644 --- a/Makefile +++ b/Makefile @@ -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) diff --git a/_tags b/_tags index 4f131897..11f07cc2 100644 --- a/_tags +++ b/_tags @@ -5,22 +5,23 @@ true: color(always) true: optimize(3), unbox_closures, unbox_closures_factor(20) # Include paths -: include -: include -: include -: include -: include -: include +: include +: include +: include +: include +: include +: include +: include # Pack options -: for-pack(Msat) -: for-pack(Msat) -: for-pack(Msat) -: for-pack(Msat) -: for-pack(Msat) +: for-pack(Msat) +: for-pack(Msat) +: for-pack(Msat) +: for-pack(Msat) +: for-pack(Msat) # more warnings -<**/*.ml>: warn_K, warn_Y, warn_X -<**/*.ml>: short_paths, safe_string, strict_sequence -<**/*.cm*>: debug +: warn_K, warn_Y, warn_X +: short_paths, safe_string, strict_sequence +: debug diff --git a/msat.odocl b/msat.odocl deleted file mode 100644 index b7562e25..00000000 --- a/msat.odocl +++ /dev/null @@ -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 - diff --git a/backend/backend_intf.ml b/src/backend/backend_intf.ml similarity index 100% rename from backend/backend_intf.ml rename to src/backend/backend_intf.ml diff --git a/backend/dedukti.ml b/src/backend/dedukti.ml similarity index 100% rename from backend/dedukti.ml rename to src/backend/dedukti.ml diff --git a/backend/dedukti.mli b/src/backend/dedukti.mli similarity index 100% rename from backend/dedukti.mli rename to src/backend/dedukti.mli diff --git a/backend/dot.ml b/src/backend/dot.ml similarity index 100% rename from backend/dot.ml rename to src/backend/dot.ml diff --git a/backend/dot.mli b/src/backend/dot.mli similarity index 100% rename from backend/dot.mli rename to src/backend/dot.mli diff --git a/solver/expr_intf.ml b/src/core/expr_intf.ml similarity index 100% rename from solver/expr_intf.ml rename to src/core/expr_intf.ml diff --git a/solver/external.ml b/src/core/external.ml similarity index 100% rename from solver/external.ml rename to src/core/external.ml diff --git a/solver/external.mli b/src/core/external.mli similarity index 100% rename from solver/external.mli rename to src/core/external.mli diff --git a/solver/formula_intf.ml b/src/core/formula_intf.ml similarity index 100% rename from solver/formula_intf.ml rename to src/core/formula_intf.ml diff --git a/solver/internal.ml b/src/core/internal.ml similarity index 100% rename from solver/internal.ml rename to src/core/internal.ml diff --git a/solver/internal.mli b/src/core/internal.mli similarity index 100% rename from solver/internal.mli rename to src/core/internal.mli diff --git a/solver/plugin_intf.ml b/src/core/plugin_intf.ml similarity index 100% rename from solver/plugin_intf.ml rename to src/core/plugin_intf.ml diff --git a/solver/res.ml b/src/core/res.ml similarity index 100% rename from solver/res.ml rename to src/core/res.ml diff --git a/solver/res.mli b/src/core/res.mli similarity index 100% rename from solver/res.mli rename to src/core/res.mli diff --git a/solver/res_intf.ml b/src/core/res_intf.ml similarity index 100% rename from solver/res_intf.ml rename to src/core/res_intf.ml diff --git a/solver/solver_intf.ml b/src/core/solver_intf.ml similarity index 100% rename from solver/solver_intf.ml rename to src/core/solver_intf.ml diff --git a/solver/solver_types.ml b/src/core/solver_types.ml similarity index 100% rename from solver/solver_types.ml rename to src/core/solver_types.ml diff --git a/solver/solver_types.mli b/src/core/solver_types.mli similarity index 100% rename from solver/solver_types.mli rename to src/core/solver_types.mli diff --git a/solver/solver_types_intf.ml b/src/core/solver_types_intf.ml similarity index 100% rename from solver/solver_types_intf.ml rename to src/core/solver_types_intf.ml diff --git a/solver/theory_intf.ml b/src/core/theory_intf.ml similarity index 100% rename from solver/theory_intf.ml rename to src/core/theory_intf.ml diff --git a/smt/cc.ml b/src/example/cc.ml similarity index 100% rename from smt/cc.ml rename to src/example/cc.ml diff --git a/smt/cc.mli b/src/example/cc.mli similarity index 100% rename from smt/cc.mli rename to src/example/cc.mli diff --git a/smt/cnf.ml b/src/example/cnf.ml similarity index 100% rename from smt/cnf.ml rename to src/example/cnf.ml diff --git a/smt/cnf.mli b/src/example/cnf.mli similarity index 100% rename from smt/cnf.mli rename to src/example/cnf.mli diff --git a/smt/expr.ml b/src/example/expr.ml similarity index 100% rename from smt/expr.ml rename to src/example/expr.ml diff --git a/smt/expr.mli b/src/example/expr.mli similarity index 100% rename from smt/expr.mli rename to src/example/expr.mli diff --git a/smt/mcsat.ml b/src/example/mcsat.ml similarity index 100% rename from smt/mcsat.ml rename to src/example/mcsat.ml diff --git a/sat/sat.ml b/src/example/sat.ml similarity index 100% rename from sat/sat.ml rename to src/example/sat.ml diff --git a/sat/sat.mli b/src/example/sat.mli similarity index 100% rename from sat/sat.mli rename to src/example/sat.mli diff --git a/smt/sig.mli b/src/example/sig.mli similarity index 100% rename from smt/sig.mli rename to src/example/sig.mli diff --git a/smt/smt.ml b/src/example/smt.ml similarity index 100% rename from smt/smt.ml rename to src/example/smt.ml diff --git a/smt/smt.mli b/src/example/smt.mli similarity index 100% rename from smt/smt.mli rename to src/example/smt.mli diff --git a/smt/unionfind.ml b/src/example/unionfind.ml similarity index 100% rename from smt/unionfind.ml rename to src/example/unionfind.ml diff --git a/smt/unionfind.mli b/src/example/unionfind.mli similarity index 100% rename from smt/unionfind.mli rename to src/example/unionfind.mli diff --git a/main.ml b/src/main.ml similarity index 100% rename from main.ml rename to src/main.ml diff --git a/msat.mlpack b/src/msat.mlpack similarity index 100% rename from msat.mlpack rename to src/msat.mlpack diff --git a/src/msat.odocl b/src/msat.odocl new file mode 100644 index 00000000..09f5e4ce --- /dev/null +++ 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 + diff --git a/solver/mcsolver.ml b/src/solver/mcsolver.ml similarity index 100% rename from solver/mcsolver.ml rename to src/solver/mcsolver.ml diff --git a/solver/mcsolver.mli b/src/solver/mcsolver.mli similarity index 100% rename from solver/mcsolver.mli rename to src/solver/mcsolver.mli diff --git a/solver/solver.ml b/src/solver/solver.ml similarity index 100% rename from solver/solver.ml rename to src/solver/solver.ml diff --git a/solver/solver.mli b/src/solver/solver.mli similarity index 100% rename from solver/solver.mli rename to src/solver/solver.mli diff --git a/solver/tseitin.ml b/src/solver/tseitin.ml similarity index 100% rename from solver/tseitin.ml rename to src/solver/tseitin.ml diff --git a/solver/tseitin.mli b/src/solver/tseitin.mli similarity index 100% rename from solver/tseitin.mli rename to src/solver/tseitin.mli diff --git a/solver/tseitin_intf.ml b/src/solver/tseitin_intf.ml similarity index 100% rename from solver/tseitin_intf.ml rename to src/solver/tseitin_intf.ml diff --git a/util/.merlin b/src/util/.merlin similarity index 100% rename from util/.merlin rename to src/util/.merlin diff --git a/util/either.ml b/src/util/either.ml similarity index 100% rename from util/either.ml rename to src/util/either.ml diff --git a/util/either.mli b/src/util/either.mli similarity index 100% rename from util/either.mli rename to src/util/either.mli diff --git a/util/iheap.ml b/src/util/iheap.ml similarity index 100% rename from util/iheap.ml rename to src/util/iheap.ml diff --git a/util/iheap.mli b/src/util/iheap.mli similarity index 100% rename from util/iheap.mli rename to src/util/iheap.mli diff --git a/util/log.ml b/src/util/log.ml similarity index 100% rename from util/log.ml rename to src/util/log.ml diff --git a/util/log.mli b/src/util/log.mli similarity index 100% rename from util/log.mli rename to src/util/log.mli diff --git a/util/log_dummy.ml b/src/util/log_dummy.ml similarity index 100% rename from util/log_dummy.ml rename to src/util/log_dummy.ml diff --git a/util/log_real.ml b/src/util/log_real.ml similarity index 100% rename from util/log_real.ml rename to src/util/log_real.ml diff --git a/util/parsedimacs.ml b/src/util/parsedimacs.ml similarity index 100% rename from util/parsedimacs.ml rename to src/util/parsedimacs.ml diff --git a/util/parsedimacs.mli b/src/util/parsedimacs.mli similarity index 100% rename from util/parsedimacs.mli rename to src/util/parsedimacs.mli diff --git a/util/smtlib/.merlin b/src/util/smtlib/.merlin similarity index 100% rename from util/smtlib/.merlin rename to src/util/smtlib/.merlin diff --git a/util/smtlib/lexsmtlib.mli b/src/util/smtlib/lexsmtlib.mli similarity index 100% rename from util/smtlib/lexsmtlib.mli rename to src/util/smtlib/lexsmtlib.mli diff --git a/util/smtlib/lexsmtlib.mll b/src/util/smtlib/lexsmtlib.mll similarity index 100% rename from util/smtlib/lexsmtlib.mll rename to src/util/smtlib/lexsmtlib.mll diff --git a/util/smtlib/parsesmtlib.mly b/src/util/smtlib/parsesmtlib.mly similarity index 100% rename from util/smtlib/parsesmtlib.mly rename to src/util/smtlib/parsesmtlib.mly diff --git a/util/smtlib/smtlib.ml b/src/util/smtlib/smtlib.ml similarity index 100% rename from util/smtlib/smtlib.ml rename to src/util/smtlib/smtlib.ml diff --git a/util/smtlib/smtlib.mli b/src/util/smtlib/smtlib.mli similarity index 100% rename from util/smtlib/smtlib.mli rename to src/util/smtlib/smtlib.mli diff --git a/util/smtlib/smtlib_syntax.ml b/src/util/smtlib/smtlib_syntax.ml similarity index 100% rename from util/smtlib/smtlib_syntax.ml rename to src/util/smtlib/smtlib_syntax.ml diff --git a/util/smtlib/smtlib_syntax.mli b/src/util/smtlib/smtlib_syntax.mli similarity index 100% rename from util/smtlib/smtlib_syntax.mli rename to src/util/smtlib/smtlib_syntax.mli diff --git a/util/smtlib/smtlib_util.ml b/src/util/smtlib/smtlib_util.ml similarity index 100% rename from util/smtlib/smtlib_util.ml rename to src/util/smtlib/smtlib_util.ml diff --git a/util/smtlib/smtlib_util.mli b/src/util/smtlib/smtlib_util.mli similarity index 100% rename from util/smtlib/smtlib_util.mli rename to src/util/smtlib/smtlib_util.mli diff --git a/util/sparse_vec.ml b/src/util/sparse_vec.ml similarity index 100% rename from util/sparse_vec.ml rename to src/util/sparse_vec.ml diff --git a/util/sparse_vec.mli b/src/util/sparse_vec.mli similarity index 100% rename from util/sparse_vec.mli rename to src/util/sparse_vec.mli diff --git a/util/vec.ml b/src/util/vec.ml similarity index 100% rename from util/vec.ml rename to src/util/vec.ml diff --git a/util/vec.mli b/src/util/vec.mli similarity index 100% rename from util/vec.mli rename to src/util/vec.mli