| 2012-12-01 |
Tim King | Adding SmtEngine::setLogic(const char* logic) so that... |
commit | commitdiff | tree |
| 2012-11-30 |
Tim King | Fixes for stricter compilers Andy brought to my attention. |
commit | commitdiff | tree |
| 2012-11-30 |
Tim King | Changing the documentation of ARR_TABLE_FUN to say... |
commit | commitdiff | tree |
| 2012-11-30 |
Morgan Deters | all API examples now have java versions too; bitvectors... |
commit | commitdiff | tree |
| 2012-11-30 |
Morgan Deters | incorporating some comments from Clark |
commit | commitdiff | tree |
| 2012-11-30 |
Clark Barrett | Fix assertion in smt_engine's getValue |
commit | commitdiff | tree |
| 2012-11-30 |
Tim King | Updating the combination.cpp example. |
commit | commitdiff | tree |
| 2012-11-30 |
Tim King | Committing tests to potentially discover an obscure... |
commit | commitdiff | tree |
| 2012-11-30 |
Morgan Deters | renaming --smtlib to --smtlib-strict; removing --smtlib... |
commit | commitdiff | tree |
| 2012-11-30 |
Morgan Deters | internal variables (skolems) aren't printed as part... |
commit | commitdiff | tree |
| 2012-11-30 |
Morgan Deters | change detection/handling of output language more reaso... |
commit | commitdiff | tree |
| 2012-11-30 |
Andrew Reynolds | quantifiers now uses master equality engine, preparatio... |
commit | commitdiff | tree |
| 2012-11-30 |
Andrew Reynolds | parametric datatypes fix related to non-ascribed type... |
commit | commitdiff | tree |
| 2012-11-30 |
Liana Hadarean | added a simple API example example showing how to use... |
commit | commitdiff | tree |
| 2012-11-30 |
Tim King | Changes to SExpr to accept autoconversion from bool... |
commit | commitdiff | tree |
| 2012-11-30 |
Tim King | Adding smtname level options for tlimit, rlimit, etc... |
commit | commitdiff | tree |
| 2012-11-30 |
Morgan Deters | Partial fix for bug 435; still needs some effort. |
commit | commitdiff | tree |
| 2012-11-30 |
Morgan Deters | Add some regressions for bug 438. |
commit | commitdiff | tree |
| 2012-11-30 |
Morgan Deters | fix rewrite-rules syntax in regression |
commit | commitdiff | tree |
| 2012-11-30 |
Morgan Deters | minor fix to release script |
commit | commitdiff | tree |
| 2012-11-30 |
François Bobot | fix the syntax of assert-rewrite/-propagation/-reductio... |
commit | commitdiff | tree |
| 2012-11-29 |
Kshitij Bansal | reliable benchmark corresponding to bug468 |
commit | commitdiff | tree |
| 2012-11-29 |
Andrew Reynolds | require type ascriptions for parametric datatype constr... |
commit | commitdiff | tree |
| 2012-11-29 |
Morgan Deters | Fix for hidden symbols in library on Mac. It's a stran... |
commit | commitdiff | tree |
| 2012-11-29 |
Andrew Reynolds | fixes bug 438, incorporate subtypes into type unificati... |
commit | commitdiff | tree |
| 2012-11-29 |
Morgan Deters | fix for andy: boolean terms stuff really shouldn't... |
commit | commitdiff | tree |
| 2012-11-29 |
Morgan Deters | minor documentation fix |
commit | commitdiff | tree |
| 2012-11-29 |
Morgan Deters | svn:ignore property |
commit | commitdiff | tree |
| 2012-11-29 |
Clark Barrett | Fix for nasty corner case found by fuzzer... |
commit | commitdiff | tree |
| 2012-11-29 |
Kshitij Bansal | Hack to support global variables for CVC language exten... |
commit | commitdiff | tree |
| 2012-11-29 |
Clark Barrett | Fixing function models with Boolean terms. Also, LAMBD... |
commit | commitdiff | tree |
| 2012-11-28 |
Tim King | Adding the helloworld.cpp example. |
commit | commitdiff | tree |
| 2012-11-28 |
Kshitij Bansal | fix a potential race (have failed to reproduce) |
commit | commitdiff | tree |
| 2012-11-28 |
Clark Barrett | Fix for getValue. Now it can handle lambda applications |
commit | commitdiff | tree |
| 2012-11-28 |
Morgan Deters | Attempted "quick-fix" for QF_UF performance regression... |
commit | commitdiff | tree |
| 2012-11-28 |
Kshitij Bansal | treat all get commands like getValue (send only to... |
commit | commitdiff | tree |
| 2012-11-28 |
Kshitij Bansal | minor |
commit | commitdiff | tree |
| 2012-11-28 |
Morgan Deters | update to release notes |
commit | commitdiff | tree |
| 2012-11-28 |
Morgan Deters | Bug fix: |
commit | commitdiff | tree |
| 2012-11-28 |
Morgan Deters | fix: correct misleading comment in dump output |
commit | commitdiff | tree |
| 2012-11-27 |
Morgan Deters | Functions and predicates over Boolean now work with... |
commit | commitdiff | tree |
| 2012-11-27 |
Kshitij Bansal | fix in CommandSequence invoke : maintain success/failur... |
commit | commitdiff | tree |
| 2012-11-27 |
Morgan Deters | more mac fixes |
commit | commitdiff | tree |
| 2012-11-27 |
Morgan Deters | fix for some Mac builds |
commit | commitdiff | tree |
| 2012-11-27 |
Kshitij Bansal | Simplify --help=decision with only currently supported... |
commit | commitdiff | tree |
| 2012-11-27 |
Morgan Deters | give warning at configure-time about unsupported langua... |
commit | commitdiff | tree |
| 2012-11-27 |
Morgan Deters | do not turn on BV for QF_SAT |
commit | commitdiff | tree |
| 2012-11-27 |
Morgan Deters | First chunk of boolean-terms support. |
commit | commitdiff | tree |
| 2012-11-27 |
Morgan Deters | Tuples and records merge. Resolves bug 270. |
commit | commitdiff | tree |
| 2012-11-27 |
Tim King | Adding an example to show how to use arithmetic. |
commit | commitdiff | tree |
| 2012-11-26 |
Tim King | Improved implementation of Integer::length() with CLN... |
commit | commitdiff | tree |
| 2012-11-26 |
Morgan Deters | include new regression directories in summary test... |
commit | commitdiff | tree |
| 2012-11-26 |
Morgan Deters | rolling back r4625 for now (closes bug 464), Andy we... |
commit | commitdiff | tree |
| 2012-11-26 |
Dejan Jovanović | fixup for incremental solving |
commit | commitdiff | tree |
| 2012-11-26 |
Tim King | Removing DioSolver::acceptableOriginalNodes(). This... |
commit | commitdiff | tree |
| 2012-11-26 |
Dejan Jovanović | Adding support for a master equality engine. Each theor... |
commit | commitdiff | tree |
| 2012-11-26 |
Tim King | Improving arithmetic debugging output. |
commit | commitdiff | tree |
| 2012-11-26 |
Tim King | Disabling test/regress/regress0/push-pop/bug396.smt2... |
commit | commitdiff | tree |
| 2012-11-26 |
Morgan Deters | don't include internal variables in model output |
commit | commitdiff | tree |
| 2012-11-26 |
Morgan Deters | some fixes to language bindings and function visibility |
commit | commitdiff | tree |
| 2012-11-26 |
Morgan Deters | Makefile fix for new versions of Make (thanks Clark... |
commit | commitdiff | tree |
| 2012-11-25 |
Tim King | Adding a regression test from bug 462. |
commit | commitdiff | tree |
| 2012-11-25 |
Tim King | This commit fixes two incompleteness bugs (461, 459... |
commit | commitdiff | tree |
| 2012-11-24 |
Tim King | Adds ensureConstraint(...) to ConstraintDatabase. This... |
commit | commitdiff | tree |
| 2012-11-23 |
François Bobot | Example of rewrite rules use that comes from an harness... |
commit | commitdiff | tree |
| 2012-11-21 |
Tim King | - Removes getDeltaValueWithNonlinear() entirely |
commit | commitdiff | tree |
| 2012-11-21 |
Tim King | Adds a number of new capabilities to DeltaRational... |
commit | commitdiff | tree |
| 2012-11-21 |
Tim King | Added debugging output to --check-models. I've found... |
commit | commitdiff | tree |
| 2012-11-19 |
Kshitij Bansal | Run lastWinner thread for all commands. Earlier behavio... |
commit | commitdiff | tree |
| 2012-11-19 |
Tim King | Adding hand minimized test for bug 450. |
commit | commitdiff | tree |
| 2012-11-19 |
Tim King | Changed the splitting-on-demand lemmas of arithmetic... |
commit | commitdiff | tree |
| 2012-11-19 |
Tim King | Fix for bug452. |
commit | commitdiff | tree |
| 2012-11-18 |
Morgan Deters | Disable predicate subtyping: |
commit | commitdiff | tree |
| 2012-11-18 |
Andrew Reynolds | support for quantifiers macros, bug fix for bug 454... |
commit | commitdiff | tree |
| 2012-11-17 |
Clark Barrett | Fixed last currently known bug in array models |
commit | commitdiff | tree |
| 2012-11-17 |
Morgan Deters | * enable previously-failing (now succeeding) datatype... |
commit | commitdiff | tree |
| 2012-11-17 |
Morgan Deters | fix for language bindings (fixes debian build fail... |
commit | commitdiff | tree |
| 2012-11-17 |
Morgan Deters | * Fix for bug 445 agreed to in meeting 11/13/2012:... |
commit | commitdiff | tree |
| 2012-11-16 |
Clark Barrett | Fix for bug451 |
commit | commitdiff | tree |
| 2012-11-16 |
Dejan Jovanović | fixing and refactoring the equality iterator |
commit | commitdiff | tree |
| 2012-11-16 |
Morgan Deters | Fix dumping of array-select expressions in CVC native... |
commit | commitdiff | tree |
| 2012-11-16 |
Morgan Deters | fix a compiler warning in models |
commit | commitdiff | tree |
| 2012-11-15 |
Kshitij Bansal | some fixes for --threads=1 |
commit | commitdiff | tree |
| 2012-11-15 |
Morgan Deters | fix for "make examples" |
commit | commitdiff | tree |
| 2012-11-15 |
Clark Barrett | More fixes to model generation, with previously failing... |
commit | commitdiff | tree |
| 2012-11-15 |
Liana Hadarean | forgot to uncomment setLogicInternal for THEORY_BV |
commit | commitdiff | tree |
| 2012-11-15 |
Liana Hadarean | changed logic options so that justification is turned... |
commit | commitdiff | tree |
| 2012-11-15 |
Morgan Deters | d_incomplete is context-dependent; we shouldn't be... |
commit | commitdiff | tree |
| 2012-11-15 |
Clark Barrett | fuzz15 should have been fuzz14 |
commit | commitdiff | tree |
| 2012-11-15 |
Tim King | Fix for bug 447. |
commit | commitdiff | tree |
| 2012-11-15 |
Clark Barrett | Fixed another AUFBV model bug. BV equality subtheory... |
commit | commitdiff | tree |
| 2012-11-15 |
Tim King | Fixing comments in print_lambda.cvc. |
commit | commitdiff | tree |
| 2012-11-14 |
Tim King | Fix for bug 407. mkAnonymousFunction() in the parser... |
commit | commitdiff | tree |
| 2012-11-14 |
Andrew Reynolds | replaced all static member data from rewrite rule trigg... |
commit | commitdiff | tree |
| 2012-11-14 |
Tim King | Fixed a typo in r4576 |
commit | commitdiff | tree |
| 2012-11-14 |
Tim King | Beautifying smt_engine.cpp. |
commit | commitdiff | tree |
| 2012-11-14 |
Tim King | Fix to bug449. Adds shared constants to the set of... |
commit | commitdiff | tree |
| 2012-11-14 |
Clark Barrett | bug fixes to models, array rewriter with previously... |
commit | commitdiff | tree |
| 2012-11-14 |
Kshitij Bansal | Quantifiers enabled with portfolio, closing bug 423. |
commit | commitdiff | tree |
| 2012-11-14 |
Kshitij Bansal | fix a race problem. due to interrupt mechanism minisat... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog