Age | Commit message (Expand) | Author |
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 simplify output for SMT2 printer. | 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 for --force-logic to extend its reach to the parser. | Morgan Deters |
2014-04-29 | fixed couple of more warnings | Kshitij Bansal |
2014-04-29 | fix was compiler warning in antlr_input, crashing test case with the old fix | Kshitij Bansal |
2014-04-29 | Revert a compiler warning fix from ea6a5a6. | 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 | cleanup | Kshitij Bansal |
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-27 | attempt to improve CVC4's "parse error" message | Kshitij Bansal |
2014-04-27 | rm undocument/non-working* "feature" | 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 | Eh, what? | Kshitij Bansal |
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-11 | Better support for building with mingw64; thanks to Nicolas Roche @ Altran fo... | Morgan Deters |
2014-04-10 | setType -> setOfType, resolves bug 556 | Morgan Deters |
2014-04-10 | Fix the build; --check-proof works for UF but not for the new UFC logic. | Morgan Deters |
2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for in... | Andrew Reynolds |
2014-04-10 | Boolean terms conversion fix for datatypes, fixes a problem Andy discovered o... | Morgan Deters |
2014-04-10 | minor fix for strings | Tianyi Liang |
2014-04-10 | Add support for cardinality constraints logic UFC. Add regressions in fmf/. ... | Andrew Reynolds |
2014-04-09 | Merge pull request #24 from kbansal/sets-model | Kshitij Bansal |
2014-04-09 | Minor change to better support parameterized partial/total kinds (for upcomin... | Morgan Deters |
2014-04-09 | Revert E-matching datatypes fix. | Andrew Reynolds |
2014-04-09 | Handle fmf.card as input from user, add support in SMT2 parser, as requested ... | Andrew Reynolds |
2014-04-09 | fix get-info error-behavior | Kshitij Bansal |