Age | Commit message (Expand) | Author |
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 |
2010-07-04 | With "-d extra-checking", rewrites are now checked (after | Morgan Deters |
2010-07-02 | * Added white-box TheoryEngine test that tests the rewriter | Morgan Deters |
2010-06-30 | * theory "tree" rewriting implemented and works | Morgan Deters |
2010-06-29 | Merging the unate-propagator branch into the trunk. This is a big update so ... | Tim King |
2010-06-15 | I made a documentation change to get() to make explicit the contract requirem... | Tim King |
2010-06-04 | ** Don't fear the files-changed list, almost all changes are in the ** | Morgan Deters |
2010-04-04 | * Node::isAtomic() now looks at an "atomic" attribute of arguments | Morgan Deters |
2010-04-01 | PARSER STUFF: | Morgan Deters |
2010-03-30 | Highlights of this commit are: | Morgan Deters |
2010-03-12 | * Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine, | Morgan Deters |