From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 25 Feb 2022 06:05:41 +0000 (-0600)
Subject: Consolidate extended rewrite preprocessing modes (#8156)
X-Git-Tag: cvc5-1.0.0~381
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aa6aa93e4c34b04e262142c9c06f486a6fcba3b4;p=cvc5.git

Consolidate extended rewrite preprocessing modes (#8156)
---

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 71c3e8f37..739f898f1 100644
--- 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 06b4f0ba1..447c17052 100644
--- 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 58c83074f..22a6bde98 100644
--- 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 3fb3a9e53..88090daec 100644
--- 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 59de5a3fb..ae9c4c2c2 100644
--- 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 1cbe0de9c..19b26295f 100644
--- 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 23a938365..605844b94 100644
--- 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 a1e2f8b87..24469d929 100644
--- 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 632622723..3184d8a4e 100644
--- 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 c540ecbe5..e007f4fbc 100644
--- 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 6de6e26b9..2f41d546a 100644
--- 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 99d945ce2..545ea3e67 100644
--- 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)