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

[cvc5.git] / src / theory / bv / bv_subtheory_core.cpp

2021-02-13	Mathias Preiner	Properly set up equality engine for BV bitblast solver...	blob \| commitdiff \| raw
2021-02-11	Gereon Kremer	Make most methods of TheoryInferenceManager expect...	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-04	Andrew Reynolds	(new theory) Update TheoryBV to new standard for collec...	blob \| commitdiff \| raw \| diff to current
2020-09-04	Mathias Preiner	Split lazy bit-vector solver from TheoryBV (#5009)	blob \| commitdiff \| raw \| diff to current
2020-09-03	Andrew Reynolds	Make ExtTheory independent of Theory (#5010)	blob \| commitdiff \| raw \| diff to current
2020-08-31	Andrew Reynolds	Simplify interface for computing relevant terms. (...	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Remove BV equality slicer (#4928)	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-15	Andrew Reynolds	Minor cleanup related to notifications (#4898)	blob \| commitdiff \| raw \| diff to current
2020-07-16	Andrew Reynolds	Make ExtTheory a utility and not a member of Theory...	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-02-20	Mathias Preiner	resource manager: Add statistic for every resource...	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-08-27	Mathias Preiner	Use std:unique_ptr instead of raw pointers in theory...	blob \| commitdiff \| raw \| diff to current
2018-07-06	Andrew Reynolds	Split ext theory to own file and document (#1809)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-06-07	Aina Niemetz	Remove invalid assertion (#1993). (#2057)	blob \| commitdiff \| raw \| diff to current
2018-03-07	Mathias Preiner	Make statistics output consistent. (#1647)	blob \| commitdiff \| raw \| diff to current
2018-02-17	Aina Niemetz	bv::utils::mk(And\|Or) Do not return true if size of...	blob \| commitdiff \| raw \| diff to current
2018-02-10	Aina Niemetz	Remove mkNode from bv::utils (#1587)	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-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-05-31	ajreynol	Fix model construction for BV with cbqi. Minor change...	blob \| commitdiff \| raw \| diff to current
2016-10-13	ajreynol	Merging bv parts of ajr/bvExt branch, minor additions...	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-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-09-02	Kshitij Bansal	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2015-08-24	Liana Hadarean	Added threshold for core bv cardinality lemmas	blob \| commitdiff \| raw \| diff to current
2015-08-24	Liana Hadarean	Fix for bv core cardinality lemma generation	blob \| commitdiff \| raw \| diff to current
2015-05-28	Liana Hadarean	added options for controlling resource step-count for...	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-25	Kshitij Bansal	change const are triggers from false to true in equalit...	blob \| commitdiff \| raw \| diff to current
2015-03-14	Tianyi Liang	Bug fix for BV	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-17	Liana Hadarean	Resource-limiting work.	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-16	lianah	core solver fix	blob \| commitdiff \| raw \| diff to current
2014-06-10	lianah	Merging CAV14 paper bit-vector work.	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-12-03	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2013-11-27	Morgan Deters	General pre-release cleanup commit	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-07-22	Andrew Reynolds	Bug fix for --fmf-fmc for non-uninterpreted sort quanti...	blob \| commitdiff \| raw \| diff to current
2013-06-25	Morgan Deters	Merge branch '1.2.x'	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-14	lianah	added some extra options to the bit-vector theory	blob \| commitdiff \| raw \| diff to current
2013-04-18	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-04-11	lianah	fixed getModelValue to only query the value of leaves...	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	lianah	fixed bug 502; now the core bv solver only gives the...	blob \| commitdiff \| raw \| diff to current
2013-03-29	Dejan Jovanović	Merge branch 'master' of github.com:CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	reverted the core solver to do static slicing, added...	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	Merge branch 'master' into bv-core	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	fixed some model stuff	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	fixed model generation bug; commented out attempt...	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	inequality solver now only splits on disequalities...	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	added model generation for bv subtheories and bv-inequa...	blob \| commitdiff \| raw \| diff to current
2013-03-26	lianah	fixed inequality bugs due to improper explanation	blob \| commitdiff \| raw \| diff to current
2013-03-26	lianah	cleaned up the bv subtheory interface; added check...	blob \| commitdiff \| raw \| diff to current
2013-03-23	lianah	fixed some explanation problems for the core theory...	blob \| commitdiff \| raw \| diff to current
2013-03-22	lianah	Merge branch 'master' into bv-core	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	lianah	fixed more equality stuff	blob \| commitdiff \| raw \| diff to current
2013-03-21	lianah	incorporated dejan's constant evaluation; now getting...	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	lianah	added regression test for constant eval	blob \| commitdiff \| raw \| diff to current
2013-03-21	lianah	Merge branch 'master' into bv-core	blob \| commitdiff \| raw \| diff to current
2013-03-20	Liana Hadarean	fixed reversed concat in core theory	blob \| commitdiff \| raw \| diff to current
2013-03-20	Liana Hadarean	merged dejan's stuff	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-16	lianah	started work on the inequality bv subtheory	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-06	lianah	more slicer changes for incremental	blob \| commitdiff \| raw \| diff to current
2013-02-14	lianah	started working on incremental slicer - not compiling	blob \| commitdiff \| raw \| diff to current
2013-02-11	lianah	undid the caching that actually hurt performance	blob \| commitdiff \| raw \| diff to current
2013-02-05	Liana Hadarean	Added path compression and caching for getBaseDecomposi...	blob \| commitdiff \| raw \| diff to current
2013-02-05	lianah	Fixing regression failure. The only unfixed ones seem...	blob \| commitdiff \| raw \| diff to current
2013-02-02	lianah	merged master into branch	blob \| commitdiff \| raw \| diff to current
2013-01-11	lianah	fixed most bugs and added paranoid assertions	blob \| commitdiff \| raw \| diff to current
2012-12-11	Liana Hadarean	fixed some slicer bugs; set up bv theory to run bit...	blob \| commitdiff \| raw \| diff to current
2012-12-11	Liana Hadarean	ported my bv-core branch from svn to git	blob \| commitdiff \| raw \| diff to current

RSS Atom