| 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 |
| 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 |
| next |
projects / cvc5.git / shortlog