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

Age	Commit message (Collapse)	Author
2018-12-11	LRAT signature (#2731)	Alex Ozdemir
	* 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.
2017-03-17	better support for proof production when encountering bool terms: handle the ↵	guykatzz
	new proof constructs generated by the equality engine. proof production for bool-array.smt2 passes
2017-03-09	bug fix	guykatzz

2017-03-09	better proof support for bools and formulas	guykatzz

2017-01-04	Marking the proof signature files as non-executable.	Tim King

2016-01-26	Merged bit-vector and uf proof branch.	Liana Hadarean

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-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-10-03	Adding example proof signatures for LFSC.	Andrew Reynolds