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

[cvc5.git] / src / theory / arith / normal_form.h

2021-12-22	Andrew Reynolds	Remove most uses of mkRationalNode (#7854)	blob \| commitdiff \| raw
2021-10-12	Ouyancheng	fix deprecation of std::iterator (#7332)	blob \| commitdiff \| raw \| diff to current
2021-06-26	yoni206	pow2 -- final changes (#6800)	blob \| commitdiff \| raw \| diff to current
2021-04-14	Aina Niemetz	Rename public and private headers in src/include. ...	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-09	Aina Niemetz	Rename CVC4__ header guards to CVC5__. (#6326)	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-09	Gereon Kremer	Some more cleanup of includes (#6083)	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-09-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-09-22	Gereon Kremer	ICP-based solver for nonlinear arithmetic (#5017)	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
2019-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	blob \| commitdiff \| raw \| diff to current
2019-04-24	Mathias Preiner	Do not use __ prefix for header guards. (#2974)	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-07	Andrew Reynolds	Add remaining transcendental functions (#1551)	blob \| commitdiff \| raw \| diff to current
2017-07-17	Tim King	Merge branch 'master' into cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-07-17	Andres Noetzli	Use is_sorted, merge, copy from std (#199)	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-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
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
2015-05-12	barrettcw	Merge pull request #74 from finnhaedicke/namespace_minisat	blob \| commitdiff \| raw \| diff to current
2015-04-22	Kshitij Bansal	Merge pull request #73 from kbansal/parser-dont-tokenize	blob \| commitdiff \| raw \| diff to current
2015-04-18	Tim King	Farkas proof coefficients.	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-26	Morgan Deters	Merge tag 'smtcomp2014-resubmission'	blob \| commitdiff \| raw \| diff to current
2014-06-22	Morgan Deters	Merge tag 'smtcomp2014-application'	blob \| commitdiff \| raw \| diff to current
2014-06-19	Morgan Deters	Fix for pre-C++11 is_sorted().	blob \| commitdiff \| raw \| diff to current
2014-06-19	Morgan Deters	Final preparations for arithmetic for building with...	blob \| commitdiff \| raw \| diff to current
2014-06-18	Morgan Deters	Fix for pre-C++11 is_sorted().	blob \| commitdiff \| raw \| diff to current
2014-06-17	Tim King	Merge pull request #33 from mdeters/arith-proposal	blob \| commitdiff \| raw \| diff to current
2014-06-17	Morgan Deters	Final preparations for arithmetic for building with...	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-06	Tim King	Merge pull request #21 from pcc/ite-fix	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-26	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-03-26	Tim King	Merging in a fix from 1.3.x.	blob \| commitdiff \| raw \| diff to current
2014-03-26	Tim King	Fixes an idempotency issue for non-linear multiplicatio...	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-02-20	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-19	Tim King	Merge branch 'master' of github.com:CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-19	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-02-19	Tim King	Stopping non-linear terms from entering the dio solver...	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-06-19	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-06-04	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-05-29	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-05-21	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-05-21	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-05-20	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-05-09	Kshitij Bansal	Merge branch 'master' of ssh://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-05-09	Tim King	Changing the integer normal form to increase matching.	blob \| commitdiff \| raw \| diff to current
2013-04-02	Morgan Deters	Regenerated copyrights: canonicalized names, no emails	blob \| commitdiff \| raw \| diff to current
2013-04-02	Morgan Deters	update copyrights	blob \| commitdiff \| raw \| diff to current
2012-11-08	Tim King	Improved support for division by zero. This adds the...	blob \| commitdiff \| raw \| diff to current
2012-11-07	Tim King	Fix to a bug in integer mod lemmas.	blob \| commitdiff \| raw \| diff to current
2012-10-11	Morgan Deters	Standardizing copyright notice. Touches ALL source...	blob \| commitdiff \| raw \| diff to current
2012-09-29	Tim King	This commit add interpretation by lemma for INTS_DIVISI...	blob \| commitdiff \| raw \| diff to current
2012-08-03	Morgan Deters	fix uses of getMetaKind() from outside the expr package...	blob \| commitdiff \| raw \| diff to current
2012-07-07	Morgan Deters	Various fixes to documentation---typos, some incomplete...	blob \| commitdiff \| raw \| diff to current
2012-06-14	Tim King	Brings the tuning branch into trunk. This includes...	blob \| commitdiff \| raw \| diff to current
2012-05-15	Tim King	This commit removes the CONST_INTEGER kind from nodes...	blob \| commitdiff \| raw \| diff to current
2012-04-17	Tim King	Merges branches/arithmetic/atom-database r2979 through...	blob \| commitdiff \| raw \| diff to current
2012-03-28	Tim King	Update to the ArithRewriter to remove REWRITE_AGAIN_FUL...	blob \| commitdiff \| raw \| diff to current
2012-02-15	Tim King	This commit merges into trunk the branch branches/arith...	blob \| commitdiff \| raw \| diff to current
2011-10-28	Tim King	Adding a check in Polynomial::parsePolynomial to better...	blob \| commitdiff \| raw \| diff to current
2011-09-16	Morgan Deters	fix numerous documentation issues; doxygen complains...	blob \| commitdiff \| raw \| diff to current
2011-09-02	Morgan Deters	Merge from my post-smtcomp branch. Includes:	blob \| commitdiff \| raw \| diff to current
2011-09-02	Morgan Deters	Partial merge of integers work; this is simple B&B...	blob \| commitdiff \| raw \| diff to current
2011-03-17	Tim King	- Removes arith_constants.h	blob \| commitdiff \| raw \| diff to current
2011-02-16	Tim King	Overview of the changes:	blob \| commitdiff \| raw \| diff to current
2011-01-05	Dejan Jovanović	Commit for the theory engine and rewriter changes....	blob \| commitdiff \| raw \| diff to current
2010-10-28	Tim King	The Row implementation has no been replaced by RowVecto...	blob \| commitdiff \| raw \| diff to current
2010-10-13	Tim King	Removed vector<Monomial> monos from Polynomial. Now...	blob \| commitdiff \| raw \| diff to current
2010-10-12	Tim King	IDENTITY has been removed.	blob \| commitdiff \| raw \| diff to current
2010-10-03	Morgan Deters	file header documentation regenerated with contributors...	blob \| commitdiff \| raw \| diff to current
2010-09-21	Morgan Deters	part of review (bug #197): coding conventions, file...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom