projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0f69a8b) | patch
New options for trigger selection, add option --strict-triggers. Do not infer alpha...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 4 Apr 2016 22:18:36 +0000 (17:18 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 4 Apr 2016 22:18:47 +0000 (17:18 -0500)
commit576d50ac7c13233a589771401537b587eb36361e
tree3f044ce37d5b3dc0f20db52339b3f1ae8cb59c8dtree
parent0f69a8ba2286bd5d9b807c10ad350705952e93d6commit | diff
New options for trigger selection, add option --strict-triggers. Do not infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted.
17 files changed:
src/options/options_handler.cpp diff | blob | history
src/options/quantifiers_modes.h diff | blob | history
src/options/quantifiers_options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/alpha_equivalence.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.h diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.h diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp 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
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history