From aa6aa93e4c34b04e262142c9c06f486a6fcba3b4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 25 Feb 2022 00:05:41 -0600 Subject: [PATCH] Consolidate extended rewrite preprocessing modes (#8156) --- src/options/smt_options.toml | 26 ++++++++++--------- .../passes/extended_rewriter_pass.cpp | 5 ++-- src/smt/process_assertions.cpp | 2 +- test/regress/regress0/fp/ext-rew-test.smt2 | 2 +- test/regress/regress0/nl/issue5737-div00.smt2 | 2 +- test/regress/regress0/sets/sets-extr.smt2 | 2 +- test/regress/regress0/strings/issue6520.smt2 | 2 +- test/regress/regress1/bv/issue3654.smt2 | 2 +- .../regress1/issue4273-ext-rew-cache.smt2 | 2 +- .../regress1/nl/ext-rew-aggr-test.smt2 | 2 +- test/regress/regress1/nl/issue3656.smt2 | 2 +- .../regress1/nl/issue3803-nl-check-model.smt2 | 2 +- 12 files changed, 27 insertions(+), 24 deletions(-) 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) -- 2.30.2