summaryrefslogtreecommitdiff
path: root/src/theory/bv/kinds
AgeCommit message (Expand)Author
2019-09-28Introduce template classes for simple type rules (#2835)Andres Noetzli
2018-12-20Clean up BV kinds and type rules. (#2766)Aina Niemetz
2018-12-20Add missing type rules for parameterized operator kinds. (#2766)Aina Niemetz
2018-05-10Refactored BVAckermann preprocessing pass. (#1889)Aina Niemetz
2017-03-06Adding support for bool-to-bvClark Barrett
2016-10-13Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.ajreynol
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2014-06-20Bit-vector kinds documentationMorgan Deters
2014-06-10Merging CAV14 paper bit-vector work.lianah
2013-11-27General pre-release cleanup commitMorgan Deters
2013-09-18Support for bv2nat/int2bv in parser and BV rewriter.Morgan Deters
2012-12-10ported my bv-core branch from svn to gitLiana Hadarean
2012-11-13added support for division by zero for bit-vector division operatorsLiana Hadarean
2012-10-10fixing the cvc bv parser and typecheckerDejan Jovanović
2012-08-28Improved compatibility layer, now supports quantifiers. Also incorporatesMorgan Deters
2012-08-07Some items from the CVC4 public interface review:Morgan Deters
2012-07-14Type enumerator infrastructure and uninterpreted constant support. No suppor...Morgan Deters
2012-04-04 * added propagation as lemmas to TheoryBV:Liana Hadarean
2012-02-25Refactored CnfStream to work with the bv theory Bitblaster:Liana Hadarean
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-04-25Weekend work. The main points:Morgan Deters
2011-03-21more bugfixes, some basic propagation, and testcases to cover themDejan Jovanović
2011-02-26adding the variables count to the statistics in the expr managerDejan Jovanović
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-10-06declare-sort, define-sort working but not thoroughly tested; define-fun half ...Morgan Deters
2010-10-05parser and core support for SMT-LIBv2 commands get-info, set-option, get-opti...Morgan Deters
2010-09-20bitvector rewriting for the core theory and testcasesDejan Jovanović
2010-06-30* theory "tree" rewriting implemented and worksMorgan Deters
2010-05-02smt parser for bit-vectorsDejan Jovanović
2010-04-29Added the capability to construct expressions by passing the operator instead...Dejan Jovanović
2010-04-14Marging from types 404:415, changes: MassiveDejan Jovanović
2010-03-30Highlights of this commit are:Morgan Deters
2010-03-25new domain-specific language for kinds files: permits characterization of dif...Morgan Deters
2010-02-26* test/unit/context/context_black.h: Test CDList<>. In particular,Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback