| 2012-02-28 |
Tim King | This commit merges in branches/arithmetic/internalbb... |
commit | commitdiff | tree |
| 2012-02-28 |
Tim King | Improves the arithmetic difference manager to delay... |
commit | commitdiff | tree |
| 2012-02-28 |
Morgan Deters | fix theory "kinds" file documentation for allowed arity... |
commit | commitdiff | tree |
| 2012-02-28 |
Tim King | Adds the CDQueue class. This is a wrapper for combinin... |
commit | commitdiff | tree |
| 2012-02-28 |
Morgan Deters | Replace the sequence of hardcoded addTheory() calls... |
commit | commitdiff | tree |
| 2012-02-27 |
Morgan Deters | fixes to new-theory script; resolves bug #307 |
commit | commitdiff | tree |
| 2012-02-25 |
Dejan Jovanović | ppAsert -> ppAssert |
commit | commitdiff | tree |
| 2012-02-25 |
Liana Hadarean | Refactored CnfStream to work with the bv theory Bitblaster: |
commit | commitdiff | tree |
| 2012-02-24 |
Dejan Jovanović | Theory interface changes: |
commit | commitdiff | tree |
| 2012-02-23 |
Morgan Deters | Added ability to set a "cvc4-specific logic" in standar... |
commit | commitdiff | tree |
| 2012-02-23 |
Morgan Deters | pcvc4 only built if --with-portfolio given to the confi... |
commit | commitdiff | tree |
| 2012-02-22 |
Tim King | Fix for bug 305. |
commit | commitdiff | tree |
| 2012-02-22 |
Morgan Deters | fixes to configure and boost.m4 to make certain boost... |
commit | commitdiff | tree |
| 2012-02-22 |
Morgan Deters | another static library unavailability issue |
commit | commitdiff | tree |
| 2012-02-22 |
Morgan Deters | make sure to clear out READLINE_LIBS if readline causes... |
commit | commitdiff | tree |
| 2012-02-22 |
Morgan Deters | Added OutputChannel::propagateAsDecision() functionalit... |
commit | commitdiff | tree |
| 2012-02-22 |
Morgan Deters | Fixes to documentation / fixes for MacOS |
commit | commitdiff | tree |
| 2012-02-22 |
Kshitij Bansal | minor change to order fn in sat solver's ElimLt |
commit | commitdiff | tree |
| 2012-02-21 |
Morgan Deters | add a "--with-portfolio" configure option that makes... |
commit | commitdiff | tree |
| 2012-02-21 |
Morgan Deters | fix src/util/hash.h to specialize GNU's hash template... |
commit | commitdiff | tree |
| 2012-02-21 |
Morgan Deters | language bindings fixes for yesterday's portfolio merge |
commit | commitdiff | tree |
| 2012-02-21 |
Dejan Jovanović | Fix for bug303. The problem was with function applicati... |
commit | commitdiff | tree |
| 2012-02-21 |
Morgan Deters | don't require libboost_thread (its presence is detected... |
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | fix sharing issue for portfolio (full lit-to-node map... |
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | fix "make dist" |
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | zlib not required; remove configure's dependency on it |
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | portfolio merge |
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | readline links in -ltermcap -ltinfo too (fixes breakage... |
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | Added Theory::postsolve() infrastructure as Clark reque... |
commit | commitdiff | tree |
| 2012-02-20 |
Morgan Deters | By default, ONLY enable symmetry breaker ONLY for QF_UF... |
commit | commitdiff | tree |
| 2012-02-16 |
Morgan Deters | clarify wording in README, thanks for finding this... |
commit | commitdiff | tree |
| 2012-02-16 |
Tim King | Last commit accidentally lacked r2778 and r2779 from... |
commit | commitdiff | tree |
| 2012-02-15 |
Tim King | This commit merges into trunk the branch branches/arith... |
commit | commitdiff | tree |
| 2012-02-13 |
François Bobot | precision in theoryskel |
commit | commitdiff | tree |
| 2012-02-13 |
Morgan Deters | proper handling of improper get-value |
commit | commitdiff | tree |
| 2012-02-12 |
Morgan Deters | copyright year updated to 2012 |
commit | commitdiff | tree |
| 2012-02-12 |
Morgan Deters | separate new-theory components into a "theoryskel"... |
commit | commitdiff | tree |
| 2012-02-11 |
Morgan Deters | ensure using bash for new-theory script |
commit | commitdiff | tree |
| 2012-02-10 |
Morgan Deters | attempt at a fix for the local regression failure ... |
commit | commitdiff | tree |
| 2012-02-10 |
Morgan Deters | script to ease creating a new theory from scratch ... |
commit | commitdiff | tree |
| 2012-02-10 |
Morgan Deters | correct comment typo found during today's architectural... |
commit | commitdiff | tree |
| 2012-02-09 |
Dejan Jovanović | fixing antoher small bug in backtracking |
commit | commitdiff | tree |
| 2012-02-08 |
Dejan Jovanović | fixing a bug in uf_engine application lookup backtracking |
commit | commitdiff | tree |
| 2012-02-08 |
Tim King | Number of changes to cvc_printer.cpp. Specialized the... |
commit | commitdiff | tree |
| 2012-02-07 |
Morgan Deters | re-adding comment about available languages |
commit | commitdiff | tree |
| 2012-02-07 |
Dejan Jovanović | removing the 100 integer benchmarks from regress0,... |
commit | commitdiff | tree |
| 2012-02-07 |
Dejan Jovanović | fixing some missing stuff |
commit | commitdiff | tree |
| 2012-02-06 |
Tim King | Fixing a bug in the integer unit tests when configured... |
commit | commitdiff | tree |
| 2012-02-05 |
Dejan Jovanović | changes to the cvc4 language printer, so that it actual... |
commit | commitdiff | tree |
| 2012-02-04 |
Andrew Reynolds | support for isWellFounded/mkGroundTerm on uninterprette... |
commit | commitdiff | tree |
| 2012-02-03 |
Dejan Jovanović | updating configure to use python-config for building... |
commit | commitdiff | tree |
| 2012-01-27 |
Morgan Deters | effecting the same change in the compat Java binding... |
commit | commitdiff | tree |
| 2012-01-25 |
Tim King | Adding regress1 test ooo.rf6.smt2. |
commit | commitdiff | tree |
| 2012-01-23 |
Tim King | Partial fix to TheoryEngine::getExplanation so that... |
commit | commitdiff | tree |
| 2012-01-23 |
Dejan Jovanović | fix for bug295 |
commit | commitdiff | tree |
| 2012-01-17 |
Andrew Reynolds | updates to smt2 parser to support datatypes, minor... |
commit | commitdiff | tree |
| 2011-12-15 |
Tim King | Partial fix to bug 295. |
commit | commitdiff | tree |
| 2011-12-15 |
Tim King | Fix to the previous commit. |
commit | commitdiff | tree |
| 2011-12-15 |
Tim King | Partial fix in arithmetic for propagating shared terms... |
commit | commitdiff | tree |
| 2011-12-14 |
Andrew Reynolds | added minor documentation for parametric datatypes... |
commit | commitdiff | tree |
| 2011-12-14 |
Morgan Deters | minor fixes to printing and parsing of CVC-language... |
commit | commitdiff | tree |
| 2011-12-14 |
Dejan Jovanović | some more bug fixes (TNode -> Node, normalize literals... |
commit | commitdiff | tree |
| 2011-12-12 |
Dejan Jovanović | * merging some uf stuff from incremental_work branch... |
commit | commitdiff | tree |
| 2011-12-10 |
Dejan Jovanović | adding additional checks for theories propagating liter... |
commit | commitdiff | tree |
| 2011-12-10 |
Dejan Jovanović | a bit more changes, when propagting equalities/dis... |
commit | commitdiff | tree |
| 2011-12-10 |
Dejan Jovanović | attempt to fix bug 293: if a split on a trivial shared... |
commit | commitdiff | tree |
| 2011-12-08 |
Morgan Deters | Disable a BV rewriter statistic (after checking with... |
commit | commitdiff | tree |
| 2011-12-06 |
Morgan Deters | LemmaStatus changes, as agreed to during 12/2 meeting. |
commit | commitdiff | tree |
| 2011-12-06 |
Morgan Deters | oops, removing some integer operations that leaked... |
commit | commitdiff | tree |
| 2011-12-06 |
Morgan Deters | fix errors in smt-lib2 output; needed for debugging |
commit | commitdiff | tree |
| 2011-12-05 |
Morgan Deters | change short-circuiting behavior of Command execution... |
commit | commitdiff | tree |
| 2011-12-02 |
Morgan Deters | Error detection is different now---with new Command... |
commit | commitdiff | tree |
| 2011-11-30 |
Morgan Deters | disable bug288.smt so that "make check" goes through... |
commit | commitdiff | tree |
| 2011-11-30 |
Morgan Deters | fix linking errors on oneiric |
commit | commitdiff | tree |
| 2011-11-30 |
Tim King | Simplified bug288.smt to reflect the problem in integer... |
commit | commitdiff | tree |
| 2011-11-30 |
Tim King | Added a failing regression test corresponding to bug... |
commit | commitdiff | tree |
| 2011-11-30 |
Tim King | Adding a failing UFLIA benchmark corresponding to bug... |
commit | commitdiff | tree |
| 2011-11-29 |
Tim King | Merging the branch branches/arithmetic/shared-terms... |
commit | commitdiff | tree |
| 2011-11-26 |
Morgan Deters | Fix Java JNI installation path |
commit | commitdiff | tree |
| 2011-11-22 |
Morgan Deters | fix module name for CVC4 jar file; part of the fix... |
commit | commitdiff | tree |
| 2011-11-22 |
Morgan Deters | More language bindings work: |
commit | commitdiff | tree |
| 2011-11-16 |
Morgan Deters | Fix "make dist". Fixes to python and ruby bindings... |
commit | commitdiff | tree |
| 2011-11-16 |
Morgan Deters | Addressed many of the concerns raised in the public... |
commit | commitdiff | tree |
| 2011-11-16 |
Morgan Deters | fix to build system for java bindings |
commit | commitdiff | tree |
| 2011-11-16 |
Morgan Deters | * Applying Andy's fix for datatypes bug #286; thanks... |
commit | commitdiff | tree |
| 2011-11-15 |
Morgan Deters | Bindings work (ocaml bindings are now sort of working... |
commit | commitdiff | tree |
| 2011-11-15 |
Morgan Deters | additional minor changes to get python binding on bette... |
commit | commitdiff | tree |
| 2011-11-15 |
Morgan Deters | fixes for python language binding, added python example |
commit | commitdiff | tree |
| 2011-11-14 |
Morgan Deters | public tests need to be linked against gmp/cln explicit... |
commit | commitdiff | tree |
| 2011-11-06 |
Morgan Deters | datatype stuff in compatibility interface implemented |
commit | commitdiff | tree |
| 2011-11-05 |
Morgan Deters | Context::ScopedPush implemented (in support of theory... |
commit | commitdiff | tree |
| 2011-11-04 |
Morgan Deters | STRING_TYPE and CONST_STRING and associate type infrast... |
commit | commitdiff | tree |
| 2011-11-02 |
Morgan Deters | Only print a shortlist of most-commonly-used options... |
commit | commitdiff | tree |
| 2011-11-02 |
Morgan Deters | give an option error if the user specifies --proof... |
commit | commitdiff | tree |
| 2011-11-02 |
Morgan Deters | fully implement the always-check-again-after-the-output... |
commit | commitdiff | tree |
| 2011-11-02 |
Morgan Deters | Sometimes antlr decides to generate lexers and parsers... |
commit | commitdiff | tree |
| 2011-11-02 |
Morgan Deters | better Integer asserts when there's overflow on convers... |
commit | commitdiff | tree |
| 2011-11-01 |
Morgan Deters | Improvements to header installation on user machines... |
commit | commitdiff | tree |
| 2011-10-31 |
Morgan Deters | fixes to assertions in GMP to match CLN behavior |
commit | commitdiff | tree |
| 2011-10-31 |
Tim King | Added assertions to the CLN implementation of Integer... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog