| Age | Commit message (Expand) | Author |
|---|
| 2012-05-15 | This commit removes the CONST_INTEGER kind from nodes. This code comes from t... | Tim King |
| 2012-05-15 | renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectively | Liana Hadarean |
| 2012-05-15 | removing all extended commands (as inspired by the Z3 extended command set) e... | Morgan Deters |
| 2012-05-15 | Fix QF_AUFLIA (resolves bug #331). | Morgan Deters |
| 2012-05-15 | fixing warnings, grr | Dejan Jovanović |
| 2012-05-15 | several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify a... | Liana Hadarean |
| 2012-05-14 | fixes for shared term registration. previously the type was not considered wh... | Dejan Jovanović |
| 2012-05-14 | Fixed assertion failures in array theory | Clark Barrett |
| 2012-05-14 | in debug builds, -d can be used for trace tags that aren't also debug tags | Morgan Deters |
| 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 | require boost library (but not the threading support---that's only necessary ... | 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 |
