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

Age	Commit message (Collapse)	Author
2017-05-15	Merge pull request #158 from 4tXJ7f/fix_sets_rewriter	Andrew Reynolds
	Fix minor bug in sets rewriter
2017-05-15	Fix minor bug in sets rewriter	Andres Noetzli
	As reported by Coverity, one of the switches in the sets rewriter had a missing break. This could lead to an assertion failure when rewriting the cardinality of a transpose as in the test case included in this commit.
2017-05-15	Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.	ajreynol

2017-05-13	Fix out-of-bounds access in test	Andres Notzli

2017-05-12	Make signal handlers safer	Andres Notzli
	As reported in bug 769, the signal handlers currently use unsafe functions such as dynamic memory allocations and fprintf. This commit fixes the issue by introducing functions for printing statistics in signal handlers (functions with the `safe` prefix). It also avoids copying statistics, which further avoids dynamic memory allocation. The safe printing of statistics has some limitations (it does not support SExprStats or printing CVC4::Result), which should not matter much in practice. Printing statistics in a non-signal handler is not affected by these changes as that uses a separate code path (the functions without the `safe` prefix). Additional changes: - Remove ListStat as it is not used anywhere - Add unit test for safe printing statistics
2017-05-10	Do not split on cardinality for string equivalence classes with non-constant ↵	ajreynol
	lengths if disequalities already imply sufficient lower bound. Fixes bug 799.
2017-05-09	Change str.replace for empty string.	ajreynol

2017-05-05	Do not eliminate extended arithmetic symbols when finite model finding is ↵	ajreynol
	on, add regression.
2017-04-28	Minor fixes	ajreynol

2017-04-28	Fix bug for real division.	ajreynol

2017-04-28	Do not eliminate non-standard arithmetic operators in recursive function ↵	ajreynol
	definitions, add regression.
2017-04-24	Fixes and simplifications for fmf mbqi.	ajreynol

2017-04-24	Fix parsing selectors for nullary constructors in smtlib 2.6 format.	ajreynol

2017-04-23	Changing spaces to tabs in Makefile.	Tim King

2017-04-21	Disabled bug639.smt2 which still fails.	Clark Barrett

2017-04-21	Add test cases for bugs 639 and 681.	Clark Barrett

2017-04-21	Fix new relations regressions to use sets-ext.	ajreynol

2017-04-21	Handle subtypes in sets. Bug fixes for tuples with subtypes.	ajreynol

2017-04-20	Support for relational operators identity and join image	Paul Meng

2017-04-19	Fixes for handling set universe: restrict upwards rule for universe to ↵	ajreynol
	memberships into variable sets, do not variable eliminate sets during ppAssert.
2017-04-14	Actively split for upwards closusure intersection. Minor clean up, add ↵	ajreynol
	regressions.
2017-04-14	Fix for fmf-fun when the option is set by user command.	ajreynol

2017-04-07	Change option names for nl.	ajreynol

2017-04-05	Merge pull request #143 from FabianWolff/master	Clark Barrett
	Fix several spelling errors
2017-04-05	Fix bug 698.	ajreynol

2017-04-05	Caching for fun def process, add regression.	ajreynol

2017-04-05	Remove extraneous portion of an nl regression.	ajreynol

2017-04-05	Add non-linear regressions, disable nlAlgSubs, do not do rep checking for ↵	ajreynol
	NONLINEAR_MULT terms. Ensure shared terms have correct model values in non-linear solver.
2017-04-05	Fix several spelling errors	Fabian Wolff

2017-04-04	Enable multi-trigger-linear by default, add option.	ajreynol

2017-04-04	Do not solve for 0-ary non-constant symbols (for which isVar returns true), ↵	ajreynol
	add regressions.
2017-04-02	Adding a model based axiom instantiation scheme for multiplication. Merge ↵	Tim King
	commit for nlAlgMaster.
2017-03-28	Refactor the standard effort of relational solver	Paul Meng

2017-03-28	Fix bug 787.	ajreynol

2017-03-28	Fix for bug 733	Clark Barrett

2017-03-24	Add some regressions. Minor.	ajreynol

2017-03-22	Minor fix for bounded integers.	ajreynol

2017-03-20	fixed cvc4 parser for set complement	Paul Meng

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-16	More fixes, features to examples.	ajreynol

2017-03-16	Minor fixes, always expand applications of lambdas at preprocess.	ajreynol

2017-03-16	Support for SMT LIB 2.6 syntax declare-datatype and match.	ajreynol

2017-03-16	Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for ↵	ajreynol
	mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
2017-03-15	Fix regress1 Makefile for rewriterules, fixes bug 783.	ajreynol

2017-03-15	Allow 0 argument recursive functions. Fixes bug 782.	ajreynol

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

2017-03-07	More fixes for printing/parsing sets, fix kind name.	ajreynol

2017-03-07	Fix cvc parser for set compliment.	ajreynol

2017-03-06	Support for set compliment and universe set. Simplify approach for sep.nil ↵	ajreynol
	nodes.
2017-03-03	Fix for collectModelInfo related to finite types + preregistration. ↵	ajreynol
	Generalize previous fix for sets, minor changes to Datatypes.