Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-08-20 | Update bv proof signature and example, after discussions with Liana. | ajreynol | |
2014-08-08 | Add draft of BV proof signature (incomplete) and example proof. | ajreynol | |
2014-05-23 | Fix bug in E-matching Real/Int terms. | Andrew Reynolds | |
2014-05-16 | lfsc_checker: fix some warnings reported by _both_ gcc and clang | Kshitij Bansal | |
2014-03-19 | Fix proof signatures makefile | Morgan Deters | |
2014-03-19 | Fix a memory leak in LFSC proof checker. Largest QF_UF proof from Morgan ↵ | Andrew Reynolds | |
(problematic-lfsc-pf) now successfully checks in 58 seconds using ~8 GB memory. Add example test proof. | |||
2014-03-14 | dos2unix on the proof signatures, and fix the makefile. | Morgan Deters | |
2014-03-13 | Add working example of LFSC proof with quantifiers. Update quantifiers ↵ | Andrew Reynolds | |
signature to avoid dependent types in side condition. | |||
2014-03-12 | Work on array pf signature, add working example. Add quantifiers proof ↵ | Andrew Reynolds | |
signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default. | |||
2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing ↵ | Andrew Reynolds | |
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. | |||
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof ↵ | Morgan Deters | |
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 | |||
2013-12-18 | Reduce autoconf version for dependence (should fix 32-bit builds). | Morgan Deters | |
2013-12-16 | First attempt at incorporating LFSC proof checker into CVC4. | Morgan Deters | |
2013-10-03 | Adding example proof signatures for LFSC. | Andrew Reynolds | |