projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2abcda1) | patch
Improvements to trigger selection, min triggers by default. Optimizations for E-match...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 31 Mar 2016 19:36:25 +0000 (14:36 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 31 Mar 2016 19:36:25 +0000 (14:36 -0500)
commitccc9cd5aad5248b4a2c86b617d76bc98063a7ea2
treecd710b7174eb3724d1b08c3261f69c7e4745a4d0tree
parent2abcda1cfcb0c6388c00d65f8a6b3e63de9d96dfcommit | diff
Improvements to trigger selection, min triggers by default. Optimizations for E-matching. Minor work to equality infer.
12 files changed:
src/options/options_handler.cpp diff | blob | history
src/options/quantifiers_modes.h diff | blob | history
src/theory/quantifiers/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/candidate_generator.h diff | blob | history
src/theory/quantifiers/equality_infer.cpp diff | blob | history
src/theory/quantifiers/equality_infer.h diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_match_generator.h diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.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