Age | Commit message (Expand) | Author |
2013-01-25 | Fix errors and reduce warnings on clang (merge from mdeters/clang) | Morgan Deters |
2013-01-24 | Add win32 support (merge from mdeters/win32, with some cleanup). | Morgan Deters |
2012-12-01 | remove instantiator framework | Morgan Deters |
2012-12-01 | drastic simplification of quantifiers code regarding equality queries, instan... | Andrew Reynolds |
2012-11-26 | Adding support for a master equality engine. Each theory gets the master equa... | Dejan Jovanović |
2012-11-17 | * Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT... | Morgan Deters |
2012-11-15 | Fixed another AUFBV model bug. BV equality subtheory needed to do something | Clark Barrett |
2012-11-08 | Review of trunk r4525 (TypeNode::getBaseType()): | Morgan Deters |
2012-10-31 | cleaning up some of the equality query stuff, implemented a new representativ... | Andrew Reynolds |
2012-10-19 | Fix for model building with shared terms for arithmetic. | Tim King |
2012-10-16 | more cleanup of quantifiers code | Andrew Reynolds |
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
2012-09-22 | Separate public-facing and internal-facing interfaces to Statistics. | Morgan Deters |
2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
2012-08-16 | Replace propagateAsDecision() with Theory::getNextDecisionRequest(): | Morgan Deters |
2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use isCon... | Morgan Deters |
2012-07-31 | Options merge. This commit: | Morgan Deters |
2012-07-27 | merging fmf-devel branch, includes refactored datatype theory, updates to mod... | Andrew Reynolds |
2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
2012-06-16 | changing theoryOf in shared mode with arrays to move equalities to arrays | Dejan Jovanović |
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 |