summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
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
2012-05-03Some cleanup starting off from trying to understand the sharing code. Changes...Dejan Jovanović
2012-05-02Changing d_sharedTermsExist to logicInfo.isSharingEnabled()Clark Barrett
2012-04-30Added map from skolem variables to new ite formulas in ite removal.Clark Barrett
2012-04-28New LogicInfo functionality.Morgan Deters
2012-04-27Fixed warning in decision_engine.h, minor tweak to caregraph function inClark Barrett
2012-04-27This merges in the branch cvc4/branches/arithmetic/matrix into trunk.Tim King
2012-04-24This commit merges in the branch branches/arithmetic/congruence into trunk. H...Tim King
2012-04-20Updates to array theory - much more lazy about introduction of readsClark Barrett
2012-04-18cout -> warning. Happening in portfolioKshitij Bansal
2012-04-17A dummy decision engine. Expected performance impact: none.Kshitij Bansal
2012-04-17Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo...Tim King
2012-04-14Fixed bug in sharing with arrays of different typesClark Barrett
2012-04-11merge from arrays-clark branchMorgan Deters
2012-04-06processing assertions in bit-vectors even when in fullcheck (needed for sharing)Dejan Jovanović
2012-04-04 * added propagation as lemmas to TheoryBV:Liana Hadarean
2012-04-02- Merged in the branch cdlist-cleanup.Tim King
2012-03-29Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function pointers...Tim King
2012-03-28enabling the --disable-arithmetic-propagation option in the arithmetic code (...Dejan Jovanović
2012-03-28Update to the ArithRewriter to remove REWRITE_AGAIN_FULL and limit REWRITE_AG...Tim King
2012-03-28getting rid of a rewrite in uf sharing, speeds things up a bitDejan Jovanović
2012-03-28fixed faulty bv rewrite ruleLiana Hadarean
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback