projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d3df62e) | patch
Prenex quantified formulas with user annotations by default (#7048)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 22 Aug 2021 19:37:50 +0000 (14:37 -0500)
committerGitHub <noreply@github.com>
Sun, 22 Aug 2021 19:37:50 +0000 (19:37 +0000)
commit78e84e867417642b04da5c136ef548dfde8ca7f0
tree835211a329d62764e8f1a724bc861d203a522429tree
parentd3df62e637057c77bab90ae644437fe250a64d37commit | diff
Prenex quantified formulas with user annotations by default (#7048)

Our policy is now accurate to the help message on prenexUserQuant: we only prenex quantified formulas if they do not have user-provided patterns. Previously we also did not prenex any quantified formulas with any annotations.

This should avoid some more "unknown" responses on facebook benchmarks.

Also fixes a minor issue with when we print warnings about quantified formulas with no triggers.

FYI @barrettcw .
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/regress1/quantifiers/ddatv-delta2.smt2 [new file with mode: 0644] blob