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

Age	Commit message (Collapse)	Author
2014-07-25	patch for regular expression intersection caching	Tianyi Liang

2014-05-13	Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ↵	ajreynol
	Add regressions.
2014-05-12	Add a benchmark that detects a bug in parsing. Thank Vijay for his bug report.	Tianyi Liang

2014-04-29	add leading zeros support for str.to.int	Tianyi Liang

2014-03-27	adds new feature: re.loop	Tianyi Liang

2014-03-07	Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵	Morgan Deters
	bodies; fix bug 551, improper ITE removal under quantifiers.
2014-02-28	a new regular expression engine for solving both positive and negative ↵	Tianyi Liang
	membership constraints
2014-02-26	bug fix (caused by merge), move cardinality option to expert option	Tianyi Liang

2014-02-20	fix makefile	Tianyi Liang

2014-02-20	add two cases to the regression test	Tianyi Liang

2014-01-16	adds partial functions	Tianyi Liang

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-03	adds LB strategy	Tianyi Liang

2013-10-21	add a string test case	Tianyi Liang

2013-10-20	adds regular expression range	Tianyi Liang

2013-10-16	adds fmf for strings	Tianyi Liang

2013-10-15	bug fix: string cache cleaning	Tianyi Liang

2013-10-14	add another regexp test	Tianyi Liang

2013-10-11	Adds regular expression support, it is actually CFL because of variables.	Tianyi Liang

2013-10-01	adds partial function substr. the use of this function should be guarded, ↵	Tianyi Liang
	especially for disequalities
2013-09-30	replace with a new method for disequality, move to QF_S	Tianyi Liang

2013-09-27	adds communication with arith engine	Tianyi Liang

2013-09-27	removes unsound cases, adds unrolling	Tianyi Liang

2013-09-27	adds model generation for strings, and a hacked way in arith engine for models	Tianyi Liang

2013-09-18	Support a personal build configuration and make rules.	Morgan Deters

2013-09-11	Theory of strings.	Tianyi Liang
	Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>