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

update benchpress file to actually run proofs

Browse source
This commit is contained in:
Simon Cruanes 2021-12-07 21:16:12 -05:00
parent 2d8fc78bc4
commit 110f3f8527
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
2 changed files with 27 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
Makefile
View file

@ -35,6 +35,9 @@ snapshots:
$(TESTTOOL)-quick: snapshots
$(TESTTOOL) run $(TESTOPTS) \
--csv snapshots/quick-$(DATE).csv --task sidekick-smt-quick
$(TESTTOOL)-quick-proofs: snapshots
$(TESTTOOL) run $(TESTOPTS) \
--csv snapshots/quick-$(DATE).csv --task sidekick-smt-quick-proofs --proof-dir out-proofs-$(DATE)/
$(TESTTOOL)-local: snapshots
$(TESTTOOL) run $(TESTOPTS) \
--csv snapshots/quick-$(DATE).csv --task sidekick-smt-local

24
tests/benchpress.sexp
View file

@ -7,6 +7,20 @@
(unknown "Timeout|Unknown")
(version "git:."))
(proof_checker
(name quip)
(cmd "quip -nc $proof_file --problem=$file")
(valid "^OK$")
(invalid "^FAIL$"))
(prover
(name sidekick-dev-p)
(inherits sidekick-dev)
(cmd "$cur_dir/../sidekick --no-check --time $timeout $file -o $proof_file")
(proof_ext ".quip.gz")
(proof_checker quip)
(produces_proof true))
(dir
(path $cur_dir)
(pattern ".*.(smt2|cnf)$")
@ -20,6 +34,16 @@
(timeout 10)
(dirs ($cur_dir/sat $cur_dir/unsat $cur_dir/pigeon)))))
; only unsat SMT problems
(task
(name sidekick-smt-quick-proofs)
(action
(run_provers
(provers (sidekick-dev sidekick-dev-p z3))
(timeout 10)
(pattern ".*.smt2$")
(dirs ($cur_dir/unsat)))))
(task
(name sidekick-smt-local)
(action