git.libre-soc.org Git - cvc5.git/search

2011-04-02	Tim King	Delayed the addition of unate propagation lemmas until...	commit \| commitdiff \| tree
2011-03-31	Tim King	Fixes to Valuation.	commit \| commitdiff \| tree
2011-03-30	Tim King	Moved the constructor for Options out of the header...	commit \| commitdiff \| tree
2011-03-30	Tim King	Added the command line flag --rewrite-arithmetic-equalities...	commit \| commitdiff \| tree
2011-03-30	Tim King	Merged the branch sparse-tableau into trunk.	commit \| commitdiff \| tree
2011-03-22	Tim King	Merges the small changes on the queue-period branch...	commit \| commitdiff \| tree
2011-03-19	Tim King	Merges the pqueue-set branch into trunk. During VarOrder...	commit \| commitdiff \| tree
2011-03-18	Tim King	- The learned clauses from the miplib trick were being...	commit \| commitdiff \| tree
2011-03-17	Tim King	Switched SimplexDecisionProcedure::d_delayedLemmas...	commit \| commitdiff \| tree
2011-03-17	Tim King	SimplexDecisionProcedure no longer takes an OutputChannel...	commit \| commitdiff \| tree
2011-03-17	Tim King	- Removes arith_constants.h	commit \| commitdiff \| tree
2011-03-17	Tim King	Adds debugging output to EngineOutputChannel::lemma.	commit \| commitdiff \| tree
2011-03-17	Tim King	Fix for the bug introduced in 1477. The stuff that...	commit \| commitdiff \| tree
2011-03-16	Tim King	- Turns on the excluded middle assertions during the...	commit \| commitdiff \| tree
2011-03-16	Tim King	- Turns on the miplibTrick. This detects during the...	commit \| commitdiff \| tree
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-03	Tim King	- Creates a queue for lemmas discovered during the...	commit \| commitdiff \| tree
2011-03-03	Tim King	Merged the tableau-copy branch into trunk. This adds...	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 addRowTimesConstant...	commit \| commitdiff \| tree
2011-02-26	Tim King	- Merged RowVector and ReducedRowVector.	commit \| commitdiff \| tree
2011-02-25	Tim King	- This commit adds some debugging information to ArithPriori...	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, Collection...	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 ArithPriorityQueue...	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/theory...	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-16	Tim King	Overview of the changes:	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
2010-11-16	Tim King	Added Theory::presolve().	commit \| commitdiff \| tree
2010-11-15	Tim King	Changes to Solver and PropEngine to support lemmasOnDemand...	commit \| commitdiff \| tree
2010-11-15	Tim King	This commit merges the arith-prop-opt branch into the...	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-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	Tim King	Adds a very small test that triggers a bug. The bug...	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 TheoryArith...	commit \| commitdiff \| tree
2010-10-28	Tim King	The Row implementation has no been replaced by RowVector...	commit \| commitdiff \| tree
2010-10-23	Tim King	Removed slack.h, and arith_activity.h. Replaced IsBasicManag...	commit \| commitdiff \| tree
2010-10-22	Tim King	Code cleanup for TheoryArith.	commit \| commitdiff \| tree
2010-10-22	Tim King	Fixes to getValue for TheoryArith.	commit \| commitdiff \| tree
2010-10-14	Tim King	Fixed computation of infinitesimals for arithmetic...	commit \| commitdiff \| tree
2010-10-13	Tim King	Removed vector<Monomial> monos from Polynomial. Now...	commit \| commitdiff \| tree
2010-10-13	Tim King	Added test/regress/regress1/arith and populated it...	commit \| commitdiff \| tree
2010-10-12	Tim King	IDENTITY has been removed.	commit \| commitdiff \| tree
2010-10-07	Tim King	Small tableau optimization.	commit \| commitdiff \| tree
2010-10-04	Tim King	Fix to bug 211. ArithVar is now typedefed to uint32_t.	commit \| commitdiff \| tree
2010-10-02	Tim King	branches/arith-indexed-variables merged into the main...	commit \| commitdiff \| tree
2010-09-27	Tim King	- This update adds DynamicArray<T>. This is a bare...	commit \| commitdiff \| tree
2010-09-16	Tim King	Bug fix to CVC4::theory::arith::VarList as well as...	commit \| commitdiff \| tree
2010-09-14	Tim King	* added test/regress/regress0/arith for easy arithmetic...	commit \| commitdiff \| tree
2010-09-13	Tim King	* New normal form for arithmetic is in place.	commit \| commitdiff \| tree
2010-07-22	Tim King	Added test file for fuzzsmt bug, bug187.smt2.	commit \| commitdiff \| tree
2010-07-08	Tim King	I am adding my smt-crunch scripts to source control...	commit \| commitdiff \| tree
2010-07-08	Tim King	Updates to the post_mortem.py script.	commit \| commitdiff \| tree
2010-07-07	Tim King	Fixes arith rewriter to allow for division by a constant...	commit \| commitdiff \| tree
2010-07-06	Tim King	Fixed exit status for competition mode.	commit \| commitdiff \| tree
2010-07-02	Tim King	Merges the cln-test branch into the main branch.	commit \| commitdiff \| tree
2010-06-29	Tim King	This commit merges the decaying-rows branch into the...	commit \| commitdiff \| tree
2010-06-29	Tim King	Update to stats.h is now back into the trunk. The...	commit \| commitdiff \| tree
2010-06-29	Tim King	Merging the unate-propagator branch into the trunk...	commit \| commitdiff \| tree
2010-06-24	Tim King	Added post_mortem.py a statistics collector for user...	commit \| commitdiff \| tree
2010-06-22	Tim King	Made ~Stat() virtual. Added some additional statistics...	commit \| commitdiff \| tree
2010-06-18	Tim King	Merging the statistics branch into the main trunk....	commit \| commitdiff \| tree
2010-06-16	Tim King	Added the experimental. +bool TheoryArith::AssertEquality...	commit \| commitdiff \| tree
2010-06-16	Tim King	More assorted changes to arithmetic in preparation...	commit \| commitdiff \| tree
2010-06-16	Tim King	This commit just contains miscellaneous arithmetic...	commit \| commitdiff \| tree
2010-06-15	Tim King	I made a documentation change to get() to make explicit...	commit \| commitdiff \| tree
2010-06-14	Tim King	Fix to arith to make sure it only attempts to report...	commit \| commitdiff \| tree
2010-06-06	Tim King	Some assorted fixes and local optimizations for theory...	commit \| commitdiff \| tree
2010-06-06	Tim King	Adding += and *= to Rational.	commit \| commitdiff \| tree
2010-06-04	Tim King	Changed how assignments are saved during check. These...	commit \| commitdiff \| tree
2010-06-04	Tim King	Changed several arguments to const references.	commit \| commitdiff \| tree
2010-06-03	Tim King	Fixes 2 issues with assignments. The first is constructing...	commit \| commitdiff \| tree
2010-06-03	Tim King	Adds toString to DeltaRational	commit \| commitdiff \| tree
2010-06-03	Tim King	Fixes a bug where registration occurs before preregistration.	commit \| commitdiff \| tree
next

RSS Atom