summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
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ć
2012-01-17updates to smt2 parser to support datatypes, minor updates to datatypes theor...Andrew Reynolds
2011-12-15Partial fix to bug 295.Tim King
2011-12-15Fix to the previous commit.Tim King
2011-12-15Partial fix in arithmetic for propagating shared terms. This partially resolv...Tim King
2011-12-14some more bug fixes (TNode -> Node, normalize literals in explanations)Dejan Jovanović
2011-12-12* merging some uf stuff from incremental_work branch that somehow nobody merg...Dejan Jovanović
2011-12-10adding additional checks for theories propagating literals that already have ...Dejan Jovanović
2011-12-10a bit more changes, when propagting equalities/dis-equalities don't assert th...Dejan Jovanović
2011-12-10attempt to fix bug 293: if a split on a trivial shared pair is requested from...Dejan Jovanović
2011-12-08Disable a BV rewriter statistic (after checking with Liana) that was static,Morgan Deters
2011-12-06LemmaStatus changes, as agreed to during 12/2 meeting.Morgan Deters
2011-11-30fix linking errors on oneiricMorgan Deters
2011-11-29Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic no...Tim King
2011-11-16Addressed many of the concerns raised in the public interface review of CVC4 ...Morgan Deters
2011-11-16* Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy!Morgan Deters
2011-11-04STRING_TYPE and CONST_STRING and associate type infrastructure implemented.Morgan Deters
2011-11-02fully implement the always-check-again-after-the-output-channel-is-used fix f...Morgan Deters
2011-11-01Improvements to header installation on user machines. Internally, we canMorgan Deters
2011-10-28* ability to output NodeBuilders without first converting them to Nodes---use...Morgan Deters
2011-10-28Adding a check in Polynomial::parsePolynomial to better enforce the arithmeti...Tim King
2011-10-23Implement changes from yesterday morning's meeting (10/21/2011):Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback