Skip to content

Initialize m_max_generation to 0#9694

Open
CanCebeci wants to merge 1 commit into
Z3Prover:masterfrom
CanCebeci:generation-fix
Open

Initialize m_max_generation to 0#9694
CanCebeci wants to merge 1 commit into
Z3Prover:masterfrom
CanCebeci:generation-fix

Conversation

@CanCebeci
Copy link
Copy Markdown
Contributor

The current implementation is sensitive to which enode within the eclass gets passed as a candidate to the mam. If the candidate has a high generation, mam will overshoot max_generation,

Below are the effects on Mariposa. This eliminates unknowns form almost all queries. In terms of additional timeouts, only d_komodo-verified-sha-sha256.i.dfyImpl___module.__default.lemma__SHA256FinalHelper1.smt2 seems to suffer significantly.

'Before' refers to existing measurements from the previous generation patch (#9628), NOT the commit this patch is based on.

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 99 0 1 98 0 2 -1 0 +1
d_fvbkv-ByteBlockCacheSystem-ByteSystem.i.dfy.Impl__ByteSystem.__default.ReqWrite2StepPreservesInv.smt2 44 0 56 43 0 57 -1 0 +1
d_fvbkv-ByteBlockCacheSystem-InterpretationDisk.i.dfy.Impl__InterpretationDisk.__default.RefinesProcessWrite.smt2 99 1 0 100 0 0 +1 -1 0
d_fvbkv-Impl-FlushPolicyImpl.i.dfy.Impl__FlushPolicyImpl.__default.runFlushPolicy.smt2 6 0 94 8 0 92 +2 0 -2
d_fvbkv-Impl-IOImpl.i.dfy.Impl__IOImpl.__default.PageInNodeResp.smt2 81 0 19 87 0 13 +6 0 -6
d_fvbkv-Impl-JournalistModel.i.dfy.CheckWellformed__JournalistModel.__default.append.smt2 99 1 0 100 0 0 +1 -1 0
d_fvbkv-Impl-QueryImpl.i.dfy.Impl__QueryImpl.__default.queryIterate.smt2 43 0 57 47 0 53 +4 0 -4
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 41 0 59 38 0 62 -3 0 +3
d_fvbkv-lib-Buckets-PackedKV.i.dfy.Impl__PackedKV.__default.BinarySearchQuery.smt2 92 1 7 87 0 13 -5 -1 +6
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 82 0 18 92 0 8 +10 0 -10
d_fvbkv-lib-DataStructures-BtreeModel.i.dfy.Impl__BtreeModel.__default.SplitIndexAllKeys.smt2 9 0 91 6 0 94 -3 0 +3
d_fvbkv-lib-DataStructures-LruImpl.i.dfy.Impl__LruImpl.LruImplQueue.Use.smt2 97 0 3 97 0 3 0 0 0
d_fvbkv-lib-DataStructures-MutableBtree.i.dfy.Impl__MutableBtree.__default.SubIndex.smt2 50 2 48 58 0 42 +8 -2 -6
d_fvbkv-lib-DataStructures-MutableBtree.i.dfy.Impl__MutableBtree.__default.SubReprLowerBound.smt2 98 2 0 100 0 0 +2 -2 0
d_fvbkv-lib-Marshalling-GenericMarshalling.i.dfy.Impl__GenericMarshalling.__default.MarshallArray.smt2 76 24 0 100 0 0 +24 -24 0
d_fvbkv-lib-Marshalling-GenericMarshalling.i.dfy.Impl__GenericMarshalling.__default.MarshallUint32Array.smt2 96 3 1 100 0 0 +4 -3 -1
d_fvbkv-lib-Marshalling-GenericMarshalling.i.dfy.Impl__GenericMarshalling.__default.MarshallUint64Array.smt2 95 5 0 100 0 0 +5 -5 0
d_fvbkv-lib-Marshalling-Math.i.dfy.Impl__Math.__default.lemma__2toX.smt2 100 0 0 100 0 0 0 0 0
d_fvbkv-lib-Marshalling-Math.i.dfy.Impl__Math.__default.lemma__div__denominator.smt2 99 0 1 90 0 10 -9 0 +9
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 68 0 32 60 0 40 -8 0 +8
d_komodo-verified-secprop-conf_ni.i.dfyImpl___module.__default.lemma__initL2PTable__loweq__pdb.smt2 85 0 15 84 0 16 -1 0 +1
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 9 0 91 5 0 95 -4 0 +4
d_komodo-verified-sha-sha256.i.dfyImpl___module.__default.lemma__SHA256FinalHelper1.smt2 95 1 4 5 0 95 -90 -1 +91
d_komodo-verified-verify.gen.dfyImpl___module.__default.va__lemma__svc__returning__verify__inner_k.smt2 6 0 94 11 0 89 +5 0 -5
d_komodo-verified-verify.gen.dfyImpl___module.__default.va__lemma__svc__returning__verify__inner.smt2 61 0 39 75 0 25 +14 0 -14
d_komodo-verified-verify.gen.dfyImpl___module.__default.va__lemma__svc__returning__verify.smt2 78 0 22 78 0 22 0 0 0
d_lvbkv-Impl-BucketGeneratorModel.i.dfy.Impl__BucketGeneratorModel.__default.GenComposeIsCompose.smt2 53 0 47 50 0 50 -3 0 +3
d_lvbkv-Impl-JournalistImpl.i.dfy.Impl__JournalistImpl.Journalist.append.smt2 96 0 4 98 0 2 +2 0 -2
d_lvbkv-Impl-MarshallingImpl.i.dfy.Impl__MarshallingImpl.__default.strictlySortedPivotsToVal.smt2 0 0 100 20 0 80 +20 0 -20
d_lvbkv-lib-Base-total_order_impl.i.dfy.Impl__Total__Order__Impl.__default.ArrayLargestLtePlus1Linear.smt2 99 1 0 100 0 0 +1 -1 0
d_lvbkv-lib-Buckets-BucketsLib.i.dfy.Impl__BucketsLib.__default.WFProperSplitBucketInList.smt2 40 15 45 58 0 42 +18 -15 -3
d_lvbkv-lib-Buckets-PackedKV.i.dfy.Impl__DynamicPkv.DynamicPkv.Append.smt2 80 0 20 79 0 21 -1 0 +1
d_lvbkv-lib-Buckets-PackedKV.i.dfy.Impl__PackedKV.__default.BinarySearchQuery.smt2 11 0 89 14 0 86 +3 0 -3
d_lvbkv-lib-Buckets-PackedStringArray.i.dfy.Impl__PackedStringArray.__default.psaCanAppendI.smt2 70 0 30 53 0 47 -17 0 +17
d_lvbkv-lib-Buckets-PackedStringArray.i.dfy.Impl__PackedStringArray.DynamicPsa.AppendSeq.smt2 4 0 96 1 0 99 -3 0 +3
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 0 0 100 1 0 99 +1 0 -1
d_lvbkv-lib-DataStructures-LinearDList.i.dfy.Impl__DList.DList.InsertAfter.smt2 0 0 100 0 2 98 0 +2 -2
d_lvbkv-lib-DataStructures-LinearDList.i.dfy.Impl__DList.DList.InsertBefore.smt2 0 1 99 0 2 98 0 +1 -1
d_lvbkv-lib-DataStructures-MutableBtree.i.dfy.Impl__LMutableBtree.__default.InsertIndex.smt2 83 0 17 80 0 20 -3 0 +3
d_lvbkv-lib-Lang-LinearSequence.i.dfy.Impl__LinearSequence__i.__default.AllocAndMoveLseq.smt2 100 0 0 100 0 0 0 0 0
d_lvbkv-lib-Marshalling-GenericMarshalling.i.dfy.Impl__GenericMarshalling.__default.MarshallArray.smt2 77 23 0 100 0 0 +23 -23 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 98 2 0 99 1 0 +1 -1 0
d_lvbkv-lib-Math-Nonlinear.i.dfy.Impl__NonlinearLemmas.__default.div__denom__ge__1.smt2 97 3 0 97 3 0 0 0 0
d_lvbkv-MapSpec-TSJMap_Refines_ThreeStateVersionedMap.i.dfy.Impl__TSJMap__Refines__ThreeStateVersionedMap.__default.RefinesReplay.smt2 66 0 34 74 0 26 +8 0 -8
d_lvbkv-PivotBetree-PivotBetreeSpecRefinement.i.dfy.Impl__PivotBetreeSpecRefinement.__default.SplitChildrenConsistent.smt2 28 0 72 42 0 58 +14 0 -14
d_lvbkv-PivotBetree-PivotBetreeSpecWFNodes.i.dfy.Impl__PivotBetreeSpecWFNodes.__default.ValidSplitWritesInvNodes.smt2 99 0 1 100 0 0 +1 0 -1
fs_dice-queries-ASN1.Low.Base-3.smt2 1 32 0 1 31 1 0 -1 +1
fs_dice-queries-L0.X509.AliasKeyTBS.Issuer-7.smt2 33 0 0 20 0 13 -13 0 +13
fs_dice-queries-L0.X509.AliasKeyTBS.Subject-7.smt2 33 0 0 22 0 11 -11 0 +11

The current implementation is sensitive to which enode within the eclass gets passed as a candidate to the mam. If the candidate has a high generation, mam will overshoot max_generation,

This patch stabilizes Mariposa's d_fvbkv-lib-Marshalling-GenericMarshalling.i.dfy.Impl__GenericMarshalling.__default.MarshallArray.smt2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant