summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
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
2012-03-28adding an extra cache check in the rewriter, speeds things a bitDejan Jovanović
2012-03-26More cleaning up.Dejan Jovanović
2012-03-25sat_module.h,cpp -> sat_solver.h,cpp (as intended)Dejan Jovanović
2012-03-23Removed the variableRemovalEnabled option and d_removedRows from TheoryArith....Tim King
2012-03-22* improving arithmetic getEqualityStatusDejan Jovanović
2012-03-22Merged updated version of the bitvector theory:Liana Hadarean
2012-03-22some improvements to the sharing mechanism/interfaceDejan Jovanović
2012-03-09Some work on the dump infrastructure to support portfolio work.Morgan Deters
2012-03-08Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.Dejan Jovanović
2012-03-06updating the equality engine to be able to give explanations for terms that w...Dejan Jovanović
2012-03-02This commit merges in the changes from branches/arithmetic/refactor0Tim King
2012-03-02CDMap -> CDHashMapDejan Jovanović
2012-03-02committing the TNode/Node fix that was in the kind-backend branch; there's st...Morgan Deters
2012-03-02Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to fun...Tim King
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
2012-03-01Fixed a copy paste error where a lower bound was looked up instead of an uppe...Tim King
2012-02-29This should fix the debian build fails:Liana Hadarean
2012-02-29fixing bug310Dejan Jovanović
2012-02-28This commit merges in branches/arithmetic/internalbb up to revision 2831. Th...Tim King
2012-02-28Improves the arithmetic difference manager to delay any work until a shared t...Tim King
2012-02-28fix theory "kinds" file documentation for allowed arity of operatorsMorgan Deters
2012-02-25ppAsert -> ppAssertDejan Jovanović
2012-02-25Refactored CnfStream to work with the bv theory Bitblaster:Liana Hadarean
2012-02-24Theory interface changes:Dejan Jovanović
2012-02-23Added ability to set a "cvc4-specific logic" in standards-compliantMorgan Deters
2012-02-22Fix for bug 305.Tim King
2012-02-22Added OutputChannel::propagateAsDecision() functionality, allowing a theoryMorgan Deters
2012-02-22Fixes to documentation / fixes for MacOSMorgan Deters
2012-02-21Fix for bug303. The problem was with function applications that get normalize...Dejan Jovanović
2012-02-20portfolio mergeMorgan Deters
2012-02-20Added Theory::postsolve() infrastructure as Clark requested.Morgan Deters
2012-02-16Last commit accidentally lacked r2778 and r2779 from integer2. I have manual...Tim King
2012-02-15This commit merges into trunk the branch branches/arithmetic/integers2 from r...Tim King
2012-02-13precision in theoryskelFrançois Bobot
2012-02-10correct comment typo found during today's architectural meetingMorgan Deters
2012-02-09fixing antoher small bug in backtrackingDejan Jovanović
2012-02-08fixing a bug in uf_engine application lookup backtrackingDejan Jovanović
2012-02-04support for isWellFounded/mkGroundTerm on uninterpretted sorts. cvc4 now ass...Andrew Reynolds
2012-01-23Partial fix to TheoryEngine::getExplanation so that SharedAssertions request ...Tim King
2012-01-23fix for bug295Dejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback