summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
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-15removing all extended commands (as inspired by the Z3 extended command set) e...Morgan Deters
2012-05-15Fix QF_AUFLIA (resolves bug #331).Morgan Deters
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-14in debug builds, -d can be used for trace tags that aren't also debug tagsMorgan Deters
2012-05-14fixing up preregistration againDejan Jovanović
2012-05-13fixing build warningsDejan Jovanović
2012-05-11fix regex in Debug_tags and Trace_tags generation for Mac OSMorgan Deters
2012-05-11fix typo in sed lineMorgan Deters
2012-05-11output a warning message when a function type (or datatype, or array, etc.) i...Morgan Deters
2012-05-11Disabled arith-rewrite-equalities by default unless in a pure arithmetic theoryClark Barrett
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-09fix 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 interfaceDejan Jovanović
2012-05-09rm something for a future merge that sneaked inKshitij Bansal
2012-05-09Merge from decision branch (ITE support)Kshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback