| 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-23 |
Morgan Deters | pcvc4 only built if --with-portfolio given to the confi... |
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-22 |
Kshitij Bansal | minor change to order fn in sat solver's ElimLt |
tree | commitdiff |
| 2012-02-21 |
Morgan Deters | fix src/util/hash.h to specialize GNU's hash template... |
tree | commitdiff |
| 2012-02-21 |
Morgan Deters | language bindings fixes for yesterday's portfolio merge |
tree | commitdiff |
| 2012-02-21 |
Dejan Jovanović | Fix for bug303. The problem was with function applicati... |
tree | commitdiff |
| 2012-02-21 |
Morgan Deters | don't require libboost_thread (its presence is detected... |
tree | commitdiff |
| 2012-02-20 |
Morgan Deters | fix sharing issue for portfolio (full lit-to-node map... |
tree | commitdiff |
| 2012-02-20 |
Morgan Deters | fix "make dist" |
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-20 |
Morgan Deters | By default, ONLY enable symmetry breaker ONLY for QF_UF... |
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-13 |
Morgan Deters | proper handling of improper get-value |
tree | commitdiff |
| 2012-02-12 |
Morgan Deters | copyright year updated to 2012 |
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-08 |
Tim King | Number of changes to cvc_printer.cpp. Specialized the... |
tree | commitdiff |
| 2012-02-07 |
Dejan Jovanović | fixing some missing stuff |
tree | commitdiff |
| 2012-02-05 |
Dejan Jovanović | changes to the cvc4 language printer, so that it actual... |
tree | commitdiff |
| 2012-02-04 |
Andrew Reynolds | support for isWellFounded/mkGroundTerm on uninterprette... |
tree | commitdiff |
| 2012-02-03 |
Dejan Jovanović | updating configure to use python-config for building... |
tree | commitdiff |
| 2012-01-27 |
Morgan Deters | effecting the same change in the compat Java binding... |
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 |
Andrew Reynolds | added minor documentation for parametric datatypes... |
tree | commitdiff |
| 2011-12-14 |
Morgan Deters | minor fixes to printing and parsing of CVC-language... |
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-12-06 |
Morgan Deters | oops, removing some integer operations that leaked... |
tree | commitdiff |
| 2011-12-06 |
Morgan Deters | fix errors in smt-lib2 output; needed for debugging |
tree | commitdiff |
| 2011-12-05 |
Morgan Deters | change short-circuiting behavior of Command execution... |
tree | commitdiff |
| 2011-12-02 |
Morgan Deters | Error detection is different now---with new Command... |
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-26 |
Morgan Deters | Fix Java JNI installation path |
tree | commitdiff |
| 2011-11-22 |
Morgan Deters | fix module name for CVC4 jar file; part of the fix... |
tree | commitdiff |
| 2011-11-22 |
Morgan Deters | More language bindings work: |
tree | commitdiff |
| 2011-11-16 |
Morgan Deters | Fix "make dist". Fixes to python and ruby bindings... |
tree | commitdiff |
| 2011-11-16 |
Morgan Deters | Addressed many of the concerns raised in the public... |
tree | commitdiff |
| 2011-11-16 |
Morgan Deters | fix to build system for java bindings |
tree | commitdiff |
| 2011-11-16 |
Morgan Deters | * Applying Andy's fix for datatypes bug #286; thanks... |
tree | commitdiff |
| 2011-11-15 |
Morgan Deters | Bindings work (ocaml bindings are now sort of working... |
tree | commitdiff |
| 2011-11-15 |
Morgan Deters | additional minor changes to get python binding on bette... |
tree | commitdiff |
| 2011-11-15 |
Morgan Deters | fixes for python language binding, added python example |
tree | commitdiff |
| 2011-11-06 |
Morgan Deters | datatype stuff in compatibility interface implemented |
tree | commitdiff |
| 2011-11-05 |
Morgan Deters | Context::ScopedPush implemented (in support of theory... |
tree | commitdiff |
| 2011-11-04 |
Morgan Deters | STRING_TYPE and CONST_STRING and associate type infrast... |
tree | commitdiff |
| 2011-11-02 |
Morgan Deters | Only print a shortlist of most-commonly-used options... |
tree | commitdiff |
| 2011-11-02 |
Morgan Deters | give an option error if the user specifies --proof... |
tree | commitdiff |
| 2011-11-02 |
Morgan Deters | fully implement the always-check-again-after-the-output... |
tree | commitdiff |
| 2011-11-02 |
Morgan Deters | Sometimes antlr decides to generate lexers and parsers... |
tree | commitdiff |
| 2011-11-02 |
Morgan Deters | better Integer asserts when there's overflow on convers... |
tree | commitdiff |
| 2011-11-01 |
Morgan Deters | Improvements to header installation on user machines... |
tree | commitdiff |
| 2011-10-31 |
Morgan Deters | fixes to assertions in GMP to match CLN behavior |
tree | commitdiff |
| 2011-10-31 |
Tim King | Added assertions to the CLN implementation of Integer... |
tree | commitdiff |
| 2011-10-31 |
Morgan Deters | fix to "make install" |
tree | commitdiff |
| 2011-10-29 |
Morgan Deters | fix some doxygen warnings |
tree | commitdiff |
| 2011-10-29 |
Morgan Deters | fix unit tests |
tree | commitdiff |
| 2011-10-29 |
Morgan Deters | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF... |
tree | commitdiff |
| 2011-10-28 |
Morgan Deters | * ability to output NodeBuilders without first converti... |
tree | commitdiff |
| 2011-10-28 |
Liana Hadarean | merged the proofgen3 branch into trunk: |
tree | commitdiff |
| 2011-10-28 |
Tim King | Adding a check in Polynomial::parsePolynomial to better... |
tree | commitdiff |
| 2011-10-25 |
Kshitij Bansal | Initialize resource limit and millisecond limit options |
tree | commitdiff |
| 2011-10-23 |
Morgan Deters | Implement changes from yesterday morning's meeting... |
tree | commitdiff |
| 2011-10-21 |
Morgan Deters | some printing and parser fixes for problems recently... |
tree | commitdiff |
| 2011-10-21 |
Morgan Deters | add gcc version information to Configuration, and warn... |
tree | commitdiff |
| 2011-10-20 |
Morgan Deters | add support for QF_AUFLIA and QF_AUFLIRA logic strings... |
tree | commitdiff |
| 2011-10-19 |
Morgan Deters | fix bug #264: competition / other static library builds... |
tree | commitdiff |
| 2011-10-19 |
Tim King | Adding support for QF_UFLIA to the smt2 parser. |
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 | fix make dist |
tree | commitdiff |
| 2011-10-13 |
Morgan Deters | Interruption, time-out, and deterministic time-out... |
tree | commitdiff |
| 2011-10-07 |
Morgan Deters | Some new Datatype public functionality, as per Chris... |
tree | commitdiff |
| 2011-10-06 |
Morgan Deters | don't build language bindings unless expressly requeste... |
tree | commitdiff |
| 2011-10-05 |
Morgan Deters | Reverting a fix from earlier today that fixed a Mac... |
tree | commitdiff |
| 2011-10-05 |
Morgan Deters | ensureLiteral() in CNF stream to support Andy's quantif... |
tree | commitdiff |
| 2011-10-05 |
Morgan Deters | minor visibility fixes |
tree | commitdiff |
| 2011-10-05 |
Morgan Deters | remove some debugging code that slowed down last night... |
tree | commitdiff |
| 2011-10-04 |
Tim King | Disabling the variable removal hueristic by default. |
tree | commitdiff |
| 2011-10-04 |
Morgan Deters | fixes to context-dependent caching substitutions |
tree | commitdiff |
| 2011-10-04 |
Morgan Deters | add a guard for history saving, to enable building... |
tree | commitdiff |
| next |
projects / cvc5.git / history