diff --git a/Makefile b/Makefile index 77d9ca76..d7d7cacc 100644 --- a/Makefile +++ b/Makefile @@ -26,22 +26,21 @@ clean: test: @dune runtest --force --no-buffer -TESTOPTS ?= -j $(J) +TESTOPTS ?= -j $(J) -c tests/logitest.sexp TESTTOOL=logitest DATE=$(shell date +%FT%H:%M) -logitest-quick: +snapshots: @mkdir -p snapshots - $(TESTTOOL) run -c tests/conf.toml $(TESTOPTS) \ - --meta `git rev-parse HEAD` --csv snapshots/quick-$(DATE).csv tests/sat tests/unsat/ tests/pigeon -logitest-smt-QF_UF: - @mkdir -p snapshots - $(TESTTOOL) run -c tests/conf.toml $(TESTOPTS) \ - --meta `git rev-parse HEAD` --csv snapshots/smt-QF_UF-$(DATE).csv tests/QF_UF -logitest-smt-QF_DT: - @mkdir -p snapshots - $(TESTTOOL) run -c tests/conf.toml $(TESTOPTS) \ - --meta `git rev-parse HEAD` --csv snapshots/smt-QF_DT-$(DATE).csv tests/QF_DT +logitest-quick: snapshots + $(TESTTOOL) run $(TESTOPTS) \ + --csv snapshots/quick-$(DATE).csv --task sidekick-smt-quick +logitest-smt-QF_UF: snapshots + $(TESTTOOL) run $(TESTOPTS) \ + --csv snapshots/smt-QF_UF-$(DATE).csv --task sidekick-smt-nodir tests/QF_UF +logitest-smt-QF_DT: snapshots + $(TESTTOOL) run $(TESTOPTS) \ + --csv snapshots/smt-QF_DT-$(DATE).csv --task sidekick-smt-nodir tests/QF_DT install: build-install @dune install diff --git a/tests/logitest.sexp b/tests/logitest.sexp index 586830a9..9a347b4f 100644 --- a/tests/logitest.sexp +++ b/tests/logitest.sexp @@ -7,6 +7,27 @@ (unknown "Timeout|Unknown") (version "git:.")) +(dir + (path $cur_dir) + (pattern ".*.(smt2|cnf)") + (expect (try (run smtlib-read-status) (run z3)))) + +(task + (name sidekick-smt-quick) + (action + (run_provers + (provers sidekick-dev z3) + (timeout 10) + (dirs $cur_dir/sat $cur_dir/unsat $cur_dir/pigeon)))) + +(task + (name sidekick-smt-nodir) + (action + (run_provers + (provers sidekick-dev z3) + (timeout 10) + (dirs)))) + (task (name sidekick-smt-all) (action