2014-08-18 |
ajreynol | Add support for quantifier-specific instantiation level... |
blob | commitdiff | raw |
2014-08-01 |
ajreynol | Minor cleanup from previous commit. Better organizatio... |
blob | commitdiff | raw | diff to current |
2014-07-31 |
ajreynol | New module for generating candidate equality conjecture... |
blob | commitdiff | raw | diff to current |
2014-07-10 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' into segfa... |
blob | commitdiff | raw | diff to current |
2014-07-01 |
Morgan Deters | Update copyrights. |
blob | commitdiff | raw | diff to current |
2014-06-26 |
Morgan Deters | Merge tag 'smtcomp2014-resubmission' |
blob | commitdiff | raw | diff to current |
2014-06-22 |
Morgan Deters | Merge tag 'smtcomp2014-application' |
blob | commitdiff | raw | diff to current |
2014-06-19 |
ajreynol | More proof support for CASC : include skolemization |
blob | commitdiff | raw | diff to current |
2014-06-16 |
ajreynol | More proof support for CASC : include skolemization |
blob | commitdiff | raw | diff to current |
2014-05-30 |
ajreynol | Fixes for --inst-max-level |
blob | commitdiff | raw | diff to current |
2014-05-12 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
2014-05-11 |
Andrew Reynolds | More preparation for CASC proofs. Minor fix for sort... |
blob | commitdiff | raw | diff to current |
2014-05-08 |
Andrew Reynolds | Fixes to quantifiers rewriter to prevent miniscoping... |
blob | commitdiff | raw | diff to current |
2014-04-28 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
2014-04-28 |
Kshitij Bansal | Merge pull request #25 from kbansal/sets |
blob | commitdiff | raw | diff to current |
2014-04-28 |
Andrew Reynolds | Preparation for models for co-inductive datatypes.... |
blob | commitdiff | raw | diff to current |
2014-04-28 |
ajreynol | Optimizations for datatypes: check for clashes modulo... |
blob | commitdiff | raw | diff to current |
2014-04-01 |
Tim King | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
2014-03-26 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
2014-03-21 |
Kshitij Bansal | Merge pull request #22 from kbansal/sets-model |
blob | commitdiff | raw | diff to current |
2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
2014-03-11 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
2014-03-11 |
Andrew Reynolds | Initial refactor of rewrite rules, make theory_rewriter... |
blob | commitdiff | raw | diff to current |
2014-02-26 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
2014-02-25 |
Andrew Reynolds | Add options --full-saturate-quant and --mbqi=trust... |
blob | commitdiff | raw | diff to current |
2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
2014-02-21 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
2014-02-19 |
Tim King | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
2014-01-27 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
2014-01-27 |
Andrew Reynolds | More optimization of QCF and instantiation caching... |
blob | commitdiff | raw | diff to current |
2014-01-26 |
Andrew Reynolds | More optimization of QCF. Fixed InstMatchTrie for... |
blob | commitdiff | raw | diff to current |
2014-01-18 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
2014-01-17 |
Kshitij Bansal | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
2014-01-10 |
Andrew Reynolds | Add new method --quant-cf for finding conflicts eagerly... |
blob | commitdiff | raw | diff to current |
2013-11-04 |
lianah | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
2013-10-15 |
Andrew Reynolds | performance optimizations for quantifier instantiation |
blob | commitdiff | raw | diff to current |
2013-10-15 |
Andrew Reynolds | performance optimizations for quantifier instantiation |
blob | commitdiff | raw | diff to current |
2013-10-07 |
Liana Hadarean | merged golden |
blob | commitdiff | raw | diff to current |
2013-10-07 |
Andrew Reynolds | Multiple fixes for datatypes theory solver: add support... |
blob | commitdiff | raw | diff to current |
2013-09-30 |
Liana Hadarean | merged golden |
blob | commitdiff | raw | diff to current |
2013-08-26 |
Kshitij Bansal | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
2013-07-02 |
Andrew Reynolds | Minor fixes for bounded integers, rewrite engine. |
blob | commitdiff | raw | diff to current |
2013-06-25 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
2013-06-19 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
2013-06-17 |
Andrew Reynolds | Make --var-elim-quant true by default. Add rewrite... |
blob | commitdiff | raw | diff to current |
2013-06-04 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
2013-05-29 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
2013-05-21 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
2013-05-21 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
2013-05-20 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
2013-05-11 |
Andrew Reynolds | Preliminary version of finite model finding over bounde... |
blob | commitdiff | raw | diff to current |
2013-05-09 |
Kshitij Bansal | Merge branch 'master' of ssh://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
2013-05-09 |
Andrew Reynolds | Add new method for checking candidate models, --fmf... |
blob | commitdiff | raw | diff to current |
2013-04-02 |
Morgan Deters | Regenerated copyrights: canonicalized names, no emails |
blob | commitdiff | raw | diff to current |
2013-04-02 |
Morgan Deters | update copyrights |
blob | commitdiff | raw | diff to current |
2013-03-20 |
Liana Hadarean | merged master with dejan's constant evaluating equality... |
blob | commitdiff | raw | diff to current |
2013-03-15 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-03-14 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-03-13 |
lianah | post failed attempts at getting the incremental solver... |
blob | commitdiff | raw | diff to current |
2013-03-11 |
Andrew Reynolds | ite removal option for quantifiers --ite-remove-quant... |
blob | commitdiff | raw | diff to current |
2013-03-05 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-03-01 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-26 |
lianah | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-24 |
Andrew Reynolds | added option --model-u-dt-enum for outputting uninterpr... |
blob | commitdiff | raw | diff to current |
2013-02-17 |
Kshitij Bansal | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-16 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-15 |
Kshitij Bansal | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-15 |
Kshitij Bansal | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-15 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-15 |
Tim King | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-08 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-05 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-05 |
Kshitij Bansal | Merge remote-tracking branch 'origin/1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-05 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-04 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-04 |
Morgan Deters | Merge branch '1.0.x' |
blob | commitdiff | raw | diff to current |
2013-02-04 |
Andrew Reynolds | Model no longer adds subterms of quantifiers to equalit... |
blob | commitdiff | raw | diff to current |
2013-02-02 |
lianah | merged master into branch |
blob | commitdiff | raw | diff to current |
2013-01-28 |
Andrew Reynolds | made QuantifiersEngine::d_inst_match_trie and Quantifie... |
blob | commitdiff | raw | diff to current |
2013-01-28 |
Andrew Reynolds | made QuantifiersEngine::d_inst_match_trie and Quantifie... |
blob | commitdiff | raw | diff to current |
2012-12-01 |
Andrew Reynolds | drastic simplification of quantifiers code regarding... |
blob | commitdiff | raw | diff to current |
2012-11-30 |
Andrew Reynolds | quantifiers now uses master equality engine, preparatio... |
blob | commitdiff | raw | diff to current |
2012-11-14 |
Andrew Reynolds | replaced all static member data from rewrite rule trigg... |
blob | commitdiff | raw | diff to current |
2012-10-31 |
Andrew Reynolds | cleaning up some of the equality query stuff, implement... |
blob | commitdiff | raw | diff to current |
2012-10-24 |
Andrew Reynolds | efficient e-matching now specific to rewrite rules |
blob | commitdiff | raw | diff to current |
2012-10-23 |
Andrew Reynolds | more major cleanup of quantifiers code, separating... |
blob | commitdiff | raw | diff to current |
2012-10-23 |
Andrew Reynolds | more updates to inst gen: fixed partial instantiations... |
blob | commitdiff | raw | diff to current |
2012-10-16 |
Andrew Reynolds | more cleanup of quantifiers code |
blob | commitdiff | raw | diff to current |
2012-10-16 |
Andrew Reynolds | first draft of new inst gen method (still with bugs... |
blob | commitdiff | raw | diff to current |
2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
blob | commitdiff | raw | diff to current |
2012-09-25 |
Morgan Deters | some buggy examples for incrementality, and make bug326... |
blob | commitdiff | raw | diff to current |
2012-09-22 |
Morgan Deters | Separate public-facing and internal-facing interfaces... |
blob | commitdiff | raw | diff to current |
2012-08-31 |
Andrew Reynolds | merge from fmf-devel branch. more updates to models... |
blob | commitdiff | raw | diff to current |
2012-07-31 |
Morgan Deters | Moving some instantiation-related stuff from src/theory... |
blob | commitdiff | raw | diff to current |
2012-07-27 |
Andrew Reynolds | merging fmf-devel branch, includes refactored datatype... |
blob | commitdiff | raw | diff to current |
2012-07-27 |
François Bobot | Merge quantifiers2-trunk: |
blob | commitdiff | raw | diff to current |
2012-07-12 |
Andrew Reynolds | merged fmf-devel branch, includes support for SMT2... |
blob | commitdiff | raw | diff to current |
2012-06-11 |
Morgan Deters | Merge from quantifiers2-trunkmerge branch. |
blob | commitdiff | raw | diff to current |
|