Consolidate extended rewrite preprocessing modes (#8156)

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 71c3e8f37d985769701774b4fa95141cb14a2e27..739f898f1bc9948cc8a3e712261e7848e796daaa 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -286,18 +286,20 @@ name   = "SMT Layer"
 [[option]]
   name       = "extRewPrep"
   category   = "regular"
-  long       = "ext-rew-prep"
-  type       = "bool"
-  default    = "false"
-  help       = "use extended rewriter as a preprocessing pass"
-
-[[option]]
-  name       = "extRewPrepAgg"
-  category   = "regular"
-  long       = "ext-rew-prep-agg"
-  type       = "bool"
-  default    = "false"
-  help       = "use aggressive extended rewriter as a preprocessing pass"
+  long       = "ext-rew-prep=MODE"
+  type       = "ExtRewPrepMode"
+  default    = "OFF"
+  help       = "mode for using extended rewriter as a preprocessing pass, see --ext-rew-prep=help"
+  help_mode  = "extended rewriter preprocessing pass modes."
+[[option.mode.OFF]]
+  name = "off"
+  help = "do not use extended rewriter as a preprocessing pass."
+[[option.mode.USE]]
+  name = "use"
+  help = "use extended rewriter as a preprocessing pass."
+[[option.mode.AGG]]
+  name = "agg"
+  help = "use aggressive extended rewriter as a preprocessing pass."
 
 [[option]]
   name       = "simplifyWithCareEnabled"

diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
index 06b4f0ba11626f9f542fb2f73a5554684476865b..447c17052f221412953d148e4b1cf2e6c61fe93f 100644 (file)
--- a/src/preprocessing/passes/extended_rewriter_pass.cpp
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -35,8 +35,9 @@ PreprocessingPassResult ExtRewPre::applyInternal(
   {
     assertionsToPreprocess->replace(
         i,
-        extendedRewrite((*assertionsToPreprocess)[i],
-                        options().smt.extRewPrepAgg));
+        extendedRewrite(
+            (*assertionsToPreprocess)[i],
+            options().smt.extRewPrep == options::ExtRewPrepMode::AGG));
   }
   return PreprocessingPassResult::NO_CONFLICT;
 }

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 58c83074f3a6359d9ba81a8df9299d269d473f2a..22a6bde98ba9c3be31b129081ce8e1301e268630 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -170,7 +170,7 @@ bool ProcessAssertions::apply(Assertions& as)
 
   bool noConflict = true;
 
-  if (options().smt.extRewPrep)
+  if (options().smt.extRewPrep != options::ExtRewPrepMode::OFF)
   {
     applyPass("ext-rew-pre", as);
   }

diff --git a/test/regress/regress0/fp/ext-rew-test.smt2 b/test/regress/regress0/fp/ext-rew-test.smt2
index 3fb3a9e53348c607f6f825fc4729a148e1bf92ab..88090daeccc690f0beb66028340407e859c0d0eb 100644 (file)
--- a/test/regress/regress0/fp/ext-rew-test.smt2
+++ b/test/regress/regress0/fp/ext-rew-test.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
+; COMMAND-LINE: --ext-rew-prep=agg
 ; EXPECT: unsat
 (set-info :smt-lib-version 2.6)
 (set-logic QF_FP)

diff --git a/test/regress/regress0/nl/issue5737-div00.smt2 b/test/regress/regress0/nl/issue5737-div00.smt2
index 59de5a3fbb8c84c9d95fd4ea642617f36e84b02d..ae9c4c2c22daf94884c9315fc66b565138f573d4 100644 (file)
--- a/test/regress/regress0/nl/issue5737-div00.smt2
+++ b/test/regress/regress0/nl/issue5737-div00.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep -q
+; COMMAND-LINE: --ext-rew-prep=use -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)

