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

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

2021-07-27	Mathias Preiner	bv: Refactor getEqualityStatus and use for both bitblas...	blob \| commitdiff \| raw
2021-07-15	Mathias Preiner	bv: Rename lazy solver to layered solver. (#6889)	blob \| commitdiff \| raw \| diff to current
2021-07-15	Mathias Preiner	bv: Rename simple solver to bitblast-internal. (#6888)	blob \| commitdiff \| raw \| diff to current
2021-06-21	Mathias Preiner	Fix model issues with --bitblast=eager. (#6753)	blob \| commitdiff \| raw \| diff to current
2021-05-24	Andrew Reynolds	Move proof utilities to src/proof/ (#6611)	blob \| commitdiff \| raw \| diff to current
2021-05-21	Aina Niemetz	BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)	blob \| commitdiff \| raw \| diff to current
2021-04-30	Mathias Preiner	bv: Refactor ppAssert and move to TheoryBV. (#6470)	blob \| commitdiff \| raw \| diff to current
2021-04-22	Andrew Reynolds	Move expand definition from Theory to TheoryRewriter...	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-05	Haniel Barbosa	[proof-new] Registering proof checkers uniformly from...	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-10	Andrew Reynolds	(proof-new) Update ppRewrite to use skolem lemmas ...	blob \| commitdiff \| raw \| diff to current
2021-03-09	Aina Niemetz	Update copyright headers to 2021. (#6081)	blob \| commitdiff \| raw \| diff to current
2021-03-06	Mathias Preiner	Remove partial UDIV/UREM operators. (#6069)	blob \| commitdiff \| raw \| diff to current
2021-03-02	Gereon Kremer	Clean up includes to reduce compile times (#6031)	blob \| commitdiff \| raw \| diff to current
2021-02-18	Gereon Kremer	Add statistic for InferenceId to TheoryInferenceManager...	blob \| commitdiff \| raw \| diff to current
2021-02-13	Mathias Preiner	Properly set up equality engine for BV bitblast solver...	blob \| commitdiff \| raw \| diff to current
2021-02-03	Mathias Preiner	Add BV solver bitblast. (#5851)	blob \| commitdiff \| raw \| diff to current
2020-12-23	Andrew Reynolds	Add option to track and notify from CNF stream (#5708)	blob \| commitdiff \| raw \| diff to current
2020-12-15	Andrew Reynolds	Remove bv divide by zero option (#5672)	blob \| commitdiff \| raw \| diff to current
2020-12-08	Mathias Preiner	Add support for BV proofs with the simple bitblasting...	blob \| commitdiff \| raw \| diff to current
2020-12-07	Andrew Reynolds	Do not expand theory definitions at the beginning of...	blob \| commitdiff \| raw \| diff to current
2020-10-06	Andrew Reynolds	(proof-new) Add interface for trusted substitution...	blob \| commitdiff \| raw \| diff to current
2020-10-03	Andrew Reynolds	Standardization of Theory (#5181)	blob \| commitdiff \| raw \| diff to current
2020-09-22	Mathias Preiner	Add simple BV solver (#5065)	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-09-01	Haniel Barbosa	Removes old proof code (#4964)	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 BV equality slicer (#4928)	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-17	Andrew Reynolds	Dynamic allocation of equality engine in Theory (#4890)	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-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-05-20	Andrew Reynolds	Do not eliminate variables that are equal to unevaluata...	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-27	Andrew Reynolds	Initial work towards -Wshadow (#3817)	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andrew Reynolds	Fix regression (#3827)	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andrew Reynolds	Fix node arity issue in reduction of int2bv (#3777)	blob \| commitdiff \| raw \| diff to current
2020-02-20	Mathias Preiner	resource manager: Add statistic for every resource...	blob \| commitdiff \| raw \| diff to current
2020-01-28	Andrew Reynolds	Avoid PLUS with one child for bv2nat elimination (...	blob \| commitdiff \| raw \| diff to current
2019-12-17	Mathias Preiner	Generate code for options with modes. (#3561)	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
2019-01-14	Alex Ozdemir	ClausalBitvectorProof (#2786)	blob \| commitdiff \| raw \| diff to current
2018-12-10	makaimann	BoolToBV modes (off, ite, all) (#2530)	blob \| commitdiff \| raw \| diff to current
2018-12-03	Alex Ozdemir	Bit vector proof superclass (#2599)	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-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
next

RSS Atom