prepare for vendoring

.header

@@ -1,5 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)

.ocp-indent

@@ -1,4 +0,0 @@
-base=2
-with=0
-type=2
-max_indent=4

.travis.yml

@@ -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

Makefile

@@ -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

TODO.md

@@ -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 ?
-

doc/deploy

@@ -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
-

doc/index.txt

@@ -1,10 +0,0 @@
-
-mSAT
-====
-Guillaume Bury <guillaume.bury@gmail.com>
-
-* link:dev[]
-* link:0.5[]
-* link:0.5.1[]
-* link:0.6[]
-

doc/release

@@ -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
-

dune

@@ -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))))
-

dune-project

@@ -1 +0,0 @@
-(lang dune 1.1)

icnf-solve.sh

@@ -1,3 +0,0 @@
-#!/bin/sh
-
-exec dune exec tests/icnf-solve/icnf_solve.exe -- $@

msat-bin.opam

@@ -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/"
-

msat.opam

@@ -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/"
-

msat.sh

@@ -1,3 +0,0 @@
-#!/bin/sh
-
-exec dune exec --profile=release src/main/main.exe -- $@

src/sat/dune

@@ -1,11 +1,10 @@
 
-(library
+(alias
-  (name msat_sat)
+ (name runtest)
-  (public_name msat.sat)
+ (deps README.md src/core/msat.cma src/sat/msat_sat.cma (source_tree src))
-  (synopsis "purely boolean interface to Msat")
+ (locks test)
-  (libraries msat)
+ (package msat)
-  (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)
+ (action (progn
-  (ocamlopt_flags :standard -O3 -color always
+          (run mdx test README.md)
-                  -unbox-closures -unbox-closures-factor 20)
+          (diff? README.md README.md.corrected))))
-  )
 

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)
+  )
+

sudoku_solve.sh

@@ -1,4 +0,0 @@
-#!/bin/sh
-
-#exec dune exec src/sudoku/sudoku_solve.exe -- $@
-exec dune exec --profile=release src/sudoku/sudoku_solve.exe -- $@