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

Age	Commit message (Collapse)	Author
2014-08-23	Some fixes for dump- and get-unsat-core.	Morgan Deters

2014-08-22	One small thing forgotten in core commit.	Morgan Deters

2014-08-22	Java-side interface improvements for unsat cores.	Morgan Deters

2014-08-22	Unsat core infrastruture and API (SMT-LIB compliance to come).	Morgan Deters

2014-08-22	Merge branch '1.4.x'	Morgan Deters

2014-08-22	Fix operator-printing issue in SMT2.	Morgan Deters

2014-08-22	Fix SMT1 parser :extrasorts/:extrapreds.	Morgan Deters

2014-08-21	Avoid doing work in quantifiers engine when no quantifiers are asserted.	ajreynol

2014-08-21	Fix --inst-max-level for strategies that use arbitrary representative terms.	ajreynol

2014-08-20	Add option for inductive strengthening based on well-founded induction for ↵	ajreynol
	integers (default schema).
2014-08-19	Merge branch '1.4.x'	Morgan Deters

2014-08-19	Produce error for bad indexed function names in SMT-LIB, remove antlr warning.	Morgan Deters

2014-08-18	Making getEqualityStatus more powerful for bit-vector theory.	lianah

2014-08-18	Merge branch '1.4.x'	Morgan Deters
	Conflicts: test/regress/regress0/Makefile.am
2014-08-18	Revert a8e0ce67 and add test case (resolves bug #578).	Morgan Deters
	This reverts commit a8e0ce673ba00533a663804cf74500e4d9a3a5cb.
2014-08-18	Add support for quantifier-specific instantiation levels. Add option for ↵	ajreynol
	setting inst-level 0 only for input terms.
2014-08-15	Update smt_engine.cpp	Kshitij Bansal
	Code changed but comment didn't, might as well get rid of it.
2014-08-06	First crack at fixing double-linking issues in build system.	Morgan Deters

2014-08-05	fixed bug575 for bv models	lianah

2014-08-05	fixed bug575 for bv models	lianah

2014-08-05	Minor fix : do not drop instantiation patterns when merging quantifiers.	ajreynol

2014-08-04	Some fixes to symmetry breaker (resolves bug 576).	Morgan Deters

2014-08-04	Some fixes to symmetry breaker (resolves bug 576).	Morgan Deters

2014-08-04	Better support for resource-limiting when there aren't any actual conflicts.	Morgan Deters

2014-08-01	Minor cleanup from previous commit. Better organization for how quantifiers ↵	ajreynol
	modules check (introduce QuantifiersEngine::QEffort).
2014-07-31	New module for generating candidate equality conjectures used in inductive ↵	ajreynol
	proofs. Filtering currently includes: LHS generalizes a term from an active conjecture, terms must be canonical, conjecture must be confirmed by a ground witness, and cannot be falsified by a ground witness. Refactoring of term database. QcfEngine now uses central data structure for term indexing. Add two options for quantifier instantiation : trigger selection mode --trigger-sel=mode, and --inst-no-entail which blocks all quantifier instantiations that are currently entailed (using an incomplete check).
2014-07-26	Minor bug fix for exhaustive instantiation in model_engine.	ajreynol

2014-07-25	bug fix for pierre 0717	Tianyi Liang

2014-07-25	fix for regexp union rewriting	Tianyi Liang

2014-07-25	patch for regular expression intersection caching	Tianyi Liang

2014-07-24	merging...	Tianyi Liang

2014-07-24	add delayed length lemmas	Tianyi Liang

2014-07-21	initialization in model_engine	Kshitij Bansal

2014-07-19	Minor fix for explanations for co-datatypes. Bug fix for explanations in ↵	ajreynol
	FMF for quantifiers over arrays.
2014-07-12	Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre ↵	Morgan Deters
	for the report.
2014-07-11	Spelling.	Morgan Deters

2014-07-11	fix for windows build	Kshitij Bansal

2014-07-10	Merge pull request #48 from kbansal/segfaultfix	Kshitij Bansal
	Segfaultfix
2014-07-10	rm warning	Kshitij Bansal

2014-07-10	membership cvc token changed to `IS_IN' to avoid conflict with IN used for let	Kshitij Bansal

2014-07-10	Merge remote-tracking branch 'origin/master' into segfaultfix	Kshitij Bansal

2014-07-10	friendlyparser: go back upto 2 words looking for match	Kshitij Bansal

2014-07-10	reorganize friendlyparser, behavior unchanged	Kshitij Bansal

2014-07-09	sets cvc parser	Kshitij Bansal

2014-07-09	sets cvc printer	Kshitij Bansal

2014-07-04	initialize variables	Kshitij Bansal

2014-07-03	change lemma generation behavior	Kshitij Bansal
	don't store lemmas in a pending queue, instead generate them right away doing with pending queue is tricky, needs rethinking to do it properly
2014-07-01	Update portfolio_util.cpp	Kshitij Bansal

2014-07-01	Update copyrights.	Morgan Deters

2014-07-01	Merge pull request #44 from mdeters/prio-queue-updates	Morgan Deters
	BinaryHeap unit test and some usability/build fixes for the data structu...