summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-02-17Removed ActivityMonitor from arithmetic. This was only used for row ejection,...Tim King
2011-02-17Row ejection is now completely disabled. Another commit cleaning this one up ...Tim King
2011-02-17Removed vestigial normal form notes file from src/theory/arith/Makefile.am. S...Tim King
2011-02-17some unit tests to work on slicingDejan Jovanović
2011-02-17I replaced the pattern "x = x + y;" with "x += y;" in a few places in DeltaRa...Tim King
2011-02-17Updates based on the group code review of arithmetic on 2011-02-15. The only...Tim King
2011-02-17Deleting depricated files.Tim King
2011-02-17getting ready for slicing bitvectorsDejan Jovanović
2011-02-16Overview of the changes:Tim King
2011-02-16updates for the rewriter, added some statisticsDejan Jovanović
2011-02-14Reverses the order of the d_possiblyInconsistent queue. (It is that old termi...Tim King
2011-02-133 heuristics were added to arithmetic. A heuristic for detecting an encoding ...Tim King
2011-01-05fix for build errorsDejan Jovanović
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-12-17tls.h, rational.h, and integer.h are only re-generated if changed. this obvi...Morgan Deters
2010-12-16minor fixes for correct doxygen outputMorgan Deters
2010-12-14make some CC module methods private that should not have been publicMorgan Deters
2010-12-14congruence closure module now supports things other than APPLY_UF; ported fro...Morgan Deters
2010-12-14permit PARAMETERIZED operators to be zero-aryMorgan Deters
2010-12-14fix to static learning application in UF, resolves bug# 239Morgan Deters
2010-11-24Changin the get() semantics to a CDQeue-sque semantics. Dejan Jovanović
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-11-19add statistics support information to --show-configMorgan Deters
2010-11-18small changes to documentation; also, '\''make doc'\'' doesn't build dot grap...Morgan Deters
2010-11-17fix improper CongruenceClosureWhite test by merging from a uf branch; fixes t...Morgan Deters
2010-11-17add some stats to UF/CCMorgan Deters
2010-11-17The "UF engineering issues" release, after much profiling.Morgan Deters
2010-11-16Added Theory::presolve().Tim King
2010-11-16SmtEngine now fails with a ModalException if --incremental is not enabledMorgan Deters
2010-11-16fix function signaturesMorgan Deters
2010-11-15cleanup from today's commits: delegate as-yet-unimplemented prettyprinters in...Morgan Deters
2010-11-15Changes to Solver and PropEngine to support lemmasOnDemand during solve but n...Tim King
2010-11-15Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printerMorgan Deters
2010-11-15This commit merges the arith-prop-opt branch into the main trunk. This was do...Tim King
2010-11-15minor tweaks to last commit, testing infrastructureMorgan Deters
2010-11-15fix some things with the build system (make dist, make install, make check)Morgan Deters
2010-11-12Some bug fixes in the SAT for lemmas, and an experiment with a more complete ...Dejan Jovanović
2010-11-11make addsourcedir executableMorgan Deters
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-11-08command-line flag to disable theory registration, also SMT-LIBv2 compliance (...Morgan Deters
2010-11-08cleanup, documentation, SMT-LIBv2 complianceMorgan Deters
2010-11-08fix out-of-date version/copyright for minisatsMorgan Deters
2010-11-05Moving Options fiddling to options.hChristopher L. Conway
2010-11-04competition mode implies --no-checkingMorgan Deters
2010-11-04Moving the post_mortem.py script out of contrib and into the cvc4 scripts dir...Tim King
2010-11-04Updates post_mortem.py script to be able to handle certain kinds of crashes a...Tim King
2010-11-04This commit adds the ejected and un-ejected statistics.Tim King
2010-11-03Adds size() to RowVector.Tim King
2010-11-03Adds statistics for the number of Uservariables and Slack variables used by a...Tim King
2010-11-03Adds AverageStat to stats.h.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback