Gus Smith
0b88cdac90
Remove req assertion; make assertion richer
2025-12-29 12:28:06 -08:00
Gus Smith
a41fdb6784
Fix: rename path
2025-12-29 11:37:48 -08:00
Gus Smith
4decc31933
Split cover stage into two final stages
2025-12-29 09:38:07 -08:00
Gus Smith
6c8a26eb86
Update script
2025-12-29 09:34:18 -08:00
Gus Smith
531e328c3d
Update sby file
2025-12-29 09:34:04 -08:00
Gus Smith
5abce0c9ee
Update readme
2025-12-29 09:32:33 -08:00
Gus Smith
4a4d75df6a
We still need to run the actual prep pass
2025-12-29 09:07:24 -08:00
Gus Smith
889bfab8c9
Explicitly skip prep
2025-12-29 09:07:11 -08:00
Gus Smith
01f5c10cd7
Adds notes to readme
2025-12-29 08:32:49 -08:00
Gus Smith
e904e88fc9
Use labels to be more like SCY
2025-12-15 17:36:36 -08:00
Gus Smith
7c66b2d132
Remove redundant cd
2025-12-15 13:24:13 -08:00
Gus Smith
07669fde92
Revert "Rework file based on new understanding of make"
...
This reverts commit 2b38c31936
2025-12-15 13:20:32 -08:00
Gus Smith
36fcd8fbc8
Revert "Get rid of unnecessary file"
...
This reverts commit f9bee0464b
2025-12-15 13:20:28 -08:00
Gus Smith
f9bee0464b
Get rid of unnecessary file
2025-12-15 13:04:25 -08:00
Gus Smith
2b38c31936
Rework file based on new understanding of make
2025-12-15 13:00:58 -08:00
Gus Smith
8274979147
Update readme
2025-12-15 12:47:36 -08:00
Gus Smith
9779436d0b
Simplify script by relying on sby's prep routine
2025-12-15 12:41:47 -08:00
Gus Smith
1ee552a502
Syntax
2025-12-15 12:41:38 -08:00
Gus Smith
358ccf3ab6
Reindent
2025-12-15 12:30:06 -08:00
Gus Smith
a0ab7de28c
Fix readme
2025-12-15 12:27:24 -08:00
Gus Smith
4be8853a32
Add readme
2025-12-09 11:20:27 -08:00
Gus Smith
ad93d4fc4f
Add initial test impl
2025-12-09 11:17:33 -08:00
Krystine Sherwin
d8e276983e
no_props.sby: Add btor_cover placeholder
...
The test infrastructure doesn't like when the `cover` tag is used but there is no task that uses it (because it thinks it is a task rather than a tag).
2025-09-30 11:22:13 +13:00
Krystine Sherwin
db782815f2
More tests without properties
...
Used `sby --autotune` to find other engines which fail (though there aren't any other exceptions that I could find).
Parse errors from `abc bmc3` and `abc sim3` instead of returning UNKNOWN.
2025-09-30 10:32:49 +13:00
Krystine Sherwin
c06d8682cd
Fix abc crash when aiger_props is empty
...
Includes test reproducer from #338 , modified to also test `abc --keep-going pdr`.
2025-09-30 10:26:36 +13:00
Krystine Sherwin
5fffe7eda6
Fix heredoc in sub dir
...
Also change log to use absolute path for consistency with the copy/link logs.
2025-08-02 10:40:52 +12:00
Krystine Sherwin
1d28294391
More directory tests
...
Confirming that the changes to path handling didn't break anything.
`~/` works locally, but I'm not sure how to actually include that as a test.
2025-08-02 10:38:35 +12:00
Krystine Sherwin
a215e3260a
tests/links/symlink: Check file count
...
And also that `src/dir/script.ys` exists
2025-08-02 10:07:06 +12:00
Krystine Sherwin
a906714c95
Add test for copying directories
...
As per https://stackoverflow.com/a/54950959 , `os.path.basename()` returns an empty string if the string ends with a trailing slash. This means that the target implied by `dir/` differs from an explicit target of `dir/`, and changes the behaviour to copy files to the root `src` directory instead.
2025-08-02 09:17:21 +12:00
Krystine Sherwin
3bf5be0637
Add jsonl status format
...
Replace `--statuscsv` and `--livecsv` with `--statusfmt <fmt>` and `--live <fmt` respectively.
Currently supports both csv and jsonl.
In the case of `--live`, updates can be printed in multiple formats, while `--statusfmt` only supports one at a time.
2025-07-29 10:00:52 +12:00
Krystine Sherwin
7c5c96f5ca
Don't use -f for intertask tests...
...
... if we expect the database to still contain previous runs.
Use `rm -rf` to clear directories by hand instead.
2025-07-09 10:40:49 +12:00
Krystine Sherwin
63b43c7e66
tests: Add long running cancellation
...
Actually exercise the database cancellation working on an already running task.
This appears to work even with `make -j1`.
2025-07-09 10:04:58 +12:00
Krystine Sherwin
360f1b03a3
tests/intertask: Use bash script
...
Somewhat hacky use of the automatic task collection splitting tasks into separate make targets.
2025-07-09 10:04:37 +12:00
Krystine Sherwin
5fc8df43f8
Intertask cancellation via database
...
Task checking via database rated limited to once every 10s.
Rename killer.sby to cancelledby.sby and add Makefile for testing.
2025-07-09 10:03:54 +12:00
Krystine Sherwin
e7c756a43f
Add cancelledby config section
2025-07-09 10:03:54 +12:00
Krystine Sherwin
a153349ac8
Initial intertask cancellation
...
Taskloops store tasks_done, tasks can be cancelled, and if a task named "killer" is in tasks_done then any other tasks are cancelled.
2025-07-09 10:03:54 +12:00
KrystalDelusion
1130847901
Merge branch 'main' into krys/symlink
2025-07-09 10:01:30 +12:00
Krystine Sherwin
73c5e5cae6
timeout.sby: Add non-timeout equivalents
...
Number of properties reported should be consistent whether the task times out or finishes.
Currently fails `btor_fin_cover`.
2025-07-08 17:10:01 +12:00
Krystine Sherwin
83723696c7
Update failing test
...
Each property can have more than one status, but we only need to test the last one.
Also fix the warning about `\c` being an invalid escape.
2025-07-08 16:04:45 +12:00
Krystine Sherwin
aa2d3ed025
Add and use --latest flag for statuses
...
Should fix CI problem of running tests twice and the verific and non verific
properties having different names when testing the statusdb.
2025-07-08 15:47:34 +12:00
Krystine Sherwin
4adf5e5259
timeout.sby: Increase depth
...
CI was too fast
2025-07-08 15:47:34 +12:00
Krystine Sherwin
41bd894eff
Test property statuses after timeout
2025-07-08 15:47:34 +12:00
Krystine Sherwin
b1d9bcbb42
tests: Add statusdb test
...
Ensures that `--statusreset` doesn't break the schema.
2025-07-08 15:44:02 +12:00
Krystine Sherwin
b80a843995
tests/links: heredocs are never linked
2025-07-05 15:46:40 +12:00
Krystine Sherwin
911ae02ee5
Test property statuses for cover_assert
...
Cover properties shouldn't be marked fail when the test failed early due to an assertion.
This should fail without other changes.
2025-07-05 12:40:57 +12:00
Krystine Sherwin
4d8462b58e
Add cover_assert option
2025-07-05 11:17:05 +12:00
Krystine Sherwin
aa7d8ab4ce
Reapply "Remove asserts during cover mode"
...
This reverts commit 205245c827
2025-07-02 18:00:28 +12:00
Krystine Sherwin
205245c827
Revert "Remove asserts during cover mode"
...
This reverts commit 81873292c9
2025-07-02 17:59:46 +12:00
Krystine Sherwin
81873292c9
Remove asserts during cover mode
2025-07-02 17:57:31 +12:00
Krystine Sherwin
2a16a48a60
collect_tests.py: Ignore sby status dirs
...
Status directories are normally ignored because they have a sqlite file, but it's possible to create a status dir without a database when using `--setup`.
2025-07-01 10:50:46 +12:00
