Age | Commit message (Expand) | Author |
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 |