Age | Commit message (Collapse) | Author |
|
This commit adds testing infrastructure for LFSC signatures that is
enabled when CVC4 is configured with LFSC. The testing infrastructure
adopts run_test.py from https://github.com/CVC4/LFSC with minor
modifications (mainly adding support for a list of include directories
that are searched to resolve *.plf dependencies). The commit uses the
existing examples and test files from proofs/signatures as the initial
set of tests.
Co-authored-by: Alex Ozdemir aozdemir@hmc.edu
|
|
* LRAT signature
Added an LRAT signature. It is almost entirely side-conditions, but it
works.
There is also a collection of tests for it. You can run them by invoking
```
lfscc smt.plf sat.plf lrat.plf lrat_test.plf
```
* Update proofs/signatures/lrat.plf per Yoni's suggestion.
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Responding to Yoni's comments.
* Removed unused varaibles
Some tests declared `var`s which were unused.
Now they don't.
|
|
new proof constructs generated by the equality engine.
proof production for bool-array.smt2 passes
|
|
|
|
|
|
|
|
|
|
signature. Add regressions.
|
|
|
|
proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
|