git.libre-soc.org Git - cvc5.git/history - src/theory/arith/arith

[cvc5.git] / src / theory / arith / arith_rewriter.cpp

2022-02-25	Gereon Kremer	Refactor rewriting of arithmetic negation and subtracti...	blob \| commitdiff \| raw
2022-02-25	Gereon Kremer	Slightly refactor arithmetic rewriting for extended...	blob \| commitdiff \| raw \| diff to current
2022-02-23	Gereon Kremer	Refactor multiplication in arithmetic rewriter (#7965)	blob \| commitdiff \| raw \| diff to current
2022-02-22	Andrew Reynolds	Change inference scheme in transcendentals to rewrite...	blob \| commitdiff \| raw \| diff to current
2022-02-05	Andrew Reynolds	Fix another rewrite involving iand (#8054)	blob \| commitdiff \| raw \| diff to current
2022-02-03	Aina Niemetz	Rename kind PLUS -> ADD. (#8036)	blob \| commitdiff \| raw \| diff to current
2022-02-02	Andrew Reynolds	Fix rewrite for eliminating constant factors of PI...	blob \| commitdiff \| raw \| diff to current
2022-02-02	Aina Niemetz	Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8035)	blob \| commitdiff \| raw \| diff to current
2022-02-02	Andrew Reynolds	Fix invalid rewrite involving iand (#8026)	blob \| commitdiff \| raw \| diff to current
2022-02-01	Gereon Kremer	Consider RANs in variable ordering (#7964)	blob \| commitdiff \| raw \| diff to current
2022-01-31	Gereon Kremer	Add utilities for flattening nodes (#7961)	blob \| commitdiff \| raw \| diff to current
2022-01-24	Gereon Kremer	Refactor how arith rewriting checks for mult-by-zero...	blob \| commitdiff \| raw \| diff to current
2022-01-20	Gereon Kremer	Refactor abs rewriting (#7935)	blob \| commitdiff \| raw \| diff to current
2022-01-19	Gereon Kremer	Make tracing for arithmetic rewriter more consistent...	blob \| commitdiff \| raw \| diff to current
2022-01-14	Gereon Kremer	refactor div rewriter, add support for ran (#7941)	blob \| commitdiff \| raw \| diff to current
2022-01-14	Gereon Kremer	Refactor arithmetic pre-rewriter for multiplication...	blob \| commitdiff \| raw \| diff to current
2022-01-14	Gereon Kremer	Add support for RANs in rewriter for `MULT` (#7940)	blob \| commitdiff \| raw \| diff to current
2022-01-14	Gereon Kremer	Add RAN support in UMINUS rewriter (#7933)	blob \| commitdiff \| raw \| diff to current
2022-01-13	Gereon Kremer	Add arithmetic rewriter for RAN (#7929)	blob \| commitdiff \| raw \| diff to current
2022-01-13	Gereon Kremer	Refactor post rewriter for addition (#7931)	blob \| commitdiff \| raw \| diff to current
2022-01-12	Gereon Kremer	Refactor atom rewriting to be RAN-aware (#7928)	blob \| commitdiff \| raw \| diff to current
2022-01-12	Gereon Kremer	Refactor rewriteMinus (#7932)	blob \| commitdiff \| raw \| diff to current
2021-12-22	Andrew Reynolds	Remove most uses of mkRationalNode (#7854)	blob \| commitdiff \| raw \| diff to current
2021-12-21	yoni206	Rewrite (pow2 x) to (pow 2 x) when x is a constant...	blob \| commitdiff \| raw \| diff to current
2021-12-20	Andrew Reynolds	Eliminating some uses of const rational in arithmetic...	blob \| commitdiff \| raw \| diff to current
2021-12-14	Andrew Reynolds	Eliminate use of rewrite, CONST_RATIONAL in ArithMSum...	blob \| commitdiff \| raw \| diff to current
2021-12-13	yoni206	Integrate new int-blaster (#7781)	blob \| commitdiff \| raw \| diff to current
2021-12-10	Ying Sheng	Array-inspired Sequence Solver - Adding the ArrayCoreSo...	blob \| commitdiff \| raw \| diff to current
2021-11-30	Andrew Reynolds	Add rewrite for is_int pi (#7711)	blob \| commitdiff \| raw \| diff to current
2021-11-12	Andres Noetzli	Remove `ConstantMap<Rational>` (#7635)	blob \| commitdiff \| raw \| diff to current
2021-06-28	yoni206	Rewrite POW to POW2 when the base is 2 (#6806)	blob \| commitdiff \| raw \| diff to current
2021-06-26	yoni206	pow2 -- final changes (#6800)	blob \| commitdiff \| raw \| diff to current
2021-06-23	yoni206	pow2: more implementations (#6756)	blob \| commitdiff \| raw \| diff to current
2021-05-26	Andres Noetzli	More precise includes of `Node` constants (#6617)	blob \| commitdiff \| raw \| diff to current
2021-04-22	Andrew Reynolds	Move expand definition from Theory to TheoryRewriter...	blob \| commitdiff \| raw \| diff to current
2021-04-12	Aina Niemetz	Refactor and update copyright headers. (#6316)	blob \| commitdiff \| raw \| diff to current
2021-04-06	Andres Noetzli	Remove template argument from `NodeBuilder` (#6290)	blob \| commitdiff \| raw \| diff to current
2021-04-01	Aina Niemetz	Rename namespace CVC5 to cvc5. (#6258)	blob \| commitdiff \| raw \| diff to current
2021-03-31	Aina Niemetz	Rename namespace CVC4 to CVC5. (#6249)	blob \| commitdiff \| raw \| diff to current
2021-03-25	Gereon Kremer	Add missing includes. (#6207)	blob \| commitdiff \| raw \| diff to current
2021-03-09	Aina Niemetz	Update copyright headers to 2021. (#6081)	blob \| commitdiff \| raw \| diff to current
2020-12-03	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-10-29	mudathirmahgoub	Add mkInteger to the API (#5274)	blob \| commitdiff \| raw \| diff to current
2020-10-28	Andrew Reynolds	Add rewrites for div/mod in the arithmetic rewriter...	blob \| commitdiff \| raw \| diff to current
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-08-05	Gereon Kremer	Improve error message for unsupported exponents (#4852)	blob \| commitdiff \| raw \| diff to current
2020-06-30	Andrew Reynolds	Add internal support for integer and operator (#4668)	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-03-09	Andrew Reynolds	Rewrite again full for DIV rewrite (#3945)	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andrew Reynolds	Initial work towards -Wshadow (#3817)	blob \| commitdiff \| raw \| diff to current
2020-01-31	Andres Noetzli	Fix arithmetic rewriter for exponential (#3688)	blob \| commitdiff \| raw \| diff to current
2019-12-02	makaimann	OpTerm Refactor: Allow retrieving OpTerm used to create...	blob \| commitdiff \| raw \| diff to current
2019-11-18	Andres Noetzli	Use -Wimplicit-fallthrough (#3464)	blob \| commitdiff \| raw \| diff to current
2019-10-31	Mathias Preiner	Fix Unimplemented() macros missed in #3366. (#3424)	blob \| commitdiff \| raw \| diff to current
2019-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	blob \| commitdiff \| raw \| diff to current
2019-10-28	Andres Noetzli	Fix integer division rewrite (#3415)	blob \| commitdiff \| raw \| diff to current
2019-10-13	Andrew Reynolds	Eliminate negative constant coefficients in div/mod...	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-02-20	Andrew Reynolds	Minor fixes and additions for transcendental functions...	blob \| commitdiff \| raw \| diff to current
2018-02-07	Andrew Reynolds	Add remaining transcendental functions (#1551)	blob \| commitdiff \| raw \| diff to current
2018-01-27	Tim King	Removing structurally dead code. (#1540)	blob \| commitdiff \| raw \| diff to current
2017-12-20	Andrew Reynolds	Transcendental functions check model (#1443)	blob \| commitdiff \| raw \| diff to current
2017-11-29	Andrew Reynolds	Improve the rewriter for SINE. (#1221)	blob \| commitdiff \| raw \| diff to current
2017-07-10	ajreynol	Merge ntExt branch. Adds support for transcendental...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-04-06	Clark Barrett	Merge pull request #143 from FabianWolff/master	blob \| commitdiff \| raw \| diff to current
2017-04-04	Fabian Wolff	Fix several spelling errors	blob \| commitdiff \| raw \| diff to current
2017-04-04	Clark Barrett	Merge pull request #141 from 4tXJ7f/remove_def	blob \| commitdiff \| raw \| diff to current
2017-04-03	Andrew Reynolds	Merge pull request #142 from timothy-king/nlAlgMerge	blob \| commitdiff \| raw \| diff to current
2017-04-03	Tim King	Adding a model based axiom instantiation scheme for...	blob \| commitdiff \| raw \| diff to current
2017-01-18	Andrew Reynolds	Merge pull request #128 from 4tXJ7f/fix_lfsc_perf	blob \| commitdiff \| raw \| diff to current
2017-01-14	Clark Barrett	Merge pull request #130 from chadbrewbaker/master	blob \| commitdiff \| raw \| diff to current
2017-01-11	Clark Barrett	Merge pull request #129 from timothy-king/regression...	blob \| commitdiff \| raw \| diff to current
2017-01-11	Tim King	Adding regression test scrubbing.	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	blob \| commitdiff \| raw \| diff to current
2016-04-09	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-04-04	Tim King	Updating the copyright headers and scripts.	blob \| commitdiff \| raw \| diff to current
2015-12-15	Tim King	Refactoring Options Handler & Library Cycle Breaking	blob \| commitdiff \| raw \| diff to current
2014-07-10	Kshitij Bansal	Merge remote-tracking branch 'origin/master' into segfa...	blob \| commitdiff \| raw \| diff to current
2014-07-01	Morgan Deters	Update copyrights.	blob \| commitdiff \| raw \| diff to current
2014-06-06	Kshitij Bansal	Merge pull request #28 from kbansal/sets	blob \| commitdiff \| raw \| diff to current
2014-06-06	Tim King	Patch for the subtype theoryof mode to make the equalit...	blob \| commitdiff \| raw \| diff to current
2014-04-01	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-26	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-21	Kshitij Bansal	Merge pull request #22 from kbansal/sets-model	blob \| commitdiff \| raw \| diff to current
2014-03-11	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-11	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-10	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-03-08	Tim King	Merge pull request #18 from timothy-king/master	blob \| commitdiff \| raw \| diff to current
2014-03-08	Tim King	Merge remote-tracking branch 'CVC4root/master'	blob \| commitdiff \| raw \| diff to current
2014-03-07	Tim King	Merging a squash of the branch timothy-king/CVC4/glpkne...	blob \| commitdiff \| raw \| diff to current
2014-03-07	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-03-05	Tim King	Improving support for POW in arithmetic. Resolves bug...	blob \| commitdiff \| raw \| diff to current
2013-12-05	Morgan Deters	Update copyrights, add missing file-level documentation...	blob \| commitdiff \| raw \| diff to current
2013-09-30	Liana Hadarean	merged golden	blob \| commitdiff \| raw \| diff to current
2013-08-26	Kshitij Bansal	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-06-25	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-06-25	Morgan Deters	Support for abs, to_int, is_int, divisible in SMT-LIB...	blob \| commitdiff \| raw \| diff to current
2013-04-02	Morgan Deters	Regenerated copyrights: canonicalized names, no emails	blob \| commitdiff \| raw \| diff to current
next

RSS Atom