| 2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
commit | commitdiff | tree |
| 2012-04-06 |
François Bobot | * Smt2 printer for datatypes |
commit | commitdiff | tree |
| 2012-04-06 |
Morgan Deters | * Fix ITEs and functions in CVC language printer. |
commit | commitdiff | tree |
| 2012-04-06 |
Morgan Deters | fix distributed builds (and therefore the Debian nightl... |
commit | commitdiff | tree |
| 2012-04-06 |
Dejan Jovanović | processing assertions in bit-vectors even when in fullc... |
commit | commitdiff | tree |
| 2012-04-05 |
Morgan Deters | Support to test the "dumper" mechanism in regressions... |
commit | commitdiff | tree |
| 2012-04-04 |
Dejan Jovanović | some settings in bvminisat |
commit | commitdiff | tree |
| 2012-04-04 |
Liana Hadarean | changed BVMinisat options to use cc_min=0 in propagate... |
commit | commitdiff | tree |
| 2012-04-04 |
Liana Hadarean | changed ccmin_mode in BvMinisat |
commit | commitdiff | tree |
| 2012-04-04 |
Liana Hadarean | * added propagation as lemmas to TheoryBV: |
commit | commitdiff | tree |
| 2012-04-03 |
Tim King | Fix for make dist. |
commit | commitdiff | tree |
| 2012-04-02 |
Tim King | Fix for broken unit tests from the previous commit. |
commit | commitdiff | tree |
| 2012-04-02 |
Tim King | - Merged in the branch cdlist-cleanup. |
commit | commitdiff | tree |
| 2012-04-02 |
Kshitij Bansal | fix for cvc4_logic dump |
commit | commitdiff | tree |
| 2012-04-02 |
Tim King | Removing large and unused regress2 benchmarks to decrea... |
commit | commitdiff | tree |
| 2012-03-30 |
Dejan Jovanović | some more build system fixes |
commit | commitdiff | tree |
| 2012-03-30 |
Dejan Jovanović | fixing some build systme warnings |
commit | commitdiff | tree |
| 2012-03-29 |
Tim King | Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is... |
commit | commitdiff | tree |
| 2012-03-29 |
Tim King | Fixes a linking problem with the new SatSolverConstruct... |
commit | commitdiff | tree |
| 2012-03-29 |
Dejan Jovanović | bringing cryptominisat into the main branch |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | enabling the --disable-arithmetic-propagation option... |
commit | commitdiff | tree |
| 2012-03-28 |
Morgan Deters | fix swig-ignored interface name; hopefully fixes Debian... |
commit | commitdiff | tree |
| 2012-03-28 |
Tim King | Update to the ArithRewriter to remove REWRITE_AGAIN_FUL... |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | Some renaming and refactoring in SAT |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | getting rid of a rewrite in uf sharing, speeds things... |
commit | commitdiff | tree |
| 2012-03-28 |
Liana Hadarean | fixed faulty bv rewrite rule |
commit | commitdiff | tree |
| 2012-03-28 |
Dejan Jovanović | adding an extra cache check in the rewriter, speeds... |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | Global registry of SAT solvers, where they are register... |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | More cleaning up. |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | more datail from the build failure |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | with a small fix |
commit | commitdiff | tree |
| 2012-03-26 |
Dejan Jovanović | forgot to commit this one, fixing build errors |
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | moving minisat implementation into their respective... |
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | sat_module.h,cpp -> sat_solver.h,cpp (as intended) |
commit | commitdiff | tree |
| 2012-03-25 |
Dejan Jovanović | sat.h,cpp -> theory_proxy.h,cpp (this is what it defines) |
commit | commitdiff | tree |
| 2012-03-24 |
Dejan Jovanović | a cute script to make a video of development from the... |
commit | commitdiff | tree |
| 2012-03-23 |
Tim King | Removed the variableRemovalEnabled option and d_removed... |
commit | commitdiff | tree |
| 2012-03-22 |
Dejan Jovanović | * improving arithmetic getEqualityStatus |
commit | commitdiff | tree |
| 2012-03-22 |
Liana Hadarean | Merged updated version of the bitvector theory: |
commit | commitdiff | tree |
| 2012-03-22 |
Dejan Jovanović | some improvements to the sharing mechanism/interface |
commit | commitdiff | tree |
| 2012-03-21 |
Morgan Deters | Disable nonclausal simplification for QF_SAT benchmarks... |
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | Some work on the dump infrastructure to support portfol... |
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | fix a "lost command" bug and associated memory leak... |
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | Strengthen minisat assertion regarding t-propagations... |
commit | commitdiff | tree |
| 2012-03-09 |
Morgan Deters | minor fixes: to "make dist" in build directories with... |
commit | commitdiff | tree |
| 2012-03-08 |
Morgan Deters | fix "make dist" |
commit | commitdiff | tree |
| 2012-03-08 |
Dejan Jovanović | Fixin the bug Clark found. In final check, enqueued... |
commit | commitdiff | tree |
| 2012-03-08 |
Dejan Jovanović | Removing QUICK_CHECK, and other unused ones, from the... |
commit | commitdiff | tree |
| 2012-03-07 |
François Bobot | cdqueue : fix size(). Thank you Clark for spotting... |
commit | commitdiff | tree |
| 2012-03-07 |
Morgan Deters | fix some Java compatibility-layer interface problems... |
commit | commitdiff | tree |
| 2012-03-06 |
Dejan Jovanović | updating the equality engine to be able to give explana... |
commit | commitdiff | tree |
| 2012-03-03 |
Morgan Deters | Changing the dependency checking; GMP is required ... |
commit | commitdiff | tree |
| 2012-03-02 |
Kshitij Bansal | Remove some commented out code from sat.h |
commit | commitdiff | tree |
| 2012-03-02 |
Tim King | This commit merges in the changes from branches/arithme... |
commit | commitdiff | tree |
| 2012-03-02 |
Dejan Jovanović | CDMap -> CDHashMap |
commit | commitdiff | tree |
| 2012-03-02 |
Morgan Deters | committing the TNode/Node fix that was in the kind... |
commit | commitdiff | tree |
| 2012-03-02 |
Tim King | Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue... |
commit | commitdiff | tree |
| 2012-03-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minis... |
commit | commitdiff | tree |
| 2012-03-01 |
François Bobot | cdqueue2 : cdlist that can be used like queue and can... |
commit | commitdiff | tree |
| 2012-03-01 |
Tim King | Fixed a copy paste error where a lower bound was looked... |
commit | commitdiff | tree |
| 2012-02-29 |
Liana Hadarean | This should fix the debian build fails: |
commit | commitdiff | tree |
| 2012-02-29 |
Dejan Jovanović | fixing bug310 |
commit | commitdiff | tree |
| 2012-02-29 |
Morgan Deters | consistency in how the Dump output stream is used |
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / shortlog