mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 11:15:43 -05:00
test: add basic test for DRUP proof production
This commit is contained in:
parent
e6fc7e7357
commit
d117d656c5
3 changed files with 26 additions and 0 deletions
10
src/tests/basic.cnf
Normal file
10
src/tests/basic.cnf
Normal file
|
|
@ -0,0 +1,10 @@
|
||||||
|
p cnf 4 8
|
||||||
|
1 2 -3 0
|
||||||
|
-1 -2 3 0
|
||||||
|
2 3 -4 0
|
||||||
|
-2 -3 4 0
|
||||||
|
1 3 4 0
|
||||||
|
-1 -3 -4 0
|
||||||
|
-1 2 4 0
|
||||||
|
1 -2 -4 0
|
||||||
|
|
||||||
4
src/tests/basic.drup.expected
Normal file
4
src/tests/basic.drup.expected
Normal file
|
|
@ -0,0 +1,4 @@
|
||||||
|
-4 -1 0
|
||||||
|
-1 0
|
||||||
|
-3 0
|
||||||
|
0
|
||||||
|
|
@ -14,3 +14,15 @@
|
||||||
(progn
|
(progn
|
||||||
(run ./run_tests.exe alcotest) ; run regressions first
|
(run ./run_tests.exe alcotest) ; run regressions first
|
||||||
(run ./run_tests.exe qcheck --verbose))))
|
(run ./run_tests.exe qcheck --verbose))))
|
||||||
|
|
||||||
|
(rule
|
||||||
|
(targets basic.drup)
|
||||||
|
(deps (:pb basic.cnf) (:solver ../main/main.exe))
|
||||||
|
(action (run %{solver} %{pb} -t 2 -o %{targets})))
|
||||||
|
|
||||||
|
(alias
|
||||||
|
(name runtest)
|
||||||
|
(locks /test)
|
||||||
|
(package sidekick-bin)
|
||||||
|
(action
|
||||||
|
(diff basic.drup basic.drup.expected)))
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue