From b334cf09f05b11150f5e1e7a915346e0d753841d Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 9 Sep 2021 17:21:57 -0700 Subject: [PATCH] Use EnvObj-based options in preprocessing (#7165) This PR is the first step in replacing options access via options::foo() to using the environment (via EnvObj and options().module.foo). It replaces all such options accesses in the preprocessing passes. --- src/preprocessing/passes/ackermann.cpp | 2 +- src/preprocessing/passes/bool_to_bv.cpp | 3 ++- src/preprocessing/passes/bv_to_int.cpp | 10 +++++----- src/preprocessing/passes/extended_rewriter_pass.cpp | 2 +- src/preprocessing/passes/ho_elim.cpp | 12 ++++++------ src/preprocessing/passes/ho_elim.h | 6 +++--- src/preprocessing/passes/int_to_bv.cpp | 4 ++-- src/preprocessing/passes/ite_simp.cpp | 10 +++++----- src/preprocessing/passes/miplib_trick.cpp | 13 +++++++------ src/preprocessing/passes/sort_infer.cpp | 4 ++-- src/preprocessing/passes/synth_rew_rules.cpp | 6 +++--- 11 files changed, 37 insertions(+), 35 deletions(-) diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index 7f3d778fd..57469ab11 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -308,7 +308,7 @@ Ackermann::Ackermann(PreprocessingPassContext* preprocContext) PreprocessingPassResult Ackermann::applyInternal( AssertionPipeline* assertionsToPreprocess) { - AlwaysAssert(!options::incrementalSolving()); + AlwaysAssert(!options().base.incrementalSolving); /* collect all function applications and generate consistency lemmas * accordingly */ diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index f5152f0d2..206f12a3f 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -20,6 +20,7 @@ #include "base/map_util.h" #include "expr/node.h" +#include "options/bv_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_statistics_registry.h" @@ -35,7 +36,7 @@ using namespace cvc5::theory; BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics() { - d_boolToBVMode = options::boolToBitvector(); + d_boolToBVMode = options().bv.boolToBitvector; }; PreprocessingPassResult BoolToBV::applyInternal( diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index cc631f4bc..f6a65f90a 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -424,13 +424,13 @@ Node BVToInt::translateWithChildren(Node original, // operators) // 3. translating into a sum uint64_t bvsize = original[0].getType().getBitVectorSize(); - if (options::solveBVAsInt() == options::SolveBVAsIntMode::IAND) + if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::IAND) { Node iAndOp = d_nm->mkConst(IntAnd(bvsize)); returnNode = d_nm->mkNode( kind::IAND, iAndOp, translated_children[0], translated_children[1]); } - else if (options::solveBVAsInt() == options::SolveBVAsIntMode::BV) + else if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::BV) { // translate the children back to BV Node intToBVOp = d_nm->mkConst(IntToBitVector(bvsize)); @@ -445,14 +445,14 @@ Node BVToInt::translateWithChildren(Node original, } else { - Assert(options::solveBVAsInt() == options::SolveBVAsIntMode::SUM); + Assert(options().smt.solveBVAsInt == options::SolveBVAsIntMode::SUM); // Construct a sum of ites, based on granularity. Assert(translated_children.size() == 2); returnNode = d_iandUtils.createSumNode(translated_children[0], translated_children[1], bvsize, - options::BVAndIntegerGranularity()); + options().smt.BVAndIntegerGranularity); } break; } @@ -657,7 +657,7 @@ Node BVToInt::translateWithChildren(Node original, * of the bounds that were relevant for the original * bit-vectors. */ - if (childrenTypesChanged(original) && options::ufHo()) + if (childrenTypesChanged(original) && options().uf.ufHo) { throw TypeCheckingExceptionPrivate( original, diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp index 7242be54c..06b4f0ba1 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.cpp +++ b/src/preprocessing/passes/extended_rewriter_pass.cpp @@ -36,7 +36,7 @@ PreprocessingPassResult ExtRewPre::applyInternal( assertionsToPreprocess->replace( i, extendedRewrite((*assertionsToPreprocess)[i], - options::extRewPrepAgg())); + options().smt.extRewPrepAgg)); } return PreprocessingPassResult::NO_CONFLICT; } diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index 515cc4a32..d3372a28e 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -180,7 +180,7 @@ Node HoElim::eliminateHo(Node n) if (cur.isVar()) { Node ret = cur; - if (options::hoElim()) + if (options().quantifiers.hoElim) { if (tn.isFunction()) { @@ -203,7 +203,7 @@ Node HoElim::eliminateHo(Node n) else { d_visited[cur] = Node::null(); - if (cur.getKind() == APPLY_UF && options::hoElim()) + if (cur.getKind() == APPLY_UF && options().quantifiers.hoElim) { Node op = cur.getOperator(); // convert apply uf with variable arguments eagerly to ho apply @@ -275,7 +275,7 @@ Node HoElim::eliminateHo(Node n) children.insert(children.begin(), retOp); } // process ho apply - if (ret.getKind() == HO_APPLY && options::hoElim()) + if (ret.getKind() == HO_APPLY && options().quantifiers.hoElim) { TypeNode tnr = ret.getType(); tnr = getUSort(tnr); @@ -382,7 +382,7 @@ PreprocessingPassResult HoElim::applyInternal( // extensionality: process all function types for (const TypeNode& ftn : d_funTypes) { - if (options::hoElim()) + if (options().quantifiers.hoElim) { Node h = getHoApplyUf(ftn); Trace("ho-elim-ax") << "Make extensionality for " << h << std::endl; @@ -406,7 +406,7 @@ PreprocessingPassResult HoElim::applyInternal( // exists another function that acts like the "store" operator for // arrays, e.g. it is the same function with one I/O pair updated. // Without this axiom, the translation is model unsound. - if (options::hoElimStoreAx()) + if (options().quantifiers.hoElimStoreAx) { Node u = nm->mkBoundVar("u", uf); Node v = nm->mkBoundVar("v", uf); @@ -428,7 +428,7 @@ PreprocessingPassResult HoElim::applyInternal( Trace("ho-elim-ax") << "...store axiom : " << store << std::endl; } } - else if (options::hoElimStoreAx()) + else if (options().quantifiers.hoElimStoreAx) { Node u = nm->mkBoundVar("u", ftn); Node v = nm->mkBoundVar("v", ftn); diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h index 8b8dc08c2..80f8cda70 100644 --- a/src/preprocessing/passes/ho_elim.h +++ b/src/preprocessing/passes/ho_elim.h @@ -73,10 +73,10 @@ namespace passes { * * Based on options, this preprocessing pass may apply a subset o the above * steps. In particular: - * * If options::hoElim() is true, then step [2] is taken and extensionality + * * If hoElim is true, then step [2] is taken and extensionality * axioms are added in step [3]. - * * If options::hoElimStoreAx() is true, then store axioms are added in step 3. - * The form of these axioms depends on whether options::hoElim() is true. If it + * * If hoElimStoreAx is true, then store axioms are added in step 3. + * The form of these axioms depends on whether hoElim is true. If it * is true, the axiom is given in terms of the uninterpreted functions that * encode function sorts. If it is false, then the store axiom is given in terms * of the original function sorts. diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 46c75b560..e6b5a4bca 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -105,9 +105,9 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) Node IntToBV::intToBV(TNode n, NodeMap& cache) { - int size = options::solveIntAsBV(); + int size = options().smt.solveIntAsBV; AlwaysAssert(size > 0); - AlwaysAssert(!options::incrementalSolving()); + AlwaysAssert(!options().base.incrementalSolving); NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 434256d28..5f9b4fb1d 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -97,7 +97,7 @@ Node ITESimp::simpITE(util::ITEUtilities* ite_utils, TNode assertion) Node result = ite_utils->simpITE(assertion); Node res_rewritten = rewrite(result); - if (options::simplifyWithCareEnabled()) + if (options().smt.simplifyWithCareEnabled) { Chat() << "starting simplifyWithCare()" << endl; Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten); @@ -119,7 +119,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) bool simpDidALotOfWork = d_iteUtilities.simpIteDidALotOfWorkHeuristic(); if (simpDidALotOfWork) { - if (options::compressItes()) + if (options().smt.compressItes) { result = d_iteUtilities.compress(assertionsToPreprocess); } @@ -128,7 +128,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) { // if false, don't bother to reclaim memory here. NodeManager* nm = NodeManager::currentNM(); - if (nm->poolSize() >= options::zombieHuntThreshold()) + if (nm->poolSize() >= options().smt.zombieHuntThreshold) { Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl; @@ -136,7 +136,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) << " nodes before cleanup" << endl; d_iteUtilities.clear(); d_env.getRewriter()->clearCaches(); - nm->reclaimZombiesUntil(options::zombieHuntThreshold()); + nm->reclaimZombiesUntil(options().smt.zombieHuntThreshold); Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl; } @@ -145,7 +145,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) // Do theory specific preprocessing passes if (logicInfo().isTheoryEnabled(theory::THEORY_ARITH) - && !options::incrementalSolving()) + && !options().base.incrementalSolving) { if (!simpDidALotOfWork) { diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 3ef4b7e9f..c40a65bc1 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -75,7 +75,7 @@ void traceBackToAssertions(booleans::CircuitPropagator* propagator, MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "miplib-trick") { - if (!options::incrementalSolving()) + if (!options().base.incrementalSolving) { NodeManager::currentNM()->subscribeEvents(this); } @@ -83,7 +83,7 @@ MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext) MipLibTrick::~MipLibTrick() { - if (!options::incrementalSolving()) + if (!options().base.incrementalSolving) { NodeManager::currentNM()->unsubscribeEvents(this); } @@ -188,7 +188,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( { Assert(assertionsToPreprocess->getRealAssertionsEnd() == assertionsToPreprocess->size()); - Assert(!options::incrementalSolving()); + Assert(!options().base.incrementalSolving); context::Context fakeContext; TheoryEngine* te = d_preprocContext->getTheoryEngine(); @@ -586,7 +586,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( Assert(top_level_substs.getSubstitution(newAssertion[0]) == newAssertion[1]); } - else if (pos.getNumChildren() <= options::arithMLTrickSubstitutions()) + else if (pos.getNumChildren() + <= options().arith.arithMLTrickSubstitutions) { top_level_substs.addSubstitution(newAssertion[0], newAssertion[1]); Debug("miplib") << "addSubs: " << newAssertion[0] << " to " @@ -596,8 +597,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( { Debug("miplib") << "skipSubs: " << newAssertion[0] << " to " << newAssertion[1] - << " (threshold is " << options::arithMLTrickSubstitutions() - << ")" << endl; + << " (threshold is " + << options().arith.arithMLTrickSubstitutions << ")" << endl; } newAssertion = rewrite(newAssertion); Debug("miplib") << " " << newAssertion << endl; diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index c139f0a86..68fb89e1f 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -41,7 +41,7 @@ PreprocessingPassResult SortInferencePass::applyInternal( theory::SortInference* si = d_preprocContext->getTheoryEngine()->getSortInference(); - if (options::sortInference()) + if (options().smt.sortInference) { si->initialize(assertionsToPreprocess->ref()); std::map model_replace_f; @@ -80,7 +80,7 @@ PreprocessingPassResult SortInferencePass::applyInternal( } // only need to compute monotonicity on the resulting formula if we are // using this option - if (options::ufssFairnessMonotone()) + if (options().uf.ufssFairnessMonotone) { si->computeMonotonicity(assertionsToPreprocess->ref()); } diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 81d5cae84..a54d220e5 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -146,7 +146,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( Trace("srs-input") << "Make synth variables for types..." << std::endl; // We will generate a fixed number of variables per type. These are the // variables that appear as free variables in the rewrites we generate. - unsigned nvars = options::sygusRewSynthInputNVars(); + unsigned nvars = options().quantifiers.sygusRewSynthInputNVars; // must have at least one variable per type nvars = nvars < 1 ? 1 : nvars; std::map > tvars; @@ -162,7 +162,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( // our input does not contain a Boolean variable, we need not allocate any // Boolean variables here. unsigned useNVars = - (options::sygusRewSynthInputUseBool() || !tn.isBoolean()) + (options().quantifiers.sygusRewSynthInputUseBool || !tn.isBoolean()) ? nvars : (hasBoolVar ? 1 : 0); for (unsigned i = 0; i < useNVars; i++) @@ -276,7 +276,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( // we add variable constructors if we are not Boolean, we are interested // in purely propositional rewrites (via the option), or this term is // a Boolean variable. - if (!ctt.isBoolean() || options::sygusRewSynthInputUseBool() + if (!ctt.isBoolean() || options().quantifiers.sygusRewSynthInputUseBool || ct.getKind() == BOUND_VARIABLE) { for (const Node& v : tvars[ctt]) -- 2.30.2