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

Age	Commit message (Collapse)	Author
2018-10-18	Non-implied mode for model cores (#2653)	Andrew Reynolds

2018-09-27	Fix Taylor overapproximation for large exponentials (#2538)	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-08-21	Makes the new row propagation system default (#2335)	Haniel Barbosa

2018-06-04	Only enable transcendentals if logic is N[I]RAT (#2052)	Andres Noetzli

2018-05-24	Fix nl regression for unsat cores. (#1973)	Andrew Reynolds

2018-05-23	Generalize check-model in NonLinearExtension for quadratic equations (#1892)	Andrew Reynolds

2018-05-01	Improve tangent planes for transcendental functions (#1832)	Andrew Reynolds

2018-04-30	Disable unsat-cores/proofs for slow regression (#1835)	Andres Noetzli

2018-04-29	Make factoring inference more aggressive (#1825)	Andrew Reynolds

2018-04-03	Use choice when expanding definitions for inverse transcendental functions ↵	Andrew Reynolds
	(#1742)
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-03-20	Internally remove redundant assertions and infer equalities in ↵	Andrew Reynolds
	NonLinearExtension (#1633)
2018-02-20	Minor fixes and additions for transcendental functions (#1612)	Andrew Reynolds
	Also adds parsing support for PI in smt2 with syntax "real.pi".
2018-02-15	Refactor regressions (#1581)	Andrew Reynolds

2017-07-10	Merge ntExt branch. Adds support for transcendental functions. Refactoring ↵	ajreynol
	of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.