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

Age	Commit message (Collapse)	Author
2020-04-20	Make option names related to CEGQI consistent (#4316)	Andrew Reynolds
	This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus. Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit. The changes were done by these commands in the given directories: src/: for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done test/regress/: for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done src/: and test/regress/: for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done test/regress/: for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done test/regress/: for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done And a few minor fixes afterwards. This should be merged close to the time of the next stable release.
2020-03-31	Fixing regressions (#4189)	Andrew Reynolds
	An option was recently deleted, forgot to disable it from a regression. Fixes a failure in regress1.
2020-03-21	Convert V1 Sygus files to V2. (#4136)	Abdalrhman Mohamed

2020-03-11	Switch to Nodes for conjecture generator (#4026)	Andrew Reynolds
	Fixes #4022.
2020-03-06	Support default sygus grammar construction for sets (#3842)	Andrew Reynolds
	Fixes #3645.
2020-02-03	Example inference utility (#3670)	Andrew Reynolds

2020-01-07	Update any-constant and normalization policies for sygus grammars (#3583)	Andrew Reynolds

2019-12-12	Make CEGIS sampling robust to non-vanilla CEGIS (#3559)	Andrew Reynolds

2019-12-05	Refactor mode options for Unif+PI (#3531)	Andrew Reynolds

2019-08-02	Support default sygus grammar for strings (#3148)	Andrew Reynolds

2019-05-15	Fix printing of bvurem (#2963)	Andrew Reynolds

2019-04-05	fix fp issue (#2940)	Haniel Barbosa

2019-01-09	Do not rewrite 1-constructor sygus testers to true (#2780)	Andrew Reynolds

2018-10-08	Address slow sygus regressions (#2598)	Andrew Reynolds

2018-10-03	Eliminate partial operators within lambdas during grammar normalization (#2570)	Andrew Reynolds

2018-08-08	Disable argument relevance for sygus by default (#2288)	Andrew Reynolds

2018-07-23	sygusComp2018: add regressions (#2191)	Andrew Reynolds

2018-05-25	Reenable repair const (#1983)	Andrew Reynolds

2018-05-22	Repair constants using symbolic constructors (#1960)	Andrew Reynolds

2018-05-15	adding regressions (#1925)	Haniel Barbosa

2018-05-14	Fix annotations in regress2. (#1917)	Andrew Reynolds

2018-05-14	Add regressions, change defaults. (#1911)	Andrew Reynolds

2018-05-14	Flag to check invariance of entire values in sygus explain (#1908)	Andrew Reynolds

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