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

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

2020-12-03	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw
2020-11-23	Andrew Reynolds	Change UF ho to ppRewrite instead of expand definition...	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-15	Andrew Reynolds	Standard equality engine notify class for Theory (...	blob \| commitdiff \| raw \| diff to current
2020-09-11	Andrew Reynolds	Move finite model minimization to UF last call effort...	blob \| commitdiff \| raw \| diff to current
2020-09-02	Andrew Reynolds	(proof-new) Add proof support in TheoryUF (#5002)	blob \| commitdiff \| raw \| diff to current
2020-09-01	Haniel Barbosa	Removes old proof code (#4964)	blob \| commitdiff \| raw \| diff to current
2020-08-27	Andrew Reynolds	(new theory) Update TheoryUF to new interface (#4944)	blob \| commitdiff \| raw \| diff to current
2020-08-24	Andrew Reynolds	Extend the standard Theory template based on equality...	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Remove spurious theory methods calls (#4931)	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Simplify and fix care graph for ufHo (#4924)	blob \| commitdiff \| raw \| diff to current
2020-08-20	Andrew Reynolds	Add TheoryState objects to each Theory (#4920)	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-07-11	Andrew Reynolds	(proof-new) Update Theory interface for proof-new ...	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-04-08	Andres Noetzli	Perform theory widening eagerly (#4044)	blob \| commitdiff \| raw \| diff to current
2020-04-03	Andres Noetzli	Update theory rewriter ownership, add stats to strings...	blob \| commitdiff \| raw \| diff to current
2020-04-02	Andres Noetzli	Initialize theory rewriters in theories (#4197)	blob \| commitdiff \| raw \| diff to current
2020-02-25	yoni206	remove redundant includes (#3815)	blob \| commitdiff \| raw \| diff to current
2019-09-12	Andrew Reynolds	Rename UF with cardinality extension (#3241)	blob \| commitdiff \| raw \| diff to current
2019-07-02	Andrew Reynolds	Use unique_ptr for UF modules (#3080)	blob \| commitdiff \| raw \| diff to current
2019-07-01	Andrew Reynolds	Split higher-order UF solver (#2890)	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-11-27	Andrew Reynolds	Make (T)NodeTrie a general utility (#2489)	blob \| commitdiff \| raw \| diff to current
2018-09-17	Andrew Reynolds	Decision strategy: incorporate UF with cardinality...	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-04-11	Andrew Reynolds	Properly implement function extensionality based on...	blob \| commitdiff \| raw \| diff to current
2018-03-05	Mathias Preiner	Enable -Wsuggest-override by default. (#1643)	blob \| commitdiff \| raw \| diff to current
2018-02-06	Tim King	Resolving warnings from -Winconsistent-missing-override...	blob \| commitdiff \| raw \| diff to current
2017-12-08	Andrew Reynolds	Make collect model info return a Bool (#1421)	blob \| commitdiff \| raw \| diff to current
2017-09-21	Andrew Reynolds	Extend quantifier-free UF solver to higher-order. This...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-04-04	ajreynol	Simplify Theory::collectModelInfo interface to not...	blob \| commitdiff \| raw \| diff to current
2017-03-21	ajreynol	Improve computeCareGraph functions to check shared...	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Eliminate Boolean term conversion. Generalizes removeIT...	blob \| commitdiff \| raw \| diff to current
2016-11-03	ajreynol	Add priorities to getNextDecision. Properly handle...	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-05-26	Clark Barrett	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-05-26	ajreynol	Use term indexing in TheoryUF::computeCareGraph. Do...	blob \| commitdiff \| raw \| diff to current
2016-05-20	ajreynol	Improvements to theory combination + strings: do not...	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-03-23	guykatzz	Merge pull request #82 from CVC4/master_for_merge	blob \| commitdiff \| raw \| diff to current
2016-03-23	Guy	squash-merge from proof branch	blob \| commitdiff \| raw \| diff to current
2016-01-28	Tim King	Adding listeners to Options.	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-06	Tim King	Add SmtGlobals Class	blob \| commitdiff \| raw \| diff to current
2015-10-26	ajreynol	Promote InstStrategyCbqi to quantifier module. Cleanup...	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-30	Morgan Deters	Fix compiler warning re: TheoryUF destructor.	blob \| commitdiff \| raw \| diff to current
2014-04-30	Morgan Deters	Mostly resolves bug #561 memory leaks, and more.	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-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-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-22	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-01-22	Morgan Deters	Delay QuantifiersEngine and UF strong solver initializa...	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-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-13	lianah	post failed attempts at getting the incremental solver...	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-24	Andrew Reynolds	added option --model-u-dt-enum for outputting uninterpr...	blob \| commitdiff \| raw \| diff to current
2012-12-01	Morgan Deters	remove instantiator framework	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-10-11	Morgan Deters	Standardizing copyright notice. Touches ALL source...	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-07-12	Andrew Reynolds	merged fmf-devel branch, includes support for SMT2...	blob \| commitdiff \| raw \| diff to current
2012-07-06	Tim King	Added virtual destructor to PpRewrite.	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-06	Dejan Jovanović	Changes to the combination mechanism, lots of details...	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-09	Dejan Jovanović	* simplifying equality engine interface	blob \| commitdiff \| raw \| diff to current
2012-05-03	Dejan Jovanović	Some cleanup starting off from trying to understand...	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-02	Dejan Jovanović	CDMap -> CDHashMap	blob \| commitdiff \| raw \| diff to current
2012-02-24	Dejan Jovanović	Theory interface changes:	blob \| commitdiff \| raw \| diff to current
2011-11-30	Morgan Deters	fix linking errors on oneiric	blob \| commitdiff \| raw \| diff to current
2011-10-17	Dejan Jovanović	Sharing work	blob \| commitdiff \| raw \| diff to current
2011-09-29	Morgan Deters	Some base infrastructure for user push/pop; a few bugfi...	blob \| commitdiff \| raw \| diff to current
2011-09-15	Dejan Jovanović	additional stuff for sharing,	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
2011-09-02	Morgan Deters	Merge from my post-smtcomp branch. Includes:	blob \| commitdiff \| raw \| diff to current
2011-07-11	Dejan Jovanović	adding disequality propagation	blob \| commitdiff \| raw \| diff to current
2011-07-11	Morgan Deters	merge from symmetry branch	blob \| commitdiff \| raw \| diff to current
next

RSS Atom