simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 12:45:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

chore: try to fix the mdx test; cleanup makefile

Browse source
This commit is contained in:
Simon Cruanes 2019-02-16 17:51:14 -06:00 • committed by Guillaume Bury
parent c2a6c2d47b
commit ed64e6b69d
3 changed files with 8 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
Makefile
View file

@ -1,17 +1,9 @@
# copyright (c) 2014, guillaume bury # copyright (c) 2014, guillaume bury
# copyright (c) 2017, simon cruanes # copyright (c) 2017, simon cruanes
BIN=main.native
TEST_BIN=tests/test_api.native
NAME=msat
J?=3 J?=3
TIMEOUT?=30
TARGETS=src/bin/main.exe
OPTS= -j $(J) OPTS= -j $(J)
LIB=$(addprefix $(NAME), .cma .cmxa .cmxs)
build: build:
@dune build $(OPTS) @install --profile=release @dune build $(OPTS) @install --profile=release
@ -20,16 +12,10 @@ dev: build-dev test
build-dev: build-dev:
@dune build $(OPTS) @install @dune build $(OPTS) @install
test: test: build-dev
@echo "run tests…" @echo "run tests…"
@OCAMLRUNPARAM=b dune runtest --force --no-buffer @OCAMLRUNPARAM=b dune runtest --force --no-buffer
enable_log:
cd src/core; ln -sf log_real.ml log.ml
disable_log:
cd src/core; ln -sf log_dummy.ml log.ml
clean: clean:
@dune clean @dune clean
@ -59,4 +45,4 @@ WATCH=all
watch: watch:
@dune build @all -w @dune build @all -w
.PHONY: clean doc all bench install uninstall remove reinstall enable_log disable_log bin test .PHONY: clean doc all bench install uninstall remove reinstall bin test

6
README.md
View file

@ -56,6 +56,7 @@ using the `msat.sat` library. It can be loaded
as shown in the following code : as shown in the following code :
```ocaml ```ocaml
# #require "msat";;
# #require "msat.sat";; # #require "msat.sat";;
# #print_depth 0;; (* do not print details *) # #print_depth 0;; (* do not print details *)
``` ```
@ -147,7 +148,8 @@ it into clauses using `make_cnf`:
The directory `src/sudoku/` contains a simple Sudoku solver that The directory `src/sudoku/` contains a simple Sudoku solver that
uses the interface `Msat.Make_cdcl_t`. uses the interface `Msat.Make_cdcl_t`.
In essence, it implements the logical theory `CDCL(Sudoku)`. In essence, it implements the logical theory `CDCL(Sudoku)`.
The script `sudoku_solve.sh` compiles and runs the solver. The script `sudoku_solve.sh` compiles and runs the solver,
as does `dune exec src/sudoku/sudoku_solve.exe`.
It's able to parse sudoku grids denoted as 81 integers It's able to parse sudoku grids denoted as 81 integers
(see `tests/sudoku/sudoku.txt` for example). (see `tests/sudoku/sudoku.txt` for example).
@ -156,7 +158,7 @@ Here is a sample grid and the output from the solver (in roughly .5s):
```sh ```sh
$ echo '..............3.85..1.2.......5.7.....4...1...9.......5......73..2.1........4...9' > sudoku.txt $ echo '..............3.85..1.2.......5.7.....4...1...9.......5......73..2.1........4...9' > sudoku.txt
$ ./sudoku_solve.sh sudoku.txt $ dune exec src/sudoku/sudoku_solve.exe -- sudoku.txt
... ...
######################### #########################
solve grid: solve grid:

3
dune
View file

@ -1,7 +1,8 @@
(alias (alias
(name runtest) (name runtest)
(deps README.md ./sudoku_solve.sh) (deps README.md)
(locks test)
(action (progn (action (progn
(run mdx test README.md) (run mdx test README.md)
(diff? README.md README.md.corrected)))) (diff? README.md README.md.corrected))))