diff --git a/_oasis b/_oasis index 66e84c5bd5f65d4e9ac35b1cc40770ac7bbcd013..0673e6d57d8d761a27195d613e1a2585ae8c68b4 100644 --- a/_oasis +++ b/_oasis @@ -5,19 +5,19 @@ Synopsis: Coalgebraic Ontology Logic solver Authors: Florian Widmann, Thorsten Wißmann License: GPL -Executable coalg +Library libcool CompiledObject: native - Path: src + Path: src/lib BuildTools: ocamlbuild + # Dependencies: BuildDepends: ocamlgraph, unix, str - MainIs: coalg.ml - CCOpt: -std=c++98 -x c++ CCLib: -lminisat -lstdc++ -lbdd -lm -lglpk # Warning: we use C++ sources in .c files because oasis does not recognize # cpp-files + CCOpt: -std=c++98 -x c++ CSources: gmlmip_stub.c, minisat_stub.c, GMLMIP-0.1/formulas/rational.h, @@ -48,6 +48,20 @@ Executable coalg GMLMIP-0.1/rules/sizefunctions.c, GMLMIP-0.1/rules/radixtree.h, GMLMIP-0.1/rules/radixtree.c + InternalModules: CoAlgLogicUtils, CoAlgLogics + Modules: CoAlgMisc, + CoAlgFormula, + CoolUtils, + GenAndComp, + CoAlgReasoner + + +Executable coalg + CompiledObject: native + Path: src/coalg/ + BuildTools: ocamlbuild + MainIs: coalg.ml + BuildDepends: libcool # some cabal similar syntax, so steal its syntax highlighting # vim: ft=cabal diff --git a/src/Makefile b/src/Makefile deleted file mode 100644 index 208f8be1e967c70d647ec7af6ad86d71232735fa..0000000000000000000000000000000000000000 --- a/src/Makefile +++ /dev/null @@ -1,166 +0,0 @@ -###################################################################### -# Makefile (use GNU-Make) -# $* part of the file name that matched the % in the target pattern. -# $@ file name of the target of the rule -# $^ names of the prerequisites -# $< name of the first prerequisite -# $? names of all the prerequisites that are newer than the target -###################################################################### - - -.DEFAULT: - @echo "This target needs remaking: default = [$<]" - @echo "No rule provided" - -# If defined, the code will be compiled into native code, -# else it will be compiled into byte code. -NATIVE := true - -# If defined, the dependencies will be updated automatically. -CHECKDEP := 1 - -# The projects which will be compiled if "make all" is used. -PROGS := coalg coalgcompare - -GMLFOBJS = \ -GMLMIP-0.1/formulas/formula.o \ -GMLMIP-0.1/formulas/GML_formula.o \ -GMLMIP-0.1/formulas/PML_formula.o \ -GMLMIP-0.1/formulas/rational.o \ -GMLMIP-0.1/formulas/satisfyingassignment.o - -GMLROBJS = \ -GMLMIP-0.1/rules/premise.o \ -GMLMIP-0.1/rules/GML_premise.o \ -GMLMIP-0.1/rules/PML_premise.o \ -GMLMIP-0.1/rules/valuation.o \ -GMLMIP-0.1/rules/setofconclusions.o \ -GMLMIP-0.1/rules/sizefunctions.o \ -GMLMIP-0.1/rules/radixtree.o - -GMLOBJS = $(GMLROBJS) $(GMLFOBJS) GMLMIP-0.1/onestep.o - -LIBS := unix str graph -SOURCESMLI := $(wildcard *.mli) -SOURCESML := $(wildcard *.ml) -INCS ?= -I/usr/include -I/usr/lib/ocaml -I/usr/local/lib/ocaml -I. -CXXFLAGS += -Wall $(INCS) -LDXX ?= g++ - -OCAMLC := ocamlc.opt -OCAMLCFLAGS := -I `ocamlfind query ocamlgraph` -OCAMLOPT := ocamlopt.opt -OCAMLOPTFLAGS := -cc $(LDXX) -ccopt -static -unsafe -inline 100 -I `ocamlfind query ocamlgraph` - -# No more user input beyond this point. - -ifdef NATIVE -OC := $(OCAMLOPT) -OCAMLDEP := ocamldep -native -SUFFIX := .cmx -SUFFIXLIB := .cmxa -FLAGS := $(OCAMLOPTFLAGS) -else -OC := $(OCAMLC) -OCAMLDEP := ocamldep -SUFFIX := .cmo -SUFFIXLIB := .cma -FLAGS := $(OCAMLCFLAGS) -endif - -LIBS := $(patsubst %,%$(SUFFIXLIB),$(LIBS)) -LIBSMLI := $(patsubst %.mli,%.cmi,$(SOURCESMLI)) -LIBSML := $(patsubst %.ml,%$(SUFFIX),$(SOURCESML)) - -.PHONY: all -all: $(PROGS) gmlmip - -.PHONY: phony -# don't do anything here -phony: - @: - -.PHONY: gmlmip -gmlmip: - make -C GMLMIP-0.1 - -minisat.cma: minisat.cmo minisat_stub.o - $(OCAMLC) -a -o minisat.cma minisat.cmo minisat_stub.o -custom -cclib -lminisat - -minisat.cmxa: minisat.cmx minisat_stub.o - $(OCAMLOPT) -a -o minisat.cmxa minisat.cmx minisat_stub.o -cclib -lminisat - -GMLMIP-0.1/onestep.o: phony - make -C GMLMIP-0.1 onestep.o - -gmlmip.cma: gmlmip.cmo gmlmip_stub.o $(GMLOBJS) - $(OCAMLC) -a -o $@ $^ -custom -cclib -lbdd -cclib -lm -cclib -lglpk - -gmlmip.cmxa: gmlmip.cmx gmlmip_stub.o $(GMLOBJS) - $(OCAMLOPT) -a -o $@ $^ -cclib -lbdd -cclib -lm -cclib -lglpk - -# Object files... sorted topologically by their dependency... -COALG_OBJS := minisat$(SUFFIXLIB) gmlmip$(SUFFIXLIB) \ - CoolUtils$(SUFFIX) \ - OWL$(SUFFIX) \ - OWLFunctionalParser$(SUFFIX) \ - genAndComp$(SUFFIX) MiscSolver$(SUFFIX) altGenlex$(SUFFIX) HashConsing$(SUFFIX) \ - ALCFormula$(SUFFIX) ALCMisc$(SUFFIX) ALCGraph$(SUFFIX) \ - CoAlgFormula$(SUFFIX) \ - CoAlgMisc$(SUFFIX) CoAlgLogicUtils$(SUFFIX) CoAlgLogics$(SUFFIX) \ - CoAlgReasoner$(SUFFIX) \ - -coalg: $(COALG_OBJS) coalg$(SUFFIX) - $(OC) -o $@ $(FLAGS) $(LIBS) $^ - -coalgcompare: $(COALG_OBJS) coalgcompare$(SUFFIX) - $(OC) -o $@ $(FLAGS) $(LIBS) $^ - - -ALC_OBJS := genAndComp$(SUFFIX) MiscSolver$(SUFFIX) altGenlex$(SUFFIX) HashConsing$(SUFFIX) \ - ALCFormula$(SUFFIX) ALCMisc$(SUFFIX) \ - ALCTree$(SUFFIX) ALCGraph$(SUFFIX) ALCGraphStates$(SUFFIX) - -alc: $(ALC_OBJS) alc$(SUFFIX) - $(OC) -o alc $(FLAGS) $(LIBS) $^ - - -%.cmi: %.mli - $(OCAMLC) -c $(OCAMLCFLAGS) $< - -%.cmo: %.ml - $(OCAMLC) -c $(OCAMLCFLAGS) $< - -%.cmx: %.ml - $(OCAMLOPT) -c $(OCAMLOPTFLAGS) $< - - -.PHONY: bintar tar - -bintar: - tar czvf cool-bin-x86_64.tar.gz coalg coalgcompare INSTALL - -tar: - @echo :: creating cool-src-`date +%Y-%m-%d`.tar.gz - tar czf cool-src-`date +%Y-%m-%d`.tar.gz `git ls-files` - - - - -.PHONY: clean -clean: - find -regextype posix-egrep -regex ".*((\.(cmi|cmo|cma|cmx|o|cmxa))|~)$$" -delete - $(RM) -f .depend - $(RM) -f $(PROGS) - $(RM) -f *.a - make -C GMLMIP-0.1 clean - -.PHONY: depend -depend: .depend - -ifdef CHECKDEP -.depend: $(SOURCESMLI) $(SOURCESML) - $(OCAMLDEP) $(SOURCESMLI) $(SOURCESML) > $@ -endif - --include .depend diff --git a/src/coalg.ml b/src/coalg/coalg.ml similarity index 93% rename from src/coalg.ml rename to src/coalg/coalg.ml index cdd028601790b18109f5a34b92eac9273cb0c783..0866924a4400b33183b6e342ffc3702b12e1d79b 100644 --- a/src/coalg.ml +++ b/src/coalg/coalg.ml @@ -6,7 +6,6 @@ module CM = CoAlgMisc module CF = CoAlgFormula -module OWLFP = OWLFunctionalParser open CoolUtils @@ -40,7 +39,7 @@ let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increm let printUsage () = print_endline "Usage: \"alc <task> <functor> [<flags>]\" where"; - print_endline " <task> in { sat print nnf prov (is »not.(sat ¬f)«) owlcat }"; + print_endline " <task> in { sat print nnf prov (is »not.(sat ¬f)«) }"; print_endline " <functor> in { MultiModalK MultiModalKD CoalitionLogic GML"; print_endline " (or: K) (or: KD) (or: CL) }"; print_endline " <flags> = a list of the following items"; @@ -145,18 +144,6 @@ let choiceNNF () = done with End_of_file -> () -let choiceOWLCat () = - let buf = ref "" in - try - while true do - let input = read_line () in - buf := !buf ^ input ^ "\n" - done - with End_of_file -> () ; - let t = OWLFP.tree_of_string !buf in - print_endline (OWLFP.string_of_tree (OWLFP.string_of_annotated id) t) - - let rec parseFlags arr offs : unit = let offs = ref (offs) in let getParam () = @@ -188,7 +175,6 @@ let _ = | "prov" -> choiceProvable () | "print" -> choicePrint () | "nnf" -> choiceNNF () - | "owlcat" -> choiceOWLCat () | _ -> printUsage () diff --git a/src/ALCFormula.ml b/src/lib/ALCFormula.ml similarity index 100% rename from src/ALCFormula.ml rename to src/lib/ALCFormula.ml diff --git a/src/ALCFormula.mli b/src/lib/ALCFormula.mli similarity index 100% rename from src/ALCFormula.mli rename to src/lib/ALCFormula.mli diff --git a/src/ALCGraph.ml b/src/lib/ALCGraph.ml similarity index 100% rename from src/ALCGraph.ml rename to src/lib/ALCGraph.ml diff --git a/src/ALCGraph.mli b/src/lib/ALCGraph.mli similarity index 100% rename from src/ALCGraph.mli rename to src/lib/ALCGraph.mli diff --git a/src/ALCMisc.ml b/src/lib/ALCMisc.ml similarity index 100% rename from src/ALCMisc.ml rename to src/lib/ALCMisc.ml diff --git a/src/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml similarity index 100% rename from src/CoAlgFormula.ml rename to src/lib/CoAlgFormula.ml diff --git a/src/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli similarity index 100% rename from src/CoAlgFormula.mli rename to src/lib/CoAlgFormula.mli diff --git a/src/CoAlgLogicUtils.ml b/src/lib/CoAlgLogicUtils.ml similarity index 100% rename from src/CoAlgLogicUtils.ml rename to src/lib/CoAlgLogicUtils.ml diff --git a/src/CoAlgLogicUtils.mli b/src/lib/CoAlgLogicUtils.mli similarity index 100% rename from src/CoAlgLogicUtils.mli rename to src/lib/CoAlgLogicUtils.mli diff --git a/src/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml similarity index 100% rename from src/CoAlgLogics.ml rename to src/lib/CoAlgLogics.ml diff --git a/src/CoAlgLogics.mli b/src/lib/CoAlgLogics.mli similarity index 100% rename from src/CoAlgLogics.mli rename to src/lib/CoAlgLogics.mli diff --git a/src/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml similarity index 100% rename from src/CoAlgMisc.ml rename to src/lib/CoAlgMisc.ml diff --git a/src/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli similarity index 100% rename from src/CoAlgMisc.mli rename to src/lib/CoAlgMisc.mli diff --git a/src/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml similarity index 100% rename from src/CoAlgReasoner.ml rename to src/lib/CoAlgReasoner.ml diff --git a/src/CoAlgReasoner.mli b/src/lib/CoAlgReasoner.mli similarity index 100% rename from src/CoAlgReasoner.mli rename to src/lib/CoAlgReasoner.mli diff --git a/src/CoolUtils.ml b/src/lib/CoolUtils.ml similarity index 100% rename from src/CoolUtils.ml rename to src/lib/CoolUtils.ml diff --git a/src/CoolUtils.mli b/src/lib/CoolUtils.mli similarity index 100% rename from src/CoolUtils.mli rename to src/lib/CoolUtils.mli diff --git a/src/GMLMIP-0.1/.gitignore b/src/lib/GMLMIP-0.1/.gitignore similarity index 100% rename from src/GMLMIP-0.1/.gitignore rename to src/lib/GMLMIP-0.1/.gitignore diff --git a/src/GMLMIP-0.1/README.txt b/src/lib/GMLMIP-0.1/README.txt similarity index 100% rename from src/GMLMIP-0.1/README.txt rename to src/lib/GMLMIP-0.1/README.txt diff --git a/src/GMLMIP-0.1/config.mk b/src/lib/GMLMIP-0.1/config.mk similarity index 100% rename from src/GMLMIP-0.1/config.mk rename to src/lib/GMLMIP-0.1/config.mk diff --git a/src/GMLMIP-0.1/formulas/GML_formula.c b/src/lib/GMLMIP-0.1/formulas/GML_formula.c similarity index 100% rename from src/GMLMIP-0.1/formulas/GML_formula.c rename to src/lib/GMLMIP-0.1/formulas/GML_formula.c diff --git a/src/GMLMIP-0.1/formulas/GML_formula.h b/src/lib/GMLMIP-0.1/formulas/GML_formula.h similarity index 100% rename from src/GMLMIP-0.1/formulas/GML_formula.h rename to src/lib/GMLMIP-0.1/formulas/GML_formula.h diff --git a/src/GMLMIP-0.1/formulas/PML_formula.c b/src/lib/GMLMIP-0.1/formulas/PML_formula.c similarity index 100% rename from src/GMLMIP-0.1/formulas/PML_formula.c rename to src/lib/GMLMIP-0.1/formulas/PML_formula.c diff --git a/src/GMLMIP-0.1/formulas/PML_formula.h b/src/lib/GMLMIP-0.1/formulas/PML_formula.h similarity index 100% rename from src/GMLMIP-0.1/formulas/PML_formula.h rename to src/lib/GMLMIP-0.1/formulas/PML_formula.h diff --git a/src/GMLMIP-0.1/formulas/formula.c b/src/lib/GMLMIP-0.1/formulas/formula.c similarity index 100% rename from src/GMLMIP-0.1/formulas/formula.c rename to src/lib/GMLMIP-0.1/formulas/formula.c diff --git a/src/GMLMIP-0.1/formulas/formula.h b/src/lib/GMLMIP-0.1/formulas/formula.h similarity index 100% rename from src/GMLMIP-0.1/formulas/formula.h rename to src/lib/GMLMIP-0.1/formulas/formula.h diff --git a/src/GMLMIP-0.1/formulas/makefile b/src/lib/GMLMIP-0.1/formulas/makefile similarity index 100% rename from src/GMLMIP-0.1/formulas/makefile rename to src/lib/GMLMIP-0.1/formulas/makefile diff --git a/src/GMLMIP-0.1/formulas/rational.c b/src/lib/GMLMIP-0.1/formulas/rational.c similarity index 100% rename from src/GMLMIP-0.1/formulas/rational.c rename to src/lib/GMLMIP-0.1/formulas/rational.c diff --git a/src/GMLMIP-0.1/formulas/rational.h b/src/lib/GMLMIP-0.1/formulas/rational.h similarity index 100% rename from src/GMLMIP-0.1/formulas/rational.h rename to src/lib/GMLMIP-0.1/formulas/rational.h diff --git a/src/GMLMIP-0.1/formulas/satisfyingassignment.c b/src/lib/GMLMIP-0.1/formulas/satisfyingassignment.c similarity index 100% rename from src/GMLMIP-0.1/formulas/satisfyingassignment.c rename to src/lib/GMLMIP-0.1/formulas/satisfyingassignment.c diff --git a/src/GMLMIP-0.1/formulas/satisfyingassignment.h b/src/lib/GMLMIP-0.1/formulas/satisfyingassignment.h similarity index 100% rename from src/GMLMIP-0.1/formulas/satisfyingassignment.h rename to src/lib/GMLMIP-0.1/formulas/satisfyingassignment.h diff --git a/src/GMLMIP-0.1/input b/src/lib/GMLMIP-0.1/input similarity index 100% rename from src/GMLMIP-0.1/input rename to src/lib/GMLMIP-0.1/input diff --git a/src/GMLMIP-0.1/main.cpp b/src/lib/GMLMIP-0.1/main.cpp similarity index 100% rename from src/GMLMIP-0.1/main.cpp rename to src/lib/GMLMIP-0.1/main.cpp diff --git a/src/GMLMIP-0.1/makefile b/src/lib/GMLMIP-0.1/makefile similarity index 100% rename from src/GMLMIP-0.1/makefile rename to src/lib/GMLMIP-0.1/makefile diff --git a/src/GMLMIP-0.1/onestep-example.cpp b/src/lib/GMLMIP-0.1/onestep-example.cpp similarity index 100% rename from src/GMLMIP-0.1/onestep-example.cpp rename to src/lib/GMLMIP-0.1/onestep-example.cpp diff --git a/src/GMLMIP-0.1/onestep.c b/src/lib/GMLMIP-0.1/onestep.c similarity index 100% rename from src/GMLMIP-0.1/onestep.c rename to src/lib/GMLMIP-0.1/onestep.c diff --git a/src/GMLMIP-0.1/onestep.h b/src/lib/GMLMIP-0.1/onestep.h similarity index 100% rename from src/GMLMIP-0.1/onestep.h rename to src/lib/GMLMIP-0.1/onestep.h diff --git a/src/GMLMIP-0.1/parser/.gitignore b/src/lib/GMLMIP-0.1/parser/.gitignore similarity index 100% rename from src/GMLMIP-0.1/parser/.gitignore rename to src/lib/GMLMIP-0.1/parser/.gitignore diff --git a/src/GMLMIP-0.1/parser/makefile b/src/lib/GMLMIP-0.1/parser/makefile similarity index 100% rename from src/GMLMIP-0.1/parser/makefile rename to src/lib/GMLMIP-0.1/parser/makefile diff --git a/src/GMLMIP-0.1/parser/mlf-driver.cpp b/src/lib/GMLMIP-0.1/parser/mlf-driver.cpp similarity index 100% rename from src/GMLMIP-0.1/parser/mlf-driver.cpp rename to src/lib/GMLMIP-0.1/parser/mlf-driver.cpp diff --git a/src/GMLMIP-0.1/parser/mlf-driver.h b/src/lib/GMLMIP-0.1/parser/mlf-driver.h similarity index 100% rename from src/GMLMIP-0.1/parser/mlf-driver.h rename to src/lib/GMLMIP-0.1/parser/mlf-driver.h diff --git a/src/GMLMIP-0.1/parser/mlf-parser.yy b/src/lib/GMLMIP-0.1/parser/mlf-parser.yy similarity index 100% rename from src/GMLMIP-0.1/parser/mlf-parser.yy rename to src/lib/GMLMIP-0.1/parser/mlf-parser.yy diff --git a/src/GMLMIP-0.1/parser/mlf-scanner.ll b/src/lib/GMLMIP-0.1/parser/mlf-scanner.ll similarity index 100% rename from src/GMLMIP-0.1/parser/mlf-scanner.ll rename to src/lib/GMLMIP-0.1/parser/mlf-scanner.ll diff --git a/src/GMLMIP-0.1/parser/test.cpp b/src/lib/GMLMIP-0.1/parser/test.cpp similarity index 100% rename from src/GMLMIP-0.1/parser/test.cpp rename to src/lib/GMLMIP-0.1/parser/test.cpp diff --git a/src/GMLMIP-0.1/rand.pl b/src/lib/GMLMIP-0.1/rand.pl similarity index 100% rename from src/GMLMIP-0.1/rand.pl rename to src/lib/GMLMIP-0.1/rand.pl diff --git a/src/GMLMIP-0.1/rules/GML_premise.c b/src/lib/GMLMIP-0.1/rules/GML_premise.c similarity index 100% rename from src/GMLMIP-0.1/rules/GML_premise.c rename to src/lib/GMLMIP-0.1/rules/GML_premise.c diff --git a/src/GMLMIP-0.1/rules/GML_premise.h b/src/lib/GMLMIP-0.1/rules/GML_premise.h similarity index 100% rename from src/GMLMIP-0.1/rules/GML_premise.h rename to src/lib/GMLMIP-0.1/rules/GML_premise.h diff --git a/src/GMLMIP-0.1/rules/PML_premise.c b/src/lib/GMLMIP-0.1/rules/PML_premise.c similarity index 100% rename from src/GMLMIP-0.1/rules/PML_premise.c rename to src/lib/GMLMIP-0.1/rules/PML_premise.c diff --git a/src/GMLMIP-0.1/rules/PML_premise.h b/src/lib/GMLMIP-0.1/rules/PML_premise.h similarity index 100% rename from src/GMLMIP-0.1/rules/PML_premise.h rename to src/lib/GMLMIP-0.1/rules/PML_premise.h diff --git a/src/GMLMIP-0.1/rules/makefile b/src/lib/GMLMIP-0.1/rules/makefile similarity index 100% rename from src/GMLMIP-0.1/rules/makefile rename to src/lib/GMLMIP-0.1/rules/makefile diff --git a/src/GMLMIP-0.1/rules/node.cpp b/src/lib/GMLMIP-0.1/rules/node.cpp similarity index 100% rename from src/GMLMIP-0.1/rules/node.cpp rename to src/lib/GMLMIP-0.1/rules/node.cpp diff --git a/src/GMLMIP-0.1/rules/node.h b/src/lib/GMLMIP-0.1/rules/node.h similarity index 100% rename from src/GMLMIP-0.1/rules/node.h rename to src/lib/GMLMIP-0.1/rules/node.h diff --git a/src/GMLMIP-0.1/rules/premise.c b/src/lib/GMLMIP-0.1/rules/premise.c similarity index 100% rename from src/GMLMIP-0.1/rules/premise.c rename to src/lib/GMLMIP-0.1/rules/premise.c diff --git a/src/GMLMIP-0.1/rules/premise.h b/src/lib/GMLMIP-0.1/rules/premise.h similarity index 100% rename from src/GMLMIP-0.1/rules/premise.h rename to src/lib/GMLMIP-0.1/rules/premise.h diff --git a/src/GMLMIP-0.1/rules/radixtree.c b/src/lib/GMLMIP-0.1/rules/radixtree.c similarity index 100% rename from src/GMLMIP-0.1/rules/radixtree.c rename to src/lib/GMLMIP-0.1/rules/radixtree.c diff --git a/src/GMLMIP-0.1/rules/radixtree.h b/src/lib/GMLMIP-0.1/rules/radixtree.h similarity index 100% rename from src/GMLMIP-0.1/rules/radixtree.h rename to src/lib/GMLMIP-0.1/rules/radixtree.h diff --git a/src/GMLMIP-0.1/rules/setofconclusions.c b/src/lib/GMLMIP-0.1/rules/setofconclusions.c similarity index 100% rename from src/GMLMIP-0.1/rules/setofconclusions.c rename to src/lib/GMLMIP-0.1/rules/setofconclusions.c diff --git a/src/GMLMIP-0.1/rules/setofconclusions.h b/src/lib/GMLMIP-0.1/rules/setofconclusions.h similarity index 100% rename from src/GMLMIP-0.1/rules/setofconclusions.h rename to src/lib/GMLMIP-0.1/rules/setofconclusions.h diff --git a/src/GMLMIP-0.1/rules/sizefunctions.c b/src/lib/GMLMIP-0.1/rules/sizefunctions.c similarity index 100% rename from src/GMLMIP-0.1/rules/sizefunctions.c rename to src/lib/GMLMIP-0.1/rules/sizefunctions.c diff --git a/src/GMLMIP-0.1/rules/sizefunctions.h b/src/lib/GMLMIP-0.1/rules/sizefunctions.h similarity index 100% rename from src/GMLMIP-0.1/rules/sizefunctions.h rename to src/lib/GMLMIP-0.1/rules/sizefunctions.h diff --git a/src/GMLMIP-0.1/rules/test.cpp b/src/lib/GMLMIP-0.1/rules/test.cpp similarity index 100% rename from src/GMLMIP-0.1/rules/test.cpp rename to src/lib/GMLMIP-0.1/rules/test.cpp diff --git a/src/GMLMIP-0.1/rules/valuation.c b/src/lib/GMLMIP-0.1/rules/valuation.c similarity index 100% rename from src/GMLMIP-0.1/rules/valuation.c rename to src/lib/GMLMIP-0.1/rules/valuation.c diff --git a/src/GMLMIP-0.1/rules/valuation.h b/src/lib/GMLMIP-0.1/rules/valuation.h similarity index 100% rename from src/GMLMIP-0.1/rules/valuation.h rename to src/lib/GMLMIP-0.1/rules/valuation.h diff --git a/src/GMLMIP-0.1/satisfyingstack.h b/src/lib/GMLMIP-0.1/satisfyingstack.h similarity index 100% rename from src/GMLMIP-0.1/satisfyingstack.h rename to src/lib/GMLMIP-0.1/satisfyingstack.h diff --git a/src/GMLMIP-0.1/timeoutwrapper.sh b/src/lib/GMLMIP-0.1/timeoutwrapper.sh similarity index 100% rename from src/GMLMIP-0.1/timeoutwrapper.sh rename to src/lib/GMLMIP-0.1/timeoutwrapper.sh diff --git a/src/HashConsing.ml b/src/lib/HashConsing.ml similarity index 100% rename from src/HashConsing.ml rename to src/lib/HashConsing.ml diff --git a/src/HashConsing.mli b/src/lib/HashConsing.mli similarity index 100% rename from src/HashConsing.mli rename to src/lib/HashConsing.mli diff --git a/src/MiscSolver.ml b/src/lib/MiscSolver.ml similarity index 100% rename from src/MiscSolver.ml rename to src/lib/MiscSolver.ml diff --git a/src/MiscSolver.mli b/src/lib/MiscSolver.mli similarity index 100% rename from src/MiscSolver.mli rename to src/lib/MiscSolver.mli diff --git a/src/altGenlex.ml b/src/lib/altGenlex.ml similarity index 100% rename from src/altGenlex.ml rename to src/lib/altGenlex.ml diff --git a/src/altGenlex.mli b/src/lib/altGenlex.mli similarity index 100% rename from src/altGenlex.mli rename to src/lib/altGenlex.mli diff --git a/src/coalgcompare.ml b/src/lib/coalgcompare.ml similarity index 100% rename from src/coalgcompare.ml rename to src/lib/coalgcompare.ml diff --git a/src/genAndComp.ml b/src/lib/genAndComp.ml similarity index 100% rename from src/genAndComp.ml rename to src/lib/genAndComp.ml diff --git a/src/gmlmip.ml b/src/lib/gmlmip.ml similarity index 100% rename from src/gmlmip.ml rename to src/lib/gmlmip.ml diff --git a/src/gmlmip.mli b/src/lib/gmlmip.mli similarity index 100% rename from src/gmlmip.mli rename to src/lib/gmlmip.mli diff --git a/src/gmlmip_stub.c b/src/lib/gmlmip_stub.c similarity index 100% rename from src/gmlmip_stub.c rename to src/lib/gmlmip_stub.c diff --git a/src/minisat.ml b/src/lib/minisat.ml similarity index 100% rename from src/minisat.ml rename to src/lib/minisat.ml diff --git a/src/minisat.mli b/src/lib/minisat.mli similarity index 100% rename from src/minisat.mli rename to src/lib/minisat.mli diff --git a/src/minisat_stub.c b/src/lib/minisat_stub.c similarity index 100% rename from src/minisat_stub.c rename to src/lib/minisat_stub.c diff --git a/src/OWL.ml b/src/owl/OWL.ml similarity index 100% rename from src/OWL.ml rename to src/owl/OWL.ml diff --git a/src/OWL.mli b/src/owl/OWL.mli similarity index 100% rename from src/OWL.mli rename to src/owl/OWL.mli diff --git a/src/OWLFunctionalParser.ml b/src/owl/OWLFunctionalParser.ml similarity index 100% rename from src/OWLFunctionalParser.ml rename to src/owl/OWLFunctionalParser.ml diff --git a/src/OWLFunctionalParser.mli b/src/owl/OWLFunctionalParser.mli similarity index 100% rename from src/OWLFunctionalParser.mli rename to src/owl/OWLFunctionalParser.mli