Fix multiple `apply` of magic wands with quantified expressions#849

Open

manud99 wants to merge 50 commits intoviperproject:masterfrom

manud99:quantified-magic-wand-maps

Commits on Apr 11, 2024

Use a Map from Snap to Snap to represent a magic wand snapshot.
manud99
committed

Commits on May 6, 2024

First optimization: Create sort MagicWandSnapFunction (MWSF) with its own function definitions to replace wand maps.
manud99
committed
Second optimization: When there is no applying expression use the original approach using MagicWandSnapSingleton.
manud99
committed

Commits on May 8, 2024

Commits on May 13, 2024

Commits on May 16, 2024

Commits on May 19, 2024

Commits on Jun 2, 2024

Recursively replace all quantification in the PCS with the freshSnapRoot.
manud99
committed

Commits on Jun 5, 2024

Try to use implications.
manud99
committed

Commits on Jun 9, 2024

Record which snapshot maps were created during packaging.
manud99
committed

Commits on Jun 10, 2024

Work on QPFields test cases.
manud99
committed

Commits on Jun 15, 2024

Update silver submodule.
manud99
committed

Commits on Jun 16, 2024

Rename state and verifier such that their numbers are incrementing in the control flow.
manud99
committed

Commits on Jun 17, 2024

Simplify conversion of snapWand from Snap to MWSF.
manud99
committed

Commits on Jun 18, 2024

Rename MWSFLookup to MWSFApply.
manud99
committed

Commits on Jun 22, 2024

Write documentation about optimizations.
manud99
committed

Commits on Jun 23, 2024

Commits on Jun 25, 2024

Implement MWSF which uses an image function to define when the definition is valid.
manud99
committed

Commits on Jun 28, 2024

Commits on Jun 30, 2024