projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d39e1b9) | patch
Fix policy for eliminating quantified formulas (#7017)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 17 Aug 2021 17:07:00 +0000 (12:07 -0500)
committerGitHub <noreply@github.com>
Tue, 17 Aug 2021 17:07:00 +0000 (17:07 +0000)
commitcf5376c18d8e4d6b3ed2d7b341279cf65fc16418
treeafbfb5162c6ccc3111827f4080b968108be83152tree
parentd39e1b906b47ef8e953dac297fa0fb565dd040a4commit | diff
Fix policy for eliminating quantified formulas (#7017)

This also consolidates the option strictTriggers into userPatMode.

Fixes #6996.
src/options/quantifiers_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/ematching/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/quantifiers_attributes.cpp diff | blob | history
src/theory/quantifiers/quantifiers_attributes.h diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/quantifiers/issue6996-trivial-elim.smt2 [new file with mode: 0644] blob