From 874350b54bd0f275fa8af7ca7a7af186bde7c030 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 1 Oct 2020 10:36:14 -0500 Subject: (proof-new) Preprocessing passes use proper interfaces to assertions pipeline (#5164) This PR eliminates all uses of assertions pipeline that are not proper, which two-fold: (1) The assertion list should never be modified in a custom way (without going through replace / push_back), (2) Places where an assertion is "conjoined" to an existing spot in the vector should use conjoin instead of replace. This is required for proper proof generation. This fixes CVC4/cvc4-projects#75. --- src/preprocessing/assertion_pipeline.h | 8 +------- src/preprocessing/passes/ackermann.cpp | 10 +++++++--- src/preprocessing/passes/bv_gauss.cpp | 20 +++++++++++++------- src/preprocessing/passes/global_negate.cpp | 3 ++- src/preprocessing/passes/global_negate.h | 2 +- src/preprocessing/passes/ho_elim.cpp | 12 ++++-------- src/preprocessing/passes/ite_removal.cpp | 4 ++-- src/preprocessing/passes/ite_simp.cpp | 8 +++++--- src/preprocessing/passes/nl_ext_purify.cpp | 15 +++++++++------ src/preprocessing/passes/non_clausal_simp.cpp | 16 +++++++--------- src/preprocessing/passes/quantifier_macros.cpp | 8 +++++--- src/preprocessing/passes/quantifier_macros.h | 12 +++++++++++- src/preprocessing/passes/sygus_inference.cpp | 2 +- src/preprocessing/passes/sygus_inference.h | 2 +- src/preprocessing/passes/synth_rew_rules.cpp | 2 +- .../passes/unconstrained_simplifier.cpp | 9 ++++++--- src/preprocessing/util/ite_utilities.cpp | 14 ++++++++------ src/preprocessing/util/ite_utilities.h | 7 ++++--- src/smt/process_assertions.cpp | 14 +++++++------- 19 files changed, 95 insertions(+), 73 deletions(-) (limited to 'src') diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index 6ca430ac4..5c50903c5 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -49,9 +49,6 @@ class AssertionPipeline */ void clear(); - /** TODO (projects #75): remove this */ - Node& operator[](size_t i) { return d_nodes[i]; } - /** Get the assertion at index i */ const Node& operator[](size_t i) const { return d_nodes[i]; } /** @@ -72,9 +69,6 @@ class AssertionPipeline /** Same as above, with TrustNode */ void pushBackTrusted(theory::TrustNode trn); - /** TODO (projects #75): remove this */ - std::vector& ref() { return d_nodes; } - /** * Get the constant reference to the underlying assertions. It is only * possible to modify these via the replace methods below. @@ -134,7 +128,7 @@ class AssertionPipeline * @param n The substitution node * @param pg The proof generator that can provide a proof of n. */ - void addSubstitutionNode(Node n, ProofGenerator* pgen = nullptr); + void addSubstitutionNode(Node n, ProofGenerator* pg = nullptr); /** * Conjoin n to the assertion vector at position i. This replaces diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index a7b33ae26..af6cae796 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -276,9 +276,13 @@ void usortsToBitVectors(const LogicInfo& d_logic, for (size_t i = 0, size = assertions->size(); i < size; ++i) { Node old = (*assertions)[i]; - assertions->replace(i, usVarsToBVVars.apply((*assertions)[i])); - Trace("uninterpretedSorts-to-bv") - << " " << old << " => " << (*assertions)[i] << "\n"; + Node newA = usVarsToBVVars.apply((*assertions)[i]); + if (newA != old) + { + assertions->replace(i, newA); + Trace("uninterpretedSorts-to-bv") + << " " << old << " => " << (*assertions)[i] << "\n"; + } } } } diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index 05fee230e..eaba90561 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -737,8 +737,8 @@ PreprocessingPassResult BVGauss::applyInternal( } std::unordered_map subst; - std::vector& atpp = assertionsToPreprocess->ref(); + NodeManager* nm = NodeManager::currentNM(); for (const auto& eq : equations) { if (eq.second.size() <= 1) { continue; } @@ -756,11 +756,12 @@ PreprocessingPassResult BVGauss::applyInternal( << std::endl; if (ret != BVGauss::Result::INVALID) { - NodeManager *nm = NodeManager::currentNM(); if (ret == BVGauss::Result::NONE) { - atpp.clear(); - atpp.push_back(nm->mkConst(false)); + assertionsToPreprocess->clear(); + Node n = nm->mkConst(false); + assertionsToPreprocess->push_back(n); + return PreprocessingPassResult::CONFLICT; } else { @@ -773,7 +774,8 @@ PreprocessingPassResult BVGauss::applyInternal( { Node a = nm->mkNode(kind::EQUAL, p.first, p.second); Trace("bv-gauss-elim") << "added assertion: " << a << std::endl; - atpp.push_back(a); + // add new assertion + assertionsToPreprocess->push_back(a); } } } @@ -782,9 +784,13 @@ PreprocessingPassResult BVGauss::applyInternal( if (!subst.empty()) { /* delete (= substitute with true) obsolete assertions */ - for (auto& a : atpp) + const std::vector& aref = assertionsToPreprocess->ref(); + for (size_t i = 0, asize = aref.size(); i < asize; ++i) { - a = a.substitute(subst.begin(), subst.end()); + Node a = aref[i]; + Node as = a.substitute(subst.begin(), subst.end()); + // replace the assertion + assertionsToPreprocess->replace(i, as); } } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index 5d29add3c..00ca1efd3 100644 --- a/src/preprocessing/passes/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -27,7 +27,8 @@ namespace CVC4 { namespace preprocessing { namespace passes { -Node GlobalNegate::simplify(std::vector& assertions, NodeManager* nm) +Node GlobalNegate::simplify(const std::vector& assertions, + NodeManager* nm) { Assert(!assertions.empty()); Trace("cegqi-gn") << "Global negate : " << std::endl; diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h index 853e5a4dd..208b8d990 100644 --- a/src/preprocessing/passes/global_negate.h +++ b/src/preprocessing/passes/global_negate.h @@ -42,7 +42,7 @@ class GlobalNegate : public PreprocessingPass AssertionPipeline* assertionsToPreprocess) override; private: - Node simplify(std::vector& assertions, NodeManager* nm); + Node simplify(const std::vector& assertions, NodeManager* nm); }; } // namespace passes diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index 2b8b6f3bd..34645b441 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -353,12 +353,10 @@ PreprocessingPassResult HoElim::applyInternal( // add lambda lifting axioms as a conjunction to the first assertion if (!axioms.empty()) { - Node orig = (*assertionsToPreprocess)[0]; - axioms.push_back(orig); - Node conj = nm->mkNode(AND, axioms); + Node conj = nm->mkAnd(axioms); conj = theory::Rewriter::rewrite(conj); Assert(!expr::hasFreeVar(conj)); - assertionsToPreprocess->replace(0, conj); + assertionsToPreprocess->conjoin(0, conj); } axioms.clear(); @@ -450,12 +448,10 @@ PreprocessingPassResult HoElim::applyInternal( // add new axioms as a conjunction to the first assertion if (!axioms.empty()) { - Node orig = (*assertionsToPreprocess)[0]; - axioms.push_back(orig); - Node conj = nm->mkNode(AND, axioms); + Node conj = nm->mkAnd(axioms); conj = theory::Rewriter::rewrite(conj); Assert(!expr::hasFreeVar(conj)); - assertionsToPreprocess->replace(0, conj); + assertionsToPreprocess->conjoin(0, conj); } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 11ad27364..a75b6f5ad 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -43,12 +43,12 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) TrustNode trn = d_preprocContext->getIteRemover()->run( (*assertions)[i], newAsserts, newSkolems, true); // process - assertions->replace(i, trn.getNode()); + assertions->replaceTrusted(i, trn); Assert(newSkolems.size() == newAsserts.size()); for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) { imap[newSkolems[j]] = assertions->size(); - assertions->ref().push_back(newAsserts[j].getNode()); + assertions->pushBackTrusted(newAsserts[j]); } } for (unsigned i = 0, size = assertions->size(); i < size; ++i) diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 49a6fe603..8c99493ba 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -127,7 +127,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) { if (options::compressItes()) { - result = d_iteUtilities.compress(assertionsToPreprocess->ref()); + result = d_iteUtilities.compress(assertionsToPreprocess); } if (result) @@ -175,7 +175,8 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) { Node more = aiteu.reduceConstantIteByGCD(res); Debug("arith::ite::red") << " gcd->" << more << endl; - (*assertionsToPreprocess)[i] = Rewriter::rewrite(more); + Node morer = Rewriter::rewrite(more); + assertionsToPreprocess->replace(i, morer); } } } @@ -214,7 +215,8 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess) << " ->" << res << endl; Node more = aiteu.reduceConstantIteByGCD(res); Debug("arith::ite::red") << " gcd->" << more << endl; - (*assertionsToPreprocess)[i] = Rewriter::rewrite(more); + Node morer = Rewriter::rewrite(more); + assertionsToPreprocess->replace(i, morer); } } } diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index e4d79d614..88bdf2e5c 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -117,16 +117,19 @@ PreprocessingPassResult NlExtPurify::applyInternal( for (unsigned i = 0; i < size; ++i) { Node a = (*assertionsToPreprocess)[i]; - assertionsToPreprocess->replace(i, purifyNlTerms(a, cache, bcache, var_eq)); - Trace("nl-ext-purify") << "Purify : " << a << " -> " - << (*assertionsToPreprocess)[i] << "\n"; + Node ap = purifyNlTerms(a, cache, bcache, var_eq); + if (a != ap) + { + assertionsToPreprocess->replace(i, ap); + Trace("nl-ext-purify") + << "Purify : " << a << " -> " << (*assertionsToPreprocess)[i] << "\n"; + } } if (!var_eq.empty()) { unsigned lastIndex = size - 1; - var_eq.insert(var_eq.begin(), (*assertionsToPreprocess)[lastIndex]); - assertionsToPreprocess->replace( - lastIndex, NodeManager::currentNM()->mkNode(kind::AND, var_eq)); + Node veq = NodeManager::currentNM()->mkAnd(var_eq); + assertionsToPreprocess->conjoin(lastIndex, veq); } return PreprocessingPassResult::NO_CONFLICT; } diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 2ca9f783f..fcb6dd171 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -375,11 +375,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal( } } - NodeBuilder<> learnedBuilder(kind::AND); Assert(assertionsToPreprocess->getRealAssertionsEnd() <= assertionsToPreprocess->size()); - learnedBuilder << (*assertionsToPreprocess) - [assertionsToPreprocess->getRealAssertionsEnd() - 1]; + std::vector learnedLitsToConjoin; for (size_t i = 0; i < learned_literals.size(); ++i) { @@ -406,7 +404,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( continue; } s.insert(learned); - learnedBuilder << learned; + learnedLitsToConjoin.push_back(learned); Trace("non-clausal-simplify") << "non-clausal learned : " << learned << std::endl; } @@ -428,7 +426,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( continue; } s.insert(cProp); - learnedBuilder << cProp; + learnedLitsToConjoin.push_back(cProp); Trace("non-clausal-simplify") << "non-clausal constant propagation : " << cProp << std::endl; } @@ -439,11 +437,11 @@ PreprocessingPassResult NonClausalSimp::applyInternal( // substituting top_level_substs.addSubstitutions(newSubstitutions); - if (learnedBuilder.getNumChildren() > 1) + if (!learnedLitsToConjoin.empty()) { - assertionsToPreprocess->replace( - assertionsToPreprocess->getRealAssertionsEnd() - 1, - Rewriter::rewrite(Node(learnedBuilder))); + size_t replIndex = assertionsToPreprocess->getRealAssertionsEnd() - 1; + Node newConj = NodeManager::currentNM()->mkAnd(learnedLitsToConjoin); + assertionsToPreprocess->conjoin(replIndex, newConj); } propagator->setNeedsFinish(true); diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 7713dbc1b..8fea4cbac 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -49,7 +49,7 @@ PreprocessingPassResult QuantifierMacros::applyInternal( bool success; do { - success = simplify(assertionsToPreprocess->ref(), true); + success = simplify(assertionsToPreprocess, true); } while (success); finalizeDefinitions(); clearMaps(); @@ -67,7 +67,9 @@ void QuantifierMacros::clearMaps() d_ground_macros = false; } -bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ +bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite) +{ + const std::vector& assertions = ap->ref(); unsigned rmax = options::macrosQuantMode() == options::MacrosQuantMode::ALL ? 2 : 1; for( unsigned r=0; r& assertions, bool doRewrite } } } - assertions[i] = curr; + ap->replace(i, curr); retVal = true; } } diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h index 59a4bee2d..c5e557a9e 100644 --- a/src/preprocessing/passes/quantifier_macros.h +++ b/src/preprocessing/passes/quantifier_macros.h @@ -64,7 +64,17 @@ class QuantifierMacros : public PreprocessingPass bool reqComplete); void addMacro(Node op, Node n, std::vector& opc); void debugMacroDefinition(Node oo, Node n); - bool simplify(std::vector& assertions, bool doRewrite = false); + /** + * This applies macro elimination to the given pipeline, which discovers + * whether there are any quantified formulas corresponding to macros. + * + * @param ap The pipeline to apply macros to. + * @param doRewrite Whether we also wish to rewrite the assertions based on + * the discovered macro definitions. + * @return Whether new definitions were inferred and we rewrote the assertions + * based on them. + */ + bool simplify(AssertionPipeline* ap, bool doRewrite = false); Node simplify(Node n); void finalizeDefinitions(); void clearMaps(); diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 0b27d0c17..cdacd740a 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -80,7 +80,7 @@ PreprocessingPassResult SygusInference::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } -bool SygusInference::solveSygus(std::vector& assertions, +bool SygusInference::solveSygus(const std::vector& assertions, std::vector& funs, std::vector& sols) { diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h index 02965c8ed..31d94efd2 100644 --- a/src/preprocessing/passes/sygus_inference.h +++ b/src/preprocessing/passes/sygus_inference.h @@ -59,7 +59,7 @@ class SygusInference : public PreprocessingPass * If this function returns true, then we add all uninterpreted symbols s in * assertions to funs and their corresponding solution to sols. */ - bool solveSygus(std::vector& assertions, + bool solveSygus(const std::vector& assertions, std::vector& funs, std::vector& sols); }; diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 2ca11eb81..8465a63a0 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -40,7 +40,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( { Trace("srs-input") << "Synthesize rewrite rules from assertions..." << std::endl; - std::vector& assertions = assertionsToPreprocess->ref(); + const std::vector& assertions = assertionsToPreprocess->ref(); if (assertions.empty()) { return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 64080987b..9b4d02032 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -842,7 +842,7 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal( { d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); - std::vector& assertions = assertionsToPreprocess->ref(); + const std::vector& assertions = assertionsToPreprocess->ref(); d_context->push(); @@ -855,9 +855,12 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal( { processUnconstrained(); // d_substitutions.print(Message.getStream()); - for (Node& assertion : assertions) + for (size_t i = 0, asize = assertions.size(); i < asize; ++i) { - assertion = Rewriter::rewrite(d_substitutions.apply(assertion)); + Node a = assertions[i]; + Node as = Rewriter::rewrite(d_substitutions.apply(a)); + // replace the assertion + assertionsToPreprocess->replace(i, as); } } diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index c72da1621..c9bf283ac 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -130,13 +130,13 @@ bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const } /* returns false if an assertion is discovered to be equal to false. */ -bool ITEUtilities::compress(std::vector& assertions) +bool ITEUtilities::compress(AssertionPipeline* assertionsToPreprocess) { if (d_compressor == NULL) { d_compressor = new ITECompressor(d_containsVisitor.get()); } - return d_compressor->compress(assertions); + return d_compressor->compress(assertionsToPreprocess); } Node ITEUtilities::simplifyWithCare(TNode e) @@ -527,17 +527,18 @@ Node ITECompressor::compressBoolean(Node toCompress) } } -bool ITECompressor::compress(std::vector& assertions) +bool ITECompressor::compress(AssertionPipeline* assertionsToPreprocess) { reset(); - d_assertions = &assertions; - d_incoming.computeReachability(assertions); + d_assertions = assertionsToPreprocess; + d_incoming.computeReachability(assertionsToPreprocess->ref()); ++(d_statistics.d_compressCalls); Chat() << "Computed reachability" << endl; bool nofalses = true; + const std::vector& assertions = assertionsToPreprocess->ref(); size_t original_size = assertions.size(); Chat() << "compressing " << original_size << endl; for (size_t i = 0; i < original_size && nofalses; ++i) @@ -545,7 +546,8 @@ bool ITECompressor::compress(std::vector& assertions) Node assertion = assertions[i]; Node compressed = compressBoolean(assertion); Node rewritten = theory::Rewriter::rewrite(compressed); - assertions[i] = rewritten; + // replace + assertionsToPreprocess->replace(i, rewritten); Assert(!d_contains->containsTermITE(rewritten)); nofalses = (rewritten != d_false); diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h index fbddf7169..c82bf7958 100644 --- a/src/preprocessing/util/ite_utilities.h +++ b/src/preprocessing/util/ite_utilities.h @@ -27,6 +27,7 @@ #include #include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" #include "util/hash.h" #include "util/statistics_registry.h" @@ -74,7 +75,7 @@ class ITEUtilities bool simpIteDidALotOfWorkHeuristic() const; /* returns false if an assertion is discovered to be equal to false. */ - bool compress(std::vector& assertions); + bool compress(AssertionPipeline* assertionsToPreprocess); Node simplifyWithCare(TNode e); @@ -167,7 +168,7 @@ class ITECompressor ~ITECompressor(); /* returns false if an assertion is discovered to be equal to false. */ - bool compress(std::vector& assertions); + bool compress(AssertionPipeline* assertionsToPreprocess); /* garbage Collects the compressor. */ void garbageCollect(); @@ -176,7 +177,7 @@ class ITECompressor Node d_true; /* Copy of true. */ Node d_false; /* Copy of false. */ ContainsTermITEVisitor* d_contains; - std::vector* d_assertions; + AssertionPipeline* d_assertions; IncomingArcCounter d_incoming; typedef std::unordered_map NodeMap; diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 504814e07..971288b67 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -339,8 +339,7 @@ bool ProcessAssertions::apply(Assertions& as) // assertion IteSkolemMap::iterator it = iskMap.begin(); IteSkolemMap::iterator iend = iskMap.end(); - NodeBuilder<> builder(AND); - builder << assertions[assertions.getRealAssertionsEnd() - 1]; + std::vector newConj; vector toErase; for (; it != iend; ++it) { @@ -367,19 +366,20 @@ bool ProcessAssertions::apply(Assertions& as) } } // Move this iteExpr into the main assertions - builder << assertions[(*it).second]; - assertions[(*it).second] = d_true; + newConj.push_back(assertions[(*it).second]); + assertions.replace((*it).second, d_true); toErase.push_back((*it).first); } - if (builder.getNumChildren() > 1) + if (!newConj.empty()) { while (!toErase.empty()) { iskMap.erase(toErase.back()); toErase.pop_back(); } - assertions[assertions.getRealAssertionsEnd() - 1] = - Rewriter::rewrite(Node(builder)); + size_t index = assertions.getRealAssertionsEnd() - 1; + Node newAssertion = NodeManager::currentNM()->mkAnd(newConj); + assertions.conjoin(index, newAssertion); } // TODO(b/1256): For some reason this is needed for some benchmarks, such // as -- cgit v1.2.3