Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-01-26 | More optimization of QCF. Fixed InstMatchTrie for caching instantiations. ↵ | Andrew Reynolds | |
Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers. | |||
2014-01-25 | replace charat uf with internal one | Tianyi Liang | |
2014-01-24 | minor fix, indexof rewriter opt | Tianyi Liang | |
2014-01-24 | fix: indexof, replace rewriting | Tianyi Liang | |
2014-01-24 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-01-24 | rev diseq | Tianyi Liang | |
2014-01-24 | rev const split | Tianyi Liang | |
2014-01-24 | optimize for the reverse direction | Tianyi Liang | |
2014-01-24 | rev diseq | Tianyi Liang | |
2014-01-24 | rev const split | Tianyi Liang | |
2014-01-24 | Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry ↵ | Andrew Reynolds | |
approach. Minor change to quantifier macros. Add option --quant-cf-mode. | |||
2014-01-24 | optimize for the reverse direction | Tianyi Liang | |
2014-01-23 | fix: constants are inferred to be the same | Tianyi Liang | |
2014-01-23 | minor fix | Tianyi Liang | |
2014-01-22 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Tianyi Liang | |
2014-01-22 | Some minor fixes to SmtEngine strings settings. | Morgan Deters | |
2014-01-22 | commented out all_supported in strings for now, it has a bug here. | Tianyi Liang | |
2014-01-22 | solve string exp issue for regexp | Tianyi Liang | |
2014-01-22 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
Conflicts: src/smt/smt_engine.cpp | |||
2014-01-22 | add warning for using strings in ALL_SUPPORTED | Tianyi Liang | |
2014-01-22 | Smarter options, but still have a bug | Tianyi Liang | |
2014-01-22 | Delay QuantifiersEngine and UF strong solver initialization until after ↵ | Morgan Deters | |
final options/logic are set. | |||
2014-01-21 | Smarter options, but still have a bug | Tianyi Liang | |
2014-01-20 | improve string contains | Tianyi Liang | |
2014-01-20 | improve string contains | Tianyi Liang | |
2014-01-18 | Fixed non-termination issue in bounded integers. | Andrew Reynolds | |
2014-01-18 | Performance optimization for E-matching, working on using QCF module for ↵ | Andrew Reynolds | |
propagations. | |||
2014-01-18 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-01-18 | strings with new ideas | Tianyi Liang | |
2014-01-17 | Merge branch '1.3.x' | Morgan Deters | |
2014-01-17 | Fix for quote-escaping in smt2 printer | Morgan Deters | |
2014-01-17 | strings with new ideas | Tianyi Liang | |
2014-01-17 | More optimizations for quantifiers conflict find. Add trust user patterns mode. | Andrew Reynolds | |
2014-01-17 | Merge branch '1.3.x' | Kshitij Bansal | |
2014-01-17 | enable search for html doc | Kshitij Bansal | |
2014-01-16 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
Conflicts: src/printer/smt2/smt2_printer.cpp | |||
2014-01-16 | adds partial functions | Tianyi Liang | |
2014-01-15 | adds smt2 print for strings | Tianyi Liang | |
2014-01-15 | adds smt2 print for strings | Tianyi Liang | |
2014-01-15 | Optimizations for quantifiers conflict find: better caching, process ↵ | Andrew Reynolds | |
matching constraints eagerly. | |||
2014-01-10 | normal form breaking | Tianyi Liang | |
2014-01-10 | add repalce | Tianyi Liang | |
2014-01-10 | Add stats to quantifiers conflict find. Added option for qcf. Working on ↵ | Andrew Reynolds | |
handling non-APPLY_UF terms. | |||
2014-01-10 | Add new method --quant-cf for finding conflicts eagerly for quantified ↵ | Andrew Reynolds | |
formulas. This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation. Clean up the rewriter, other minor cleanup. | |||
2014-01-09 | move new functions under exp options | Tianyi Liang | |
2014-01-09 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-01-09 | add constant replace, indexof | Tianyi Liang | |
2014-01-09 | add constant replace, indexof | Tianyi Liang | |
2014-01-09 | Merge branch '1.3.x' | Morgan Deters | |
2014-01-09 | gmp is again default, not cln, for build ID (reverting due to license ↵ | Morgan Deters | |
discussion at Monday meeting) |