summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ar...Dejan Jovanović
2012-06-06Fixed problem causing crash at destruction timeClark Barrett
2012-06-05More clean-upClark Barrett
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-06-01add a global user-context push/pop in smt engine, just like clark's addition ...Morgan Deters
2012-05-31Fixed bug in bv: one more case where non-shared equality was getting propagatedClark Barrett
2012-05-31svn:ignore a parallel-tests driver file that automake deposits in config/Morgan Deters
2012-05-31pass JAVA_CPPFLAGS properlyMorgan Deters
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 traceClark Barrett
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-21main() no longer catches non-CVC4 exceptions. This means on memout and other...Morgan Deters
2012-05-19Adding regress test for bug 341.Tim King
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-18Removing long unsigned operator+ from CDList's const_iterator.Tim King
2012-05-18removing failing regressionDejan Jovanović
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-17Adding failing regression for ite type computation.Tim King
2012-05-17Queueing up asserted literals in the proxy instead of sending them off to the...Dejan Jovanović
2012-05-16adding simple-minded handling of (dis-)equalities where constants are involvedDejan Jovanović
2012-05-16Fixing C compatibility library (it still had a reference to CONST_INTEGER).Morgan Deters
2012-05-16testcase for bug 337Dejan 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-16removing duplicate literals in explanations of propagationsDejan 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-15(no commit message)Dejan Jovanović
2012-05-15test casesDejan Jovanović
2012-05-15Fix to shared terms visitor.Tim King
2012-05-15Implement TypeNode::isComparableTo() and add a unit test for it.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback