diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-28 21:43:49 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-28 21:43:49 -0600 |
commit | 940a25255469bbeea95df14ef25036e6c0565c3e (patch) | |
tree | 5d00490debcd9c96de307810daf2aa5d8935a233 /src/options | |
parent | a975f3af51a3730f5b848d2b55f9c6d4027fe763 (diff) |
Replace conditional rewrite pass in quantifiers with the extended rewriter (#3841)
Fixes #3839.
Previously, the quantifiers rewriter had a rewriting step that was an ad-hoc version of some of the rewrites that have been incorporated into the extended rewriter. Moreover, the code for that pass was buggy.
This eliminates the previous conditional rewriting step from the "term process" rewrite pass in quantifiers. It additional adds an optional (disabled by default) rewriting pass that calls the extended rewriter on the body of quantified formulas. This subsumes the previous behavior and should not be buggy.
Notice that the indentation in computeProcessTerms changed and subsequently has been updated to the new coding standards.
This PR relies on #3840.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/quantifiers_options.toml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index cb989b433..1101f70c5 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -189,13 +189,13 @@ header = "options/quantifiers_options.h" help = "eliminate extended arithmetic symbols in quantified formulas" [[option]] - name = "condRewriteQuant" + name = "extRewriteQuant" category = "regular" - long = "cond-rewrite-quant" + long = "ext-rewrite-quant" type = "bool" - default = "true" + default = "false" read_only = true - help = "conditional rewriting of quantified formulas" + help = "apply extended rewriting to bodies of quantified formulas" [[option]] name = "globalNegate" |