projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a582fa3) | patch
More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Cleanup...
authorajreynol <andrew.j.reynolds@gmail.com>
Sun, 16 Aug 2015 10:44:11 +0000 (12:44 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Sun, 16 Aug 2015 10:44:11 +0000 (12:44 +0200)
commit7c798a5a2085754b26a0720d162b2ee45a705c4e
tree1d9d8614b69389b11eb0737989f4db2299e59269tree
parenta582fa3ea1de3b6419797bbebdcb415ff4d0c0d0commit | diff
More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/macros.cpp diff | blob | history
src/theory/quantifiers/macros.h diff | blob | history
src/theory/quantifiers/modes.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/options_handlers.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/quantifiers/trigger.h diff | blob | history
test/regress/regress0/push-pop/quant-fun-proc.smt2 diff | blob | history