| 2014-04-01 |
Tim King | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-03-26 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-03-21 |
Kshitij Bansal | Merge pull request #22 from kbansal/sets-model |
tree | commitdiff |
| 2014-03-20 |
Andrew Reynolds | Minor fix for CBQI, ignore inst constant nodes. |
tree | commitdiff |
| 2014-03-12 |
Andrew Reynolds | Work on array pf signature, add working example. Add... |
tree | commitdiff |
| 2014-03-12 |
Andrew Reynolds | Minor fixes post-merge of RR. |
tree | commitdiff |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-03-11 |
Morgan Deters | Fix for rewriterules build breakage. |
tree | commitdiff |
| 2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-03-11 |
Andrew Reynolds | Initial refactor of rewrite rules, make theory_rewriter... |
tree | commitdiff |
| 2014-03-10 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-03-08 |
Tim King | Merge remote-tracking branch 'CVC4root/master' |
tree | commitdiff |
| 2014-03-08 |
Morgan Deters | Remove --ite-remove-quant; support pulling ground ITEs... |
tree | commitdiff |
| 2014-03-07 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-03-04 |
Morgan Deters | Don't theory-preprocess under quantifiers; but DO theor... |
tree | commitdiff |
| 2014-03-01 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-02-27 |
Andrew Reynolds | Bug fix for QCF algorithm, was missing instantiations... |
tree | commitdiff |
| 2014-02-26 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-02-25 |
Andrew Reynolds | Add options --full-saturate-quant and --mbqi=trust... |
tree | commitdiff |
| 2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-02-21 |
Kshitij Bansal | Merge pull request #10 from kbansal/sets-for-merge |
tree | commitdiff |
| 2014-02-21 |
Kshitij Bansal | fix a -Wunused |
tree | commitdiff |
| 2014-02-20 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-02-20 |
Andrew Reynolds | Fix ite and iff handling in QCF. Add option for heuris... |
tree | commitdiff |
| 2014-02-19 |
Tim King | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-02-17 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-02-14 |
Andrew Reynolds | Make QCF more incremental. Fix bug in QCF handling... |
tree | commitdiff |
| 2014-02-11 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-02-09 |
Andrew Reynolds | More complete guess instantiation strategy, cvc4 now... |
tree | commitdiff |
| 2014-02-05 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-02-05 |
Andrew Reynolds | Bug fix for theory strings related to old cycle detecti... |
tree | commitdiff |
| 2014-02-04 |
Andrew Reynolds | Add variable ordering for QCF to accelerate matching... |
tree | commitdiff |
| 2014-02-03 |
Andrew Reynolds | Handle nested (universal) quantifiers in QCF algorithm... |
tree | commitdiff |
| 2014-01-30 |
Andrew Reynolds | Refactor QCF slightly. Bug fix for relevant domain... |
tree | commitdiff |
| 2014-01-28 |
Andrew Reynolds | More optimizations of quantifier instantiation data... |
tree | commitdiff |
| 2014-01-27 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-01-27 |
Andrew Reynolds | More optimization of QCF and instantiation caching... |
tree | commitdiff |
| 2014-01-26 |
Andrew Reynolds | More optimization of QCF. Fixed InstMatchTrie for... |
tree | commitdiff |
| 2014-01-24 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-01-24 |
Andrew Reynolds | Simplify the QCF algorithm by more aggressive flattenin... |
tree | commitdiff |
| 2014-01-22 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-01-22 |
Tianyi Liang | Smarter options, but still have a bug |
tree | commitdiff |
| 2014-01-22 |
Morgan Deters | Delay QuantifiersEngine and UF strong solver initializa... |
tree | commitdiff |
| 2014-01-21 |
Tianyi Liang | Smarter options, but still have a bug |
tree | commitdiff |
| 2014-01-18 |
Andrew Reynolds | Fixed non-termination issue in bounded integers. |
tree | commitdiff |
| 2014-01-18 |
Andrew Reynolds | Performance optimization for E-matching, working on... |
tree | commitdiff |
| 2014-01-18 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-01-18 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-01-17 |
Andrew Reynolds | More optimizations for quantifiers conflict find. ... |
tree | commitdiff |
| 2014-01-17 |
Kshitij Bansal | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-01-16 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2014-01-15 |
Andrew Reynolds | Optimizations for quantifiers conflict find: better... |
tree | commitdiff |
| 2014-01-10 |
Andrew Reynolds | Add stats to quantifiers conflict find. Added option... |
tree | commitdiff |
| 2014-01-10 |
Andrew Reynolds | Add new method --quant-cf for finding conflicts eagerly... |
tree | commitdiff |
| 2014-01-09 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-01-08 |
Morgan Deters | Merge branch '1.3.x' |
tree | commitdiff |
| 2014-01-04 |
Andrew Reynolds | Removing and consolidating options for uf-ss and quanti... |
tree | commitdiff |
| 2014-01-03 |
Andrew Reynolds | Added support for proof production in Equality Engine... |
tree | commitdiff |
| 2013-12-05 |
Morgan Deters | Update copyrights, add missing file-level documentation... |
tree | commitdiff |
| 2013-12-03 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2013-11-27 |
Morgan Deters | General pre-release cleanup commit |
tree | commitdiff |
| 2013-11-27 |
Andrew Reynolds | Bug fix for E-matching select terms, minor fix for... |
tree | commitdiff |
| 2013-11-11 |
Morgan Deters | Flatten libcvc4 build structure; remove some #include... |
tree | commitdiff |
| 2013-11-07 |
Morgan Deters | Flatten libcvc4 build structure; remove some #include... |
tree | commitdiff |
| 2013-11-06 |
Andrew Reynolds | Bug fixes for bounded integer quantification. Current... |
tree | commitdiff |
| 2013-11-06 |
Andrew Reynolds | Bug fixes for bounded integer quantification. Current... |
tree | commitdiff |
| 2013-10-07 |
Liana Hadarean | merged golden |
tree | commitdiff |
| 2013-10-07 |
Andrew Reynolds | Multiple fixes for datatypes theory solver: add support... |
tree | commitdiff |
| 2013-09-30 |
Liana Hadarean | merged golden |
tree | commitdiff |
| 2013-09-30 |
Andrew Reynolds | Bug fixes and improvements for symmetry breaking, it... |
tree | commitdiff |
| 2013-09-27 |
Morgan Deters | Merge branch 'master' of github.com:tiliang/CVC4 |
tree | commitdiff |
| 2013-09-27 |
Andrew Reynolds | Add new symmetry breaking technique for finite model... |
tree | commitdiff |
| 2013-09-15 |
Andrew Reynolds | Change default option of simple ite lifting within... |
tree | commitdiff |
| 2013-09-13 |
Morgan Deters | Documentation fixes, some code typo fixes, file perms... |
tree | commitdiff |
| 2013-08-26 |
Kshitij Bansal | Merge branch '1.2.x' |
tree | commitdiff |
| 2013-08-13 |
Morgan Deters | Minor cleanup. |
tree | commitdiff |
| 2013-08-13 |
Andrew Reynolds | Minor fixes for --fmf-fmc for quantifiers containing... |
tree | commitdiff |
| 2013-08-13 |
Andrew Reynolds | initial modifications for per-ic cbqi |
tree | commitdiff |
| 2013-07-29 |
Morgan Deters | Fix numerous compiler warnings on various platforms |
tree | commitdiff |
| 2013-07-22 |
Andrew Reynolds | Add option --cbqi-recurse. |
tree | commitdiff |
| 2013-07-22 |
Andrew Reynolds | Bug fix for --fmf-fmc for non-uninterpreted sort quanti... |
tree | commitdiff |
| 2013-07-18 |
Andrew Reynolds | Fix quantifier instantiation bug in cbqi, add default... |
tree | commitdiff |
| 2013-07-09 |
Andrew Reynolds | add relevant domain computation |
tree | commitdiff |
| 2013-07-02 |
Andrew Reynolds | Minor fixes for bounded integers, rewrite engine. |
tree | commitdiff |
| 2013-06-28 |
Andrew Reynolds | More bug fixes for interval models. |
tree | commitdiff |
| 2013-06-26 |
Andrew Reynolds | Add support for interval models in bounded integers... |
tree | commitdiff |
| 2013-06-25 |
Morgan Deters | Merge branch '1.2.x' |
tree | commitdiff |
| 2013-06-25 |
Andrew Reynolds | Refactoring of model engine to separate individual... |
tree | commitdiff |
| 2013-06-24 |
Andrew Reynolds | Add options for symmetry breaking in uf+ss totality... |
tree | commitdiff |
| 2013-06-19 |
Morgan Deters | Merge branch '1.2.x' |
tree | commitdiff |
| 2013-06-17 |
Andrew Reynolds | Make --var-elim-quant true by default. Add rewrite... |
tree | commitdiff |
| 2013-06-05 |
Andrew Reynolds | Fix bug in --fmf-fmc for producing models of functions... |
tree | commitdiff |
| 2013-06-04 |
Morgan Deters | Merge branch '1.2.x' |
tree | commitdiff |
| 2013-06-04 |
Andrew Reynolds | Add partial support for MBQI with arrays when using... |
tree | commitdiff |
| 2013-06-03 |
Morgan Deters | Merge tag 'casc24' |
tree | commitdiff |
| 2013-05-29 |
Morgan Deters | Merge branch '1.2.x' |
tree | commitdiff |
| 2013-05-23 |
Andrew Reynolds | Refactoring to prepare for MBQI with integer quantifica... |
tree | commitdiff |
| 2013-05-22 |
Andrew Reynolds | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2013-05-22 |
Andrew Reynolds | Significant work on bounded integer quantification... |
tree | commitdiff |
| next |
projects / cvc5.git / history