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

Age	Commit message (Collapse)	Author
2018-07-31	Fix option handler for lazy/bv-sat-solver combinations. (#2225)	Mathias Preiner
	Further, unifies all limitHandler and limitPerHandler to limitHandler.
2018-07-27	Require argument description for non-{bool,void} options. (#2228)	Mathias Preiner
	Not adding the argument description for non-{bool,void} options is now an error. Further, adds missing argument descriptions.
2018-06-27	Synthesize candidate-rewrites from standard inputs (#1918)	Andrew Reynolds

2018-05-09	Add the symmetry breaker module (#1847)	PaulMeng

2018-04-30	Refactor real2int (#1813)	Haniel Barbosa
	This commit refactors the real2int preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass.
2018-04-20	Symmetry detection module (#1749)	PaulMeng

2018-03-21	Refactor mkoptions (#1631)	Mathias Preiner
	This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation. The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick. This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.