cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2015-04-23	A few more minor updates to match google repository with CVC4 repository	Clark Barrett
	(mostly whitespace differences).
2015-04-21	Changes needed to compile at Google, plus some bug fixes from Google.	Clark Barrett

2015-03-10	CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf ↵	ajreynol
	signature. Add regressions.
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