| 2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Corrected fix for missing case in model postprocessor... |
tree | commitdiff |
| 2014-11-07 |
ajreynol | Enable --quant-cf by default. Fix bug in qcf for mixed... |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Revert "Fix missing case in model postprocessor (resolv... |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Revert "Fix missing case in model postprocessor (resolv... |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-07 |
Morgan Deters | Fix missing case in model postprocessor (resolves bug... |
tree | commitdiff |
| 2014-11-07 |
ajreynol | Properly distinguish which EQC to assign values in... |
tree | commitdiff |
| 2014-11-06 |
ajreynol | Minor fix for getInstCons |
tree | commitdiff |
| 2014-11-06 |
ajreynol | Reenable regression. Add (for now, disabled) changes... |
tree | commitdiff |
| 2014-11-05 |
ajreynol | Fix model bug in --mbqi=fmc. Minor cleanup in datatypes. |
tree | commitdiff |
| 2014-11-05 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-11-05 |
ajreynol | More work on datatypes theory combination: fix bug... |
tree | commitdiff |
| 2014-11-02 |
Clark Barrett | Added cache to getModelValue |
tree | commitdiff |
| 2014-11-01 |
ajreynol | Fix cegqi for synthesis without syntax. |
tree | commitdiff |
| 2014-11-01 |
ajreynol | Simplify which lemmas to communicate in dt. |
tree | commitdiff |
| 2014-11-01 |
ajreynol | Fix bug 592: introduce skolem for dt instantiate lemma... |
tree | commitdiff |
| 2014-11-01 |
ajreynol | Fix some mistakes in datatypes theory combination,... |
tree | commitdiff |
| 2014-10-31 |
ajreynol | Do not allow duplication of function definitions. ... |
tree | commitdiff |
| 2014-10-30 |
Clark Barrett | Be more lazy about generating array lemmas |
tree | commitdiff |
| 2014-10-30 |
Clark Barrett | Added new, much faster, care graph computation for... |
tree | commitdiff |
| 2014-10-28 |
ajreynol | Preprocessing step for finding finite runs of well... |
tree | commitdiff |
| 2014-10-28 |
ajreynol | Initial infrastructure for function definition quantifi... |
tree | commitdiff |
| 2014-10-28 |
ajreynol | Improve stats in conjecture generator, minor cleanup. |
tree | commitdiff |
| 2014-10-25 |
ajreynol | Minor fix for --user-pat=resort |
tree | commitdiff |
| 2014-10-24 |
Morgan Deters | Fix typo. |
tree | commitdiff |
| 2014-10-24 |
Morgan Deters | Minor parser performance fix. |
tree | commitdiff |
| 2014-10-24 |
ajreynol | Add --user-pat=resort. Minor cleanup of options. |
tree | commitdiff |
| 2014-10-23 |
Morgan Deters | Parsing and infrastructure support for SMT-LIBv2.5... |
tree | commitdiff |
| 2014-10-23 |
lianah | Fixed inefficiency in bit-vector rewrite rule. |
tree | commitdiff |
| 2014-10-22 |
Tianyi Liang | Fixed bug 589 |
tree | commitdiff |
| 2014-10-21 |
Clark Barrett | Fixed bug 590, added regression test |
tree | commitdiff |
| 2014-10-20 |
ajreynol | Minor cleanup in datatypes. |
tree | commitdiff |
| 2014-10-20 |
Kshitij Bansal | Merge pull request #59 from kbansal/sets3 |
tree | commitdiff |
| 2014-10-20 |
Kshitij Bansal | Finish sets type enumerator implementation. |
tree | commitdiff |
| 2014-10-20 |
Kshitij Bansal | fix statistic in decision engine |
tree | commitdiff |
| 2014-10-18 |
ajreynol | Fix assertion. |
tree | commitdiff |
| 2014-10-18 |
ajreynol | Add dt lemma: zero size implies nullary constructor. |
tree | commitdiff |
| 2014-10-18 |
ajreynol | Fix for bounded integers when incremental, fixes bug... |
tree | commitdiff |
| 2014-10-17 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-17 |
Tianyi Liang | Minor change for performance according to Andy's sugges... |
tree | commitdiff |
| 2014-10-16 |
Morgan Deters | Fix clang warnings |
tree | commitdiff |
| 2014-10-16 |
ajreynol | Make --user-pat=trust default. Fix a few warnings... |
tree | commitdiff |
| 2014-10-16 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-16 |
ajreynol | Use n-ary splits instead of binary splits in theory... |
tree | commitdiff |
| 2014-10-16 |
ajreynol | Add dt.size to datatypes theory. Add option for fairne... |
tree | commitdiff |
| 2014-10-14 |
lianah | fix for memory leak in BVQuickCheck |
tree | commitdiff |
| 2014-10-14 |
Morgan Deters | Merge pull request #58 from mdeters/smt-attributes |
tree | commitdiff |
| 2014-10-14 |
Morgan Deters | Context-dependent expr attributes are now attached... |
tree | commitdiff |
| 2014-10-14 |
Kshitij Bansal | amend prvs commit |
tree | commitdiff |
| 2014-10-14 |
Kshitij Bansal | trace decision-node |
tree | commitdiff |
| 2014-10-13 |
ajreynol | CEGQI uses model. Enforce fairness in CEGQI natively. |
tree | commitdiff |
| 2014-10-13 |
ajreynol | Model building into quantifiers engine. Simplify axiom... |
tree | commitdiff |
| 2014-10-13 |
ajreynol | Refactor model builder from model engine to quant engin... |
tree | commitdiff |
| 2014-10-11 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-11 |
Morgan Deters | Some defensive programming at destruction time, and... |
tree | commitdiff |
| 2014-10-10 |
Kshitij Bansal | Merge remote-tracking branch 'origin/1.4.x' |
tree | commitdiff |
| 2014-10-10 |
ajreynol | Initial draft of CEGQI. |
tree | commitdiff |
| 2014-10-10 |
Kshitij Bansal | Fix issue with shared but non-preregistered term setup... |
tree | commitdiff |
| 2014-10-10 |
Morgan Deters | Cleanup |
tree | commitdiff |
| 2014-10-10 |
ajreynol | Add owner map to better manage QuantifiersModules.... |
tree | commitdiff |
| 2014-10-09 |
ajreynol | Refactor quantifier prenex option. By default, do... |
tree | commitdiff |
| 2014-10-09 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-09 |
Morgan Deters | Add unsat cores support to CVC native language. |
tree | commitdiff |
| 2014-10-08 |
Morgan Deters | Some minor cleanup. |
tree | commitdiff |
| 2014-10-08 |
Morgan Deters | Remove private header from public driver. |
tree | commitdiff |
| 2014-10-08 |
Kshitij Bansal | Fix portoflio issues (debugging code was being called... |
tree | commitdiff |
| 2014-10-07 |
Kshitij Bansal | Merge remote-tracking branch 'upstream/master' into... |
tree | commitdiff |
| 2014-10-07 |
Kshitij Bansal | update default Sets options |
tree | commitdiff |
| 2014-10-07 |
Kshitij Bansal | whitespace fixes |
tree | commitdiff |
| 2014-10-07 |
ajreynol | Cache for getInstance, thanks to Johannes Kanig for... |
tree | commitdiff |
| 2014-10-07 |
Kshitij Bansal | add couple of stats |
tree | commitdiff |
| 2014-10-07 |
Kshitij Bansal | sets stronger equality propagator |
tree | commitdiff |
| 2014-10-07 |
ajreynol | Refactor quantifiers attributes. |
tree | commitdiff |
| 2014-10-07 |
Morgan Deters | define-const is an extended command, not permitted... |
tree | commitdiff |
| 2014-10-07 |
Morgan Deters | Fix a resource limiting issue where interruption didn... |
tree | commitdiff |
| 2014-10-07 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-07 |
Morgan Deters | Fix a bug in tuple-record handling. Thanks to Saumya... |
tree | commitdiff |
| 2014-10-07 |
Morgan Deters | Some minor cleanup. |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-06 |
Kshitij Bansal | fix for bug586 |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Print array constants in SMT-LIB models with new syntax. |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Clear out decls/defs with RESET command. |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Fix native language parsing of chained-store expression... |
tree | commitdiff |
| 2014-10-06 |
Morgan Deters | Support for RESET command in CVC native language (and... |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Support exporting array-store-all expressions to other... |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Fix output of integer-valued real constants in SMT... |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Improve error in CVC parser in presence of unrecognized... |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | More array constants and parsing: better error messages... |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Minor fixes to CVC printer. |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | SMT-LIB parser support for array constants (Z3 syntax). |
tree | commitdiff |
| 2014-10-03 |
Morgan Deters | Merge branch '1.4.x' |
tree | commitdiff |
| 2014-10-02 |
Clark Barrett | Added internal support for constant arrays. |
tree | commitdiff |
| 2014-10-02 |
Morgan Deters | Merge branch '1.4.x'. |
tree | commitdiff |
| 2014-10-02 |
Clark Barrett | Added option for developer use only |
tree | commitdiff |
| 2014-10-02 |
Clark Barrett | More model-based combination for arrays |
tree | commitdiff |
| 2014-10-02 |
Clark Barrett | Better getEqualityStatus for arrays, smarter combinatio... |
tree | commitdiff |
| 2014-10-02 |
Morgan Deters | Fix comment in SmtEngine. |
tree | commitdiff |
| next |
projects / cvc5.git / history