| 2014-05-19 |
Tim King | More documentation fixes. Apologies for multiple commits. |
commit | commitdiff | tree |
| 2014-05-19 |
Tim King | Fixing documentation for glpk configuration. |
commit | commitdiff | tree |
| 2014-05-19 |
Tianyi Liang | minor fix for string equality engine assertion. |
commit | commitdiff | tree |
| 2014-05-17 |
Kshitij Bansal | Merge pull request #26 from kbansal/sets |
commit | commitdiff | tree |
| 2014-05-16 |
Kshitij Bansal | lfsc_checker: fix some warnings reported by _both_... |
commit | commitdiff | tree |
| 2014-05-16 |
Kshitij Bansal | sets: fix a bug in model building, another in handling... |
commit | commitdiff | tree |
| 2014-05-16 |
Kshitij Bansal | minor improvements (fixes) to did-you-mean suggestions |
commit | commitdiff | tree |
| 2014-05-15 |
Andrew Reynolds | Minor fixes. Add SMTCOMP 2014 script. |
commit | commitdiff | tree |
| 2014-05-14 |
Andrew Reynolds | Finish --dump-instantiations option. Update scripts. |
commit | commitdiff | tree |
| 2014-05-13 |
Tianyi Liang | Reject native extended ASCII characters. It requires... |
commit | commitdiff | tree |
| 2014-05-13 |
Tianyi Liang | Reject un-escaped extended ASCII characters |
commit | commitdiff | tree |
| 2014-05-13 |
ajreynol | Add lazy strategy for bounded integers to avoid non... |
commit | commitdiff | tree |
| 2014-05-13 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-05-13 |
Tianyi Liang | Fix a bug in the IndexOf function. |
commit | commitdiff | tree |
| 2014-05-13 |
Tianyi Liang | Fix a bug in the IndexOf function. |
commit | commitdiff | tree |
| 2014-05-12 |
Andrew Reynolds | Minor updates/fix to --cbqi-recurse |
commit | commitdiff | tree |
| 2014-05-12 |
Tim King | Merge remote-tracking branch 'timothy-king/master' |
commit | commitdiff | tree |
| 2014-05-12 |
Tim King | Merging in additional glpk options and statistics from... |
commit | commitdiff | tree |
| 2014-05-12 |
Tianyi Liang | Add a benchmark that detects a bug in parsing. Thank... |
commit | commitdiff | tree |
| 2014-05-12 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-05-12 |
Tianyi Liang | Replace lemma sending with EQ assertions. Fix a typo... |
commit | commitdiff | tree |
| 2014-05-12 |
Tianyi Liang | Replace lemma sending with EQ assertions. Fix a typo... |
commit | commitdiff | tree |
| 2014-05-11 |
Andrew Reynolds | More preparation for CASC proofs. Minor fix for sort... |
commit | commitdiff | tree |
| 2014-05-10 |
Andrew Reynolds | Bug fixes to CBQI. Add first draft of CASC j7 TFF... |
commit | commitdiff | tree |
| 2014-05-10 |
Morgan Deters | Fix for example installation. |
commit | commitdiff | tree |
| 2014-05-09 |
Andrew Reynolds | Initial draft of run scripts for CASC j7 |
commit | commitdiff | tree |
| 2014-05-09 |
Andrew Reynolds | Add variable ordering to ambqi. Bug fix to macros... |
commit | commitdiff | tree |
| 2014-05-08 |
ajreynol | Major simplifications to macros module. |
commit | commitdiff | tree |
| 2014-05-08 |
Andrew Reynolds | Fixes to quantifiers rewriter to prevent miniscoping... |
commit | commitdiff | tree |
| 2014-05-08 |
Andrew Reynolds | Basic optimizations for ambqi : only normalize UF appli... |
commit | commitdiff | tree |
| 2014-05-08 |
Dejan Jovanovic | Adding encoding of sha1 collision for the hashing example |
commit | commitdiff | tree |
| 2014-05-08 |
Tianyi Liang | patch to the last commit: add a single character case |
commit | commitdiff | tree |
| 2014-05-07 |
Tianyi Liang | fix a bug in contain |
commit | commitdiff | tree |
| 2014-05-07 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-05-07 |
Tianyi Liang | add splits |
commit | commitdiff | tree |
| 2014-05-07 |
Tianyi Liang | add splits |
commit | commitdiff | tree |
| 2014-05-07 |
Andrew Reynolds | Fixes to ambqi, now solution-sound. |
commit | commitdiff | tree |
| 2014-05-06 |
Andrew Reynolds | First draft of ambqi_builder (new implementation of... |
commit | commitdiff | tree |
| 2014-05-06 |
Tianyi Liang | fix a bug in replace and contains |
commit | commitdiff | tree |
| 2014-05-05 |
Tianyi Liang | add constant regular expression check for intersection. |
commit | commitdiff | tree |
| 2014-05-05 |
Tim King | Improving documentation for glpk-cut-log switch. |
commit | commitdiff | tree |
| 2014-05-05 |
Morgan Deters | Valuation::entailmentCheck() proxy for TheoryEngine... |
commit | commitdiff | tree |
| 2014-05-02 |
Morgan Deters | Fix typo in bitvectors example; thanks to Adam Gashlin... |
commit | commitdiff | tree |
| 2014-05-02 |
Andrew Reynolds | Simplification of EqualityEngine::areDisequal. Compari... |
commit | commitdiff | tree |
| 2014-05-02 |
ajreynol | Fix assertion from previous commit. |
commit | commitdiff | tree |
| 2014-05-02 |
Andrew Reynolds | Add option --dt-stc-ind for strengthening skolemization... |
commit | commitdiff | tree |
| 2014-05-02 |
ajreynol | More minor optimizations for datatypes. |
commit | commitdiff | tree |
| 2014-05-01 |
ajreynol | Minor optimizations to datatypes, revert to checkClash... |
commit | commitdiff | tree |
| 2014-05-01 |
Kshitij Bansal | Merge remote-tracking branch 'upstream/master' into... |
commit | commitdiff | tree |
| 2014-05-01 |
Kshitij Bansal | decision engine: cache start index for and/or nodes |
commit | commitdiff | tree |
| 2014-04-30 |
Tim King | T-entailment work, and QCF (quant conflict find) work... |
commit | commitdiff | tree |
| 2014-04-30 |
Morgan Deters | Fix warnings, cleanup in strings typechecker. |
commit | commitdiff | tree |
| 2014-04-30 |
Morgan Deters | Fix compiler warning re: TheoryUF destructor. |
commit | commitdiff | tree |
| 2014-04-30 |
Morgan Deters | Fix simplify output for SMT2 printer. |
commit | commitdiff | tree |
| 2014-04-30 |
Morgan Deters | Fix for (user) context-dependence of arith TO_INT/IS_IN... |
commit | commitdiff | tree |
| 2014-04-30 |
Morgan Deters | Mostly resolves bug #561 memory leaks, and more. |
commit | commitdiff | tree |
| 2014-04-29 |
Morgan Deters | Fix for --force-logic to extend its reach to the parser. |
commit | commitdiff | tree |
| 2014-04-29 |
Kshitij Bansal | fixed couple of more warnings |
commit | commitdiff | tree |
| 2014-04-29 |
Kshitij Bansal | fix was compiler warning in antlr_input, crashing test... |
commit | commitdiff | tree |
| 2014-04-29 |
Morgan Deters | Revert a compiler warning fix from ea6a5a6. |
commit | commitdiff | tree |
| 2014-04-29 |
Tianyi Liang | fix a typo: --string-exp => --strings-exp; fix a signed... |
commit | commitdiff | tree |
| 2014-04-29 |
Tianyi Liang | add leading zeros support for str.to.int |
commit | commitdiff | tree |
| 2014-04-29 |
ajreynol | Significantly improve performance for producing datatyp... |
commit | commitdiff | tree |
| 2014-04-28 |
Kshitij Bansal | Merge remote-tracking branch 'upstream/master' into... |
commit | commitdiff | tree |
| 2014-04-28 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-04-28 |
Tianyi Liang | add strings-opt2 for regular splitting |
commit | commitdiff | tree |
| 2014-04-28 |
Kshitij Bansal | cleanup |
commit | commitdiff | tree |
| 2014-04-28 |
Tianyi Liang | minor change with kshitij's change |
commit | commitdiff | tree |
| 2014-04-28 |
Kshitij Bansal | nodemanager robust skolem numbering |
commit | commitdiff | tree |
| 2014-04-28 |
Tianyi Liang | add strings-opt2 for regular splitting |
commit | commitdiff | tree |
| 2014-04-28 |
Kshitij Bansal | Merge pull request #25 from kbansal/sets |
commit | commitdiff | tree |
| 2014-04-28 |
Andrew Reynolds | Preparation for models for co-inductive datatypes.... |
commit | commitdiff | tree |
| 2014-04-28 |
ajreynol | Optimizations for datatypes: check for clashes modulo... |
commit | commitdiff | tree |
| 2014-04-28 |
Kshitij Bansal | minor fix |
commit | commitdiff | tree |
| 2014-04-28 |
Kshitij Bansal | Merge remote-tracking branch 'upstream/master' into... |
commit | commitdiff | tree |
| 2014-04-28 |
Kshitij Bansal | travis, please! |
commit | commitdiff | tree |
| 2014-04-27 |
Kshitij Bansal | attempt to improve CVC4's "parse error" message |
commit | commitdiff | tree |
| 2014-04-27 |
Kshitij Bansal | rm undocument/non-working* "feature" |
commit | commitdiff | tree |
| 2014-04-24 |
Tianyi Liang | minor change: add a heuristic for preventing constant... |
commit | commitdiff | tree |
| 2014-04-24 |
Kshitij Bansal | optimization |
commit | commitdiff | tree |
| 2014-04-24 |
ajreynol | Avoid assigning constructor terms to 1-constructor... |
commit | commitdiff | tree |
| 2014-04-24 |
Andrew Reynolds | Compute care graph for datatypes. Preliminary results... |
commit | commitdiff | tree |
| 2014-04-24 |
Andrew Reynolds | Add --inst-max-level=N option for Kshitij. Support... |
commit | commitdiff | tree |
| 2014-04-22 |
Andrew Reynolds | Minor fix to avoid rewriting datatype equalities into... |
commit | commitdiff | tree |
| 2014-04-19 |
Kshitij Bansal | Eh, what? |
commit | commitdiff | tree |
| 2014-04-19 |
Kshitij Bansal | fix warnings in strings/ |
commit | commitdiff | tree |
| 2014-04-17 |
Morgan Deters | Allow fmf-bound-int to be set with set-option and via... |
commit | commitdiff | tree |
| 2014-04-17 |
Kshitij Bansal | simplify mkSkolem naming system: don't use $$ |
commit | commitdiff | tree |
| 2014-04-17 |
Kshitij Bansal | use internal skolem numbering |
commit | commitdiff | tree |
| 2014-04-17 |
Andrew Reynolds | Minor refactoring and optimizing. |
commit | commitdiff | tree |
| 2014-04-14 |
Andrew Reynolds | Fix bug in mbqi=fmc handling theory symbols. Fix mbqi... |
commit | commitdiff | tree |
| 2014-04-14 |
Andrew Reynolds | Add initial support for co-datatypes. |
commit | commitdiff | tree |
| 2014-04-11 |
Morgan Deters | Better support for building with mingw64; thanks to... |
commit | commitdiff | tree |
| 2014-04-11 |
Morgan Deters | setType -> setOfType, resolves bug 556 |
commit | commitdiff | tree |
| 2014-04-10 |
Morgan Deters | Fix the build; --check-proof works for UF but not for... |
commit | commitdiff | tree |
| 2014-04-10 |
Andrew Reynolds | Expand definitions in theory datatypes, now has the... |
commit | commitdiff | tree |
| 2014-04-10 |
Morgan Deters | Boolean terms conversion fix for datatypes, fixes a... |
commit | commitdiff | tree |
| 2014-04-10 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
commit | commitdiff | tree |
| 2014-04-10 |
Tianyi Liang | minor fix for strings |
commit | commitdiff | tree |
| 2014-04-10 |
Tianyi Liang | minor fix for strings |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog