| 2010-07-06 |
Clark Barrett | Moved registration to theory engine |
commit | commitdiff | tree |
| 2010-07-06 |
Christopher... | Adding Array types to SMT2 parser |
commit | commitdiff | tree |
| 2010-07-06 |
Christopher... | Adding arithmetic symbols to CVC parser (Fixes: #176) |
commit | commitdiff | tree |
| 2010-07-06 |
Morgan Deters | merge from CC work: pieces of the parser need to be... |
commit | commitdiff | tree |
| 2010-07-06 |
Morgan Deters | Fixes for doubled-statistics (bug 171), a fix to muzzle... |
commit | commitdiff | tree |
| 2010-07-06 |
Morgan Deters | add regressions from bug reports |
commit | commitdiff | tree |
| 2010-07-05 |
Morgan Deters | better exception wording, assertion-handling in multipl... |
commit | commitdiff | tree |
| 2010-07-05 |
Morgan Deters | better exception wording, assertion-handling in multipl... |
commit | commitdiff | tree |
| 2010-07-05 |
Morgan Deters | workaround for strange CIMS installation of automake... |
commit | commitdiff | tree |
| 2010-07-05 |
Clark Barrett | Added Cesare to list of authors |
commit | commitdiff | tree |
| 2010-07-05 |
Clark Barrett | Changed AUTHORS - removed references to earlier CVC... |
commit | commitdiff | tree |
| 2010-07-04 |
Morgan Deters | Considerably simplified the way output streams are... |
commit | commitdiff | tree |
| 2010-07-04 |
Morgan Deters | assigning benchmark statuses |
commit | commitdiff | tree |
| 2010-07-04 |
Morgan Deters | better detection for static binary building |
commit | commitdiff | tree |
| 2010-07-04 |
Morgan Deters | fix to production build |
commit | commitdiff | tree |
| 2010-07-04 |
Morgan Deters | enable arrays |
commit | commitdiff | tree |
| 2010-07-04 |
Morgan Deters | don't do extra-checking for all regressions; that's... |
commit | commitdiff | tree |
| 2010-07-04 |
Morgan Deters | With "-d extra-checking", rewrites are now checked... |
commit | commitdiff | tree |
| 2010-07-04 |
Morgan Deters | bug 168 fixed (TheoryEngine::rewrite is not fully rewri... |
commit | commitdiff | tree |
| 2010-07-04 |
Morgan Deters | make dist && make distcheck functional, other fixes |
commit | commitdiff | tree |
| 2010-07-03 |
Morgan Deters | fix warnings |
commit | commitdiff | tree |
| 2010-07-03 |
Morgan Deters | better config.reconfig script auto-generated |
commit | commitdiff | tree |
| 2010-07-03 |
Morgan Deters | With this commit come a number of changes to build... |
commit | commitdiff | tree |
| 2010-07-02 |
Tim King | Merges the cln-test branch into the main branch. |
commit | commitdiff | tree |
| 2010-07-02 |
Morgan Deters | re-generated comment headers of source files |
commit | commitdiff | tree |
| 2010-07-02 |
Morgan Deters | roll back a small change that made arith fail some... |
commit | commitdiff | tree |
| 2010-07-02 |
Morgan Deters | * Added white-box TheoryEngine test that tests the... |
commit | commitdiff | tree |
| 2010-06-30 |
Morgan Deters | add documentation for additional clarity, re-add addTerm() |
commit | commitdiff | tree |
| 2010-06-30 |
Christopher... | Parsing support for SMT divisions: LRA, QF_UFLIA, QF_UF... |
commit | commitdiff | tree |
| 2010-06-30 |
Christopher... | Adding documentation for --strict-parsing (Closes:... |
commit | commitdiff | tree |
| 2010-06-30 |
Morgan Deters | fix to switch fall-through; stats now off by default... |
commit | commitdiff | tree |
| 2010-06-30 |
Morgan Deters | checking in CC module interface for reference. |
commit | commitdiff | tree |
| 2010-06-30 |
Morgan Deters | Support for failing .smt and .smt2 regressions (and... |
commit | commitdiff | tree |
| 2010-06-30 |
Morgan Deters | * theory "tree" rewriting implemented and works |
commit | commitdiff | tree |
| 2010-06-29 |
Morgan Deters | add --default-expr-depth=N command line parameter,... |
commit | commitdiff | tree |
| 2010-06-29 |
Tim King | This commit merges the decaying-rows branch into the... |
commit | commitdiff | tree |
| 2010-06-29 |
Tim King | Update to stats.h is now back into the trunk. The... |
commit | commitdiff | tree |
| 2010-06-29 |
Tim King | Merging the unate-propagator branch into the trunk... |
commit | commitdiff | tree |
| 2010-06-29 |
Morgan Deters | * Add CDMap<>::insertAtContextLevelZero(k, d) for inser... |
commit | commitdiff | tree |
| 2010-06-24 |
Tim King | Added post_mortem.py a statistics collector for user... |
commit | commitdiff | tree |
| 2010-06-22 |
Tim King | Made ~Stat() virtual. Added some additional statistics... |
commit | commitdiff | tree |
| 2010-06-18 |
Morgan Deters | "statistics" and "staticbinary" are now tags on the... |
commit | commitdiff | tree |
| 2010-06-18 |
Tim King | Merging the statistics branch into the main trunk.... |
commit | commitdiff | tree |
| 2010-06-18 |
Morgan Deters | bug fix (unreported on bugzilla): skolem variables... |
commit | commitdiff | tree |
| 2010-06-17 |
Morgan Deters | fix some minor annoyances in the regression test Makefi... |
commit | commitdiff | tree |
| 2010-06-16 |
Tim King | Added the experimental. +bool TheoryArith::AssertEquali... |
commit | commitdiff | tree |
| 2010-06-16 |
Tim King | More assorted changes to arithmetic in preparation... |
commit | commitdiff | tree |
| 2010-06-16 |
Tim King | This commit just contains miscellaneous arithmetic... |
commit | commitdiff | tree |
| 2010-06-15 |
Morgan Deters | fix last commit gcc options (-wunknown-pragmas ==>... |
commit | commitdiff | tree |
| 2010-06-15 |
Morgan Deters | remove warnings about unknown #pragma GCC diagnostic... |
commit | commitdiff | tree |
| 2010-06-15 |
Tim King | I made a documentation change to get() to make explicit... |
commit | commitdiff | tree |
| 2010-06-15 |
Morgan Deters | (minor) fix for file documentation |
commit | commitdiff | tree |
| 2010-06-14 |
Christopher... | Adding array select/store to SMT v1 and v2 parsers |
commit | commitdiff | tree |
| 2010-06-14 |
Tim King | Fix to arith to make sure it only attempts to report... |
commit | commitdiff | tree |
| 2010-06-14 |
Clark Barrett | Started work on array theory |
commit | commitdiff | tree |
| 2010-06-06 |
Tim King | Some assorted fixes and local optimizations for theory... |
commit | commitdiff | tree |
| 2010-06-06 |
Tim King | Adding += and *= to Rational. |
commit | commitdiff | tree |
| 2010-06-04 |
Tim King | Changed how assignments are saved during check. These... |
commit | commitdiff | tree |
| 2010-06-04 |
Tim King | Changed several arguments to const references. |
commit | commitdiff | tree |
| 2010-06-04 |
Christopher... | Adding QF_SAT to SMT parsers |
commit | commitdiff | tree |
| 2010-06-04 |
Christopher... | Reimplementing AntlrInputStream::newStreamInputStream |
commit | commitdiff | tree |
| 2010-06-04 |
Morgan Deters | ** Don't fear the files-changed list, almost all change... |
commit | commitdiff | tree |
| 2010-06-04 |
Christopher... | Missing files in last commit |
commit | commitdiff | tree |
| 2010-06-04 |
Christopher... | Enabling RDL/IDL in SMT v1 and adding some simple tests |
commit | commitdiff | tree |
| 2010-06-03 |
Christopher... | Implementing input from stdin (Fixes: #144) |
commit | commitdiff | tree |
| 2010-06-03 |
Tim King | Fixes 2 issues with assignments. The first is construct... |
commit | commitdiff | tree |
| 2010-06-03 |
Tim King | Adds toString to DeltaRational |
commit | commitdiff | tree |
| 2010-06-03 |
Tim King | Fixes a bug where registration occurs before preregistr... |
commit | commitdiff | tree |
| 2010-06-03 |
Christopher... | Changing ANTLR3 detection in configure (Fixes #147) |
commit | commitdiff | tree |
| 2010-06-03 |
Morgan Deters | * Added NodeBuilder<>::getChild() to make interface... |
commit | commitdiff | tree |
| 2010-06-03 |
Morgan Deters | resolving bug 139: metaKindOf() warnings still exist... |
commit | commitdiff | tree |
| 2010-06-02 |
Morgan Deters | added a handful of debugTagIsOn("context") checks to... |
commit | commitdiff | tree |
| 2010-06-02 |
Morgan Deters | more VERBOSE test failures |
commit | commitdiff | tree |
| 2010-06-01 |
Christopher... | Fixing test failures in production build |
commit | commitdiff | tree |
| 2010-06-01 |
Tim King | This commit adds a debugTagIsOn() guard around some... |
commit | commitdiff | tree |
| 2010-06-01 |
Tim King | This commit is a fix for a bug in removeITEs(). The... |
commit | commitdiff | tree |
| 2010-06-01 |
Christopher... | Adding SMT v2 parsing support for: QF_IDL, QF_NIA,... |
commit | commitdiff | tree |
| 2010-06-01 |
Christopher... | Checking for executable permission on antlr3 script |
commit | commitdiff | tree |
| 2010-06-01 |
Tim King | Fixed a bug in partial_model.cpp where the data was... |
commit | commitdiff | tree |
| 2010-06-01 |
Christopher... | Fixing failing test in r521 |
commit | commitdiff | tree |
| 2010-06-01 |
Dejan Jovanović | In order for splitting on demand to be able to retract... |
commit | commitdiff | tree |
| 2010-05-31 |
Christopher... | First draft implementation of mkAssociative |
commit | commitdiff | tree |
| 2010-05-29 |
Tim King | Adding a couple of example from fuzzsmt to regress1. |
commit | commitdiff | tree |
| 2010-05-29 |
Tim King | Couple of fixes to theory arith. pivotAndUpdate now... |
commit | commitdiff | tree |
| 2010-05-29 |
Tim King | After blasting the disjuncts, TheoryEngine rewrite... |
commit | commitdiff | tree |
| 2010-05-28 |
Tim King | This update enables TheoryArith to accept assertions... |
commit | commitdiff | tree |
| 2010-05-28 |
Tim King | Bug fixes for combining coefficients of rewritten nodes. |
commit | commitdiff | tree |
| 2010-05-28 |
Tim King | Added printModel() to src/theory/arith/partial_model... |
commit | commitdiff | tree |
| 2010-05-28 |
Tim King | A few changes to the organization of TheoryEngine rewri... |
commit | commitdiff | tree |
| 2010-05-28 |
Tim King | Moving the ITE removal from CnfStream to TheoryEngine... |
commit | commitdiff | tree |
| 2010-05-27 |
Morgan Deters | fix bug #134: infinite deallocation loop |
commit | commitdiff | tree |
| 2010-05-27 |
Morgan Deters | small cosmetic change to tests summary output |
commit | commitdiff | tree |
| 2010-05-27 |
Morgan Deters | Remove isAtomic() as per 4/27/2010 meeting. Add commen... |
commit | commitdiff | tree |
| 2010-05-27 |
Morgan Deters | fix compiler comparison-signedness warnings |
commit | commitdiff | tree |
| 2010-05-27 |
Tim King | Reverting this file to not include any comments. (Morga... |
commit | commitdiff | tree |
| 2010-05-27 |
Morgan Deters | added the ability to add custom expected stdout, stderr... |
commit | commitdiff | tree |
| 2010-05-27 |
Tim King | Preregistration has been turned on. Highly experimental... |
commit | commitdiff | tree |
| 2010-05-27 |
Morgan Deters | Use the newer automake test driver "parallel-tests... |
commit | commitdiff | tree |
| 2010-05-27 |
Christopher... | Adding debug assertions on most TNode operations |
commit | commitdiff | tree |
| 2010-05-27 |
Christopher... | Adding NodeManager::prepareToBeDestroyed() (Fixes:... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog