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

Age	Commit message (Collapse)	Author
2018-08-02	Parse standard separation logic inputs (#2257)	Andrew Reynolds

2018-07-17	Refactor sep-pre-skolem-emp preprocessing pass	yoni206

2018-03-21	Move regression tests to single Makefile.am (#1658)	Andres Noetzli
	Until now, regression tests were split across tens of different Makefile.am, which required a lot of code duplication and does not really seem to be in the spirit of automake. If we want to change the LOG_COMPILER/LOG_DRIVER for example, we have to change every single Makefile.am, which is cumbersome (I was able to get something semi-working by exporting those variables but it didn't seem very clean). Additionally, it made the output of the regression tests fairly verbose and split the output across multiple log files. Finally it also limited parallelism when running the regression tests (this fix lowers the time it takes to run regression level 1 from 3m to 1m45s on my machine with 16 threads). This commit moves all the regression tests into test/regress/Makefile.tests and changes test/regress/Makefile.am to deal with this new structure. Finally, it changes how the test summary in test/Makefile.am is produced: instead of relying on the log files for the subdirectories, it greps for the test results in the log files of the individual tests. Not the most elegant solution but we should probably anyway delegate that task to a Python script at some point.
2018-02-15	Refactor regressions (#1581)	Andrew Reynolds

2017-08-04	Set default language to smt lib 2.6 (including as a base language for ↵	ajreynol
	sygus), update regressions.
2017-04-04	Do not solve for 0-ary non-constant symbols (for which isVar returns true), ↵	ajreynol
	add regressions.
2017-01-04	Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor ↵	ajreynol
	changes.
2017-01-04	Marking regression test files as non-executable.	Tim King

2016-11-17	Fix Makefiles in test	Andres Notzli
	With the recent changes to the regress tests, some of the Makefiles were not in sync anymore. This commit fixes that.
2016-11-08	Add a few options to separation logic and sets. Minor changes to separation ↵	ajreynol
	logic, change syntax for empty heap constraint.
2016-11-03	Add priorities to getNextDecision. Properly handle case for finite types + ↵	ajreynol
	unbounded heaps in sep logic. Fix another simple memory leak in sygus.
2016-11-02	Add missing regression.	ajreynol

2016-11-02	Fix bug in separation logic for finite pto-data types. Minor cleanup in sep. ↵	ajreynol
	Fix a few more memory leaks.
2016-10-21	Move slow regress0 benchmarks to regress1, increment regress1 through regress3.	ajreynol

2016-09-12	Ensure sep.nil is unique per type at NodeManager level. Add simple symmetry ↵	ajreynol
	breaking in theory sep.
2016-09-09	Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.	ajreynol

2016-09-09	Support for separation logic + EPR. Refactor preprocessing of sep.nil, only ↵	ajreynol
	allow sep disequal card constants when type is monotonic. Update logics on sep regressions.
2016-08-09	Fixes for sep star rewrite.	ajreynol

2016-07-07	Ensure heap disjointness in sep refinements.	ajreynol

2016-07-05	Refactor last call for theories, only create one model when quantifiers are ↵	ajreynol
	enabled. Fix sep.nil preregistration in TheorySep.
2016-06-17	Support for separation logic. Enable cbqi by default for pure BV.	ajreynol