Age | Commit message (Expand) | Author |
2012-06-11 | Merge from quantifiers2-trunkmerge branch. | Morgan Deters |
2012-06-07 | fixing some bugs in propagation of disequalities | Dejan Jovanović |
2012-05-21 | Updating equality manager to handle tagged trigger terms. Notifications are p... | Dejan Jovanović |
2012-05-14 | fixes for shared term registration. previously the type was not considered wh... | Dejan Jovanović |
2012-05-03 | Some cleanup starting off from trying to understand the sharing code. Changes... | Dejan Jovanović |
2012-04-28 | New LogicInfo functionality. | Morgan Deters |
2012-04-17 | Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo... | Tim King |
2012-04-11 | merge from arrays-clark branch | Morgan Deters |
2012-03-22 | some improvements to the sharing mechanism/interface | Dejan Jovanović |
2012-03-09 | Some work on the dump infrastructure to support portfolio work. | Morgan Deters |
2012-03-08 | Removing QUICK_CHECK, and other unused ones, from the Theory::Effort. | Dejan Jovanović |
2012-03-01 | Partial merge from kind-backend branch, including Minisat and CNF work to | Morgan Deters |
2012-02-25 | ppAsert -> ppAssert | Dejan Jovanović |
2012-02-24 | Theory interface changes: | Dejan Jovanović |
2012-02-23 | Added ability to set a "cvc4-specific logic" in standards-compliant | Morgan Deters |
2012-02-21 | Fix for bug303. The problem was with function applications that get normalize... | Dejan Jovanović |
2012-02-20 | Added Theory::postsolve() infrastructure as Clark requested. | Morgan Deters |
2012-02-13 | precision in theoryskel | François Bobot |
2012-01-23 | fix for bug295 | Dejan Jovanović |
2011-10-17 | Sharing work | Dejan Jovanović |
2011-09-29 | Some base infrastructure for user push/pop; a few bugfixes to user push/pop a... | Morgan Deters |
2011-09-15 | additional stuff for sharing, | Dejan Jovanović |
2011-09-02 | Merge from my post-smtcomp branch. Includes: | Morgan Deters |
2011-09-02 | Partial merge of integers work; this is simple B&B and some pseudoboolean | Morgan Deters |
2011-09-02 | * Changing pre-registration to be context dependent -- it is called from the ... | Dejan Jovanović |
2011-08-27 | Removing Theory::registerTerm() as discussed in the meeting. Now pre-register... | Dejan Jovanović |
2011-08-24 | Simplification of the preregister and register throught a NodeVisitor class. ... | Dejan Jovanović |
2011-07-12 | fix bug 272, array unsoundness, and some array cleanup | Morgan Deters |
2011-07-11 | fix some confusing debug output (bogus counter) | Morgan Deters |
2011-07-10 | Reverting mistaken check-in | Clark Barrett |
2011-07-10 | Fixed bug in default solve - wasn't returning when it was supposed to | Clark Barrett |
2011-07-05 | updated preprocessing and rewriting input equalities into inequalities for LRA | Dejan Jovanović |
2011-05-13 | * fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio | Morgan Deters |
2011-05-05 | Merge from nonclausal-simplification-v2 branch: | Morgan Deters |
2011-04-20 | Tuesday end-of-day commit. | Morgan Deters |
2011-04-01 | This commit is a merge from the "betterstats" branch, which: | Morgan Deters |
2011-03-25 | This is a merge from the "theoryfixes+cdattrhash" branch. The changes | Morgan Deters |
2011-03-08 | Clean up Theory base class as per code review bug #60; also fixes to CodeTime... | Morgan Deters |
2011-02-27 | - Adds a path for Theory to be passed a reference to Options. | Tim King |
2011-02-26 | Merge from theory-break-dependences branch to break Theory and TheoryEngine d... | Morgan Deters |
2011-01-05 | Commit for the theory engine and rewriter changes. Changes are substantial an... | Dejan Jovanović |
2010-11-24 | Changin the get() semantics to a CDQeue-sque semantics. | Dejan Jovanović |
2010-11-19 | Merge from ufprop branch, including: | Morgan Deters |
2010-11-16 | Added Theory::presolve(). | Tim King |
2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters |
2010-10-03 | file header documentation regenerated with contributors names; no code modifi... | Morgan Deters |
2010-08-19 | UF theory bug fixes, code cleanup, and extra debugging output. | Morgan Deters |
2010-07-07 | Shared term manager tested and working | Clark Barrett |
2010-07-07 | Added shared term manager. Basic mechanism for identifying shared terms is | Clark Barrett |
2010-07-06 | Moved registration to theory engine | Clark Barrett |