From 7d70b721f43157e01bc6166a822df79250df632a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 10 Oct 2018 20:44:02 -0500
Subject: Synthesize rewrite rules from inputs (#2608)

---
 src/options/quantifiers_options.toml | 24 ++++++++++++++++++++++++
 src/options/smt_options.toml         | 16 ----------------
 2 files changed, 24 insertions(+), 16 deletions(-)

(limited to 'src/options')

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index cbc380f43..c844a197d 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1316,6 +1316,30 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "use satisfiability check to verify correctness of candidate rewrites"
 
+[[option]]
+  name       = "sygusRewSynthInput"
+  category   = "regular"
+  long       = "sygus-rr-synth-input"
+  type       = "bool"
+  default    = "false"
+  help       = "synthesize rewrite rules based on the input formula"
+
+[[option]]
+  name       = "sygusRewSynthInputNVars"
+  category   = "regular"
+  long       = "sygus-rr-synth-input-nvars=N"
+  type       = "int"
+  default    = "3"
+  help       = "the maximum number of variables per type that appear in rewrites from sygus-rr-synth-input"
+
+[[option]]
+  name       = "sygusRewSynthInputUseBool"
+  category   = "regular"
+  long       = "sygus-rr-synth-input-use-bool"
+  type       = "bool"
+  default    = "false"
+  help       = "synthesize Boolean rewrite rules based on the input formula"
+
 [[option]]
   name       = "sygusExprMinerCheckTimeout"
   category   = "regular"
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 93e892943..8af1000ba 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -295,22 +295,6 @@ header = "options/smt_options.h"
   default    = "false"
   help       = "use aggressive extended rewriter as a preprocessing pass"
 
-[[option]]
-  name       = "synthRrPrep"
-  category   = "regular"
-  long       = "synth-rr-prep"
-  type       = "bool"
-  default    = "false"
-  help       = "synthesize and output rewrite rules during preprocessing"
-
-[[option]]
-  name       = "synthRrPrepExtRew"
-  category   = "regular"
-  long       = "synth-rr-prep-ext-rew"
-  type       = "bool"
-  default    = "false"
-  help       = "use the extended rewriter for synthRrPrep"
-
 [[option]]
   name       = "simplifyWithCareEnabled"
   category   = "regular"
-- 
cgit v1.2.3