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

Age	Commit message (Collapse)	Author
2018-08-01	Fix bool-to-bv preprocessing pass for non-{bv,bool} equalities. (#2251)	Mathias Preiner

2018-07-23	Generalize symmetry detection for 1 symmetry variable mapped to n input ↵	Andrew Reynolds
	variables (#1888)
2018-07-17	Refactor sep-pre-skolem-emp preprocessing pass	yoni206

2018-07-10	Move rewrite to pass (#2128)	Caleb Donovick

2018-07-02	Refactor ApplySubsts preprocessing pass. (#2120)	Aina Niemetz

2018-06-27	Synthesize candidate-rewrites from standard inputs (#1918)	Andrew Reynolds

2018-06-25	Updated copyright headers.	Aina Niemetz

2018-05-21	Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)	makaimann

2018-05-15	Refactor static learning preprocessing pass (#1857)	yoni206

2018-05-11	Fix ackermannize preprocessing pass. (#1904)	Aina Niemetz
	Ackermannization did not consider cases where UF are Boolean. Model generation is still not supported, but now guarded against when bit-vectors are combined with arrays and/or uninterpreted functions and --bitblast=eager.
2018-05-10	Refactored BVAckermann preprocessing pass. (#1889)	Aina Niemetz

2018-05-09	Reorder class members in bv-to-bool and bool-to-bv preprocessing passes. (#1893)	yoni206

2018-05-09	Make symmetry-breaker-exp into a preprocessing pass (#1890)	Andrew Reynolds

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

2018-05-08	Refactor bv-abstraction preprocessing pass. (#1860)	Mathias Preiner

2018-05-03	Refactor bv-intro-pow2 preprocessing pass. (#1851)	Mathias Preiner

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-30	Remove dead code in bv-to-bool preprocessing pass (#1828)	Andres Noetzli
	Fixes Coverity issue 1468436. As Coverity correctly detects, kind::BITVECTOR_XOR is dealt with in an if-statement before the switch statement on kind. This is because kind::XOR is binary while kind::BITVECTOR_XOR is n-ary (as a comment in the code correctly indicates).
2018-04-25	Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)	yoni206

2018-04-20	Symmetry detection module (#1749)	PaulMeng

2018-04-19	Refactor pbRewrites preprocessing pass (#1767)	Andres Noetzli
	This commit refactors the pbRewrites preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass. It also makes use of the AssertionPipeline::replace function to do proper dependency tracking.
2018-04-10	Refactored BVGauss preprocessing pass. (#1766)	Aina Niemetz

2018-04-03	Refactor IntToBV preprocessing pass (#1716)	Andres Noetzli
	This commit refactors the IntToBV preprocessing pass into the new style. This commit is essentially just a code move, it does not attempt to fix issues (e.g. #1715).