summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2012-06-05Fixed a performance issue with unconstrained simplifierClark Barrett
2012-06-05Adding missing files...Clark Barrett
2012-06-04Added preprocessing pass that propagates unconstrained values - solves all ofClark Barrett
2012-05-31Fixed bug in bv: one more case where non-shared equality was getting propagatedClark Barrett
2012-05-30Added BitwiseEq bitvector rewriteClark Barrett
2012-05-30Fixed problem with array queue growing too largeClark Barrett
2012-05-30remove unused/broken check build targetMorgan Deters
2012-05-29removing now-unused TheoryEngine::setLogic() interface functionMorgan Deters
2012-05-29Enabled SolveEq bv rewriteClark Barrett
2012-05-28Added some BV rewrites, fixed bugs in array theory, made ite simp work with BVClark Barrett
2012-05-27some reordering to keep invariantsDejan Jovanović
2012-05-27Committing the work on equality engine, I need to see how it does on the regr...Dejan Jovanović
2012-05-27Another expensive function call in a Debug lineClark Barrett
2012-05-25init bug fixKshitij Bansal
2012-05-25Checking in fix for bug 340 - somehow didn't get checked in earlierClark Barrett
2012-05-24Separating the subtheory implementations in the bitvector theory.Dejan Jovanović
2012-05-24Significant changes to the internals of the equality engine. Equality is not ...Dejan Jovanović
2012-05-22This commit merges in the branch arithmetic/cprop.Tim King
2012-05-21Updating equality manager to handle tagged trigger terms. Notifications are p...Dejan Jovanović
2012-05-19- The array type rules were fixed to use isSubtypeOf.Tim King
2012-05-18This commit adds TypeNode::leastCommonTypeNode(). The special case for arith...Tim King
2012-05-18This commit removes the dead psuedoboolean code.Tim King
2012-05-17This fixes a fascinating segfault. This is the sequence of events:Tim King
2012-05-17Fixing an issue with LogicInfo::isPure() that turned off simplification in QF...Morgan Deters
2012-05-17Fixed bug 338:Liana Hadarean
2012-05-16adding simple-minded handling of (dis-)equalities where constants are involvedDejan Jovanović
2012-05-16Changes to SAT solver:Dejan Jovanović
2012-05-16equality status for bitvectors can now look into the sat solver to check for ...Dejan Jovanović
2012-05-16refactored TheoryBV bitblaster and equality engine into subtheories (similar ...Liana Hadarean
2012-05-15fixed QF_BV performance problem due to using CDList instead of CDQueueLiana Hadarean
2012-05-15Fix to shared terms visitor.Tim King
2012-05-15Fixed several bugs in shared terms databaseClark Barrett
2012-05-15This commit removes the CONST_INTEGER kind from nodes. This code comes from t...Tim King
2012-05-15renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectivelyLiana Hadarean
2012-05-15fixing warnings, grrDejan Jovanović
2012-05-15several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify a...Liana Hadarean
2012-05-14fixes for shared term registration. previously the type was not considered wh...Dejan Jovanović
2012-05-14Fixed assertion failures in array theoryClark Barrett
2012-05-14fixing up preregistration againDejan Jovanović
2012-05-13fixing build warningsDejan Jovanović
2012-05-11Added some ITE rewrites,Clark Barrett
2012-05-11Partially fixes something-like-a-problem with TheoryArith::getDeltaValue().Tim King
2012-05-10Removing now unneeded (as of r3425) typenames from EqualityEngine. trunk now ...Tim King
2012-05-09* simplifying equality engine interfaceDejan Jovanović
2012-05-09Merge from decision branch (ITE support)Kshitij Bansal
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
2012-05-07Fixing a bug with TheoryArith::ppAssert() and shared terms.Tim King
2012-05-07Fixes a sign bug in the DioSolver.Tim King
2012-05-04Guard for expensive Debug traceClark Barrett
2012-05-04- This fixes a problem where simplex produced the same conflict in the single...Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback