projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 69769da) | patch
Add options --partial-triggers, --elim-taut-quant, improve robustness of --purify...
authorajreynol <andrew.j.reynolds@gmail.com>
Sun, 5 Jul 2015 17:56:42 +0000 (19:56 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Sun, 5 Jul 2015 17:56:42 +0000 (19:56 +0200)
commitba56661b4a49d4b470c6298d3531324b3bf15005
tree6dee0cde13ab4e86a6bde22bf130e1d3f70c2a6ftree
parent69769dae4886621f82c2905b82db727bf2e8cf3fcommit | diff
Add options --partial-triggers, --elim-taut-quant, improve robustness of --purify-triggers. Enable --quant-alpha-equiv by default. Fix fairness issue when combining cbqi+E-matching.  Avoid unecessary delta lemmas.  Update casc scripts.
12 files changed:
contrib/run-script-casc25-fof diff | blob | history
contrib/run-script-casc25-tfa diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/ce_guided_single_inv.h diff | blob | history
src/theory/quantifiers/inst_match_generator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history