mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-11 05:28:34 -05:00
Cleaned makefile a bit + moved the testing binary
This commit is contained in:
parent
f348dcd5ae
commit
cb8092af3b
6 changed files with 8 additions and 62 deletions
2
.gitignore
vendored
2
.gitignore
vendored
|
|
@ -1,5 +1,4 @@
|
||||||
_build/
|
_build/
|
||||||
tests/main
|
|
||||||
*.annot
|
*.annot
|
||||||
*.native
|
*.native
|
||||||
*.log
|
*.log
|
||||||
|
|
@ -8,3 +7,4 @@ tests/main
|
||||||
.session
|
.session
|
||||||
*.docdir
|
*.docdir
|
||||||
util/log.ml
|
util/log.ml
|
||||||
|
msat
|
||||||
|
|
|
||||||
18
Makefile
18
Makefile
|
|
@ -6,8 +6,7 @@ FLAGS=
|
||||||
#-ocamlc ocamlopt -cflag -O3
|
#-ocamlc ocamlopt -cflag -O3
|
||||||
DIRS=-Is solver,sat,smt,backend,util,util/smtlib
|
DIRS=-Is solver,sat,smt,backend,util,util/smtlib
|
||||||
DOC=msat.docdir/index.html
|
DOC=msat.docdir/index.html
|
||||||
TEST=sat_solve.native
|
BIN=main.native
|
||||||
|
|
||||||
NAME=msat
|
NAME=msat
|
||||||
|
|
||||||
LIB=$(addprefix $(NAME), .cma .cmxa .cmxs)
|
LIB=$(addprefix $(NAME), .cma .cmxa .cmxs)
|
||||||
|
|
@ -20,10 +19,11 @@ lib:
|
||||||
doc:
|
doc:
|
||||||
$(COMP) $(FLAGS) $(DIRS) $(DOC)
|
$(COMP) $(FLAGS) $(DIRS) $(DOC)
|
||||||
|
|
||||||
build-test:
|
bin:
|
||||||
$(COMP) $(FLAGS) $(DIRS) $(TEST)
|
$(COMP) $(FLAGS) $(DIRS) $(BIN)
|
||||||
|
cp $(BIN) $(NAME) && rm $(BIN)
|
||||||
|
|
||||||
test: build-test
|
test: bin
|
||||||
@/usr/bin/time -f "%e" ./tests/run smt
|
@/usr/bin/time -f "%e" ./tests/run smt
|
||||||
@/usr/bin/time -f "%e" ./tests/run mcsat
|
@/usr/bin/time -f "%e" ./tests/run mcsat
|
||||||
|
|
||||||
|
|
@ -33,12 +33,6 @@ enable_log:
|
||||||
disable_log:
|
disable_log:
|
||||||
cd util; ln -sf log_dummy.ml log.ml
|
cd util; ln -sf log_dummy.ml log.ml
|
||||||
|
|
||||||
bench: build-test
|
|
||||||
cd bench && $(MAKE)
|
|
||||||
|
|
||||||
stats:
|
|
||||||
@./bench_stats.native
|
|
||||||
|
|
||||||
log:
|
log:
|
||||||
cat _build/$(LOG) || true
|
cat _build/$(LOG) || true
|
||||||
|
|
||||||
|
|
@ -57,4 +51,4 @@ reinstall: all
|
||||||
ocamlfind remove msat || true
|
ocamlfind remove msat || true
|
||||||
ocamlfind install msat $(TO_INSTALL)
|
ocamlfind install msat $(TO_INSTALL)
|
||||||
|
|
||||||
.PHONY: clean doc all bench install uninstall reinstall enable_log disable_log
|
.PHONY: clean doc all bench install uninstall reinstall enable_log disable_log bin test
|
||||||
|
|
|
||||||
|
|
@ -1,36 +0,0 @@
|
||||||
SOLVER :=../sat_solve.native
|
|
||||||
OPTIONS :=-time 30s -size 1G
|
|
||||||
|
|
||||||
LOGDIR := $(shell echo "./logs/`git rev-parse HEAD`")
|
|
||||||
INDEX := $(shell echo "./$(LOGDIR)/index")
|
|
||||||
CNF := $(shell find -L ./ -name "*.cnf" -type f)
|
|
||||||
DONE := $(addprefix $(LOGDIR)/raw/, $(CNF:=.done))
|
|
||||||
|
|
||||||
PROVER := $(shell echo "./$(LOGDIR)/prover")
|
|
||||||
CMD := $(PROVER) $(OPTIONS)
|
|
||||||
|
|
||||||
DATE = date +'%H:%M:%S %d/%m/%Y'
|
|
||||||
|
|
||||||
all: $(INDEX)
|
|
||||||
|
|
||||||
sync:
|
|
||||||
rsync -avz rsync://gbury.eu/benchs/ ./
|
|
||||||
|
|
||||||
$(INDEX): dummy $(PROVER) $(DONE)
|
|
||||||
@echo "Bench ended for commit `git rev-parse HEAD` at `$(DATE)`" | tee -a $(INDEX)
|
|
||||||
|
|
||||||
dummy: $(PROVER)
|
|
||||||
@echo "Bench started for commit `git rev-parse HEAD` at `$(DATE)`" | tee -a $(INDEX)
|
|
||||||
|
|
||||||
$(PROVER): $(SOLVER)
|
|
||||||
@mkdir -p $(LOGDIR)/raw
|
|
||||||
@cp $(SOLVER) $(PROVER)
|
|
||||||
|
|
||||||
$(SOLVER):
|
|
||||||
cd .. && $(MAKE)
|
|
||||||
|
|
||||||
$(LOGDIR)/raw/%.done : dummy $(PROVER)
|
|
||||||
@mkdir -p $(dir $@)
|
|
||||||
@echo "solving problem $*..." | tee -a $(INDEX)
|
|
||||||
@./run_prover "$(CMD)" "$*" "$@"
|
|
||||||
|
|
||||||
|
|
@ -1,12 +0,0 @@
|
||||||
#!/bin/bash
|
|
||||||
|
|
||||||
CMD="$1"
|
|
||||||
FILE="$2"
|
|
||||||
LOG="$3"
|
|
||||||
|
|
||||||
/usr/bin/time -f "%e" $CMD $FILE > $3 2>&1
|
|
||||||
RET=$?
|
|
||||||
if [ $RET -ne 0 ];
|
|
||||||
then
|
|
||||||
echo "Error code $RET while solving $FILE"
|
|
||||||
fi
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
#!/bin/bash
|
#!/bin/bash
|
||||||
|
|
||||||
CURDIR=`dirname $0`
|
CURDIR=`dirname $0`
|
||||||
SOLVER="$CURDIR/../sat_solve.native"
|
SOLVER="$CURDIR/../msat"
|
||||||
|
|
||||||
solvertest () {
|
solvertest () {
|
||||||
for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'`
|
for f in `find -L $1 -type f -name '*.cnf' -o -name '*.smt2'`
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue