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

[cvc5.git] / src / theory / uf / equality_engine.h

2019-04-17	Andrew Reynolds	Cache explanations in the equality engine (#2937)	blob \| commitdiff \| raw
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-03-05	Mathias Preiner	Enable -Wsuggest-override by default. (#1643)	blob \| commitdiff \| raw \| diff to current
2017-10-25	Tim King	Switching EqProof to use shared_ptr everywhere. (...	blob \| commitdiff \| raw \| diff to current
2017-09-13	Andrew Reynolds	Modify equality engine to allow operators to be marked...	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Merge branch 'master' into cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Moving from the gnu extensions for hash maps to the...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Eliminate Boolean term conversion. Generalizes removeIT...	blob \| commitdiff \| raw \| diff to current
2016-10-11	Paul Meng	Merge branch 'origin' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-09-02	Tim King	Merge pull request #91 from timothy-king/no-throw	blob \| commitdiff \| raw \| diff to current
2016-09-01	Tim King	Relaxing the throw specifiers for the destructors for...	blob \| commitdiff \| raw \| diff to current
2016-07-05	PaulMeng	Merge branch 'master' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-06-06	guykatzz	Merge pull request #85 from CVC4/master_for_proof_merge	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Merge from proof branch	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Revert "Merging proof branch"	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Merging proof branch	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
2016-04-03	Guy	Removed the theory-specific merge reason types. Instead...	blob \| commitdiff \| raw \| diff to current
2016-03-24	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-03-24	Guy	Refactored the equality engine in order to remove theor...	blob \| commitdiff \| raw \| diff to current
2016-01-27	Liana Hadarean	Merged bit-vector and uf proof branch.	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-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-11-27	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-11-20	Dejan Jovanović	Making construction of trigger sets not use the global...	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-17	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-03-14	Andrew Reynolds	Add ability to provide theory-specific proof rules...	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-02-21	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-02-21	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-02-21	Kshitij Bansal	Merge pull request #10 from kbansal/sets-for-merge	blob \| commitdiff \| raw \| diff to current
2014-02-21	Kshitij Bansal	add new theory (sets)	blob \| commitdiff \| raw \| diff to current
2014-02-19	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-27	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-18	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-17	Kshitij Bansal	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-09	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-08	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-03	Andrew Reynolds	Added support for proof production in Equality Engine...	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-11-11	Morgan Deters	Flatten libcvc4 build structure; remove some #include...	blob \| commitdiff \| raw \| diff to current
2013-11-07	Morgan Deters	Flatten libcvc4 build structure; remove some #include...	blob \| commitdiff \| raw \| diff to current
2013-09-30	Liana Hadarean	merged golden	blob \| commitdiff \| raw \| diff to current
2013-09-13	Morgan Deters	Documentation fixes, some code typo fixes, file perms...	blob \| commitdiff \| raw \| diff to current
2013-08-26	Kshitij Bansal	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-07-19	Dejan Jovanovic	possible fix for bug 521	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-04-01	Morgan Deters	Merging some cleanup work:	blob \| commitdiff \| raw \| diff to current
2013-03-21	lianah	Merge branch 'master' into bv-core	blob \| commitdiff \| raw \| diff to current
2013-03-21	Dejan Jovanović	fixing markings of internal nodes in equality engine	blob \| commitdiff \| raw \| diff to current
2013-03-21	lianah	Merge branch 'master' into bv-core	blob \| commitdiff \| raw \| diff to current
2013-03-21	Dejan Jovanović	fixing constant evaluation bugs	blob \| commitdiff \| raw \| diff to current
2013-03-20	Liana Hadarean	merged master with dejan's constant evaluating equality...	blob \| commitdiff \| raw \| diff to current
2013-03-20	Dejan Jovanović	Adding evaluation of constant terms to the equality...	blob \| commitdiff \| raw \| diff to current
2012-11-26	Dejan Jovanović	Adding support for a master equality engine. Each theor...	blob \| commitdiff \| raw \| diff to current
2012-11-16	Dejan Jovanović	fixing and refactoring the equality iterator	blob \| commitdiff \| raw \| diff to current
2012-10-11	Morgan Deters	Standardizing copyright notice. Touches ALL source...	blob \| commitdiff \| raw \| diff to current
2012-10-09	Dejan Jovanović	fix for bug 415	blob \| commitdiff \| raw \| diff to current
2012-10-09	Dejan Jovanović	adding mergePredicates method to the equality engine...	blob \| commitdiff \| raw \| diff to current
2012-09-22	Morgan Deters	Separate public-facing and internal-facing interfaces...	blob \| commitdiff \| raw \| diff to current
2012-09-19	Dejan Jovanović	Changing the equality engines's euivalence class iterat...	blob \| commitdiff \| raw \| diff to current
2012-08-31	Andrew Reynolds	merge from fmf-devel branch. more updates to models...	blob \| commitdiff \| raw \| diff to current
2012-08-29	Morgan Deters	* Numerous documentation fixes (fix doxygen warnings...	blob \| commitdiff \| raw \| diff to current
2012-08-14	Tim King	Switched a number of EqClassIterator operations to...	blob \| commitdiff \| raw \| diff to current
2012-07-27	François Bobot	Merge quantifiers2-trunk:	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	Dejan Jovanović	changing to a more natural propagation order in uf...	blob \| commitdiff \| raw \| diff to current
2012-06-12	Morgan Deters	minor cleanup, and replace a "private:" in equality...	blob \| commitdiff \| raw \| diff to current
2012-06-11	Morgan Deters	Merge from quantifiers2-trunkmerge branch.	blob \| commitdiff \| raw \| diff to current
2012-06-10	Dejan Jovanović	fixes for bug347	blob \| commitdiff \| raw \| diff to current
2012-06-07	Dejan Jovanović	fixing the wrong results. arrays equality adaptor had...	blob \| commitdiff \| raw \| diff to current
2012-06-07	Dejan Jovanović	fixing some bugs in propagation of disequalities	blob \| commitdiff \| raw \| diff to current
2012-06-06	Dejan Jovanović	Changes to the combination mechanism, lots of details...	blob \| commitdiff \| raw \| diff to current
2012-05-27	Dejan Jovanović	Committing the work on equality engine, I need to see...	blob \| commitdiff \| raw \| diff to current
2012-05-24	Dejan Jovanović	Significant changes to the internals of the equality...	blob \| commitdiff \| raw \| diff to current
2012-05-21	Dejan Jovanović	Updating equality manager to handle tagged trigger...	blob \| commitdiff \| raw \| diff to current
2012-05-16	Dejan Jovanović	adding simple-minded handling of (dis-)equalities where...	blob \| commitdiff \| raw \| diff to current
2012-05-09	Dejan Jovanović	* simplifying equality engine interface	blob \| commitdiff \| raw \| diff to current
2012-05-08	Liana Hadarean	Merging in bvprop branch, with proper bit-vector propag...	blob \| commitdiff \| raw \| diff to current
2012-04-11	Morgan Deters	merge from arrays-clark branch	blob \| commitdiff \| raw \| diff to current
2012-03-22	Dejan Jovanović	some improvements to the sharing mechanism/interface	blob \| commitdiff \| raw \| diff to current
2012-03-06	Dejan Jovanović	updating the equality engine to be able to give explana...	blob \| commitdiff \| raw \| diff to current
2012-02-21	Dejan Jovanović	Fix for bug303. The problem was with function applicati...	blob \| commitdiff \| raw \| diff to current
2012-02-08	Dejan Jovanović	fixing a bug in uf_engine application lookup backtracking	blob \| commitdiff \| raw \| diff to current
2011-12-12	Dejan Jovanović	* merging some uf stuff from incremental_work branch...	blob \| commitdiff \| raw \| diff to current
2011-10-17	Dejan Jovanović	Sharing work	blob \| commitdiff \| raw \| diff to current
2011-09-07	Dejan Jovanović	fixes for uf/equality engine from the quantifiers branc...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom