Age | Commit message (Expand) | Author |
2014-11-05 | Fix model bug in --mbqi=fmc. Minor cleanup in datatypes. | ajreynol |
2014-11-05 | More work on datatypes theory combination: fix bug in care graph, do not assi... | ajreynol |
2014-11-01 | Added cache to getModelValue | Clark Barrett |
2014-11-01 | Fix cegqi for synthesis without syntax. | ajreynol |
2014-11-01 | Simplify which lemmas to communicate in dt. | ajreynol |
2014-11-01 | Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in lemma... | ajreynol |
2014-11-01 | Fix some mistakes in datatypes theory combination, disable two regressions. ... | ajreynol |
2014-10-31 | Do not allow duplication of function definitions. Set incomplete flag in mod... | ajreynol |
2014-10-30 | Be more lazy about generating array lemmas | Clark Barrett |
2014-10-29 | Added new, much faster, care graph computation for arrays | Clark Barrett |
2014-10-28 | Preprocessing step for finding finite runs of well-defined function definitio... | ajreynol |
2014-10-28 | Initial infrastructure for function definition quantifiers, internal parsing ... | ajreynol |
2014-10-28 | Improve stats in conjecture generator, minor cleanup. | ajreynol |
2014-10-25 | Minor fix for --user-pat=resort | ajreynol |
2014-10-24 | Fix typo. | Morgan Deters |
2014-10-24 | Minor parser performance fix. | Morgan Deters |
2014-10-24 | Add --user-pat=resort. Minor cleanup of options. | ajreynol |
2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters |
2014-10-23 | Fixed inefficiency in bit-vector rewrite rule. | lianah |
2014-10-21 | Fixed bug 589 | Tianyi Liang |
2014-10-21 | Fixed bug 590, added regression test | Clark Barrett |
2014-10-20 | Minor cleanup in datatypes. | ajreynol |
2014-10-19 | Finish sets type enumerator implementation. | Kshitij Bansal |
2014-10-19 | fix statistic in decision engine | Kshitij Bansal |
2014-10-18 | Fix assertion. | ajreynol |
2014-10-18 | Add dt lemma: zero size implies nullary constructor. | ajreynol |
2014-10-18 | Fix for bounded integers when incremental, fixes bug 588. Add option --dt-bi... | ajreynol |
2014-10-17 | Minor change for performance according to Andy's suggestion. | Tianyi Liang |
2014-10-16 | Fix clang warnings | Morgan Deters |
2014-10-16 | Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ch... | ajreynol |
2014-10-16 | Use n-ary splits instead of binary splits in theory datatypes. | ajreynol |
2014-10-16 | Add dt.size to datatypes theory. Add option for fairness strategy used by CE... | ajreynol |
2014-10-14 | fix for memory leak in BVQuickCheck | lianah |
2014-10-14 | Context-dependent expr attributes are now attached to a specific SmtEngine, a... | Morgan Deters |
2014-10-14 | amend prvs commit | Kshitij Bansal |
2014-10-14 | trace decision-node | Kshitij Bansal |
2014-10-13 | CEGQI uses model. Enforce fairness in CEGQI natively. | ajreynol |
2014-10-13 | Model building into quantifiers engine. Simplify axiom-inst mode. | ajreynol |
2014-10-13 | Refactor model builder from model engine to quant engine. Work on fairness s... | ajreynol |
2014-10-11 | Merge branch '1.4.x' | Morgan Deters |
2014-10-11 | Some defensive programming at destruction time, and fix a latent dangling poi... | Morgan Deters |
2014-10-10 | Merge remote-tracking branch 'origin/1.4.x' | Kshitij Bansal |
2014-10-10 | Initial draft of CEGQI. | ajreynol |
2014-10-10 | Fix issue with shared but non-preregistered term setup. Thanks Alvise Rabitti... | Kshitij Bansal |
2014-10-10 | Cleanup | Morgan Deters |
2014-10-10 | Add owner map to better manage QuantifiersModules. Initial infrastructure fo... | ajreynol |
2014-10-09 | Refactor quantifier prenex option. By default, do not pull quantifiers with ... | ajreynol |
2014-10-08 | Merge branch '1.4.x' | Morgan Deters |
2014-10-08 | Add unsat cores support to CVC native language. | Morgan Deters |
2014-10-08 | Some minor cleanup. | Morgan Deters |