| 2010-08-16 |
Morgan Deters | add zlib checks to configure (new minisat requires... |
commit | commitdiff | tree |
| 2010-08-16 |
Dejan Jovanović | Fixing failures in minisat |
commit | commitdiff | tree |
| 2010-08-15 |
Dejan Jovanović | (no commit message) |
commit | commitdiff | tree |
| 2010-08-15 |
Dejan Jovanović | (no commit message) |
commit | commitdiff | tree |
| 2010-08-13 |
Dejan Jovanović | renaming minisat .C to .cc |
commit | commitdiff | tree |
| 2010-08-13 |
Dejan Jovanović | Adding the changes to the original copy |
commit | commitdiff | tree |
| 2010-08-13 |
Christopher... | Importing MiniSat2 070721 into trunk |
commit | commitdiff | tree |
| 2010-08-13 |
Christopher... | Removing newer version of MiniSat for Dejan's preferred... |
commit | commitdiff | tree |
| 2010-08-13 |
Christopher... | Importing MiniSat2 2.2.0 into trunk |
commit | commitdiff | tree |
| 2010-08-13 |
Christopher... | Removing old version of MiniSat for proper vendor import |
commit | commitdiff | tree |
| 2010-07-29 |
Christopher... | Adding configuration_private.h to allow inlining of... |
commit | commitdiff | tree |
| 2010-07-29 |
Morgan Deters | fix TheoryEngineWhite, add documentation; related to... |
commit | commitdiff | tree |
| 2010-07-28 |
Christopher... | Adding TypeCheckingException to throws clause in SMT... |
commit | commitdiff | tree |
| 2010-07-28 |
Christopher... | Forcing a type check on Node construction in debug... |
commit | commitdiff | tree |
| 2010-07-28 |
Morgan Deters | fixed theory engine white test for new (old) theoryOf... |
commit | commitdiff | tree |
| 2010-07-27 |
Christopher... | Moving EQ->IFF handling from TheoryEngine to parser... |
commit | commitdiff | tree |
| 2010-07-27 |
Christopher... | Adding optional 'check' parameter to getType() methods |
commit | commitdiff | tree |
| 2010-07-22 |
Morgan Deters | incorporate a fix from smtcomp2010 version for handling... |
commit | commitdiff | tree |
| 2010-07-22 |
Tim King | Added test file for fuzzsmt bug, bug187.smt2. |
commit | commitdiff | tree |
| 2010-07-10 |
Morgan Deters | add >, <=, and >= comparisons for Exprs and Nodes |
commit | commitdiff | tree |
| 2010-07-10 |
Dejan Jovanović | Fix for the type in sat propagation. |
commit | commitdiff | tree |
| 2010-07-09 |
Dejan Jovanović | the tableaux optimization |
commit | commitdiff | tree |
| 2010-07-08 |
Christopher... | Moving cluster-qf_lra-full to scripts project |
commit | commitdiff | tree |
| 2010-07-08 |
Christopher... | Moving cluster-qf_lra-benchmark to scripts project |
commit | commitdiff | tree |
| 2010-07-08 |
Christopher... | Adding missing operators in SMT2 parser: UMINUS, DIVISI... |
commit | commitdiff | tree |
| 2010-07-08 |
Christopher... | Fixing Array type in SMT v1.2 |
commit | commitdiff | tree |
| 2010-07-08 |
Tim King | I am adding my smt-crunch scripts to source control... |
commit | commitdiff | tree |
| 2010-07-08 |
Morgan Deters | context work to support cdmaps with elements allocated... |
commit | commitdiff | tree |
| 2010-07-08 |
Tim King | Updates to the post_mortem.py script. |
commit | commitdiff | tree |
| 2010-07-07 |
Clark Barrett | Shared term manager tested and working |
commit | commitdiff | tree |
| 2010-07-07 |
Christopher... | Making plus-mult.cvc test a bit more torturous (as... |
commit | commitdiff | tree |
| 2010-07-07 |
Tim King | Fixes arith rewriter to allow for division by a constan... |
commit | commitdiff | tree |
| 2010-07-07 |
Christopher... | Fixing test plus-mult.cvc by making it linear (Fixes... |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | minor changes to cdmap/cdset interface for detection... |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | chris and i committed the same fix; reverting the ... |
commit | commitdiff | tree |
| 2010-07-07 |
Clark Barrett | Updated headers |
commit | commitdiff | tree |
| 2010-07-07 |
Clark Barrett | Added shared term manager. Basic mechanism for identif... |
commit | commitdiff | tree |
| 2010-07-07 |
Christopher... | Disabling failing tests |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | add exit status to regression that was failing |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | some build system changes reverted after the CLN build... |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | competition submission should be fully static |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | fixed submission target |
commit | commitdiff | tree |
| 2010-07-07 |
Morgan Deters | things for competition upload: new "make submission... |
commit | commitdiff | tree |
| 2010-07-07 |
Christopher... | Adding tests for precedence of arithmetic in CVC inputs |
commit | commitdiff | tree |
| 2010-07-07 |
Christopher... | Adding config.reconfig to .gitignore |
commit | commitdiff | tree |
| 2010-07-06 |
Tim King | Fixed exit status for competition mode. |
commit | commitdiff | tree |
| 2010-07-06 |
Morgan Deters | Don't eagerly collect zombies. This should speed up... |
commit | commitdiff | tree |
| 2010-07-06 |
Morgan Deters | add Configuration::isCompetitionBuild() and some main... |
commit | commitdiff | tree |
| 2010-07-06 |
Morgan Deters | fix crash on command line parsing |
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / shortlog