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.

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"