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

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

2021-06-26	yoni206	pow2 -- final changes (#6800)	blob \| commitdiff \| raw
2021-05-24	Andrew Reynolds	Move proof utilities to src/proof/ (#6611)	blob \| commitdiff \| raw \| diff to current
2021-05-20	Alex Ozdemir	Expand arith's farkas lemma rule as a macro (#6577)	blob \| commitdiff \| raw \| diff to current
2021-04-14	Gereon Kremer	Refactor / reimplement statistics (#6162)	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-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-10-07	Alex Ozdemir	(proof-new) proofs in ee -> arith pipeline (#5215)	blob \| commitdiff \| raw \| diff to current
2020-10-06	Alex Ozdemir	(proof-new) proofs for ArithCongMan -> ee facts (#5207)	blob \| commitdiff \| raw \| diff to current
2020-10-03	Andrew Reynolds	Standardization of Theory (#5181)	blob \| commitdiff \| raw \| diff to current
2020-10-02	Alex Ozdemir	(proof-new) New proofs in arith::Constraint::externalEx...	blob \| commitdiff \| raw \| diff to current
2020-09-29	Alex Ozdemir	(proof-new) Add proof managers and eager gens to arith...	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-20	Andrew Reynolds	Simplify trigger notifications in equality engine ...	blob \| commitdiff \| raw \| diff to current
2020-08-17	Andrew Reynolds	Dynamic allocation of equality engine in Theory (#4890)	blob \| commitdiff \| raw \| diff to current
2020-08-14	Andrew Reynolds	Simplify equality engine notifications (#4896)	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-06-11	Andrew Reynolds	(proof-new) Remove arith-snorm option. (#4591)	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-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-09-05	Mathias Preiner	Use std::uniqe_ptr for d_eq_infer to make Coverity...	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	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
2017-03-02	ajreynol	Eliminate Boolean term conversion. Generalizes removeIT...	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	blob \| commitdiff \| raw \| diff to current
2016-04-14	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-04-14	ajreynol	Add option --snorm-infer-eq to infer equalities based...	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
2016-01-09	Tim King	Removing StatisticsRegistry's static functions current...	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
2015-04-17	Kshitij Bansal	Merge pull request #72 from kbansal/decision-requirephase	blob \| commitdiff \| raw \| diff to current
2015-04-02	Kshitij Bansal	Merge pull request #71 from kbansal/const-are-triggers	blob \| commitdiff \| raw \| diff to current
2015-03-28	Tianyi Liang	printer change for string smtlib2	blob \| commitdiff \| raw \| diff to current
2015-03-25	Kshitij Bansal	change const are triggers from false to true in equalit...	blob \| commitdiff \| raw \| diff to current
2015-01-07	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-12-27	Dejan Jovanovic	Adding an option to the equality engine constructor...	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-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
2013-12-05	Morgan Deters	Update copyrights, add missing file-level documentation...	blob \| commitdiff \| raw \| diff to current
2013-04-30	lianah	fixed merge conflicts	blob \| commitdiff \| raw \| diff to current
2013-04-26	Tim King	FCSimplex branch merge	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
2013-03-15	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-03-14	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-03-05	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-03-01	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-26	lianah	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-17	Kshitij Bansal	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-16	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-15	Kshitij Bansal	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-15	Kshitij Bansal	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-15	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-15	Tim King	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-08	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-05	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-05	Kshitij Bansal	Merge remote-tracking branch 'origin/1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-05	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-04	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-04	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-01	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-01-31	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-01-28	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-01-27	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-01-23	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-01-22	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-01-22	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-01-19	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2012-12-22	Dejan Jovanović	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2012-12-18	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2012-12-15	Tim King	Merging in patch from branch '1.0.x'.	blob \| commitdiff \| raw \| diff to current
2012-12-12	Dejan Jovanović	Merge pull request #2 from CVC4/1.0.x	blob \| commitdiff \| raw \| diff to current
2012-12-11	Morgan Deters	Merge branch '1.0.x', getting fix for bug 480	blob \| commitdiff \| raw \| diff to current
2012-12-11	Morgan Deters	Merge branch '1.0.x' (getting fix for bug 479)	blob \| commitdiff \| raw \| diff to current
2012-12-11	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2012-12-08	Morgan Deters	Merge from 1.0.x (bugfix for 476).	blob \| commitdiff \| raw \| diff to current
2012-12-07	François Bobot	Merge release branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2012-12-06	François Bobot	Merge branch 'release-1.0.x'	blob \| commitdiff \| raw \| diff to current
next

RSS Atom