| 2012-02-25 |
Liana Hadarean | Refactored CnfStream to work with the bv theory Bitblaster: |
tree | commitdiff |
| 2012-02-24 |
Dejan Jovanović | Theory interface changes: |
tree | commitdiff |
| 2012-02-23 |
Morgan Deters | Added ability to set a "cvc4-specific logic" in standar... |
tree | commitdiff |
| 2012-02-22 |
Tim King | Fix for bug 305. |
tree | commitdiff |
| 2012-02-22 |
Morgan Deters | Added OutputChannel::propagateAsDecision() functionalit... |
tree | commitdiff |
| 2012-02-22 |
Morgan Deters | Fixes to documentation / fixes for MacOS |
tree | commitdiff |
| 2012-02-21 |
Dejan Jovanović | Fix for bug303. The problem was with function applicati... |
tree | commitdiff |
| 2012-02-20 |
Morgan Deters | portfolio merge |
tree | commitdiff |
| 2012-02-20 |
Morgan Deters | Added Theory::postsolve() infrastructure as Clark reque... |
tree | commitdiff |
| 2012-02-16 |
Tim King | Last commit accidentally lacked r2778 and r2779 from... |
tree | commitdiff |
| 2012-02-15 |
Tim King | This commit merges into trunk the branch branches/arith... |
tree | commitdiff |
| 2012-02-13 |
François Bobot | precision in theoryskel |
tree | commitdiff |
| 2012-02-10 |
Morgan Deters | correct comment typo found during today's architectural... |
tree | commitdiff |
| 2012-02-09 |
Dejan Jovanović | fixing antoher small bug in backtracking |
tree | commitdiff |
| 2012-02-08 |
Dejan Jovanović | fixing a bug in uf_engine application lookup backtracking |
tree | commitdiff |
| 2012-02-04 |
Andrew Reynolds | support for isWellFounded/mkGroundTerm on uninterprette... |
tree | commitdiff |
| 2012-01-23 |
Tim King | Partial fix to TheoryEngine::getExplanation so that... |
tree | commitdiff |
| 2012-01-23 |
Dejan Jovanović | fix for bug295 |
tree | commitdiff |
| 2012-01-17 |
Andrew Reynolds | updates to smt2 parser to support datatypes, minor... |
tree | commitdiff |
| 2011-12-15 |
Tim King | Partial fix to bug 295. |
tree | commitdiff |
| 2011-12-15 |
Tim King | Fix to the previous commit. |
tree | commitdiff |
| 2011-12-15 |
Tim King | Partial fix in arithmetic for propagating shared terms... |
tree | commitdiff |
| 2011-12-14 |
Dejan Jovanović | some more bug fixes (TNode -> Node, normalize literals... |
tree | commitdiff |
| 2011-12-12 |
Dejan Jovanović | * merging some uf stuff from incremental_work branch... |
tree | commitdiff |
| 2011-12-10 |
Dejan Jovanović | adding additional checks for theories propagating liter... |
tree | commitdiff |
| 2011-12-10 |
Dejan Jovanović | a bit more changes, when propagting equalities/dis... |
tree | commitdiff |
| 2011-12-10 |
Dejan Jovanović | attempt to fix bug 293: if a split on a trivial shared... |
tree | commitdiff |
| 2011-12-08 |
Morgan Deters | Disable a BV rewriter statistic (after checking with... |
tree | commitdiff |
| 2011-12-06 |
Morgan Deters | LemmaStatus changes, as agreed to during 12/2 meeting. |
tree | commitdiff |
| 2011-11-30 |
Morgan Deters | fix linking errors on oneiric |
tree | commitdiff |
| 2011-11-29 |
Tim King | Merging the branch branches/arithmetic/shared-terms... |
tree | commitdiff |
| 2011-11-16 |
Morgan Deters | Addressed many of the concerns raised in the public... |
tree | commitdiff |
| 2011-11-16 |
Morgan Deters | * Applying Andy's fix for datatypes bug #286; thanks... |
tree | commitdiff |
| 2011-11-04 |
Morgan Deters | STRING_TYPE and CONST_STRING and associate type infrast... |
tree | commitdiff |
| 2011-11-02 |
Morgan Deters | fully implement the always-check-again-after-the-output... |
tree | commitdiff |
| 2011-11-01 |
Morgan Deters | Improvements to header installation on user machines... |
tree | commitdiff |
| 2011-10-28 |
Morgan Deters | * ability to output NodeBuilders without first converti... |
tree | commitdiff |
| 2011-10-28 |
Tim King | Adding a check in Polynomial::parsePolynomial to better... |
tree | commitdiff |
| 2011-10-23 |
Morgan Deters | Implement changes from yesterday morning's meeting... |
tree | commitdiff |
| 2011-10-19 |
Tim King | Merging the branch branches/arithmetic/push-pop-support... |
tree | commitdiff |
| 2011-10-17 |
Dejan Jovanović | Sharing work |
tree | commitdiff |
| 2011-10-13 |
Morgan Deters | Interruption, time-out, and deterministic time-out... |
tree | commitdiff |
| 2011-10-05 |
Morgan Deters | ensureLiteral() in CNF stream to support Andy's quantif... |
tree | commitdiff |
| 2011-10-05 |
Morgan Deters | remove some debugging code that slowed down last night... |
tree | commitdiff |
| 2011-10-04 |
Morgan Deters | fixes to context-dependent caching substitutions |
tree | commitdiff |
| 2011-09-30 |
Morgan Deters | more push/pop infrastructure, some SAT stuff |
tree | commitdiff |
| 2011-09-30 |
Morgan Deters | fixes to incremental simplification, cnf routines,... |
tree | commitdiff |
| 2011-09-29 |
Morgan Deters | build system fixes |
tree | commitdiff |
| 2011-09-29 |
Morgan Deters | Some base infrastructure for user push/pop; a few bugfi... |
tree | commitdiff |
| 2011-09-28 |
Morgan Deters | variety of visibility fixes (should clean up some of... |
tree | commitdiff |
| 2011-09-16 |
Morgan Deters | include example theory (former "UF-Tim") that's include... |
tree | commitdiff |
| 2011-09-16 |
Morgan Deters | final(?) documentation fixes |
tree | commitdiff |
| 2011-09-16 |
Morgan Deters | fix up more documentation |
tree | commitdiff |
| 2011-09-16 |
Morgan Deters | fix serious issue with copyright-updating script |
tree | commitdiff |
| 2011-09-16 |
Morgan Deters | fix numerous documentation issues; doxygen complains... |
tree | commitdiff |
| 2011-09-15 |
Dejan Jovanović | tim's fixes for context-dependent pre-registration |
tree | commitdiff |
| 2011-09-15 |
Dejan Jovanović | additional stuff for sharing, |
tree | commitdiff |
| 2011-09-07 |
Dejan Jovanović | fixes for uf/equality engine from the quantifiers branc... |
tree | commitdiff |
| 2011-09-03 |
Dejan Jovanović | removing an assert i forgot to remove that andy found |
tree | commitdiff |
| 2011-09-02 |
Morgan Deters | Merge from my post-smtcomp branch. Includes: |
tree | commitdiff |
| 2011-09-02 |
Morgan Deters | Partial merge of integers work; this is simple B&B... |
tree | commitdiff |
| 2011-09-02 |
Dejan Jovanović | * Changing pre-registration to be context dependent... |
tree | commitdiff |
| 2011-08-27 |
Dejan Jovanović | Removing Theory::registerTerm() as discussed in the... |
tree | commitdiff |
| 2011-08-24 |
Dejan Jovanović | Simplification of the preregister and register throught... |
tree | commitdiff |
| 2011-08-23 |
Dejan Jovanović | some uf cleanup |
tree | commitdiff |
| 2011-08-17 |
Dejan Jovanović | new implementation of lemmas on demand |
tree | commitdiff |
| 2011-07-12 |
Morgan Deters | fix bug 272, array unsoundness, and some array cleanup |
tree | commitdiff |
| 2011-07-11 |
Morgan Deters | fixing out of place typename (error on g++ 4.4.3-4ubuntu5) |
tree | commitdiff |
| 2011-07-11 |
Clark Barrett | Adding static_fact_manager |
tree | commitdiff |
| 2011-07-11 |
Clark Barrett | Clark's work on array theory - can now solve all QF_AX... |
tree | commitdiff |
| 2011-07-11 |
Morgan Deters | fix some confusing debug output (bogus counter) |
tree | commitdiff |
| 2011-07-11 |
Morgan Deters | if running in QF_AX, equalities over terms of uninterpr... |
tree | commitdiff |
| 2011-07-11 |
Dejan Jovanović | adding disequality propagation |
tree | commitdiff |
| 2011-07-11 |
Morgan Deters | merge from symmetry branch |
tree | commitdiff |
| 2011-07-10 |
Clark Barrett | Reverting mistaken check-in |
tree | commitdiff |
| 2011-07-10 |
Clark Barrett | Fixed bug in default solve - wasn't returning when... |
tree | commitdiff |
| 2011-07-10 |
Dejan Jovanović | another typo |
tree | commitdiff |
| 2011-07-10 |
Dejan Jovanović | yet another uf bug fix, hopefully the last |
tree | commitdiff |
| 2011-07-10 |
Dejan Jovanović | another bugfix for uf |
tree | commitdiff |
| 2011-07-09 |
Dejan Jovanović | some immediate bug fixes |
tree | commitdiff |
| 2011-07-09 |
Morgan Deters | minor fixups |
tree | commitdiff |
| 2011-07-09 |
Dejan Jovanović | surprize surprize |
tree | commitdiff |
| 2011-07-06 |
Dejan Jovanović | Fixing two bugs: |
tree | commitdiff |
| 2011-07-05 |
Dejan Jovanović | updated preprocessing and rewriting input equalities... |
tree | commitdiff |
| 2011-06-30 |
Tim King | Merging the playground branch upto r1957 into trunk. |
tree | commitdiff |
| 2011-06-30 |
Morgan Deters | only use theory registration if (1) a theory requests... |
tree | commitdiff |
| 2011-06-03 |
Andrew Reynolds | fixed various bugs related to ambiguous parametric... |
tree | commitdiff |
| 2011-06-03 |
Morgan Deters | datatypes work |
tree | commitdiff |
| 2011-06-02 |
Andrew Reynolds | added (temporary) support for ensuring that all ambiguo... |
tree | commitdiff |
| 2011-06-01 |
Morgan Deters | minor fix, and better output for type errors |
tree | commitdiff |
| 2011-06-01 |
Morgan Deters | type ascriptions (casts) for parameterized datatypes... |
tree | commitdiff |
| 2011-05-31 |
Tim King | This commit contains the code for allowing arbitrary... |
tree | commitdiff |
| 2011-05-26 |
Morgan Deters | apply arithmetic static learner's miplibtrick in a... |
tree | commitdiff |
| 2011-05-23 |
Morgan Deters | fixes for "make dist" and "make doc", minor cleanups |
tree | commitdiff |
| 2011-05-23 |
Morgan Deters | Merge from arrays2 branch. |
tree | commitdiff |
| 2011-05-14 |
Morgan Deters | fix production-build compiler warning |
tree | commitdiff |
| 2011-05-14 |
Morgan Deters | add AscriptionType stuff to support nullary parameteriz... |
tree | commitdiff |
| 2011-05-13 |
Andrew Reynolds | added support for parametric datatypes, updated cvc... |
tree | commitdiff |
| 2011-05-13 |
Morgan Deters | * fix for Mac OS (includes some ThreadLocal stuff copie... |
tree | commitdiff |
| 2011-05-06 |
Tim King | Deleting dead code. |
tree | commitdiff |
| next |
projects / cvc5.git / history