cvc5.git
2011-04-05 Morgan DetersMemory fix for congruence closure; affects many UF...
2011-04-05 Tim KingAdded options for setting the random decision frequency...
2011-04-05 Morgan DetersMinor adjustments to the Registrar commit in 1644,...
2011-04-04 Tim KingMerging the satliteral-before-prereg branch into trunk...
2011-04-04 Tim KingReverts previous commit r1636.
2011-04-04 Morgan DetersAdd documentation to Node and TNode (closes bug #201).
2011-04-02 Tim KingDelayed the addition of unate propagation lemmas until...
2011-04-02 Morgan Deterswith --with-google-perftools, don't just take it on...
2011-04-02 Morgan Detersminor fixes
2011-04-01 Morgan Detersminor bugfixes (fixes broken dynamic-library build...
2011-04-01 Morgan Detersdocumentation fix
2011-04-01 Morgan DetersThis commit is a merge from the "betterstats" branch...
2011-03-31 Tim KingFixes to Valuation.
2011-03-30 Morgan Detersimprove recent low-coverage complaints
2011-03-30 Dejan Jovanovićadding CVC4:: qualifier to the #define for debugging...
2011-03-30 Tim KingMoved the constructor for Options out of the header...
2011-03-30 Tim KingAdded the command line flag --rewrite-arithmetic-equali...
2011-03-30 Morgan DetersAdd Valuation::getSatValue() so that theories can acces...
2011-03-30 Tim KingMerged the branch sparse-tableau into trunk.
2011-03-27 Morgan Detersfixes to attribute-internals warnings on 64-bit; also...
2011-03-26 Dejan Jovanovićfix for bug 253, was propagating an asserted literal
2011-03-26 Morgan Detersfix typo
2011-03-25 Morgan DetersThis is a merge from the "theoryfixes+cdattrhash" branc...
2011-03-25 Morgan DetersFix for a bug Andrew Reynolds found for iterators that...
2011-03-22 Tim KingMerges the small changes on the queue-period branch...
2011-03-22 Dejan Jovanovićupdating debug output usage to eliviate impact of bug 252
2011-03-21 Dejan Jovanovićmore bugfixes, some basic propagation, and testcases...
2011-03-21 Dejan Jovanovićfixing a bug in the BV rewrite, off by one error when...
2011-03-20 Dejan Jovanovićagain a typo
2011-03-20 Dejan Jovanovićmore bugfixes for bitvectors
2011-03-20 Dejan Jovanovićfixing the failure from last nigth, due to using a...
2011-03-20 Dejan Jovanovićmissed one case
2011-03-20 Dejan Jovanovićcommit for the version of bitvectors that passes all...
2011-03-19 Tim KingMerges the pqueue-set branch into trunk. During VarOrd...
2011-03-18 Tim King- The learned clauses from the miplib trick were being...
2011-03-17 Tim KingSwitched SimplexDecisionProcedure::d_delayedLemmas...
2011-03-17 Tim KingSimplexDecisionProcedure no longer takes an OutputChann...
2011-03-17 Tim King- Removes arith_constants.h
2011-03-17 Tim KingAdds debugging output to EngineOutputChannel::lemma.
2011-03-17 Tim KingFix for the bug introduced in 1477. The stuff that...
2011-03-17 Dejan Jovanovićpush and pop manipulators for output stream so that...
2011-03-16 Tim King- Turns on the excluded middle assertions during the...
2011-03-16 Tim King- Turns on the miplibTrick. This detects during the...
2011-03-15 Dejan Jovanovićreal fix for bug 245, previous one was faulty
2011-03-15 Morgan Deterssmall fixes for run_regression script to workaround...
2011-03-15 Dejan Jovanovićfix for bug 254, lemmas were propagating at lower level...
2011-03-15 Morgan DetersMerge from cudd branch. This mostly just adds support...
2011-03-14 Dejan Jovanovićadding support for google performance tools to the...
2011-03-14 Morgan Deterschange to the run_regression script to better manage...
2011-03-14 Morgan DetersFix to bug 251 (non-spurious warnings in builds) by...
2011-03-10 Morgan DetersFix bug 246 (occasional buffer overflow related to...
2011-03-10 Morgan DetersITE removal in TheoryEngine was not properly handling...
2011-03-08 Morgan DetersClean up Theory base class as per code review bug ...
2011-03-08 Tim King- Merges queue-interrogation branch into the trunk...
2011-03-07 Tim KingMerges branches/arithmetic/tableau-reset into the trunk...
2011-03-05 Tim King- Adds PermissiveBackArithVarSet. This is very similar...
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:
next