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

Age	Commit message (Collapse)	Author
2018-08-22	global-negate preprocessing pass (#2317)	yoni206

2018-08-22	Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253)	yoni206

2018-08-21	Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350)	Mathias Preiner

2018-08-20	Make sygus inference a preprocessing pass (#2334)	Andrew Reynolds

2018-08-16	Refactor eager atoms preprocessing pass. (#2318)	Mathias Preiner

2018-08-16	Make quantifiers-preprocess preprocessing pass (#2322)	Caleb Donovick

2018-08-16	Refactor IteRemoval preprocessing pass (#1793)	Andres Noetzli
	This commit refactors the IteRemoval pass to follow the new format. In addition to moving the code, this entails the following changes: - The timer for the ITE removal is now called differently (the default timer of PreprocessingPass is used) and measures just the preprocessing pass without applySubstitutions(). It also measures the time used by both invocations of the ITE removal pass. - Debug output will be slightly different because we now just rely on the default functionality of PreprocessingPass. - d_iteRemover is now passed into the PreprocessingPassContext. - AssertionPipeline now owns the d_iteSkolemMap, which makes it accessible by preprocessing passes. The idea behind this is that the preprocessing passes collect information in AssertionPipeline and d_iteSkolemMap fits that pattern.
2018-08-16	Refactor extended rewriter preprocessing pass (#2324)	Haniel Barbosa

2018-08-16	Refactor apply2const (#2316)	Haniel Barbosa

2018-08-15	Make sort inference a preprocessing pass (#2309)	Andrew Reynolds

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).
2017-12-10	Add new infrastructure for preprocessing passes (#1053)	justinxu421
	This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits).