Age | Commit message (Expand) | Author |
2012-05-29 | Enabled SolveEq bv rewrite | Clark Barrett |
2012-05-28 | Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV | Clark Barrett |
2012-05-27 | some reordering to keep invariants | Dejan Jovanović |
2012-05-27 | Committing the work on equality engine, I need to see how it does on the regr... | Dejan Jovanović |
2012-05-27 | Another expensive function call in a Debug trace | Clark Barrett |
2012-05-27 | Another expensive function call in a Debug line | Clark Barrett |
2012-05-25 | init bug fix | Kshitij Bansal |
2012-05-25 | Checking in fix for bug 340 - somehow didn't get checked in earlier | Clark Barrett |
2012-05-24 | Separating the subtheory implementations in the bitvector theory. | Dejan Jovanović |
2012-05-24 | Significant changes to the internals of the equality engine. Equality is not ... | Dejan Jovanović |
2012-05-22 | This commit merges in the branch arithmetic/cprop. | Tim King |
2012-05-21 | Updating equality manager to handle tagged trigger terms. Notifications are p... | Dejan Jovanović |
2012-05-21 | main() no longer catches non-CVC4 exceptions. This means on memout and other... | Morgan Deters |
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 | This commit removes the dead psuedoboolean code. | Tim King |
2012-05-18 | Removing long unsigned operator+ from CDList's const_iterator. | Tim King |
2012-05-17 | This fixes a fascinating segfault. This is the sequence of events: | Tim King |
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 | Queueing up asserted literals in the proxy instead of sending them off to the... | Dejan Jovanović |
2012-05-16 | adding simple-minded handling of (dis-)equalities where constants are involved | Dejan Jovanović |
2012-05-16 | Fixing C compatibility library (it still had a reference to CONST_INTEGER). | Morgan Deters |
2012-05-16 | Changes to SAT solver: | Dejan Jovanović |
2012-05-16 | equality status for bitvectors can now look into the sat solver to check for ... | Dejan Jovanović |
2012-05-16 | removing duplicate literals in explanations of propagations | Dejan Jovanović |
2012-05-16 | refactored TheoryBV bitblaster and equality engine into subtheories (similar ... | Liana Hadarean |
2012-05-15 | fixed QF_BV performance problem due to using CDList instead of CDQueue | Liana Hadarean |
2012-05-15 | Fix to shared terms visitor. | Tim King |
2012-05-15 | Implement TypeNode::isComparableTo() and add a unit test for it. | Morgan Deters |
2012-05-15 | Fixed several bugs in shared terms database | Clark Barrett |
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 |