| 2011-03-08 |
Tim King | - Merges queue-interrogation branch into the trunk... |
commit | commitdiff | tree |
| 2011-03-07 |
Tim King | Merges branches/arithmetic/tableau-reset into the trunk... |
commit | commitdiff | tree |
| 2011-03-05 |
Tim King | - Adds PermissiveBackArithVarSet. This is very similar... |
commit | commitdiff | tree |
| 2011-03-05 |
Tim King | Enables the PreferenceFunction minBoundAndRowCount. |
commit | commitdiff | tree |
| 2011-03-05 |
Tim King | - Adds "PreferenceFunction" to SimplexDecisionProcedure... |
commit | commitdiff | tree |
| 2011-03-05 |
Tim King | - Made Rational::sgn() function const. |
commit | commitdiff | tree |
| 2011-03-05 |
Morgan Deters | adding three features to CVC parser that drastically... |
commit | commitdiff | tree |
| 2011-03-03 |
Morgan Deters | fix for bug #244, "Segfault if file cannot be found... |
commit | commitdiff | tree |
| 2011-03-03 |
Tim King | - Creates a queue for lemmas discovered during the... |
commit | commitdiff | tree |
| 2011-03-03 |
Morgan Deters | resurrecting triple.h from r1023 (after which it was... |
commit | commitdiff | tree |
| 2011-03-03 |
Tim King | Merged the tableau-copy branch into trunk. This adds... |
commit | commitdiff | tree |
| 2011-03-03 |
Dejan Jovanović | fixing a type that caused the segfaults in the regressions |
commit | commitdiff | tree |
| 2011-03-02 |
Dejan Jovanović | fixing the big with lemma reallocation in minisat garba... |
commit | commitdiff | tree |
| 2011-02-28 |
Morgan Deters | CongruenceClosure module now should support nullary... |
commit | commitdiff | tree |
| 2011-02-28 |
Morgan Deters | Review of mktheorytraits, mkrewriter, and recent change... |
commit | commitdiff | tree |
| 2011-02-28 |
Morgan Deters | minor doxygen build target fixes |
commit | commitdiff | tree |
| 2011-02-28 |
Morgan Deters | Review of statistics code. Added lots of documentation... |
commit | commitdiff | tree |
| 2011-02-27 |
Tim King | - Adds a path for Theory to be passed a reference to... |
commit | commitdiff | tree |
| 2011-02-27 |
Tim King | - Makes VarCoeffPair a class instead of a typedef of... |
commit | commitdiff | tree |
| 2011-02-27 |
Tim King | - Adds a buffer to the ReducedRowVector addRowTimesCons... |
commit | commitdiff | tree |
| 2011-02-26 |
Tim King | - Merged RowVector and ReducedRowVector. |
commit | commitdiff | tree |
| 2011-02-26 |
Morgan Deters | Commit to fix bug 241 (improper "using namespace std... |
commit | commitdiff | tree |
| 2011-02-26 |
Morgan Deters | Merge from theory-break-dependences branch to break... |
commit | commitdiff | tree |
| 2011-02-26 |
Morgan Deters | fix serious regression breakage (segfaults) caused... |
commit | commitdiff | tree |
| 2011-02-26 |
Dejan Jovanović | adding the variables count to the statistics in the... |
commit | commitdiff | tree |
| 2011-02-26 |
Dejan Jovanović | adding statistics about how many different kinds of... |
commit | commitdiff | tree |
| 2011-02-25 |
Tim King | - This commit adds some debugging information to ArithP... |
commit | commitdiff | tree |
| 2011-02-25 |
Dejan Jovanović | slicing manager is not breaking the old regressions... |
commit | commitdiff | tree |
| 2011-02-24 |
Tim King | - Adds an additional round of checks for a conflict... |
commit | commitdiff | tree |
| 2011-02-24 |
Tim King | - Adds an additional mode to ArithPriorityQueue, Collec... |
commit | commitdiff | tree |
| 2011-02-24 |
Tim King | - Changes ArithPriorityQueue to use stl::vector<>'s... |
commit | commitdiff | tree |
| 2011-02-22 |
Tim King | - Adds column based iterators. |
commit | commitdiff | tree |
| 2011-02-21 |
Tim King | - Adds the ArithPriorityQueue class. The ArithPriorityQ... |
commit | commitdiff | tree |
| 2011-02-21 |
Tim King | - Adds the statistic d_avgNumRowsNotContainingOnPivot. |
commit | commitdiff | tree |
| 2011-02-19 |
Tim King | Changes: |
commit | commitdiff | tree |
| 2011-02-18 |
Tim King | Changes: |
commit | commitdiff | tree |
| 2011-02-17 |
Tim King | This commit merges the branch branches/arithmetic/quick... |
commit | commitdiff | tree |
| 2011-02-17 |
Tim King | This commit is the promised clean up after removing... |
commit | commitdiff | tree |
| 2011-02-17 |
Tim King | Removed ActivityMonitor from arithmetic. This was only... |
commit | commitdiff | tree |
| 2011-02-17 |
Tim King | Row ejection is now completely disabled. Another commit... |
commit | commitdiff | tree |
| 2011-02-17 |
Tim King | Removed vestigial normal form notes file from src/theor... |
commit | commitdiff | tree |
| 2011-02-17 |
Dejan Jovanović | some unit tests to work on slicing |
commit | commitdiff | tree |
| 2011-02-17 |
Tim King | I replaced the pattern "x = x + y;" with "x += y;"... |
commit | commitdiff | tree |
| 2011-02-17 |
Tim King | Updates based on the group code review of arithmetic... |
commit | commitdiff | tree |
| 2011-02-17 |
Tim King | Deleting depricated files. |
commit | commitdiff | tree |
| 2011-02-17 |
Dejan Jovanović | getting ready for slicing bitvectors |
commit | commitdiff | tree |
| 2011-02-16 |
Tim King | Overview of the changes: |
commit | commitdiff | tree |
| 2011-02-16 |
Dejan Jovanović | updates for the rewriter, added some statistics |
commit | commitdiff | tree |
| 2011-02-14 |
Tim King | Reverses the order of the d_possiblyInconsistent queue... |
commit | commitdiff | tree |
| 2011-02-13 |
Tim King | 3 heuristics were added to arithmetic. A heuristic... |
commit | commitdiff | tree |
| 2011-01-05 |
Dejan Jovanović | fix for build errors |
commit | commitdiff | tree |
| 2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes.... |
commit | commitdiff | tree |
| 2010-12-17 |
Morgan Deters | tls.h, rational.h, and integer.h are only re-generated... |
commit | commitdiff | tree |
| 2010-12-16 |
Morgan Deters | minor fixes for correct doxygen output |
commit | commitdiff | tree |
| 2010-12-14 |
Morgan Deters | make some CC module methods private that should not... |
commit | commitdiff | tree |
| 2010-12-14 |
Morgan Deters | congruence closure module now supports things other... |
commit | commitdiff | tree |
| 2010-12-14 |
Morgan Deters | permit PARAMETERIZED operators to be zero-ary |
commit | commitdiff | tree |
| 2010-12-14 |
Morgan Deters | fix to static learning application in UF, resolves... |
commit | commitdiff | tree |
| 2010-11-24 |
Dejan Jovanović | Changin the get() semantics to a CDQeue-sque semantics. |
commit | commitdiff | tree |
| 2010-11-19 |
Morgan Deters | Merge from ufprop branch, including: |
commit | commitdiff | tree |
| 2010-11-19 |
Morgan Deters | add statistics support information to --show-config |
commit | commitdiff | tree |
| 2010-11-18 |
Morgan Deters | small changes to documentation; also, '\''make doc... |
commit | commitdiff | tree |
| 2010-11-17 |
Morgan Deters | fix improper CongruenceClosureWhite test by merging... |
commit | commitdiff | tree |
| 2010-11-17 |
Morgan Deters | add some stats to UF/CC |
commit | commitdiff | tree |
| 2010-11-17 |
Morgan Deters | The "UF engineering issues" release, after much profiling. |
commit | commitdiff | tree |
| 2010-11-16 |
Tim King | Added Theory::presolve(). |
commit | commitdiff | tree |
| 2010-11-16 |
Morgan Deters | SmtEngine now fails with a ModalException if --incremen... |
commit | commitdiff | tree |
| 2010-11-16 |
Morgan Deters | fix function signatures |
commit | commitdiff | tree |
| 2010-11-15 |
Morgan Deters | cleanup from today's commits: delegate as-yet-unimpleme... |
commit | commitdiff | tree |
| 2010-11-15 |
Tim King | Changes to Solver and PropEngine to support lemmasOnDem... |
commit | commitdiff | tree |
| 2010-11-15 |
Morgan Deters | Pretty-printer infrastructure created (in src/printer... |
commit | commitdiff | tree |
| 2010-11-15 |
Tim King | This commit merges the arith-prop-opt branch into the... |
commit | commitdiff | tree |
| 2010-11-15 |
Morgan Deters | minor tweaks to last commit, testing infrastructure |
commit | commitdiff | tree |
| 2010-11-15 |
Morgan Deters | fix some things with the build system (make dist, make... |
commit | commitdiff | tree |
| 2010-11-12 |
Dejan Jovanović | Some bug fixes in the SAT for lemmas, and an experiment... |
commit | commitdiff | tree |
| 2010-11-11 |
Morgan Deters | make addsourcedir executable |
commit | commitdiff | tree |
| 2010-11-09 |
Dejan Jovanović | Lemmas on demand work, push-pop, some cleanup. |
commit | commitdiff | tree |
| 2010-11-08 |
Morgan Deters | command-line flag to disable theory registration, also... |
commit | commitdiff | tree |
| 2010-11-08 |
Morgan Deters | cleanup, documentation, SMT-LIBv2 compliance |
commit | commitdiff | tree |
| 2010-11-08 |
Morgan Deters | fix out-of-date version/copyright for minisats |
commit | commitdiff | tree |
| 2010-11-05 |
Christopher... | Moving Options fiddling to options.h |
commit | commitdiff | tree |
| 2010-11-04 |
Morgan Deters | competition mode implies --no-checking |
commit | commitdiff | tree |
| 2010-11-04 |
Tim King | Moving the post_mortem.py script out of contrib and... |
commit | commitdiff | tree |
| 2010-11-04 |
Tim King | Updates post_mortem.py script to be able to handle... |
commit | commitdiff | tree |
| 2010-11-04 |
Tim King | This commit adds the ejected and un-ejected statistics. |
commit | commitdiff | tree |
| 2010-11-03 |
Tim King | Adds size() to RowVector. |
commit | commitdiff | tree |
| 2010-11-03 |
Tim King | Adds statistics for the number of Uservariables and... |
commit | commitdiff | tree |
| 2010-11-03 |
Tim King | Adds AverageStat to stats.h. |
commit | commitdiff | tree |
| 2010-10-31 |
Morgan Deters | small fix to debug segfaults |
commit | commitdiff | tree |
| 2010-10-31 |
Morgan Deters | enable dependence graphs in doxygen; fix lots of doxyge... |
commit | commitdiff | tree |
| 2010-10-31 |
Morgan Deters | maximize stack limit, handle SEGV signals on an alterna... |
commit | commitdiff | tree |
| 2010-10-30 |
Tim King | Adds a hueristic from Alberto's thesis. For a fixed... |
commit | commitdiff | tree |
| 2010-10-29 |
Tim King | Fix for a problem caused by using a != instead of ... |
commit | commitdiff | tree |
| 2010-10-29 |
Morgan Deters | portability updates to build system |
commit | commitdiff | tree |
| 2010-10-29 |
Tim King | Adds a very small test that triggers a bug. The bug... |
commit | commitdiff | tree |
| 2010-10-29 |
Morgan Deters | minor fixes as a result of review of Chris's getType... |
commit | commitdiff | tree |
| 2010-10-29 |
Tim King | Fixes RowVector::has(). |
commit | commitdiff | tree |
| 2010-10-29 |
Tim King | Factors out the QF_LRA decision procedure from TheoryAr... |
commit | commitdiff | tree |
| 2010-10-28 |
Tim King | The Row implementation has no been replaced by RowVecto... |
commit | commitdiff | tree |
| 2010-10-28 |
Christopher... | Changing NodeBuilder::debugCheckType() to maybeCheckType() |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog