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

Age	Commit message (Collapse)	Author
2016-09-25	Adding virtual destructors to several classes in expr.h .	Tim King

2016-08-15	Expression sharing on demand in LFSC (replace definitionally equivalent ↵	ajreynol
	child arguments after successful comparison).
2016-05-05	Compute term indices lazily in TermDb. Optimization for qcf to recognize ↵	ajreynol
	irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
2016-05-02	Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ↵	ajreynol
	do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
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

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 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.
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