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

Age	Commit message (Collapse)	Author
2021-09-22	Remove CVC language support (#7219)	Mathias Preiner
	This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.
2021-06-02	Remove redundant logic ALL_SUPPORTED. (#6664)	Aina Niemetz

2019-03-28	Fix issues in cvc parser (#2901)	Andrew Reynolds

2018-09-22	cmake: Added regression tests and target make regress.	Aina Niemetz

2018-09-22	cmake: Added initial build infrastructure.	Aina Niemetz

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-12-27	Rel smt parser (#1446)	Arjun Viswanathan

2017-09-10	Ensure that expand definitions is called on all non-variable expressi… (#1070)	Andrew Reynolds
	* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions. * Add comments concerning expandDefinitions * Expand comment, move to .h
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-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-14	Actively split for upwards closusure intersection. Minor clean up, add ↵	ajreynol
	regressions.
2017-04-04	Do not solve for 0-ary non-constant symbols (for which isVar returns true), ↵	ajreynol
	add regressions.
2017-03-28	Refactor the standard effort of relational solver	Paul Meng

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-10-26	New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵	ajreynol
	as extension of sets solver, add regressions.