diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-06 17:44:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-06 17:44:09 -0500 |
commit | 4ac6c5179265ef9895bc9e939be0e47b3754137e (patch) | |
tree | bf2cd175a534e5ca9a383a63cd6a086f1d5f45d0 /src/options/smt_options.toml | |
parent | b023494b8914be03d8f8ca26c1b1db332944f3fe (diff) |
Integrate learned rewrite preprocessing pass (#6840)
This adds the learned rewrite preprocessing pass, which rewrites the input formula based on (typically theory specific) reasoning about learned literals. The main motivation is for preprocessing ints division/modulus based on bounds.
Diffstat (limited to 'src/options/smt_options.toml')
-rw-r--r-- | src/options/smt_options.toml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 4d08aa672..9b5a93486 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -48,6 +48,14 @@ name = "SMT Layer" help = "use static learning (on by default)" [[option]] + name = "learnedRewrite" + category = "regular" + long = "learned-rewrite" + type = "bool" + default = "false" + help = "rewrite the input based on learned literals" + +[[option]] name = "expandDefinitions" long = "expand-definitions" category = "regular" |