git.libre-soc.org Git - cvc5.git/history

[cvc5.git] / src / theory / arith / kinds

2021-06-15	yoni206	pow2: adding a kind, inference rules, and some implemen...	blob \| commitdiff \| raw
2021-05-26	Andres Noetzli	More precise includes of `Node` constants (#6617)	blob \| commitdiff \| raw \| diff to current
2021-04-15	Aina Niemetz	Rename occurrences of CVC4 to CVC5. (#6351)	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-02-22	Gereon Kremer	(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDIC...	blob \| commitdiff \| raw \| diff to current
2020-10-29	mudathirmahgoub	Add mkInteger to the API (#5274)	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
2019-09-29	Andres Noetzli	Introduce template classes for simple type rules (...	blob \| commitdiff \| raw \| diff to current
2018-12-20	Aina Niemetz	Add missing type rules for parameterized operator kinds...	blob \| commitdiff \| raw \| diff to current
2018-02-07	Andrew Reynolds	Add remaining transcendental functions (#1551)	blob \| commitdiff \| raw \| diff to current
2017-07-13	Aina Niemetz	Merge pull request #188 from aniemetz/cx11	blob \| commitdiff \| raw \| diff to current
2017-07-12	ajreynol	Make type rules more strict for operators whose type...	blob \| commitdiff \| raw \| diff to current
2017-07-10	ajreynol	Merge ntExt branch. Adds support for transcendental...	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
2014-07-10	Kshitij Bansal	Merge remote-tracking branch 'origin/master' into segfa...	blob \| commitdiff \| raw \| diff to current
2014-06-30	Kshitij Bansal	Merge pull request #47 from kbansal/sets	blob \| commitdiff \| raw \| diff to current
2014-06-26	Morgan Deters	Merge tag 'smtcomp2014-resubmission'	blob \| commitdiff \| raw \| diff to current
2014-06-25	Andrew Reynolds	Merge pull request #34 from mdeters/datatypes-kinds	blob \| commitdiff \| raw \| diff to current
2014-06-25	Andrew Reynolds	Merge pull request #37 from mdeters/quants-kinds	blob \| commitdiff \| raw \| diff to current
2014-06-25	Andrew Reynolds	Merge pull request #38 from mdeters/uf-kinds	blob \| commitdiff \| raw \| diff to current
2014-06-22	Morgan Deters	Merge tag 'smtcomp2014-application'	blob \| commitdiff \| raw \| diff to current
2014-06-22	lianah	Merge pull request #35 from mdeters/bv-kinds	blob \| commitdiff \| raw \| diff to current
2014-06-21	Morgan Deters	Slightly-improved kinds documentation for builtin,...	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
2012-12-01	Andrew Reynolds	drastic simplification of quantifiers code regarding...	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-10-08	Morgan Deters	* Models' SubstitutionMaps are now attached to the...	blob \| commitdiff \| raw \| diff to current
2012-08-16	Morgan Deters	Replace propagateAsDecision() with Theory::getNextDecis...	blob \| commitdiff \| raw \| diff to current
2012-08-07	Morgan Deters	Some items from the CVC4 public interface review:	blob \| commitdiff \| raw \| diff to current
2012-07-14	Morgan Deters	Type enumerator infrastructure and uninterpreted consta...	blob \| commitdiff \| raw \| diff to current
2012-06-11	Morgan Deters	Merge from quantifiers2-trunkmerge branch.	blob \| commitdiff \| raw \| diff to current
2012-05-18	Tim King	This commit removes the dead psuedoboolean code.	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-03-01	Morgan Deters	Partial merge from kind-backend branch, including Minis...	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-04-25	Morgan Deters	Monday tasks:	blob \| commitdiff \| raw \| diff to current
2011-04-25	Morgan Deters	Weekend work. The main points:	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-12	Tim King	IDENTITY has been removed.	blob \| commitdiff \| raw \| diff to current
2010-10-05	Morgan Deters	parser and core support for SMT-LIBv2 commands get...	blob \| commitdiff \| raw \| diff to current
2010-09-13	Tim King	* New normal form for arithmetic is in place.	blob \| commitdiff \| raw \| diff to current
2010-05-20	Tim King	Added the division symbol to the parser, and minimal...	blob \| commitdiff \| raw \| diff to current
2010-04-28	Tim King	Added theory/arith/kind and enabled the smt parser...	blob \| commitdiff \| raw \| diff to current
2010-04-01	Morgan Deters	PARSER STUFF:	blob \| commitdiff \| raw \| diff to current
2010-03-30	Morgan Deters	Highlights of this commit are:	blob \| commitdiff \| raw \| diff to current
2010-03-25	Morgan Deters	new domain-specific language for kinds files: permits...	blob \| commitdiff \| raw \| diff to current
2010-02-27	Morgan Deters	A bag of unrelated fixes to bring trunk more in-line...	blob \| commitdiff \| raw \| diff to current
2010-02-04	Morgan Deters	Added theory output channel interfaces and "Interrupted...	blob \| commitdiff \| raw \| diff to current

RSS Atom