| Age | Commit message (Expand) | Author |
|---|
| 2012-05-14 | fixing up preregistration again | Dejan Jovanović |
| 2012-05-13 | fixing build warnings | Dejan Jovanović |
| 2012-05-11 | fix regex in Debug_tags and Trace_tags generation for Mac OS | Morgan Deters |
| 2012-05-11 | fix typo in sed line | Morgan Deters |
| 2012-05-11 | output a warning message when a function type (or datatype, or array, etc.) i... | Morgan Deters |
| 2012-05-11 | Disabled arith-rewrite-equalities by default unless in a pure arithmetic theory | Clark Barrett |
| 2012-05-11 | Added some ITE rewrites, | Clark Barrett |
| 2012-05-11 | Partially fixes something-like-a-problem with TheoryArith::getDeltaValue(). | Tim King |
| 2012-05-10 | Removing now unneeded (as of r3425) typenames from EqualityEngine. trunk now ... | Tim King |
| 2012-05-09 | fix an issue which breaks language bindings (so this commit fixes debian nigh... | Morgan Deters |
| 2012-05-09 | --disable-tracing at configure time now disables Trace() and Debug() gestures... | Morgan Deters |
| 2012-05-09 | * simplifying equality engine interface | Dejan Jovanović |
| 2012-05-09 | rm something for a future merge that sneaked in | Kshitij Bansal |
| 2012-05-09 | Merge from decision branch (ITE support) | Kshitij Bansal |
| 2012-05-09 | Fixing the debug tags generation and related methods in configuration.cpp tha... | Dejan Jovanović |
| 2012-05-08 | Merging in bvprop branch, with proper bit-vector propagation. | Liana Hadarean |
| 2012-05-07 | Fixing a bug with TheoryArith::ppAssert() and shared terms. | Tim King |
| 2012-05-07 | Fixes a sign bug in the DioSolver. | Tim King |
| 2012-05-04 | Guard for expensive Debug trace | Clark Barrett |
| 2012-05-04 | options: fail if the debug or trace tag specified doesn't exist (-d -t) | François Bobot |
| 2012-05-04 | fix: getNumTraceTags, getNumDebugTags | François Bobot |
| 2012-05-04 | - This fixes a problem where simplex produced the same conflict in the single... | Tim King |
| 2012-05-03 | Some cleanup starting off from trying to understand the sharing code. Changes... | Dejan Jovanović |
| 2012-05-02 | Changing d_sharedTermsExist to logicInfo.isSharingEnabled() | Clark Barrett |
| 2012-04-30 | Added map from skolem variables to new ite formulas in ite removal. | Clark Barrett |
| 2012-04-28 | New LogicInfo functionality. | Morgan Deters |
| 2012-04-28 | undo, again | Morgan Deters |
| 2012-04-28 | adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to the theory enumeration m... | Morgan Deters |
| 2012-04-27 | undo previous commit (as it will break a number of things without additional ... | Morgan Deters |
| 2012-04-27 | adding THEORY_QUANTIFIERS and THEORY_REWRITERULES to the theory enumeration m... | Morgan Deters |
| 2012-04-27 | fix parser logic-handling oversights: QF_UFBV should now be supported | Morgan Deters |
| 2012-04-27 | break dependence on zlib-dev for now | Morgan Deters |
| 2012-04-27 | Fixed warning in decision_engine.h, minor tweak to caregraph function in | Clark Barrett |
| 2012-04-27 | This merges in the branch cvc4/branches/arithmetic/matrix into trunk. | Tim King |
| 2012-04-25 | portfolio driver: respect parseOnly option | Kshitij Bansal |
| 2012-04-25 | fix for de+lemmas | Kshitij Bansal |
| 2012-04-24 | This commit merges in the branch branches/arithmetic/congruence into trunk. H... | Tim King |
| 2012-04-23 | Merge from decision branch -- partially working justification heuristic | Kshitij Bansal |
| 2012-04-20 | Updates to array theory - much more lazy about introduction of reads | Clark Barrett |
| 2012-04-19 | In the constructor of DecisionEngine, there were 2 pointers that were assumed... | Tim King |
| 2012-04-18 | cout -> warning. Happening in portfolio | Kshitij Bansal |
| 2012-04-18 | disabling the problematic pragma in node_manager.h on gcc < 4.6 until we figu... | Dejan Jovanović |
| 2012-04-17 | Fix for thos annoying "array index" warnings in production builds | Dejan Jovanović |
| 2012-04-17 | A dummy decision engine. Expected performance impact: none. | Kshitij Bansal |
| 2012-04-17 | Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo... | Tim King |
| 2012-04-14 | Fixed bug in sharing with arrays of different types | Clark Barrett |
| 2012-04-13 | Fix SExpr name qualification for swig, and #include integer and rational head... | Morgan Deters |
| 2012-04-12 | Adds an operator<< to SExpr::SexprTypes. This fixes bug 317. In debug builds,... | Tim King |
| 2012-04-11 | merge from arrays-clark branch | Morgan Deters |
| 2012-04-06 | * Smt2 printer for datatypes | François Bobot |
