projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bb2a0e0) | patch
The "UF engineering issues" release, after much profiling.
authorMorgan Deters <mdeters@gmail.com>
Wed, 17 Nov 2010 01:39:37 +0000 (01:39 +0000)
committerMorgan Deters <mdeters@gmail.com>
Wed, 17 Nov 2010 01:39:37 +0000 (01:39 +0000)
commitc7a70635797fe4205b27d29546dd4fe763220794
tree715eb2c43beebaaa725a3064597761f60975fea6tree
parentbb2a0e0e12f39a1b4dea8fb0c990decba4708a1ccommit | diff
The "UF engineering issues" release, after much profiling.

* swap in backtracking data structures (that use and maintain their own
  undo stack) in some places instead of the usual Context-aware
  paradigm (MUCH faster).

* cosmetic changes to UF, CC modules.
src/theory/theory_engine.cpp diff | blob | history
src/theory/uf/morgan/Makefile.am diff | blob | history
src/theory/uf/morgan/stacking_map.cpp [new file with mode: 0644] blob
src/theory/uf/morgan/stacking_map.h [new file with mode: 0644] blob
src/theory/uf/morgan/theory_uf_morgan.cpp diff | blob | history
src/theory/uf/morgan/theory_uf_morgan.h diff | blob | history
src/theory/uf/morgan/union_find.cpp [new file with mode: 0644] blob
src/theory/uf/morgan/union_find.h [new file with mode: 0644] blob
src/theory/uf/tim/theory_uf_tim.h diff | blob | history
src/util/congruence_closure.h diff | blob | history