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

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

2018-08-27	Mathias Preiner	Use std:unique_ptr instead of raw pointers in theory...	blob \| commitdiff \| raw
2018-08-21	Tim King	Add constexpr annotations to help coverity understand...	blob \| commitdiff \| raw \| diff to current
2018-08-16	Andres Noetzli	Move node algorithms to separate file (#2311)	blob \| commitdiff \| raw \| diff to current
2018-08-01	Andrew Reynolds	Fix issues with bv2nat (#2219)	blob \| commitdiff \| raw \| diff to current
2018-08-01	Mathias Preiner	Remove hasAssertions() method from eager BV solver...	blob \| commitdiff \| raw \| diff to current
2018-07-30	Mathias Preiner	Add support for incremental eager bit-blasting. (#1838)	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-05-30	Mathias Preiner	Normalize negated bit-vector terms over equalities...	blob \| commitdiff \| raw \| diff to current
2018-05-23	Andrew Reynolds	Add notions of evaluated kinds in TheoryModel (#1947)	blob \| commitdiff \| raw \| diff to current
2018-05-10	Aina Niemetz	Refactored BVAckermann preprocessing pass. (#1889)	blob \| commitdiff \| raw \| diff to current
2018-04-20	yoni206	Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv...	blob \| commitdiff \| raw \| diff to current
2018-03-07	Mathias Preiner	Make statistics output consistent. (#1647)	blob \| commitdiff \| raw \| diff to current
2018-02-10	Aina Niemetz	Remove mkNode from bv::utils (#1587)	blob \| commitdiff \| raw \| diff to current
2018-01-16	Tim King	Removing more miscellaneous throw specifiers. (#1509)	blob \| commitdiff \| raw \| diff to current
2018-01-09	Aina Niemetz	Add bv util mkConst(unsigned, Integer&). (#1499)	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-10-21	Mathias Preiner	Add rewriting rules for Eq/Ult with sign_extend and...	blob \| commitdiff \| raw \| diff to current
2017-08-24	Andrew Reynolds	Merge pull request #191 from timothy-king/cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-08-24	Andres Noetzli	Fix typos	blob \| commitdiff \| raw \| diff to current
2017-08-09	Aina Niemetz	Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp	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-28	Tim King	Minor cleanups to ExtTheory.	blob \| commitdiff \| raw \| diff to current
2017-03-27	Clark Barrett	Merge pull request #137 from 4tXJ7f/throw_quals	blob \| commitdiff \| raw \| diff to current
2017-03-27	Tim King	Making the ExtTheory object a private member of Theory.	blob \| commitdiff \| raw \| diff to current
2016-12-03	Clark Barrett	Fix for bug 734	blob \| commitdiff \| raw \| diff to current
2016-11-16	Clark Barrett	Merge pull request #108 from timothy-king/smt2-parser...	blob \| commitdiff \| raw \| diff to current
2016-11-14	ajreynol	Minor improvement to caching for extf bv inferences.	blob \| commitdiff \| raw \| diff to current
2016-11-12	Tim King	Merge pull request #105 from timothy-king/delete-maxed-out	blob \| commitdiff \| raw \| diff to current
2016-11-11	Clark Barrett	Enable eager bitblasting for QF_ABV when no stores...	blob \| commitdiff \| raw \| diff to current
2016-11-11	ajreynol	Add simple inferences for extended bitvector functions...	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-10-11	Paul Meng	Merge branch 'origin' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-10-01	Tim King	Merge pull request #93 from timothy-king/clang-format	blob \| commitdiff \| raw \| diff to current
2016-09-26	Tim King	Deleting the eager bitblasting solver if present in...	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-08-16	ajreynol	Initial infrastructure for ExtTheory, generalize extend...	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-05-27	Clark Barrett	Merged QF_UFBV support from experimental 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-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-09	Tim King	Removing StatisticsRegistry's static functions current...	blob \| commitdiff \| raw \| diff to current
2016-01-06	Tim King	Add SmtGlobals Class	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-29	lianah	changed resource step options to unsigned	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-05-12	barrettcw	Merge pull request #74 from finnhaedicke/namespace_minisat	blob \| commitdiff \| raw \| diff to current
2015-04-23	Clark Barrett	Merge branch 'master' into google	blob \| commitdiff \| raw \| diff to current
2015-04-21	Clark Barrett	Changes needed to compile at Google, plus some bug...	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	Morgan Deters	New, uniform checkTime statistic for all theories ...	blob \| commitdiff \| raw \| diff to current
2014-11-17	Liana Hadarean	Resource-limiting work.	blob \| commitdiff \| raw \| diff to current
2014-11-10	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Fix memory issues in bitvector theory, which is now...	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-05	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-17	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-16	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-11	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-10	Kshitij Bansal	Merge remote-tracking branch 'origin/1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-09	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-02	Morgan Deters	Merge branch '1.4.x'.	blob \| commitdiff \| raw \| diff to current
2014-09-30	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-27	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-26	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-17	Kshitij Bansal	Merge branch '1.4.x' while ignoring commit 8d5eb49.	blob \| commitdiff \| raw \| diff to current
2014-09-17	Kshitij Bansal	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-03	Kshitij Bansal	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2014-09-03	Kshitij Bansal	check() optimization	blob \| commitdiff \| raw \| diff to current
2014-08-22	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-22	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-19	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-19	lianah	Making getEqualityStatus more powerful for bit-vector...	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-26	Morgan Deters	Merge tag 'smtcomp2014-resubmission'	blob \| commitdiff \| raw \| diff to current
2014-06-22	Morgan Deters	Merge tag 'smtcomp2014-application'	blob \| commitdiff \| raw \| diff to current
2014-06-19	lianah	fixed merge conflict	blob \| commitdiff \| raw \| diff to current
2014-06-19	lianah	added model generation to eager bit-blasting and turned...	blob \| commitdiff \| raw \| diff to current
2014-06-16	lianah	fixed bv bug due to applying equisatisfiable transforma...	blob \| commitdiff \| raw \| diff to current
2014-06-15	lianah	Evil bitvector preprocessing pass for simplifying power...	blob \| commitdiff \| raw \| diff to current
2014-06-15	lianah	bv static learning and rewrites for power of 2 terms	blob \| commitdiff \| raw \| diff to current
2014-06-14	lianah	more bv rewrites	blob \| commitdiff \| raw \| diff to current
2014-06-14	lianah	fixed merge	blob \| commitdiff \| raw \| diff to current
2014-06-14	lianah	added bv inequality rewrite	blob \| commitdiff \| raw \| diff to current
next

RSS Atom