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