| Age | Commit message (Expand) | Author |
|---|
| 2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ... | Andrew Reynolds |
| 2014-05-10 | Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, m... | Andrew Reynolds |
| 2014-05-09 | Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC... | Andrew Reynolds |
| 2014-05-08 | Major simplifications to macros module. | ajreynol |
| 2014-05-08 | Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Min... | Andrew Reynolds |
| 2014-05-08 | Basic optimizations for ambqi : only normalize UF applied to variables, direc... | Andrew Reynolds |
| 2014-05-07 | patch to the last commit: add a single character case | Tianyi Liang |
| 2014-05-07 | fix a bug in contain | Tianyi Liang |
| 2014-05-07 | add splits | Tianyi Liang |
| 2014-05-07 | Fixes to ambqi, now solution-sound. | Andrew Reynolds |
| 2014-05-06 | First draft of ambqi_builder (new implementation of MBQI based on disjoint se... | Andrew Reynolds |
| 2014-05-05 | fix a bug in replace and contains | Tianyi Liang |
| 2014-05-05 | add constant regular expression check for intersection. | Tianyi Liang |
| 2014-05-05 | Valuation::entailmentCheck() proxy for TheoryEngine version. Signature and c... | Morgan Deters |
| 2014-05-02 | Simplification of EqualityEngine::areDisequal. Comparison for production : h... | Andrew Reynolds |
| 2014-05-02 | Fix assertion from previous commit. | ajreynol |
| 2014-05-02 | Add option --dt-stc-ind for strengthening skolemization. Refactor skolemizat... | Andrew Reynolds |
| 2014-05-02 | More minor optimizations for datatypes. | ajreynol |
| 2014-05-01 | Minor optimizations to datatypes, revert to checkClash not mod eq. Minor cle... | ajreynol |
| 2014-04-30 | T-entailment work, and QCF (quant conflict find) work that uses it. | Tim King |
| 2014-04-29 | Fix warnings, cleanup in strings typechecker. | Morgan Deters |
| 2014-04-29 | Fix compiler warning re: TheoryUF destructor. | Morgan Deters |
| 2014-04-29 | Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and rewrit... | Morgan Deters |
| 2014-04-29 | Mostly resolves bug #561 memory leaks, and more. | Morgan Deters |
| 2014-04-29 | fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlr | Tianyi Liang |
| 2014-04-29 | add leading zeros support for str.to.int | Tianyi Liang |
| 2014-04-29 | Significantly improve performance for producing datatypes models. | ajreynol |
| 2014-04-28 | Merge remote-tracking branch 'upstream/master' into sets | Kshitij Bansal |
| 2014-04-28 | add strings-opt2 for regular splitting | Tianyi Liang |
| 2014-04-28 | nodemanager robust skolem numbering | Kshitij Bansal |
| 2014-04-28 | Merge pull request #25 from kbansal/sets | Kshitij Bansal |
| 2014-04-28 | Preparation for models for co-inductive datatypes. Minor cleanup. | Andrew Reynolds |
| 2014-04-28 | Optimizations for datatypes: check for clashes modulo equality. Avoid buildi... | ajreynol |
| 2014-04-28 | minor fix | Kshitij Bansal |
| 2014-04-28 | Merge remote-tracking branch 'upstream/master' into sets | Kshitij Bansal |
| 2014-04-24 | minor change: add a heuristic for preventing constant splitting. | Tianyi Liang |
| 2014-04-24 | optimization | Kshitij Bansal |
| 2014-04-24 | Avoid assigning constructor terms to 1-constructor datatype eqcs, when possib... | ajreynol |
| 2014-04-24 | Compute care graph for datatypes. Preliminary results show 20x speed up on l... | Andrew Reynolds |
| 2014-04-24 | Add --inst-max-level=N option for Kshitij. Support define-const command in S... | Andrew Reynolds |
| 2014-04-22 | Minor fix to avoid rewriting datatype equalities into non-equalitiers, as req... | Andrew Reynolds |
| 2014-04-19 | fix warnings in strings/ | Kshitij Bansal |
| 2014-04-17 | Allow fmf-bound-int to be set with set-option and via API. | Morgan Deters |
| 2014-04-17 | simplify mkSkolem naming system: don't use $$ | Kshitij Bansal |
| 2014-04-17 | use internal skolem numbering | Kshitij Bansal |
| 2014-04-17 | Minor refactoring and optimizing. | Andrew Reynolds |
| 2014-04-14 | Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ... | Andrew Reynolds |
| 2014-04-14 | Add initial support for co-datatypes. | Andrew Reynolds |
| 2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for in... | Andrew Reynolds |
| 2014-04-10 | minor fix for strings | Tianyi Liang |
