| Age | Commit message (Expand) | Author |
|---|
| 2021-02-22 | (proof-new) Add new arithmetic kind INDEXED_ROOT_PREDICATE. (#5949) | Gereon Kremer |
| 2020-10-29 | Add mkInteger to the API (#5274) | mudathirmahgoub |
| 2020-06-29 | Add internal support for integer and operator (#4668) | Andrew Reynolds |
| 2019-09-28 | Introduce template classes for simple type rules (#2835) | Andres Noetzli |
| 2018-12-20 | Add missing type rules for parameterized operator kinds. (#2766) | Aina Niemetz |
| 2018-02-07 | Add remaining transcendental functions (#1551) | Andrew Reynolds |
| 2017-07-12 | Make type rules more strict for operators whose type rules involve subtypes. ... | ajreynol |
| 2017-07-10 | Merge ntExt branch. Adds support for transcendental functions. Refactoring of... | ajreynol |
| 2017-04-02 | Adding a model based axiom instantiation scheme for multiplication. Merge com... | Tim King |
| 2014-06-21 | Slightly-improved kinds documentation for builtin, Boolean, arrays, strings, ... | Morgan Deters |
| 2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al... | Morgan Deters |
| 2012-12-01 | drastic simplification of quantifiers code regarding equality queries, instan... | Andrew Reynolds |
| 2012-11-08 | Improved support for division by zero. This adds the *_TOTAL kinds and unint... | Tim King |
| 2012-10-08 | * Models' SubstitutionMaps are now attached to the user context | Morgan Deters |
| 2012-08-16 | Replace propagateAsDecision() with Theory::getNextDecisionRequest(): | Morgan Deters |
| 2012-08-07 | Some items from the CVC4 public interface review: | Morgan Deters |
| 2012-07-14 | Type enumerator infrastructure and uninterpreted constant support. No suppor... | Morgan Deters |
| 2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
| 2012-05-18 | This commit removes the dead psuedoboolean code. | Tim King |
| 2012-05-15 | This commit removes the CONST_INTEGER kind from nodes. This code comes from t... | Tim King |
| 2012-03-01 | Partial merge from kind-backend branch, including Minisat and CNF work to | Morgan Deters |
| 2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
| 2011-09-02 | Partial merge of integers work; this is simple B&B and some pseudoboolean | Morgan Deters |
| 2011-04-25 | Monday tasks: | Morgan Deters |
| 2011-04-25 | Weekend work. The main points: | Morgan Deters |
| 2011-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial an... | Dejan Jovanović |
| 2010-10-12 | IDENTITY has been removed. | Tim King |
| 2010-10-05 | parser and core support for SMT-LIBv2 commands get-info, set-option, get-opti... | Morgan Deters |
| 2010-09-13 | * New normal form for arithmetic is in place. | Tim King |
| 2010-05-20 | Added the division symbol to the parser, and minimal support for it in Theory... | Tim King |
| 2010-04-28 | Added theory/arith/kind and enabled the smt parser to read in these symbols. ... | Tim King |
| 2010-04-01 | PARSER STUFF: | Morgan Deters |
| 2010-03-30 | Highlights of this commit are: | Morgan Deters |
| 2010-03-25 | new domain-specific language for kinds files: permits characterization of dif... | Morgan Deters |
| 2010-02-27 | A bag of unrelated fixes to bring trunk more in-line with recent | Morgan Deters |
| 2010-02-04 | Added theory output channel interfaces and "Interrupted" exception. | Morgan Deters |
