| 2014-04-17 |
Kshitij Bansal | simplify mkSkolem naming system: don't use $$ |
blob | commitdiff | raw |
| 2014-04-09 |
Andrew Reynolds | Revert E-matching datatypes fix. |
blob | commitdiff | raw | diff to current |
| 2014-04-09 |
Andrew Reynolds | Handle fmf.card as input from user, add support in... |
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-12 |
Andrew Reynolds | Work on array pf signature, add working example. Add... |
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 | Fix for rewriterules build breakage. |
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-03-10 |
Tianyi Liang | Merge branch 'master' of github.com:tiliang/CVC4 |
blob | commitdiff | raw | diff to current |
| 2014-03-08 |
Tim King | Merge remote-tracking branch 'CVC4root/master' |
blob | commitdiff | raw | diff to current |
| 2014-03-08 |
Morgan Deters | Remove --ite-remove-quant; support pulling ground ITEs... |
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-28 |
Andrew Reynolds | More optimizations of quantifier instantiation data... |
blob | commitdiff | raw | diff to current |
| 2014-01-27 |
Morgan Deters | Merge branch '1.3.x' |
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-09 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-08 |
Morgan Deters | Merge branch '1.3.x' |
blob | commitdiff | raw | diff to current |
| 2014-01-03 |
Andrew Reynolds | Added support for proof production in Equality Engine... |
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-08-13 |
Andrew Reynolds | Minor fixes for --fmf-fmc for quantifiers containing... |
blob | commitdiff | raw | diff to current |
| 2013-07-18 |
Andrew Reynolds | Fix quantifier instantiation bug in cbqi, add default... |
blob | commitdiff | raw | diff to current |
| 2013-06-26 |
Andrew Reynolds | Add support for interval models in bounded integers... |
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-04 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
| 2013-06-03 |
Morgan Deters | Merge tag 'casc24' |
blob | commitdiff | raw | diff to current |
| 2013-05-29 |
Morgan Deters | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
| 2013-05-22 |
Andrew Reynolds | Merge branch 'master' of https://github.com/CVC4/CVC4 |
blob | commitdiff | raw | diff to current |
| 2013-05-22 |
Andrew Reynolds | Significant work on bounded integer quantification... |
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-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-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-06 |
Andrew Reynolds | fixed two bugs for the new E-matching implementation... |
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 |
| 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-11-13 |
Andrew Reynolds | refactoring of quantifiers rewriter based on code revie... |
blob | commitdiff | raw | diff to current |
| 2012-11-02 |
Andrew Reynolds | more minor updates to inst gen and representative selec... |
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-17 |
Andrew Reynolds | first working version of new inst-gen-style quantifier... |
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-10-10 |
Andrew Reynolds | cleanup up some static data members in the quantifiers... |
blob | commitdiff | raw | diff to current |
| 2012-09-19 |
Morgan Deters | General subscriber infrastructure for NodeManager,... |
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-08-27 |
Morgan Deters | * Reversing commit r4258 (which disabled failing regres... |
blob | commitdiff | raw | diff to current |
| 2012-08-24 |
Morgan Deters | * disallow internal uses of mkVar() (you have to mkSkol... |
blob | commitdiff | raw | diff to current |
| 2012-08-20 |
Morgan Deters | remove duplicate function TheoryEngine::getTheory(Theor... |
blob | commitdiff | raw | diff to current |
| 2012-07-31 |
Morgan Deters | Options merge. This commit: |
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 |
|
projects / cvc5.git / history