diff --git a/.header b/.header deleted file mode 100644 index fe8863b5..00000000 --- a/.header +++ /dev/null @@ -1,5 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) diff --git a/.ocp-indent b/.ocp-indent deleted file mode 100644 index 1bfc9294..00000000 --- a/.ocp-indent +++ /dev/null @@ -1,4 +0,0 @@ -base=2 -with=0 -type=2 -max_indent=4 diff --git a/.travis.yml b/.travis.yml deleted file mode 100644 index 69defb26..00000000 --- a/.travis.yml +++ /dev/null @@ -1,18 +0,0 @@ -language: c -install: wget https://raw.githubusercontent.com/ocaml/ocaml-ci-scripts/master/.travis-docker.sh -script: bash -ex .travis-docker.sh -services: -- docker -env: - global: - - PINS="msat:. msat-bin:." - - DISTRO="ubuntu-16.04" - matrix: - - PACKAGE="msat" CAML_VERSION="4.03" - - PACKAGE="msat" CAML_VERSION="4.04" - #- PACKAGE="msat" CAML_VERSION="4.05" - - PACKAGE="msat" CAML_VERSION="4.06" - #- PACKAGE="msat" CAML_VERSION="4.08" - - PACKAGE="msat" CAML_VERSION="4.09" - - PACKAGE="msat" CAML_VERSION="4.10" - - PACKAGE="msat-bin" CAML_VERSION="4.06" TESTS=false diff --git a/Makefile b/Makefile deleted file mode 100644 index c8f09a05..00000000 --- a/Makefile +++ /dev/null @@ -1,48 +0,0 @@ -# copyright (c) 2014, guillaume bury -# copyright (c) 2017, simon cruanes - -J?=3 -OPTS= -j $(J) - -build: - @dune build $(OPTS) @install --profile=release - -dev: build-dev test - -build-dev: - @dune build $(OPTS) @install - -test: build-dev - @echo "run tests…" - @OCAMLRUNPARAM=b dune runtest --force --no-buffer - -clean: - @dune clean - -install: build-install - @dune install - -uninstall: - @dune uninstall - -doc: - @dune build $(OPTS) @doc - - -reinstall: | uninstall install - -ocp-indent: - @which ocp-indent > /dev/null || { \ - echo 'ocp-indent not found; please run `opam install ocp-indent`'; \ - exit 1 ; \ - } - -reindent: ocp-indent - @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 echo "reindenting: " - @find src '(' -name '*.ml' -or -name '*.mli' ')' -print0 | xargs -0 ocp-indent -i - -WATCH=all -watch: - @dune build @all -w - -.PHONY: clean doc all bench install uninstall remove reinstall bin test diff --git a/TODO.md b/TODO.md deleted file mode 100644 index ec05fdb5..00000000 --- a/TODO.md +++ /dev/null @@ -1,17 +0,0 @@ -# Goals - -## Main goals - -- Add a backend to send proofs to dedukti - * First, pure resolution proofs - * Then, require theories to output lemma proofs for dedukti (in some format yet to be decided) -- Allow to plug one's code into boolean propagation - * react upon propagation (possibly by propagating more, or side-effect) - * more advanced/specific propagation (2-clauses)? - * implement 'constraints' (see https://www.lri.fr/~conchon/TER/2013/3/minisat.pdf ) - -## Long term goals - -- max-sat/max-smt -- coq proofs ? - diff --git a/articles/icfp_2017.pdf b/articles/icfp_2017.pdf deleted file mode 100644 index 6251453f..00000000 Binary files a/articles/icfp_2017.pdf and /dev/null differ diff --git a/articles/mcsat-vmcai2013.pdf b/articles/mcsat-vmcai2013.pdf deleted file mode 100644 index e89e32d7..00000000 Binary files a/articles/mcsat-vmcai2013.pdf and /dev/null differ diff --git a/articles/mcsat_design.pdf b/articles/mcsat_design.pdf deleted file mode 100644 index 60ed51f0..00000000 Binary files a/articles/mcsat_design.pdf and /dev/null differ diff --git a/articles/minisat.pdf b/articles/minisat.pdf deleted file mode 100644 index 21de5cdf..00000000 Binary files a/articles/minisat.pdf and /dev/null differ diff --git a/doc/deploy b/doc/deploy deleted file mode 100755 index 8a1cb92c..00000000 --- a/doc/deploy +++ /dev/null @@ -1,28 +0,0 @@ -#!/bin/bash -e - -# Ensure we are on master branch -git checkout master - -# Generate documentation -make doc -(cd doc && asciidoc index.txt) - -# Checkout gh-pages -git checkout gh-pages -git pull - -# Copy doc to the right locations -cp doc/index.html ./ -cp msat.docdir/* ./dev/ - -# Add potentially new pages -git add ./dev/* -git add ./index.html - -# Commit it all & push -git commit -m 'Doc update' -git push - -# Get back to master branch -git checkout master - diff --git a/doc/index.txt b/doc/index.txt deleted file mode 100644 index 504ff7c5..00000000 --- a/doc/index.txt +++ /dev/null @@ -1,10 +0,0 @@ - -mSAT -==== -Guillaume Bury - -* link:dev[] -* link:0.5[] -* link:0.5.1[] -* link:0.6[] - diff --git a/doc/release b/doc/release deleted file mode 100755 index c4564484..00000000 --- a/doc/release +++ /dev/null @@ -1,34 +0,0 @@ -#!/bin/bash -e - -# Get current verison number -version=`cat VERSION` - -# Enssure we are on master branch -git checkout master - -# Generate documentation -make doc -(cd doc && asciidoc index.txt) - -# Checkout gh-pages -git checkout gh-pages -git pull - -# Create doc folder if it does not exists -mkdir -p ./$version - -# Copy doc to the right locations -cp doc/index.html ./ -cp msat.docdir/* ./$version/ - -# Add potentially new pages -git add ./$version/* -git add ./index.html - -# Commit it all & push -git commit -m "Doc release $version" -git push - -# Get back to master branch -git checkout master - diff --git a/dune b/dune deleted file mode 100644 index 8b682629..00000000 --- a/dune +++ /dev/null @@ -1,10 +0,0 @@ - -(alias - (name runtest) - (deps README.md src/core/msat.cma src/sat/msat_sat.cma (source_tree src)) - (locks test) - (package msat) - (action (progn - (run mdx test README.md) - (diff? README.md README.md.corrected)))) - diff --git a/dune-project b/dune-project deleted file mode 100644 index 7655de07..00000000 --- a/dune-project +++ /dev/null @@ -1 +0,0 @@ -(lang dune 1.1) diff --git a/icnf-solve.sh b/icnf-solve.sh deleted file mode 100755 index b8c59e75..00000000 --- a/icnf-solve.sh +++ /dev/null @@ -1,3 +0,0 @@ -#!/bin/sh - -exec dune exec tests/icnf-solve/icnf_solve.exe -- $@ diff --git a/msat-bin.opam b/msat-bin.opam deleted file mode 100644 index c31e7e3b..00000000 --- a/msat-bin.opam +++ /dev/null @@ -1,23 +0,0 @@ -opam-version: "2.0" -name: "msat-bin" -synopsis: "SAT solver binary based on the msat library" -license: "Apache-2.0" -version: "0.9.1" -author: ["Simon Cruanes" "Guillaume Bury"] -maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"] -build: [ - ["dune" "build" "@install" "-p" name "-j" jobs] - #["dune" "runtest" "-p" name "-j" jobs] {with-test} -] -depends: [ - "ocaml" { >= "4.03" } - "dune" { >= "1.1" } - "msat" { = version } - "containers" { >= "2.8.1" & < "4.0" } - "camlzip" -] -tags: [ "sat" ] -homepage: "https://github.com/Gbury/mSAT" -dev-repo: "git+https://github.com/Gbury/mSAT.git" -bug-reports: "https://github.com/Gbury/mSAT/issues/" - diff --git a/msat.opam b/msat.opam deleted file mode 100644 index 69093cae..00000000 --- a/msat.opam +++ /dev/null @@ -1,24 +0,0 @@ -opam-version: "2.0" -name: "msat" -synopsis: "Library containing a SAT solver that can be parametrized by a theory" -license: "Apache-2.0" -version: "0.9.1" -author: ["Simon Cruanes" "Guillaume Bury"] -maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"] -build: [ - ["dune" "build" "@install" "-p" name "-j" jobs] - ["dune" "build" "@doc" "-p" name] {with-doc} - ["dune" "runtest" "-p" name] {with-test} -] -depends: [ - "ocaml" { >= "4.03" } - "dune" { >= "1.1" } - "iter" { >= "1.2" } - "containers" {with-test & >= "2.8.1" & < "4.0" } - "mdx" {with-test} -] -tags: [ "sat" "smt" "cdcl" "functor" ] -homepage: "https://github.com/Gbury/mSAT" -dev-repo: "git+https://github.com/Gbury/mSAT.git" -bug-reports: "https://github.com/Gbury/mSAT/issues/" - diff --git a/msat.sh b/msat.sh deleted file mode 100755 index 6428999f..00000000 --- a/msat.sh +++ /dev/null @@ -1,3 +0,0 @@ -#!/bin/sh - -exec dune exec --profile=release src/main/main.exe -- $@ diff --git a/.gitignore b/src/sat/.gitignore similarity index 100% rename from .gitignore rename to src/sat/.gitignore diff --git a/CHANGELOG.md b/src/sat/CHANGELOG.md similarity index 100% rename from CHANGELOG.md rename to src/sat/CHANGELOG.md diff --git a/LICENSE b/src/sat/LICENSE similarity index 100% rename from LICENSE rename to src/sat/LICENSE diff --git a/README.md b/src/sat/README.md similarity index 100% rename from README.md rename to src/sat/README.md diff --git a/src/sat/dune b/src/sat/dune index 624b2a57..8b682629 100644 --- a/src/sat/dune +++ b/src/sat/dune @@ -1,11 +1,10 @@ -(library - (name msat_sat) - (public_name msat.sat) - (synopsis "purely boolean interface to Msat") - (libraries msat) - (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat) - (ocamlopt_flags :standard -O3 -color always - -unbox-closures -unbox-closures-factor 20) - ) +(alias + (name runtest) + (deps README.md src/core/msat.cma src/sat/msat_sat.cma (source_tree src)) + (locks test) + (package msat) + (action (progn + (run mdx test README.md) + (diff? README.md README.md.corrected)))) diff --git a/src/backend/Backend_intf.ml b/src/sat/src/backend/Backend_intf.ml similarity index 100% rename from src/backend/Backend_intf.ml rename to src/sat/src/backend/Backend_intf.ml diff --git a/src/backend/Coq.ml b/src/sat/src/backend/Coq.ml similarity index 100% rename from src/backend/Coq.ml rename to src/sat/src/backend/Coq.ml diff --git a/src/backend/Coq.mli b/src/sat/src/backend/Coq.mli similarity index 100% rename from src/backend/Coq.mli rename to src/sat/src/backend/Coq.mli diff --git a/src/backend/Dedukti.ml b/src/sat/src/backend/Dedukti.ml similarity index 100% rename from src/backend/Dedukti.ml rename to src/sat/src/backend/Dedukti.ml diff --git a/src/backend/Dedukti.mli b/src/sat/src/backend/Dedukti.mli similarity index 100% rename from src/backend/Dedukti.mli rename to src/sat/src/backend/Dedukti.mli diff --git a/src/backend/Dot.ml b/src/sat/src/backend/Dot.ml similarity index 100% rename from src/backend/Dot.ml rename to src/sat/src/backend/Dot.ml diff --git a/src/backend/Dot.mli b/src/sat/src/backend/Dot.mli similarity index 100% rename from src/backend/Dot.mli rename to src/sat/src/backend/Dot.mli diff --git a/src/backend/dune b/src/sat/src/backend/dune similarity index 100% rename from src/backend/dune rename to src/sat/src/backend/dune diff --git a/src/backtrack/Backtrackable_ref.ml b/src/sat/src/backtrack/Backtrackable_ref.ml similarity index 100% rename from src/backtrack/Backtrackable_ref.ml rename to src/sat/src/backtrack/Backtrackable_ref.ml diff --git a/src/backtrack/Backtrackable_ref.mli b/src/sat/src/backtrack/Backtrackable_ref.mli similarity index 100% rename from src/backtrack/Backtrackable_ref.mli rename to src/sat/src/backtrack/Backtrackable_ref.mli diff --git a/src/backtrack/Msat_backtrack.ml b/src/sat/src/backtrack/Msat_backtrack.ml similarity index 100% rename from src/backtrack/Msat_backtrack.ml rename to src/sat/src/backtrack/Msat_backtrack.ml diff --git a/src/backtrack/dune b/src/sat/src/backtrack/dune similarity index 100% rename from src/backtrack/dune rename to src/sat/src/backtrack/dune diff --git a/src/core/Heap.ml b/src/sat/src/core/Heap.ml similarity index 100% rename from src/core/Heap.ml rename to src/sat/src/core/Heap.ml diff --git a/src/core/Heap.mli b/src/sat/src/core/Heap.mli similarity index 100% rename from src/core/Heap.mli rename to src/sat/src/core/Heap.mli diff --git a/src/core/Heap_intf.ml b/src/sat/src/core/Heap_intf.ml similarity index 100% rename from src/core/Heap_intf.ml rename to src/sat/src/core/Heap_intf.ml diff --git a/src/core/Internal.ml b/src/sat/src/core/Internal.ml similarity index 100% rename from src/core/Internal.ml rename to src/sat/src/core/Internal.ml diff --git a/src/core/Log.ml b/src/sat/src/core/Log.ml similarity index 100% rename from src/core/Log.ml rename to src/sat/src/core/Log.ml diff --git a/src/core/Log.mli b/src/sat/src/core/Log.mli similarity index 100% rename from src/core/Log.mli rename to src/sat/src/core/Log.mli diff --git a/src/core/Msat.ml b/src/sat/src/core/Msat.ml similarity index 100% rename from src/core/Msat.ml rename to src/sat/src/core/Msat.ml diff --git a/src/core/Solver.ml b/src/sat/src/core/Solver.ml similarity index 100% rename from src/core/Solver.ml rename to src/sat/src/core/Solver.ml diff --git a/src/core/Solver.mli b/src/sat/src/core/Solver.mli similarity index 100% rename from src/core/Solver.mli rename to src/sat/src/core/Solver.mli diff --git a/src/core/Solver_intf.ml b/src/sat/src/core/Solver_intf.ml similarity index 100% rename from src/core/Solver_intf.ml rename to src/sat/src/core/Solver_intf.ml diff --git a/src/core/Vec.ml b/src/sat/src/core/Vec.ml similarity index 100% rename from src/core/Vec.ml rename to src/sat/src/core/Vec.ml diff --git a/src/core/Vec.mli b/src/sat/src/core/Vec.mli similarity index 100% rename from src/core/Vec.mli rename to src/sat/src/core/Vec.mli diff --git a/src/core/dune b/src/sat/src/core/dune similarity index 100% rename from src/core/dune rename to src/sat/src/core/dune diff --git a/src/core/msat.mld b/src/sat/src/core/msat.mld similarity index 100% rename from src/core/msat.mld rename to src/sat/src/core/msat.mld diff --git a/src/dune b/src/sat/src/dune similarity index 100% rename from src/dune rename to src/sat/src/dune diff --git a/src/index.mld b/src/sat/src/index.mld similarity index 100% rename from src/index.mld rename to src/sat/src/index.mld diff --git a/src/main/Dimacs_lex.mll b/src/sat/src/main/Dimacs_lex.mll similarity index 100% rename from src/main/Dimacs_lex.mll rename to src/sat/src/main/Dimacs_lex.mll diff --git a/src/main/Dimacs_parse.mly b/src/sat/src/main/Dimacs_parse.mly similarity index 100% rename from src/main/Dimacs_parse.mly rename to src/sat/src/main/Dimacs_parse.mly diff --git a/src/main/dune b/src/sat/src/main/dune similarity index 100% rename from src/main/dune rename to src/sat/src/main/dune diff --git a/src/main/main.ml b/src/sat/src/main/main.ml similarity index 100% rename from src/main/main.ml rename to src/sat/src/main/main.ml diff --git a/src/sat/Int_lit.ml b/src/sat/src/sat/Int_lit.ml similarity index 100% rename from src/sat/Int_lit.ml rename to src/sat/src/sat/Int_lit.ml diff --git a/src/sat/Int_lit.mli b/src/sat/src/sat/Int_lit.mli similarity index 100% rename from src/sat/Int_lit.mli rename to src/sat/src/sat/Int_lit.mli diff --git a/src/sat/Msat_sat.ml b/src/sat/src/sat/Msat_sat.ml similarity index 100% rename from src/sat/Msat_sat.ml rename to src/sat/src/sat/Msat_sat.ml diff --git a/src/sat/Msat_sat.mli b/src/sat/src/sat/Msat_sat.mli similarity index 100% rename from src/sat/Msat_sat.mli rename to src/sat/src/sat/Msat_sat.mli diff --git a/src/sat/src/sat/dune b/src/sat/src/sat/dune new file mode 100644 index 00000000..624b2a57 --- /dev/null +++ b/src/sat/src/sat/dune @@ -0,0 +1,11 @@ + +(library + (name msat_sat) + (public_name msat.sat) + (synopsis "purely boolean interface to Msat") + (libraries msat) + (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat) + (ocamlopt_flags :standard -O3 -color always + -unbox-closures -unbox-closures-factor 20) + ) + diff --git a/src/sudoku/dune b/src/sat/src/sudoku/dune similarity index 100% rename from src/sudoku/dune rename to src/sat/src/sudoku/dune diff --git a/src/sudoku/sudoku_solve.ml b/src/sat/src/sudoku/sudoku_solve.ml similarity index 100% rename from src/sudoku/sudoku_solve.ml rename to src/sat/src/sudoku/sudoku_solve.ml diff --git a/src/tseitin/Msat_tseitin.ml b/src/sat/src/tseitin/Msat_tseitin.ml similarity index 100% rename from src/tseitin/Msat_tseitin.ml rename to src/sat/src/tseitin/Msat_tseitin.ml diff --git a/src/tseitin/Msat_tseitin.mli b/src/sat/src/tseitin/Msat_tseitin.mli similarity index 100% rename from src/tseitin/Msat_tseitin.mli rename to src/sat/src/tseitin/Msat_tseitin.mli diff --git a/src/tseitin/Tseitin_intf.ml b/src/sat/src/tseitin/Tseitin_intf.ml similarity index 100% rename from src/tseitin/Tseitin_intf.ml rename to src/sat/src/tseitin/Tseitin_intf.ml diff --git a/src/tseitin/dune b/src/sat/src/tseitin/dune similarity index 100% rename from src/tseitin/dune rename to src/sat/src/tseitin/dune diff --git a/sudoku_solve.sh b/sudoku_solve.sh deleted file mode 100755 index 93e8a2fa..00000000 --- a/sudoku_solve.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/sh - -#exec dune exec src/sudoku/sudoku_solve.exe -- $@ -exec dune exec --profile=release src/sudoku/sudoku_solve.exe -- $@