The "chain of tests" (as explained in the "Towards a Dynabook…" paper) follows the structure of the processing pipeline, i.e., for MachineArithmetic in particular,
SpriteLang → Horn → SMT,
meaning we have 6 kinds of tests. However, if we zoom in, we shall see an intermediate processing stage:
SpriteLang → Horn → FInfo → SMT.
In March 2024, the upstream LiquidFixpoint switched to "new format" tests (e.g. tests/pos/*.fq) where FInfos are spelled out explicitly. This PR ports these "new-format" capability to MA. This is important because much of essential functionality is covered by the "new-format" tests but not the Horn tests.
The "chain of tests" (as explained in the "Towards a Dynabook…" paper) follows the structure of the processing pipeline, i.e., for MachineArithmetic in particular,
meaning we have 6 kinds of tests. However, if we zoom in, we shall see an intermediate processing stage:
In March 2024, the upstream LiquidFixpoint switched to "new format" tests (e.g.
tests/pos/*.fq) where FInfos are spelled out explicitly. This PR ports these "new-format" capability to MA. This is important because much of essential functionality is covered by the "new-format" tests but not the Horn tests.