Age | Commit message (Expand) | Author |
2012-06-06 | Fixed broken test case, removed one that is a mistake | Clark Barrett |
2012-06-06 | unconstrained regressions are now run with "make check", but with --unconstra... | Morgan Deters |
2012-06-06 | Fixing numerous issues with tests and "make dist": | Morgan Deters |
2012-06-06 | Changes to the combination mechanism, lots of details. Not done yet, there ar... | Dejan Jovanović |
2012-06-04 | Added preprocessing pass that propagates unconstrained values - solves all of | Clark Barrett |
2012-05-22 | This commit merges in the branch arithmetic/cprop. | Tim King |
2012-05-19 | Adding regress test for bug 341. | Tim King |
2012-05-19 | - The array type rules were fixed to use isSubtypeOf. | Tim King |
2012-05-18 | This commit adds TypeNode::leastCommonTypeNode(). The special case for arith... | Tim King |
2012-05-18 | removing failing regression | Dejan Jovanović |
2012-05-17 | Fixing an issue with LogicInfo::isPure() that turned off simplification in QF... | Morgan Deters |
2012-05-17 | Fixed bug 338: | Liana Hadarean |
2012-05-17 | Adding failing regression for ite type computation. | Tim King |
2012-05-16 | testcase for bug 337 | Dejan Jovanović |
2012-05-15 | test cases | Dejan Jovanović |
2012-05-15 | Implement TypeNode::isComparableTo() and add a unit test for it. | Morgan Deters |
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-14 | Fixed assertion failures in array theory | Clark Barrett |
2012-05-09 | * simplifying equality engine interface | 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-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-24 | This commit merges in the branch branches/arithmetic/congruence into trunk. H... | Tim King |
2012-04-18 | add the missing BINARY variable in some test/regress makefiles | Kshitij Bansal |
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-04-06 | * Smt2 printer for datatypes | François Bobot |
2012-04-05 | Support to test the "dumper" mechanism in regressions (feeding dump output ba... | Morgan Deters |
2012-04-04 | * added propagation as lemmas to TheoryBV: | Liana Hadarean |
2012-04-02 | Fix for broken unit tests from the previous commit. | Tim King |
2012-04-02 | - Merged in the branch cdlist-cleanup. | Tim King |
2012-04-02 | Removing large and unused regress2 benchmarks to decrease the size of checkouts. | Tim King |
2012-03-26 | More cleaning up. | Dejan Jovanović |
2012-03-26 | forgot to commit this one, fixing build errors | Dejan Jovanović |
2012-03-22 | some improvements to the sharing mechanism/interface | Dejan Jovanović |
2012-03-09 | minor fixes: to "make dist" in build directories with language bindings enabl... | Morgan Deters |
2012-03-08 | Removing QUICK_CHECK, and other unused ones, from the Theory::Effort. | Dejan Jovanović |
2012-03-02 | CDMap -> CDHashMap | Dejan Jovanović |
2012-03-01 | Partial merge from kind-backend branch, including Minisat and CNF work to | Morgan Deters |
2012-02-29 | fixing bug310 | Dejan Jovanović |
2012-02-25 | Refactored CnfStream to work with the bv theory Bitblaster: | Liana Hadarean |
2012-02-22 | Added OutputChannel::propagateAsDecision() functionality, allowing a theory | Morgan Deters |
2012-02-21 | Fix for bug303. The problem was with function applications that get normalize... | Dejan Jovanović |
2012-02-20 | portfolio merge | Morgan Deters |
2012-02-16 | Last commit accidentally lacked r2778 and r2779 from integer2. I have manual... | Tim King |
2012-02-15 | This commit merges into trunk the branch branches/arithmetic/integers2 from r... | Tim King |
2012-02-10 | attempt at a fix for the local regression failure (CLN linking issues on oneiric | Morgan Deters |