From c3f5365a95a7eac2419a2f95ff240909f275cc08 Mon Sep 17 00:00:00 2001 From: Can Cebeci Date: Tue, 26 May 2026 15:08:11 -0700 Subject: [PATCH] Update generation number of already-internalized enodes (#9628) Below are the effects on Mariposa's unsat core: | Query | Unsats before | Unknowns before | Timeouts before | Unsats after | Unknowns after | Timeouts after | Delta Unsat | Delta Unknown | Delta Timeout | |---|---:|---:|---:|---:|---:|---:|---:|---:|---:| | d_fvbkv-Betree-BetreeInv.i.dfy.Impl__BetreeInv.__default.FlushPreservesLookups.smt2 | 94 | 5 | 1 | 99 | 0 | 1 | +5 | -5 | +0 | | d_fvbkv-ByteBlockCacheSystem-ByteSystem.i.dfy.Impl__ByteSystem.__default.ReqWrite2StepPreservesInv.smt2 | 41 | 0 | 59 | 44 | 0 | 56 | +3 | +0 | -3 | | d_fvbkv-ByteBlockCacheSystem-InterpretationDisk.i.dfy.Impl__InterpretationDisk.__default.RefinesProcessWrite.smt2 | 75 | 25 | 0 | 99 | 1 | 0 | +24 | -24 | +0 | | d_fvbkv-Impl-FlushPolicyImpl.i.dfy.Impl__FlushPolicyImpl.__default.runFlushPolicy.smt2 | 12 | 0 | 88 | 6 | 0 | 94 | -6 | +0 | +6 | | d_fvbkv-Impl-IOImpl.i.dfy.Impl__IOImpl.__default.PageInNodeResp.smt2 | 84 | 0 | 16 | 81 | 0 | 19 | -3 | +0 | +3 | | d_fvbkv-Impl-JournalistModel.i.dfy.CheckWellformed__JournalistModel.__default.append.smt2 | 88 | 12 | 0 | 99 | 1 | 0 | +11 | -11 | +0 | | d_fvbkv-Impl-QueryImpl.i.dfy.Impl__QueryImpl.__default.queryIterate.smt2 | 48 | 0 | 52 | 43 | 0 | 57 | -5 | +0 | +5 | | d_fvbkv-lib-Base-BitsetLemmas.i.dfy.Impl__BitsetLemmas.__default.set__bit__to__0__self__uint64.smt2 | 100 | 0 | 0 | 100 | 0 | 0 | +0 | +0 | +0 | | d_fvbkv-lib-Base-BitsetLemmas.i.dfy.Impl__BitsetLemmas.__default.set__bit__to__1__self__uint64.smt2 | 100 | 0 | 0 | 100 | 0 | 0 | +0 | +0 | +0 | | d_fvbkv-lib-Buckets-KMBPKVOps.i.dfy.Impl__KMBPKVOps.__default.IndexFillDpkv.smt2 | 42 | 0 | 58 | 41 | 0 | 59 | -1 | +0 | +1 | | d_fvbkv-lib-Buckets-PackedKV.i.dfy.Impl__PackedKV.__default.BinarySearchQuery.smt2 | 78 | 5 | 17 | 92 | 1 | 7 | +14 | -4 | -10 | | d_fvbkv-lib-Buckets-PackedStringArray.i.dfy.Impl__PackedStringArray.__default.UniqueRepr.smt2 | 100 | 0 | 0 | 100 | 0 | 0 | +0 | +0 | +0 | | d_fvbkv-lib-Buckets-PackedStringArray.i.dfy.Impl__PackedStringArray.__default.WFpsaSubSeq.smt2 | 90 | 1 | 9 | 82 | 0 | 18 | -8 | -1 | +9 | | d_fvbkv-lib-DataStructures-BtreeModel.i.dfy.Impl__BtreeModel.__default.SplitIndexAllKeys.smt2 | 8 | 0 | 92 | 9 | 0 | 91 | +1 | +0 | -1 | | d_fvbkv-lib-DataStructures-LruImpl.i.dfy.Impl__LruImpl.LruImplQueue.Use.smt2 | 92 | 5 | 3 | 97 | 0 | 3 | +5 | -5 | +0 | | d_fvbkv-lib-DataStructures-MutableBtree.i.dfy.Impl__MutableBtree.__default.SubIndex.smt2 | 44 | 28 | 28 | 50 | 2 | 48 | +6 | -26 | +20 | | d_fvbkv-lib-DataStructures-MutableBtree.i.dfy.Impl__MutableBtree.__default.SubReprLowerBound.smt2 | 96 | 4 | 0 | 98 | 2 | 0 | +2 | -2 | +0 | | d_fvbkv-lib-Marshalling-GenericMarshalling.i.dfy.Impl__GenericMarshalling.__default.MarshallArray.smt2 | 46 | 54 | 0 | 76 | 24 | 0 | +30 | -30 | +0 | | d_fvbkv-lib-Marshalling-GenericMarshalling.i.dfy.Impl__GenericMarshalling.__default.MarshallUint32Array.smt2 | 81 | 19 | 0 | 96 | 3 | 1 | +15 | -16 | +1 | | d_fvbkv-lib-Marshalling-GenericMarshalling.i.dfy.Impl__GenericMarshalling.__default.MarshallUint64Array.smt2 | 85 | 15 | 0 | 95 | 5 | 0 | +10 | -10 | +0 | | d_fvbkv-lib-Marshalling-Math.i.dfy.Impl__Math.__default.lemma__2toX.smt2 | 74 | 26 | 0 | 100 | 0 | 0 | +26 | -26 | +0 | | d_fvbkv-lib-Marshalling-Math.i.dfy.Impl__Math.__default.lemma__div__denominator.smt2 | 93 | 0 | 7 | 99 | 0 | 1 | +6 | +0 | -6 | | d_fvbkv-lib-Math-mod_auto_proofs.i.dfy.Impl__Math____mod__auto__proofs__i.__default.lemma__mod__induction__forall2.smt2 | 67 | 0 | 33 | 67 | 0 | 33 | +0 | +0 | +0 | | d_fvbkv-lib-Math-mod_auto_proofs.i.dfy.Impl__Math____mod__auto__proofs__i.__default.lemma__mod__induction__forall.smt2 | 0 | 0 | 100 | 0 | 0 | 100 | +0 | +0 | +0 | | d_fvbkv-lib-Math-mul.i.dfy.Impl__Math____mul__i.__default.lemma__mul__nonnegative.smt2 | 0 | 0 | 100 | 0 | 0 | 100 | +0 | +0 | +0 | | d_komodo-verified-ptebits.i.dfyImpl___module.__default.lemma__l1ptesmatch.smt2 | 59 | 0 | 41 | 68 | 0 | 32 | +9 | +0 | -9 | | d_komodo-verified-secprop-conf_ni.i.dfyImpl___module.__default.lemma__initL2PTable__loweq__pdb.smt2 | 81 | 0 | 19 | 85 | 0 | 15 | +4 | +0 | -4 | | d_komodo-verified-sha-sha256-body-00-15.gen.dfyImpl___module.__default.va__refined__Body__00__15UnrolledRecursive.smt2 | 0 | 0 | 100 | 0 | 0 | 100 | +0 | +0 | +0 | | d_komodo-verified-sha-sha256-body-16-xx.gen.dfyImpl___module.__default.va__refined__Body__16__XXUnroller.smt2 | 8 | 0 | 92 | 9 | 0 | 91 | +1 | +0 | -1 | | d_komodo-verified-sha-sha256.i.dfyImpl___module.__default.lemma__SHA256FinalHelper1.smt2 | 95 | 0 | 5 | 95 | 1 | 4 | +0 | +1 | -1 | | d_komodo-verified-verify.gen.dfyImpl___module.__default.va__lemma__svc__returning__verify__inner_k.smt2 | 9 | 0 | 91 | 6 | 0 | 94 | -3 | +0 | +3 | | d_komodo-verified-verify.gen.dfyImpl___module.__default.va__lemma__svc__returning__verify__inner.smt2 | 69 | 0 | 31 | 61 | 0 | 39 | -8 | +0 | +8 | | d_komodo-verified-verify.gen.dfyImpl___module.__default.va__lemma__svc__returning__verify.smt2 | 85 | 0 | 15 | 78 | 0 | 22 | -7 | +0 | +7 | | d_lvbkv-Impl-BucketGeneratorModel.i.dfy.Impl__BucketGeneratorModel.__default.GenComposeIsCompose.smt2 | 53 | 0 | 47 | 53 | 0 | 47 | +0 | +0 | +0 | | d_lvbkv-Impl-JournalistImpl.i.dfy.Impl__JournalistImpl.Journalist.append.smt2 | 93 | 4 | 3 | 96 | 0 | 4 | +3 | -4 | +1 | | d_lvbkv-Impl-MarshallingImpl.i.dfy.Impl__MarshallingImpl.__default.strictlySortedPivotsToVal.smt2 | 5 | 0 | 95 | 0 | 0 | 100 | -5 | +0 | +5 | | d_lvbkv-lib-Base-total_order_impl.i.dfy.Impl__Total__Order__Impl.__default.ArrayLargestLtePlus1Linear.smt2 | 48 | 52 | 0 | 99 | 1 | 0 | +51 | -51 | +0 | | d_lvbkv-lib-Buckets-BucketsLib.i.dfy.Impl__BucketsLib.__default.WFProperSplitBucketInList.smt2 | 39 | 22 | 39 | 40 | 15 | 45 | +1 | -7 | +6 | | d_lvbkv-lib-Buckets-PackedKV.i.dfy.Impl__DynamicPkv.DynamicPkv.Append.smt2 | 80 | 0 | 20 | 80 | 0 | 20 | +0 | +0 | +0 | | d_lvbkv-lib-Buckets-PackedKV.i.dfy.Impl__PackedKV.__default.BinarySearchQuery.smt2 | 15 | 5 | 80 | 11 | 0 | 89 | -4 | -5 | +9 | | d_lvbkv-lib-Buckets-PackedStringArray.i.dfy.Impl__PackedStringArray.__default.psaCanAppendI.smt2 | 61 | 0 | 39 | 70 | 0 | 30 | +9 | +0 | -9 | | d_lvbkv-lib-Buckets-PackedStringArray.i.dfy.Impl__PackedStringArray.DynamicPsa.AppendSeq.smt2 | 2 | 0 | 98 | 4 | 0 | 96 | +2 | +0 | -2 | | d_lvbkv-lib-Checksums-BitLemmas.i.dfy.Impl__BitLemmas.__default.eq__from__unpack__LittleEndian__Uint32__eq.smt2 | 99 | 0 | 1 | 99 | 0 | 1 | +0 | +0 | +0 | | d_lvbkv-lib-DataStructures-LinearContentMutableMap.i.dfy.Impl__LinearContentMutableMap.__default.Realloc.smt2 | 1 | 0 | 99 | 0 | 0 | 100 | -1 | +0 | +1 | | d_lvbkv-lib-DataStructures-LinearDList.i.dfy.Impl__DList.DList.InsertAfter.smt2 | 0 | 0 | 100 | 0 | 0 | 100 | +0 | +0 | +0 | | d_lvbkv-lib-DataStructures-LinearDList.i.dfy.Impl__DList.DList.InsertBefore.smt2 | 0 | 2 | 98 | 0 | 1 | 99 | +0 | -1 | +1 | | d_lvbkv-lib-DataStructures-MutableBtree.i.dfy.Impl__LMutableBtree.__default.InsertIndex.smt2 | 98 | 0 | 2 | 83 | 0 | 17 | -15 | +0 | +15 | | d_lvbkv-lib-Lang-LinearSequence.i.dfy.Impl__LinearSequence__i.__default.AllocAndMoveLseq.smt2 | 97 | 3 | 0 | 100 | 0 | 0 | +3 | -3 | +0 | | d_lvbkv-lib-Marshalling-GenericMarshalling.i.dfy.Impl__GenericMarshalling.__default.MarshallArray.smt2 | 79 | 21 | 0 | 77 | 23 | 0 | -2 | +2 | +0 | | d_lvbkv-lib-Marshalling-GenericMarshalling.i.dfy.Impl__GenericMarshalling.__default.MarshallByteArrayInterior.smt2 | 100 | 0 | 0 | 100 | 0 | 0 | +0 | +0 | +0 | | d_lvbkv-lib-Marshalling-GenericMarshalling.i.dfy.Impl__GenericMarshalling.__default.MarshallByteArray.smt2 | 94 | 6 | 0 | 98 | 2 | 0 | +4 | -4 | +0 | | d_lvbkv-lib-Math-Nonlinear.i.dfy.Impl__NonlinearLemmas.__default.div__denom__ge__1.smt2 | 91 | 9 | 0 | 97 | 3 | 0 | +6 | -6 | +0 | | d_lvbkv-MapSpec-TSJMap_Refines_ThreeStateVersionedMap.i.dfy.Impl__TSJMap__Refines__ThreeStateVersionedMap.__default.RefinesReplay.smt2 | 69 | 0 | 31 | 66 | 0 | 34 | -3 | +0 | +3 | | d_lvbkv-PivotBetree-PivotBetreeSpecRefinement.i.dfy.Impl__PivotBetreeSpecRefinement.__default.SplitChildrenConsistent.smt2 | 31 | 0 | 69 | 28 | 0 | 72 | -3 | +0 | +3 | | d_lvbkv-PivotBetree-PivotBetreeSpecWFNodes.i.dfy.Impl__PivotBetreeSpecWFNodes.__default.ValidSplitWritesInvNodes.smt2 | 100 | 0 | 0 | 99 | 0 | 1 | -1 | +0 | +1 | | fs_dice-queries-ASN1.Low.Base-3.smt2 | 1 | 32 | 0 | 1 | 32 | 0 | +0 | +0 | +0 | | fs_dice-queries-L0.X509.AliasKeyTBS.Issuer-7.smt2 | 33 | 0 | 0 | 33 | 0 | 0 | +0 | +0 | +0 | | fs_dice-queries-L0.X509.AliasKeyTBS.Subject-7.smt2 | 33 | 0 | 0 | 33 | 0 | 0 | +0 | +0 | +0 | | s_komodo-1504.4.smt2 | 0 | 0 | 100 | 0 | 0 | 100 | +0 | +0 | +0 | --------- Co-authored-by: Can Cebeci Co-authored-by: Nikolaj Bjorner --- src/smt/smt_case_split_queue.cpp | 2 +- src/smt/smt_context.h | 7 +++++++ src/smt/smt_enode.cpp | 5 +++-- src/smt/smt_enode.h | 2 +- src/smt/smt_internalizer.cpp | 18 +++++++++++++++--- 5 files changed, 27 insertions(+), 7 deletions(-) diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index d43dd0fb8..029758b85 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -1046,7 +1046,7 @@ namespace { void operator()(expr * e) { if (m_context.e_internalized(e)) { enode * n = m_context.get_enode(e); - n->set_generation(m_context, m_generation); + n->set_generation(&m_context, m_generation); } } }; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 02da5d15f..6b84e8d6a 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -785,6 +785,13 @@ namespace smt { return get_bdata(get_bool_var(n)); } + void update_generation(enode * n); + + void update_generation(expr * e) { + if (is_app(e) && e_internalized(e)) + update_generation(get_enode(to_app(e))); + } + typedef std::pair expr_bool_pair; void ts_visit_child(expr * n, bool gate_ctx, svector & todo, bool & visited); diff --git a/src/smt/smt_enode.cpp b/src/smt/smt_enode.cpp index 99424c8ed..b1965c2f3 100644 --- a/src/smt/smt_enode.cpp +++ b/src/smt/smt_enode.cpp @@ -136,10 +136,11 @@ namespace smt { \brief Push old value of generation on the context trail stack and update the generation. */ - void enode::set_generation(context & ctx, unsigned generation) { + void enode::set_generation(context * ctx, unsigned generation) { if (m_generation == generation) return; - ctx.push_trail(value_trail(m_generation)); + if (ctx) + ctx->push_trail(value_trail(m_generation)); m_generation = generation; } diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index 3f488a3b7..ab3dcd141 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -386,7 +386,7 @@ namespace smt { return m_generation; } - void set_generation(context & ctx, unsigned generation); + void set_generation(context * ctx, unsigned generation); /** \brief Return the enode n that is in the eqc of *this, and has the minimal generation. diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index d742aadf1..7e32eaaf6 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -101,6 +101,11 @@ namespace smt { } } + void context::update_generation(enode * e) { + if (0 < m_generation && m_generation < e->get_generation()) + e->set_generation(nullptr, m_generation); + } + void context::ts_visit_child(expr * n, bool gate_ctx, svector & todo, bool & visited) { if (get_color(tcolors, fcolors, n, gate_ctx) == White) { todo.push_back(expr_bool_pair(n, gate_ctx)); @@ -115,12 +120,16 @@ namespace smt { return true; SASSERT(is_app(n)); if (m.is_bool(n)) { - if (b_internalized(n)) + if (b_internalized(n)) { + update_generation(n); return true; + } } else { - if (e_internalized(n)) + update_generation(n); + if (e_internalized(n)) return true; + } bool visited = true; @@ -404,6 +413,8 @@ namespace smt { bool_var v = get_bool_var(n); TRACE(internalize_bug, tout << "#" << n->get_id() << " already has bool_var v" << v << "\n";); + update_generation(n); + // n was already internalized as boolean, but an enode was // not associated with it. So, an enode is necessary, if // n is not in the context of a gate and is an application. @@ -810,6 +821,8 @@ namespace smt { */ void context::internalize_term(app * n) { if (e_internalized(n)) { + enode * e = get_enode(n); + update_generation(e); theory * th = m_theories.get_plugin(n->get_family_id()); if (th != nullptr) { // This code is necessary because some theories may decide @@ -822,7 +835,6 @@ namespace smt { // Later, the core tries to internalize (f (* 2 x)). // Now, (* 2 x) is not internal to arithmetic anymore, // and a theory variable must be created for it. - enode * e = get_enode(n); if (!th->is_attached_to_var(e)) th->internalize_term(n); }