| 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 |
| 2012-11-13 |
Clark Barrett | More bugfixes for models |
commit | commitdiff | tree |
| 2012-11-13 |
Tim King | SmtEngine::checkModel() should only be called if the... |
commit | commitdiff | tree |
| 2012-11-13 |
Andrew Reynolds | refactoring of quantifiers rewriter based on code revie... |
commit | commitdiff | tree |
| 2012-11-13 |
Liana Hadarean | fixed failed bv regressions by refactoring out some... |
commit | commitdiff | tree |
| 2012-11-13 |
Liana Hadarean | added support for division by zero for bit-vector divis... |
commit | commitdiff | tree |
| 2012-11-13 |
Clark Barrett | Relaxing too-strict assertion |
commit | commitdiff | tree |
| 2012-11-13 |
Clark Barrett | Fixed an array rewriting bug found by fuzzer |
commit | commitdiff | tree |
| 2012-11-13 |
Clark Barrett | Testcases for fixed bugs |
commit | commitdiff | tree |
| 2012-11-13 |
Clark Barrett | Fixed bug in array constant normalization found by... |
commit | commitdiff | tree |
| 2012-11-12 |
Tim King | Improved error reporting for improperly using non-linea... |
commit | commitdiff | tree |
| 2012-11-12 |
Tim King | Delta is now generated in arithmetic to keep consistent... |
commit | commitdiff | tree |
| 2012-11-12 |
Liana Hadarean | changed BitVector::unsignedRem to match the behavior... |
commit | commitdiff | tree |
| 2012-11-12 |
Morgan Deters | Fix for bug 444, dealing with the placing of set-logic... |
commit | commitdiff | tree |
| 2012-11-12 |
Morgan Deters | * Fix language bindings: various issues |
commit | commitdiff | tree |
| 2012-11-12 |
Andrew Reynolds | minor bug fixes for quantifiers, added sort inference... |
commit | commitdiff | tree |
| 2012-11-11 |
Tim King | Fixes for the arithmetic normal form and rewriter to... |
commit | commitdiff | tree |
| 2012-11-10 |
Tim King | Beautifying integer_cln_imp.h |
commit | commitdiff | tree |
| 2012-11-10 |
Tim King | Fix to quantifier rewritting not being idempotent.... |
commit | commitdiff | tree |
| 2012-11-10 |
Tim King | Removing rewriter call in SmtEngine::addFormula(). |
commit | commitdiff | tree |
| 2012-11-10 |
Clark Barrett | Fixed missing \ in uflra/Makefile.ma |
commit | commitdiff | tree |
| 2012-11-10 |
Tim King | Fix for bug 439. Delta computation now includes disequa... |
commit | commitdiff | tree |
| 2012-11-10 |
Morgan Deters | Change run-regression script to *additionally* run... |
commit | commitdiff | tree |
| 2012-11-10 |
Morgan Deters | Updates to Clark's commit r4540: |
commit | commitdiff | tree |
| 2012-11-10 |
Morgan Deters | fix typo in language bindings |
commit | commitdiff | tree |
| 2012-11-10 |
Clark Barrett | Finally tracked down problems in regressions and fuzz... |
commit | commitdiff | tree |
| 2012-11-09 |
Morgan Deters | TheoryEngineModelBuilder::buildModel() is only called... |
commit | commitdiff | tree |
| 2012-11-09 |
Kshitij Bansal | export null nodes (fixes a bug in portfolio model stuff) |
commit | commitdiff | tree |
| 2012-11-09 |
Tim King | Test that breaks arithmetic model building due to diseq... |
commit | commitdiff | tree |
| 2012-11-09 |
Tim King | Arithmetic problem that fails --check-models due incomp... |
commit | commitdiff | tree |
| 2012-11-09 |
Morgan Deters | Bug-fix for a crash involving improperly-thrown excepti... |
commit | commitdiff | tree |
| 2012-11-09 |
Morgan Deters | In non-linear logics, rewrite DIVISION, INTS_DIVISION... |
commit | commitdiff | tree |
| 2012-11-09 |
Morgan Deters | another DISTCLEANFILES entry, for proper "make distclea... |
commit | commitdiff | tree |
| 2012-11-09 |
Clark Barrett | Fix for another model assertion failure |
commit | commitdiff | tree |
| 2012-11-08 |
Tim King | Turns on TheoryUF when non-linear arithmetic is turned... |
commit | commitdiff | tree |
| 2012-11-08 |
Morgan Deters | fix "make distcheck" |
commit | commitdiff | tree |
| 2012-11-08 |
Morgan Deters | Review of trunk r4525 (TypeNode::getBaseType()): |
commit | commitdiff | tree |
| 2012-11-08 |
Tim King | Improved support for division by zero. This adds the... |
commit | commitdiff | tree |
| 2012-11-08 |
Morgan Deters | exception fix |
commit | commitdiff | tree |
| 2012-11-08 |
Clark Barrett | Fixed two small bugs in model generation |
commit | commitdiff | tree |
| 2012-11-08 |
Clark Barrett | Added getBaseType - Morgan please check |
commit | commitdiff | tree |
| 2012-11-08 |
Andrew Reynolds | added support for parametric datatypes in smt2 parser... |
commit | commitdiff | tree |
| 2012-11-07 |
Morgan Deters | * Type ascription bug fixed (resolves bug 432), but... |
commit | commitdiff | tree |
| 2012-11-07 |
Tim King | Fix to a bug in integer mod lemmas. |
commit | commitdiff | tree |
| 2012-11-06 |
Morgan Deters | fix issue in compatibility layer that could segfault |
commit | commitdiff | tree |
| 2012-11-05 |
Tim King | Fix to the context dependent static learning code. |
commit | commitdiff | tree |
| 2012-11-05 |
Morgan Deters | fixes for replacement function library |
commit | commitdiff | tree |
| 2012-11-05 |
Morgan Deters | fixes for mac os |
commit | commitdiff | tree |
| 2012-11-05 |
Morgan Deters | fix for tarball building (fixes debian and distcheck... |
commit | commitdiff | tree |
| 2012-11-02 |
Andrew Reynolds | more minor updates to inst gen and representative selec... |
commit | commitdiff | tree |
| 2012-10-31 |
Andrew Reynolds | cleaning up some of the equality query stuff, implement... |
commit | commitdiff | tree |
| 2012-10-30 |
Dejan Jovanović | delta of a model-building failure case |
commit | commitdiff | tree |
| 2012-10-29 |
Andrew Reynolds | more updates and minor bug fixes for fmf/inst-gen quant... |
commit | commitdiff | tree |
| 2012-10-29 |
Clark Barrett | Tweak to options configuration for turning off minisat... |
commit | commitdiff | tree |
| 2012-10-29 |
Clark Barrett | Disable minisat elimination when models are on |
commit | commitdiff | tree |
| 2012-10-29 |
Clark Barrett | Disable some array optimizations when models are on |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog