mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 11:45:41 -05:00
Makefile for benchs.
This commit is contained in:
parent
3422634923
commit
b6aa6ed2fc
3 changed files with 31 additions and 51 deletions
|
|
@ -1,27 +1,28 @@
|
|||
SOLVER =../sat_solve.native
|
||||
OPTIONS =-t 30s -s 1G
|
||||
CMD = $(SOLVER) $(OPTIONS)
|
||||
SOLVER :=../sat_solve.native
|
||||
OPTIONS :=-t 30s -s 1G
|
||||
|
||||
LOGDIR := logs
|
||||
LOG := $(shell date +'$(LOGDIR)/sat_%Y-%m-%d-%H%M')
|
||||
CNF := $(shell find ./ -name "*.cnf" -type f)
|
||||
DONE := $(CNF:.cnf=.done)
|
||||
LOGDIR := $(shell echo "logs/`git rev-parse HEAD`")
|
||||
LOGDIRE := $(shell echo "logs\/`git rev-parse HEAD`")
|
||||
INDEX := $(shell echo "$(LOGDIR)/index")
|
||||
CNF := $(shell find ./ -name "*.cnf" -type f)
|
||||
DONE := $(addprefix $(LOGDIR)/raw/, $(CNF:.cnf=.done))
|
||||
|
||||
all: $(LOG) $(DONE)
|
||||
@find ./ -name "*.done" -type f -delete
|
||||
PROVER := $(shell echo "$(LOGDIR)/prover")
|
||||
CMD := $(PROVER) $(OPTIONS)
|
||||
|
||||
all: $(INDEX)
|
||||
@echo "All done."
|
||||
|
||||
$(LOG):
|
||||
@mkdir -p $(LOGDIR)
|
||||
@touch $(LOG)
|
||||
@echo "Log file : $(LOG)"
|
||||
@echo "Date : `date +'%H:%M %d-%m-%Y'`" | tee -a $(LOG)
|
||||
@echo "Command : '$(CMD)'" | tee -a $(LOG)
|
||||
@echo "Commit : `git rev-parse HEAD`" | tee -a $(LOG)
|
||||
$(INDEX): $(PROVER) $(DONE)
|
||||
@echo "Ended at `date +'%H:%M:%S %d/%m/%Y'`" > $(INDEX)
|
||||
@echo "Index created"
|
||||
|
||||
%.done : %.cnf $(LOG)
|
||||
@./run_prover "$(CMD)" "$*" "$(LOG)"
|
||||
@touch $*.done
|
||||
$(PROVER):
|
||||
@echo "Creating log directory..." && mkdir -p $(LOGDIR)/raw
|
||||
@echo "Copying prover..." && cp $(SOLVER) $(PROVER)
|
||||
|
||||
$(LOGDIR)/raw/%.done : $(PROVER)
|
||||
@mkdir -p $(dir $@)
|
||||
@echo "solving problem $*.cnf..."
|
||||
@./run_prover "$(CMD)" "$*.cnf" "$@"
|
||||
|
||||
clean:
|
||||
@find ./ -name "*.done" -type f -delete
|
||||
|
|
|
|||
26
bench/run
26
bench/run
|
|
@ -1,26 +0,0 @@
|
|||
#!/bin/bash
|
||||
|
||||
CURDIR=`dirname $0`
|
||||
SOLVER="$CURDIR/../sat_solve.native"
|
||||
|
||||
solvertest () {
|
||||
for f in `find -L $1 -name *.cnf -type f`
|
||||
do
|
||||
echo -ne "\r\033[KTesting $f..."
|
||||
"$SOLVER" -t 5s -s 1G $f | grep $2 > /dev/null 2> /dev/null
|
||||
RET=$?
|
||||
if [ $RET -ne 0 ];
|
||||
then
|
||||
echo -e "\r\033[K\e[31m[KO]\e[0m $f"
|
||||
exit 2
|
||||
fi
|
||||
done
|
||||
echo -e "\r\033[K\e[32m[OK]\e[0m $2"
|
||||
}
|
||||
|
||||
all () {
|
||||
solvertest "$CURDIR/flatgraph/" "Sat"
|
||||
solvertest "$CURDIR/morphgraph/" "Sat"
|
||||
}
|
||||
|
||||
time all
|
||||
|
|
@ -1,7 +1,12 @@
|
|||
#!/bin/bash
|
||||
|
||||
CMD="$0"
|
||||
FILE="$1"
|
||||
LOG="$2"
|
||||
CMD="$1"
|
||||
FILE="$2"
|
||||
LOG="$3"
|
||||
|
||||
sleep 1
|
||||
/usr/bin/time -f "%e" $CMD $FILE > $3 2>&1
|
||||
RET=$?
|
||||
if [ $RET -ne 0 ];
|
||||
then
|
||||
echo "Error code $RET while solving $FILE"
|
||||
fi
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue