Age | Commit message (Expand) | Author |
2013-03-22 | Support for Boolean term conversion in datatypes. | Morgan Deters |
2013-03-21 | Some model and printing fixes for defined functions in input. | Morgan Deters |
2013-03-21 | Fix for SmtEngine::expandDefinitions()---improper TypeCheckingException | Morgan Deters |
2013-03-20 | Some statistics for narrowing down incrementality issues (push/pop vs solve t... | Morgan Deters |
2013-03-19 | Fixes for miplib-trick application (and a new testcase) | Morgan Deters |
2013-03-11 | ite removal option for quantifiers --ite-remove-quant, e-matching for boolean... | Andrew Reynolds |
2013-03-05 | Merge branch '1.0.x' | Morgan Deters |
2013-03-05 | Bugfix for SmtEngine: proper unsubscribing for NodeManager events | Morgan Deters |
2013-02-20 | Some exception specification fixes in SmtEngine/Command infrastructure | Morgan Deters |
2013-02-16 | Some cleanup and copyright updating | Morgan Deters |
2013-02-12 | Fix a preprocessing performance issue. | Morgan Deters |
2013-02-07 | Merge branch '1.0.x' | Morgan Deters |
2013-02-07 | Significant work on bug #491 (not yet closed). | Morgan Deters |
2013-02-05 | Fix to miplib trick to make it less "cautious" and apply in more cases | Morgan Deters |
2013-02-04 | Some fixes for the miplib preprocessing pass. | Morgan Deters |
2013-02-04 | Model no longer adds subterms of quantifiers to equality engine, this fixed b... | Andrew Reynolds |
2013-02-03 | Some cleanup of miplib regressions and options | Morgan Deters |
2013-02-03 | new option for doing top-level miplib substitutions (or not) | Morgan Deters |
2013-02-03 | extended miplib trick to 6 vars, should work on pp miplib examples now | Morgan Deters |
2013-02-03 | new miplib pass, works for 1 or 2 vars | Morgan Deters |
2013-01-27 | some fixes for Intel benchmarks regarding quantifiers and datatypes, datatype... | Andrew Reynolds |
2013-01-27 | some fixes for Intel benchmarks regarding quantifiers and datatypes, datatype... | Andrew Reynolds |
2013-01-25 | fix --check-model --finite-model-find when used together (related to bug 486) | Morgan Deters |
2013-01-25 | fix --check-model --finite-model-find when used together (related to bug 486) | Morgan Deters |
2012-12-11 | SMT-LIB compliance fix to get-assignment; resolves bug 480 | Morgan Deters |
2012-12-01 | Fix the way abstract values are typed; fixes some compliance issues. | Morgan Deters |
2012-12-01 | definition-expansion fixed for get-model, resolves bug 411 | Morgan Deters |
2012-12-01 | Adding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA");... | Tim King |
2012-11-30 | Fix assertion in smt_engine's getValue | Clark Barrett |
2012-11-29 | Fix for nasty corner case found by fuzzer... | Clark Barrett |
2012-11-29 | Fixing function models with Boolean terms. Also, LAMBDA's should not be const. | Clark Barrett |
2012-11-28 | Attempted "quick-fix" for QF_UF performance regression since Boolean terms ad... | Morgan Deters |
2012-11-28 | fix: correct misleading comment in dump output | Morgan Deters |
2012-11-27 | Functions and predicates over Boolean now work with --check-models and output... | Morgan Deters |
2012-11-27 | do not turn on BV for QF_SAT | Morgan Deters |
2012-11-27 | First chunk of boolean-terms support. | Morgan Deters |
2012-11-27 | Tuples and records merge. Resolves bug 270. | Morgan Deters |
2012-11-26 | rolling back r4625 for now (closes bug 464), Andy we should talk about this a... | Morgan Deters |
2012-11-26 | Adding support for a master equality engine. Each theory gets the master equa... | Dejan Jovanović |
2012-11-26 | don't include internal variables in model output | Morgan Deters |
2012-11-18 | support for quantifiers macros, bug fix for bug 454 involving E-matching Arra... | Andrew Reynolds |
2012-11-17 | * Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT... | Morgan Deters |
2012-11-16 | Fix for bug451 | Clark Barrett |
2012-11-15 | forgot to uncomment setLogicInternal for THEORY_BV | Liana Hadarean |
2012-11-15 | changed logic options so that justification is turned on for QF_ABV and QF_UF... | Liana Hadarean |
2012-11-14 | replaced all static member data from rewrite rule triggers, added infrastruct... | Andrew Reynolds |
2012-11-14 | Beautifying smt_engine.cpp. | Tim King |
2012-11-13 | SmtEngine::checkModel() should only be called if the result is sat or unknown... | Tim King |
2012-11-13 | fixed failed bv regressions by refactoring out some rewrite rules from smt_en... | Liana Hadarean |
2012-11-13 | added support for division by zero for bit-vector division operators | Liana Hadarean |