| 2013-02-26 |
lianah | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-24 |
Andrew Reynolds | added option --model-u-dt-enum for outputting uninterpr... |
tree | commitdiff |
| 2013-02-20 |
Morgan Deters | Some exception specification fixes in SmtEngine/Command... |
tree | commitdiff |
| 2013-02-17 |
Kshitij Bansal | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-17 |
Kshitij Bansal | Merge pull request #6 from kbansal/decNewoptions |
tree | commitdiff |
| 2013-02-16 |
Morgan Deters | Some cleanup and copyright updating |
tree | commitdiff |
| 2013-02-16 |
Morgan Deters | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-15 |
Kshitij Bansal | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-15 |
Kshitij Bansal | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-15 |
Morgan Deters | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-15 |
Tim King | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-13 |
Morgan Deters | Fix a preprocessing performance issue. |
tree | commitdiff |
| 2013-02-08 |
Morgan Deters | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-07 |
Morgan Deters | Significant work on bug #491 (not yet closed). |
tree | commitdiff |
| 2013-02-05 |
Morgan Deters | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-05 |
Kshitij Bansal | Merge remote-tracking branch 'origin/1.0.x' |
tree | commitdiff |
| 2013-02-05 |
Morgan Deters | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-05 |
Morgan Deters | Fix to miplib trick to make it less "cautious" and... |
tree | commitdiff |
| 2013-02-04 |
Morgan Deters | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-04 |
Morgan Deters | Some fixes for the miplib preprocessing pass. |
tree | commitdiff |
| 2013-02-04 |
Morgan Deters | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-02-04 |
Andrew Reynolds | Model no longer adds subterms of quantifiers to equalit... |
tree | commitdiff |
| 2013-02-03 |
Morgan Deters | Some cleanup of miplib regressions and options |
tree | commitdiff |
| 2013-02-03 |
Morgan Deters | Merge from mdeters/miplib branch (commit 'ce7c485182902... |
tree | commitdiff |
| 2013-02-03 |
Morgan Deters | new option for doing top-level miplib substitutions... |
tree | commitdiff |
| 2013-02-03 |
Morgan Deters | extended miplib trick to 6 vars, should work on pp... |
tree | commitdiff |
| 2013-02-03 |
Morgan Deters | new miplib pass, works for 1 or 2 vars |
tree | commitdiff |
| 2013-02-01 |
Morgan Deters | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-01-31 |
Morgan Deters | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-01-28 |
Morgan Deters | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-01-27 |
Andrew Reynolds | some fixes for Intel benchmarks regarding quantifiers... |
tree | commitdiff |
| 2013-01-27 |
Andrew Reynolds | some fixes for Intel benchmarks regarding quantifiers... |
tree | commitdiff |
| 2013-01-27 |
Morgan Deters | Merge branch '1.0.x' |
tree | commitdiff |
| 2013-01-25 |
Morgan Deters | fix --check-model --finite-model-find when used togethe... |
tree | commitdiff |
| 2013-01-25 |
Morgan Deters | Fix errors and reduce warnings on clang (merge from... |
tree | commitdiff |
| 2013-01-25 |
Morgan Deters | fix --check-model --finite-model-find when used togethe... |
tree | commitdiff |
| 2013-01-24 |
Morgan Deters | Add win32 support (merge from mdeters/win32, with some... |
tree | commitdiff |
| 2012-12-15 |
Tim King | Merge remote-tracking branch 'main-repo/1.0.x' into... |
tree | commitdiff |
| 2012-12-11 |
Morgan Deters | Merge branch '1.0.x', getting fix for bug 480 |
tree | commitdiff |
| 2012-12-11 |
Morgan Deters | SMT-LIB compliance fix to get-assignment; resolves... |
tree | commitdiff |
| 2012-12-01 |
Morgan Deters | Fix the way abstract values are typed; fixes some compl... |
tree | commitdiff |
| 2012-12-01 |
Morgan Deters | remove an obsolete (and incorrect) assertion in boolean... |
tree | commitdiff |
| 2012-12-01 |
Morgan Deters | Some fixes for boolean arrays |
tree | commitdiff |
| 2012-12-01 |
Morgan Deters | definition-expansion fixed for get-model, resolves... |
tree | commitdiff |
| 2012-12-01 |
Tim King | Adding SmtEngine::setLogic(const char* logic) so that... |
tree | commitdiff |
| 2012-11-30 |
Clark Barrett | Fix assertion in smt_engine's getValue |
tree | commitdiff |
| 2012-11-30 |
Tim King | Adding smtname level options for tlimit, rlimit, etc... |
tree | commitdiff |
| 2012-11-29 |
Morgan Deters | fix for andy: boolean terms stuff really shouldn't... |
tree | commitdiff |
| 2012-11-29 |
Clark Barrett | Fix for nasty corner case found by fuzzer... |
tree | commitdiff |
| 2012-11-29 |
Clark Barrett | Fixing function models with Boolean terms. Also, LAMBD... |
tree | commitdiff |
| 2012-11-28 |
Morgan Deters | Attempted "quick-fix" for QF_UF performance regression... |
tree | commitdiff |
| 2012-11-28 |
Morgan Deters | fix: correct misleading comment in dump output |
tree | commitdiff |
| 2012-11-27 |
Morgan Deters | Functions and predicates over Boolean now work with... |
tree | commitdiff |
| 2012-11-27 |
Morgan Deters | do not turn on BV for QF_SAT |
tree | commitdiff |
| 2012-11-27 |
Morgan Deters | First chunk of boolean-terms support. |
tree | commitdiff |
| 2012-11-27 |
Morgan Deters | Tuples and records merge. Resolves bug 270. |
tree | commitdiff |
| 2012-11-26 |
Morgan Deters | rolling back r4625 for now (closes bug 464), Andy we... |
tree | commitdiff |
| 2012-11-26 |
Dejan Jovanović | Adding support for a master equality engine. Each theor... |
tree | commitdiff |
| 2012-11-26 |
Morgan Deters | don't include internal variables in model output |
tree | commitdiff |
| 2012-11-26 |
Morgan Deters | some fixes to language bindings and function visibility |
tree | commitdiff |
| 2012-11-18 |
Andrew Reynolds | support for quantifiers macros, bug fix for bug 454... |
tree | commitdiff |
| 2012-11-17 |
Morgan Deters | * Fix for bug 445 agreed to in meeting 11/13/2012:... |
tree | commitdiff |
| 2012-11-16 |
Clark Barrett | Fix for bug451 |
tree | commitdiff |
| 2012-11-15 |
Liana Hadarean | forgot to uncomment setLogicInternal for THEORY_BV |
tree | commitdiff |
| 2012-11-15 |
Liana Hadarean | changed logic options so that justification is turned... |
tree | commitdiff |
| 2012-11-14 |
Andrew Reynolds | replaced all static member data from rewrite rule trigg... |
tree | commitdiff |
| 2012-11-14 |
Tim King | Beautifying smt_engine.cpp. |
tree | commitdiff |
| 2012-11-13 |
Tim King | SmtEngine::checkModel() should only be called if the... |
tree | commitdiff |
| 2012-11-13 |
Liana Hadarean | fixed failed bv regressions by refactoring out some... |
tree | commitdiff |
| 2012-11-13 |
Liana Hadarean | added support for division by zero for bit-vector divis... |
tree | commitdiff |
| 2012-11-12 |
Morgan Deters | Fix for bug 444, dealing with the placing of set-logic... |
tree | commitdiff |
| 2012-11-12 |
Andrew Reynolds | minor bug fixes for quantifiers, added sort inference... |
tree | commitdiff |
| 2012-11-10 |
Tim King | Removing rewriter call in SmtEngine::addFormula(). |
tree | commitdiff |
| 2012-11-10 |
Morgan Deters | Updates to Clark's commit r4540: |
tree | commitdiff |
| 2012-11-10 |
Morgan Deters | fix typo in language bindings |
tree | commitdiff |
| 2012-11-10 |
Clark Barrett | Finally tracked down problems in regressions and fuzz... |
tree | commitdiff |
| 2012-11-09 |
Morgan Deters | Bug-fix for a crash involving improperly-thrown excepti... |
tree | commitdiff |
| 2012-11-09 |
Morgan Deters | In non-linear logics, rewrite DIVISION, INTS_DIVISION... |
tree | commitdiff |
| 2012-11-08 |
Tim King | Turns on TheoryUF when non-linear arithmetic is turned... |
tree | commitdiff |
| 2012-10-29 |
Clark Barrett | Tweak to options configuration for turning off minisat... |
tree | commitdiff |
| 2012-10-29 |
Clark Barrett | Disable minisat elimination when models are on |
tree | commitdiff |
| 2012-10-26 |
Clark Barrett | More bug fixes and more checks for models |
tree | commitdiff |
| 2012-10-17 |
Andrew Reynolds | first working version of new inst-gen-style quantifier... |
tree | commitdiff |
| 2012-10-14 |
Morgan Deters | fix #line number warnings (sorry!) |
tree | commitdiff |
| 2012-10-11 |
Morgan Deters | Fix bug 421, again, and add a second, independent test... |
tree | commitdiff |
| 2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
tree | commitdiff |
| 2012-10-10 |
Morgan Deters | Abstract values for SMT-LIB. |
tree | commitdiff |
| 2012-10-09 |
Morgan Deters | * make Model class private (as discussed at meeting... |
tree | commitdiff |
| 2012-10-08 |
Morgan Deters | * Models' SubstitutionMaps are now attached to the... |
tree | commitdiff |
| 2012-10-06 |
Morgan Deters | * more complete support for --dump assertions:{pre... |
tree | commitdiff |
| 2012-10-06 |
Morgan Deters | * Clean up some options documentation |
tree | commitdiff |
| 2012-10-06 |
Morgan Deters | * Include a few bug testcases for resolved bugs. |
tree | commitdiff |
| 2012-10-05 |
Morgan Deters | Bug-related: |
tree | commitdiff |
| 2012-10-05 |
Dejan Jovanović | BoolExpr removed and replaced with Expr |
tree | commitdiff |
| 2012-10-04 |
Clark Barrett | Implemented array type enumerator, more fixes for models |
tree | commitdiff |
| 2012-10-03 |
Liana Hadarean | added support for interrupting TheoryBV |
tree | commitdiff |
| 2012-10-03 |
Dejan Jovanović | adding ::getBooleanVariables to the PropEngine |
tree | commitdiff |
| 2012-10-02 |
Morgan Deters | * re-enable some Z3 extended commands: |
tree | commitdiff |
| 2012-10-01 |
Kshitij Bansal | "Fix" (disable) portfolio when using quantifiers |
tree | commitdiff |
| 2012-10-01 |
Morgan Deters | fix for dejan: term ITEs now dumped correctly |
tree | commitdiff |
| next |
projects / cvc5.git / history