Code

LRS updates and fixes#643

Code

Merged

quickbeam123 merged 32 commits intomastervprover/vampire:masterfrom martin-lrs-fixesvprover/vampire:martin-lrs-fixesCopy head branch name to clipboardJan 15, 2025

+2,031-1,624

Commits

Commits on Jan 9, 2025

• use a more precise statistics for the LRS estimate

  quickbeam123

  committed
  bc48b2b

  Copy full SHA for bc48b2b

• more precise stats

  quickbeam123

  committed
  b3b7c86

  Copy full SHA for b3b7c86

• why not stronger?

  quickbeam123

  committed
  716ddac

  Copy full SHA for 716ddac

• more precise way of keeping track of completeness than LRS was doing before

  quickbeam123

  committed
  a274a9f

  Copy full SHA for a274a9f

• fix a bug in fulfilsAgeLimit and simplify fulfilsWeightLimit (where the corrosponding fix made matters worse)

  quickbeam123

  committed
  11fb394

  Copy full SHA for 11fb394

• removed AgeWeightRatioShape logic, to simplify further transitions

  quickbeam123

  committed
  c46ccaa

  Copy full SHA for c46ccaa

• reorder, simplify, fix comment

  quickbeam123

  committed
  5e9e86f

  Copy full SHA for 5e9e86f

Commits on Jan 10, 2025

• remove shape options

  quickbeam123

  committed
  c939e09

  Copy full SHA for c939e09

• also from schedules

  quickbeam123

  committed
  8d6530c

  Copy full SHA for 8d6530c

• don't try to estimate limits until it's at least 10 activations o'clock (just moved an existing rule a bit forward)

  quickbeam123

  committed
  6aeac11

  Copy full SHA for 6aeac11

• initialization (until the first activation) does not count for LRS estimates

  quickbeam123

  committed
  924100a

  Copy full SHA for 924100a

• working on abstract SingleQueuePassiveClauseContainer (not yet used) lead to a redefinition of the PassiveClauseContainer LRS-interface, hopefully to something easier to understand. Will now check …

  Show description for 03a10cb
  quickbeam123

  committed
  03a10cb

  Copy full SHA for 03a10cb

• samplers support single queue (either just A or just W)

  quickbeam123

  committed
  02878ae

  Copy full SHA for 02878ae

• explicit (but very conservative, LRS-wise) single-queue solutions from Age and Weight

  quickbeam123

  committed
  b4ec20a

  Copy full SHA for b4ec20a

• making AgeBasedPassiveClauseContainer LRS-compatible with DiscriminateClausesUnderConstructionOnLimits

  quickbeam123

  committed
  64c8a67

  Copy full SHA for 64c8a67

• further simplified exceedsAgeLimit

  quickbeam123

  committed
  38b7c43

  Copy full SHA for 38b7c43

• AgeBasedPassiveClauseContainer DiscriminateChildrenOnLimits

  quickbeam123

  committed
  7ef23ac

  Copy full SHA for 7ef23ac

• a performance note about AgeBasedPassiveClauseContainer under LRS

  quickbeam123

  committed
  61854e1

  Copy full SHA for 61854e1

• a (temporary) implimentation of fancy LRS calls for WeightBasedPassiveClauseContainer

  quickbeam123

  committed
  50b89ed

  Copy full SHA for 50b89ed

Commits on Jan 11, 2025

• more explanation comments

  quickbeam123

  committed
  020d1d5

  Copy full SHA for 020d1d5

• simplified AWPassiveClauseContainer based on the new stronger assumption (both queus are always active)

  quickbeam123

  committed
  1619a44

  Copy full SHA for 1619a44

• SingleQueuePassiveClauseContainer's descendants may use allChildrenNecessarilyExceedLimits in onLimitsUpdated to delete even more

  quickbeam123

  committed
  05757cd

  Copy full SHA for 05757cd

• get rid of the callback subscription thingie

  quickbeam123

  committed
  d8bbb28

  Copy full SHA for d8bbb28

• also samplers without awrs(f)

  quickbeam123

  committed
  e5eeba8

  Copy full SHA for e5eeba8

• for AWPassiveClauseContainer, limits don't need to be active together; also a fix where mayBeAbleToDiscriminateClausesUnderConstructionOnLimits is more precise now

  quickbeam123

  committed
  eb460ed

  Copy full SHA for eb460ed

• align comment with reality on the PassiveClauseContainer interface

  quickbeam123

  committed
  c22ef51

  Copy full SHA for c22ef51

• lrs retroactive deletes as an option (defaults to false, as they don't lead to better performance in general)

  quickbeam123

  committed
  55d9a36

  Copy full SHA for 55d9a36

• updated samplers

  quickbeam123

  committed
  a354f56

  Copy full SHA for a354f56

Commits on Jan 12, 2025

• streamlined based on Michael's comments

  quickbeam123

  committed
  8f3a33e

  Copy full SHA for 8f3a33e

Commits on Jan 13, 2025

• it also make more sense for Unprocessed to work as FIFO - performance got better

  quickbeam123

  committed
  a96cdbd

  Copy full SHA for a96cdbd

• remove the goto; it's not very useful here

  quickbeam123

  committed
  891bd37

  Copy full SHA for 891bd37

Commits on Jan 15, 2025

• no indirect callbacks on unprocessed (better documents what's going on)

  quickbeam123

  committed
  045bd83

  Copy full SHA for 045bd83