summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-01-26More 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-25replace charat uf with internal oneTianyi Liang
2014-01-24minor fix, indexof rewriter optTianyi Liang
2014-01-24fix: indexof, replace rewritingTianyi Liang
2014-01-24Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-01-24rev diseqTianyi Liang
2014-01-24rev const splitTianyi Liang
2014-01-24optimize for the reverse directionTianyi Liang
2014-01-24rev diseqTianyi Liang
2014-01-24rev const splitTianyi Liang
2014-01-24Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry ↵Andrew Reynolds
approach. Minor change to quantifier macros. Add option --quant-cf-mode.
2014-01-24optimize for the reverse directionTianyi Liang
2014-01-23fix: constants are inferred to be the sameTianyi Liang
2014-01-23minor fixTianyi Liang
2014-01-22Merge branch 'master' of https://github.com/CVC4/CVC4Tianyi Liang
2014-01-22Some minor fixes to SmtEngine strings settings.Morgan Deters
2014-01-22commented out all_supported in strings for now, it has a bug here.Tianyi Liang
2014-01-22solve string exp issue for regexpTianyi Liang
2014-01-22Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
Conflicts: src/smt/smt_engine.cpp
2014-01-22add warning for using strings in ALL_SUPPORTEDTianyi Liang
2014-01-22Smarter options, but still have a bugTianyi Liang
2014-01-22Delay QuantifiersEngine and UF strong solver initialization until after ↵Morgan Deters
final options/logic are set.
2014-01-21Smarter options, but still have a bugTianyi Liang
2014-01-20improve string containsTianyi Liang
2014-01-20improve string containsTianyi Liang
2014-01-18Fixed non-termination issue in bounded integers.Andrew Reynolds
2014-01-18Performance optimization for E-matching, working on using QCF module for ↵Andrew Reynolds
propagations.
2014-01-18Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-01-18strings with new ideasTianyi Liang
2014-01-17Merge branch '1.3.x'Morgan Deters
2014-01-17Fix for quote-escaping in smt2 printerMorgan Deters
2014-01-17strings with new ideasTianyi Liang
2014-01-17More optimizations for quantifiers conflict find. Add trust user patterns mode.Andrew Reynolds
2014-01-17Merge branch '1.3.x'Kshitij Bansal
2014-01-17enable search for html docKshitij Bansal
2014-01-16Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
Conflicts: src/printer/smt2/smt2_printer.cpp
2014-01-16adds partial functionsTianyi Liang
2014-01-15adds smt2 print for stringsTianyi Liang
2014-01-15adds smt2 print for stringsTianyi Liang
2014-01-15Optimizations for quantifiers conflict find: better caching, process ↵Andrew Reynolds
matching constraints eagerly.
2014-01-10normal form breakingTianyi Liang
2014-01-10add repalceTianyi Liang
2014-01-10Add stats to quantifiers conflict find. Added option for qcf. Working on ↵Andrew Reynolds
handling non-APPLY_UF terms.
2014-01-10Add 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-09move new functions under exp optionsTianyi Liang
2014-01-09Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2014-01-09add constant replace, indexofTianyi Liang
2014-01-09add constant replace, indexofTianyi Liang
2014-01-09Merge branch '1.3.x'Morgan Deters
2014-01-09gmp is again default, not cln, for build ID (reverting due to license ↵Morgan Deters
discussion at Monday meeting)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback