summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
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
2011-10-19Merging the branch branches/arithmetic/push-pop-support from r2247 to r2256 i...Tim King
2011-10-17Sharing workDejan Jovanović
2011-10-13Interruption, time-out, and deterministic time-out ("resource-out") features.Morgan Deters
2011-10-05ensureLiteral() in CNF stream to support Andy's quantifiers work; an update t...Morgan Deters
2011-10-05remove some debugging code that slowed down last night's regressionsMorgan Deters
2011-10-04fixes to context-dependent caching substitutionsMorgan Deters
2011-09-30more push/pop infrastructure, some SAT stuffMorgan Deters
2011-09-30fixes to incremental simplification, cnf routines, other stuff in preparation...Morgan Deters
2011-09-29build system fixesMorgan Deters
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop a...Morgan Deters
2011-09-28variety of visibility fixes (should clean up some of the many warnings on Mac...Morgan Deters
2011-09-16include example theory (former "UF-Tim") that's included in the dist but not ...Morgan Deters
2011-09-16final(?) documentation fixesMorgan Deters
2011-09-16fix up more documentationMorgan Deters
2011-09-16fix serious issue with copyright-updating scriptMorgan Deters
2011-09-16fix numerous documentation issues; doxygen complains much less, nowMorgan Deters
2011-09-15tim's fixes for context-dependent pre-registrationDejan Jovanović
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-07fixes for uf/equality engine from the quantifiers branch. mainly backtracking...Dejan Jovanović
2011-09-03removing an assert i forgot to remove that andy foundDejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
2011-09-02* Changing pre-registration to be context dependent -- it is called from the ...Dejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback