projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a58abbe) | patch
Add option --trigger-active-sel. Recognize simple triggers with polarity. Do not...
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 5 Jul 2016 20:11:28 +0000 (15:11 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 5 Jul 2016 20:11:38 +0000 (15:11 -0500)
commit967747b7b279256bd9368e2d392ae71dec1bb1c1
tree18a811b16d7552c1ae52fadfe34e54acde68e6a8tree
parenta58abbe71fb1fc07129ff9c7568ac544145fb57ccommit | diff
Add option --trigger-active-sel. Recognize simple triggers with polarity. Do not drop patterns from merged prenex (fixes bug 743).
12 files changed:
src/options/options_handler.cpp diff | blob | history
src/options/options_handler.h diff | blob | history
src/options/quantifiers_modes.h diff | blob | history
src/options/quantifiers_options 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/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/quantifiers/trigger.h diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/bug_743.smt2 [new file with mode: 0644] blob