git.libre-soc.org Git - cvc5.git/history - src/theory/arith/theory

[cvc5.git] / src / theory / arith / theory_arith.h

2011-04-18	Tim King	This commit merges the branch arithmetic/propagation...	blob \| commitdiff \| raw
2011-04-04	Tim King	Reverts previous commit r1636.	blob \| commitdiff \| raw \| diff to current
2011-04-02	Tim King	Delayed the addition of unate propagation lemmas until...	blob \| commitdiff \| raw \| diff to current
2011-04-01	Morgan Deters	This commit is a merge from the "betterstats" branch...	blob \| commitdiff \| raw \| diff to current
2011-03-30	Tim King	Merged the branch sparse-tableau into trunk.	blob \| commitdiff \| raw \| diff to current
2011-03-25	Morgan Deters	This is a merge from the "theoryfixes+cdattrhash" branc...	blob \| commitdiff \| raw \| diff to current
2011-03-17	Tim King	SimplexDecisionProcedure no longer takes an OutputChann...	blob \| commitdiff \| raw \| diff to current
2011-03-17	Tim King	- Removes arith_constants.h	blob \| commitdiff \| raw \| diff to current
2011-03-15	Morgan Deters	Merge from cudd branch. This mostly just adds support...	blob \| commitdiff \| raw \| diff to current
2011-03-07	Tim King	Merges branches/arithmetic/tableau-reset into the trunk...	blob \| commitdiff \| raw \| diff to current
2011-03-03	Tim King	Merged the tableau-copy branch into trunk. This adds...	blob \| commitdiff \| raw \| diff to current
2011-02-27	Tim King	- Adds a path for Theory to be passed a reference to...	blob \| commitdiff \| raw \| diff to current
2011-02-26	Morgan Deters	Merge from theory-break-dependences branch to break...	blob \| commitdiff \| raw \| diff to current
2011-02-19	Tim King	Changes:	blob \| commitdiff \| raw \| diff to current
2011-02-18	Tim King	Changes:	blob \| commitdiff \| raw \| diff to current
2011-02-17	Tim King	Removed ActivityMonitor from arithmetic. This was only...	blob \| commitdiff \| raw \| diff to current
2011-02-16	Tim King	Overview of the changes:	blob \| commitdiff \| raw \| diff to current
2011-02-13	Tim King	3 heuristics were added to arithmetic. A heuristic...	blob \| commitdiff \| raw \| diff to current
2011-01-05	Dejan Jovanović	Commit for the theory engine and rewriter changes....	blob \| commitdiff \| raw \| diff to current
2010-11-16	Tim King	Added Theory::presolve().	blob \| commitdiff \| raw \| diff to current
2010-11-15	Tim King	This commit merges the arith-prop-opt branch into the...	blob \| commitdiff \| raw \| diff to current
2010-11-09	Dejan Jovanović	Lemmas on demand work, push-pop, some cleanup.	blob \| commitdiff \| raw \| diff to current
2010-10-29	Tim King	Factors out the QF_LRA decision procedure from TheoryAr...	blob \| commitdiff \| raw \| diff to current
2010-10-23	Tim King	Removed slack.h, and arith_activity.h. Replaced IsBasic...	blob \| commitdiff \| raw \| diff to current
2010-10-22	Tim King	Code cleanup for TheoryArith.	blob \| commitdiff \| raw \| diff to current
2010-10-09	Morgan Deters	Model generation for arith, boolean, and uf theories via	blob \| commitdiff \| raw \| diff to current
2010-10-02	Tim King	branches/arith-indexed-variables merged into the main...	blob \| commitdiff \| raw \| diff to current
2010-09-21	Morgan Deters	part of review (bug #197): coding conventions, file...	blob \| commitdiff \| raw \| diff to current
2010-09-13	Tim King	* New normal form for arithmetic is in place.	blob \| commitdiff \| raw \| diff to current
2010-07-07	Clark Barrett	Added shared term manager. Basic mechanism for identif...	blob \| commitdiff \| raw \| diff to current
2010-07-04	Morgan Deters	With "-d extra-checking", rewrites are now checked...	blob \| commitdiff \| raw \| diff to current
2010-06-30	Morgan Deters	* theory "tree" rewriting implemented and works	blob \| commitdiff \| raw \| diff to current
2010-06-29	Tim King	This commit merges the decaying-rows branch into the...	blob \| commitdiff \| raw \| diff to current
2010-06-29	Tim King	Merging the unate-propagator branch into the trunk...	blob \| commitdiff \| raw \| diff to current
2010-06-18	Tim King	Merging the statistics branch into the main trunk....	blob \| commitdiff \| raw \| diff to current
2010-06-16	Tim King	Added the experimental. +bool TheoryArith::AssertEquali...	blob \| commitdiff \| raw \| diff to current
2010-06-16	Tim King	More assorted changes to arithmetic in preparation...	blob \| commitdiff \| raw \| diff to current
2010-06-06	Tim King	Some assorted fixes and local optimizations for theory...	blob \| commitdiff \| raw \| diff to current
2010-06-04	Tim King	Changed how assignments are saved during check. These...	blob \| commitdiff \| raw \| diff to current
2010-06-04	Morgan Deters	** Don't fear the files-changed list, almost all change...	blob \| commitdiff \| raw \| diff to current
2010-06-03	Tim King	Fixes 2 issues with assignments. The first is construct...	blob \| commitdiff \| raw \| diff to current
2010-05-27	Tim King	Preregistration has been turned on. Highly experimental...	blob \| commitdiff \| raw \| diff to current
2010-05-20	Tim King	Added the division symbol to the parser, and minimal...	blob \| commitdiff \| raw \| diff to current
2010-05-19	Tim King	Significant revision to theory/arith. The new draft...	blob \| commitdiff \| raw \| diff to current
2010-04-28	Tim King	Merging the arithmetic theory draft (lra-init) back...	blob \| commitdiff \| raw \| diff to current
2010-04-04	Morgan Deters	* Node::isAtomic() now looks at an "atomic" attribute...	blob \| commitdiff \| raw \| diff to current
2010-02-26	Morgan Deters	* test/unit/context/context_black.h: Test CDList<>...	blob \| commitdiff \| raw \| diff to current
2010-02-25	Morgan Deters	* src/expr/node.h: add a copy constructor. Apparently...	blob \| commitdiff \| raw \| diff to current

RSS Atom