diff --git a/test/regress/regress0/sets/sets-extr.smt2 b/test/regress/regress0/sets/sets-extr.smt2
index 1cbe0de9c8c894a75beb36fdc10ad50aa1deb3ba..19b26295fd8cd482152fc98ae787596ffba2a5e2 100644 (file)
--- a/test/regress/regress0/sets/sets-extr.smt2
+++ b/test/regress/regress0/sets/sets-extr.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
+; COMMAND-LINE: --ext-rew-prep=agg
 ; EXPECT: sat
 (set-logic ALL)
 (declare-sort Atom 0)

diff --git a/test/regress/regress0/strings/issue6520.smt2 b/test/regress/regress0/strings/issue6520.smt2
index 23a938365e0d6112426e58e1046e2851fe9ecf1f..605844b94fa60433f20c4a4d29d0952cf459fe27 100644 (file)
--- a/test/regress/regress0/strings/issue6520.smt2
+++ b/test/regress/regress0/strings/issue6520.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep
+; COMMAND-LINE: --ext-rew-prep=use
 (set-logic QF_SLIA)
 (declare-fun a () String)
 (declare-fun b () String)

diff --git a/test/regress/regress1/bv/issue3654.smt2 b/test/regress/regress1/bv/issue3654.smt2
index a1e2f8b875f54ef8934febd63903647a91e4df57..24469d929821474e242ff2b26c26c6d75d5a8e38 100644 (file)
--- a/test/regress/regress1/bv/issue3654.smt2
+++ b/test/regress/regress1/bv/issue3654.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep
+; COMMAND-LINE: --ext-rew-prep=use
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 4))

diff --git a/test/regress/regress1/issue4273-ext-rew-cache.smt2 b/test/regress/regress1/issue4273-ext-rew-cache.smt2
index 63262272365d8704ac2d91ad08217ca63716e20d..3184d8a4e7389d1bd47608b03f4b78d94dedab4b 100644 (file)
--- a/test/regress/regress1/issue4273-ext-rew-cache.smt2
+++ b/test/regress/regress1/issue4273-ext-rew-cache.smt2
@@ -15,7 +15,7 @@
 (declare-fun _substvar_3545_ () Bool)
 (declare-fun _substvar_3627_ () Bool) 
 (set-option :ext-rewrite-quant true)
-(set-option :ext-rew-prep true)
+(set-option :ext-rew-prep use)
 (declare-const v0 Bool)
 (declare-const i2 Int)
 (declare-const i3 Int) 

diff --git a/test/regress/regress1/nl/ext-rew-aggr-test.smt2 b/test/regress/regress1/nl/ext-rew-aggr-test.smt2
index c540ecbe5514ea2acff12fbc7217a9f612e9299f..e007f4fbc70c86ec1b319f113bdd776f4b2dddb1 100644 (file)
--- a/test/regress/regress1/nl/ext-rew-aggr-test.smt2
+++ b/test/regress/regress1/nl/ext-rew-aggr-test.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg --no-new-prop --nl-ext-tplanes
+; COMMAND-LINE: --ext-rew-prep=agg --no-new-prop --nl-ext-tplanes
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic QF_NIA)

diff --git a/test/regress/regress1/nl/issue3656.smt2 b/test/regress/regress1/nl/issue3656.smt2
index 6de6e26b97a74ddbb5d61aa4283e4bb2275514a1..2f41d546aaa8ca88c49ba53826010a554b765e28 100644 (file)
--- a/test/regress/regress1/nl/issue3656.smt2
+++ b/test/regress/regress1/nl/issue3656.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep
+; COMMAND-LINE: --ext-rew-prep=use
 ; EXPECT: sat
 (set-logic QF_NRA)   
 (set-info :status sat)  

diff --git a/test/regress/regress1/nl/issue3803-nl-check-model.smt2 b/test/regress/regress1/nl/issue3803-nl-check-model.smt2
index 99d945ce270cc5b441d2e25142265e9c2d7892f1..545ea3e67066a39526c386066dacac28f2941de0 100644 (file)
--- a/test/regress/regress1/nl/issue3803-nl-check-model.smt2
+++ b/test/regress/regress1/nl/issue3803-nl-check-model.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep -q
+; COMMAND-LINE: --ext-rew-prep=use -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)