cvc5.git
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:
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...
next