Simplify kvar solutions in fqout files by facundominguez · Pull Request #741 · ucsd-progsys/liquid-fixpoint

facundominguez · 2025-03-09T22:39:39Z

This PR eliminates much of the bindings in the kvar solutions in fqout files.
Many bindings are inconsequential because they are existential variables that appear only once in one of the sides of an equality, and are never related again to another term.

Before this change:

k_##1604 := exists [lq_karg$Test.extendSubst##k_##1604 : func(0 , [func(0 , [int;
                                                                              @(1330)]);
                                                                    int;
                                                                    @(1330);
                                                                    int;
                                                                    @(1330)]);
                     lq_karg$lq_anf$##7205759403792797858##d16G##k_##1604 : bool;
                     lq_karg$j##aXR##k_##1604 : int;
                     lq_karg$ds_d15x##k_##1604 : Test.Exp;
                     lq_karg$VV##1603##k_##1604 : Test.Exp;
                     lq_karg$Test.freshVar##k_##1604 : func(0 , [(Set_Set int); int]);
                     lq_karg$lq_anf$##7205759403792797857##d16F##k_##1604 : bool;
                     lq_karg$scope##aXJ##k_##1604 : (Set_Set int);
                     lq_karg$Test.substitute##k_##1604 : func(0 , [(Set_Set int);
                                                                   func(0 , [int; Test.Exp]);
                                                                   Test.Exp;
                                                                   Test.Exp]);
                     lq_karg$f##aXK##k_##1604 : func(0 , [int; Test.Exp]);
                     lq_karg$i##aXO##k_##1604 : int;
                     lq_karg$lq_anf$##7205759403792797854##d16C##k_##1604 : Test.Exp;
                     lq_karg$lq_anf$##7205759403792797861##d16J##k_##1604 : Test.Exp;
                     lq_karg$lq_anf$##7205759403792797860##d16I##k_##1604 : (Set_Set int);
                     lq_karg$e##aXP##k_##1604 : Test.Exp;
                     lq_tmp$x##1598 : int;
                     VV##F##4 : Test.Exp]
               . lq_karg$Test.extendSubst##k_##1604 == Test.extendSubst
                 && lq_karg$Test.freshVar##k_##1604 == Test.freshVar
                 && lq_karg$Test.substitute##k_##1604 == Test.substitute
                 && lq_karg$VV##1603##k_##1604 == VV##F##4
                 && lq_karg$ds_d15x##k_##1604 == ds_d15x
                 && lq_karg$e##aXP##k_##1604 == e##aXP
                 && lq_karg$f##aXK##k_##1604 == f##aXK
                 && lq_karg$i##aXO##k_##1604 == i##aXO
                 && lq_karg$j##aXR##k_##1604 == j##aXR
                 && lq_karg$lq_anf$##7205759403792797854##d16C##k_##1604 == lq_anf$##7205759403792797854##d16C
                 && lq_karg$lq_anf$##7205759403792797857##d16F##k_##1604 == lq_anf$##7205759403792797857##d16F
                 && lq_karg$lq_anf$##7205759403792797858##d16G##k_##1604 == lq_anf$##7205759403792797858##d16G
                 && lq_karg$lq_anf$##7205759403792797861##d16J##k_##1604 == lq_anf$##7205759403792797861##d16J
                 && cast_as_int lq_karg$lq_anf$##7205759403792797860##d16I##k_##1604 == cast_as_int lq_anf$##7205759403792797860##d16I
                 && cast_as_int lq_karg$scope##aXJ##k_##1604 == cast_as_int scope##aXJ
                 && arr_const_s true == arr_map_imp (Test.freeVars VV##F##4) scope##aXJ
             || exists [lq_karg$Test.extendSubst##k_##1604 : func(0 , [func(0 , [int;
                                                                                 @(1337)]);
                                                                       int;
                                                                       @(1337);
                                                                       int;
                                                                       @(1337)]);
                        lq_karg$lq_anf$##7205759403792797858##d16G##k_##1604 : bool;
                        lq_karg$j##aXR##k_##1604 : int;
                        lq_karg$ds_d15x##k_##1604 : Test.Exp;
                        lq_karg$VV##1603##k_##1604 : Test.Exp;
                        lq_karg$Test.freshVar##k_##1604 : func(0 , [(Set_Set int); int]);
                        lq_karg$lq_anf$##7205759403792797857##d16F##k_##1604 : bool;
                        lq_karg$scope##aXJ##k_##1604 : (Set_Set int);
                        lq_karg$Test.substitute##k_##1604 : func(0 , [(Set_Set int);
                                                                      func(0 , [int; Test.Exp]);
                                                                      Test.Exp;
                                                                      Test.Exp]);
                        lq_karg$f##aXK##k_##1604 : func(0 , [int; Test.Exp]);
                        lq_karg$i##aXO##k_##1604 : int;
                        lq_karg$lq_anf$##7205759403792797854##d16C##k_##1604 : Test.Exp;
                        lq_karg$lq_anf$##7205759403792797861##d16J##k_##1604 : Test.Exp;
                        lq_karg$lq_anf$##7205759403792797860##d16I##k_##1604 : (Set_Set int);
                        lq_karg$e##aXP##k_##1604 : Test.Exp;
                        VV##F##3 : Test.Exp]
                  . lq_karg$Test.extendSubst##k_##1604 == Test.extendSubst
                    && lq_karg$Test.freshVar##k_##1604 == Test.freshVar
                    && lq_karg$Test.substitute##k_##1604 == Test.substitute
                    && lq_karg$VV##1603##k_##1604 == VV##F##3
                    && lq_karg$ds_d15x##k_##1604 == ds_d15x
                    && lq_karg$e##aXP##k_##1604 == e##aXP
                    && lq_karg$f##aXK##k_##1604 == f##aXK
                    && lq_karg$i##aXO##k_##1604 == i##aXO
                    && lq_karg$j##aXR##k_##1604 == j##aXR
                    && lq_karg$lq_anf$##7205759403792797854##d16C##k_##1604 == lq_anf$##7205759403792797854##d16C
                    && lq_karg$lq_anf$##7205759403792797857##d16F##k_##1604 == lq_anf$##7205759403792797857##d16F
                    && lq_karg$lq_anf$##7205759403792797858##d16G##k_##1604 == lq_anf$##7205759403792797858##d16G
                    && lq_karg$lq_anf$##7205759403792797861##d16J##k_##1604 == lq_anf$##7205759403792797861##d16J
                    && VV##F##3 == lq_anf$##7205759403792797861##d16J
                    && VV##F##3 == Test.Var j##aXR
                    && Test.freeVars VV##F##3 == arr_store_s (arr_const_s false) j##aXR true
                    && cast_as_int lq_karg$lq_anf$##7205759403792797860##d16I##k_##1604 == cast_as_int lq_anf$##7205759403792797860##d16I
                    && cast_as_int lq_karg$scope##aXJ##k_##1604 == cast_as_int scope##aXJ

After this change:

$k_##1604 := exists [VV##F##4 : Test.Exp]
               . arr_const_s true == arr_map_imp (Test.freeVars VV##F##4) scope##aXJ
             || exists [VV##F##3 : Test.Exp]
                  . VV##F##3 == lq_anf$##7205759403792797861##d16J
                    && VV##F##3 == Test.Var j##aXR
                    && Test.freeVars VV##F##3 == arr_store_s (arr_const_s false) j##aXR true

facundominguez · 2025-03-09T22:44:40Z

@ranjitjhala, should I try this simplification elsewhere in the pipeline?

It is only used for pretty printing at the moment, and it relies much on list traversals.

ranjitjhala · 2025-03-09T22:46:29Z

Sure! - Ranjit.

…

On Sun, Mar 9, 2025 at 3:45 PM Facundo Domínguez ***@***.***> wrote: @ranjitjhala <https://urldefense.com/v3/__https://github.com/ranjitjhala__;!!Mih3wA!HRkqcoiNfXqQXQdWygGsHx3hQOYYF0fOnoNP1QWYMdQt7_7Hz5DA6Q-7vS_nZegQxrk25zxjO0QXAMrqHP7I_-sv$>, should I try this simplification elsewhere in the pipeline? It is only used for pretty printing at the moment, and it relies much on list traversals. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/pull/741*issuecomment-2709110976__;Iw!!Mih3wA!HRkqcoiNfXqQXQdWygGsHx3hQOYYF0fOnoNP1QWYMdQt7_7Hz5DA6Q-7vS_nZegQxrk25zxjO0QXAMrqHBYauKhk$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OAOG7XEVBNPCSQ5G2L2TS763AVCNFSM6AAAAABYUXVAV2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDOMBZGEYTAOJXGY__;!!Mih3wA!HRkqcoiNfXqQXQdWygGsHx3hQOYYF0fOnoNP1QWYMdQt7_7Hz5DA6Q-7vS_nZegQxrk25zxjO0QXAMrqHN9FE17N$> . You are receiving this because you were mentioned.Message ID: ***@***.***> [image: facundominguez]*facundominguez* left a comment (ucsd-progsys/liquid-fixpoint#741) <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/pull/741*issuecomment-2709110976__;Iw!!Mih3wA!HRkqcoiNfXqQXQdWygGsHx3hQOYYF0fOnoNP1QWYMdQt7_7Hz5DA6Q-7vS_nZegQxrk25zxjO0QXAMrqHBYauKhk$> @ranjitjhala <https://urldefense.com/v3/__https://github.com/ranjitjhala__;!!Mih3wA!HRkqcoiNfXqQXQdWygGsHx3hQOYYF0fOnoNP1QWYMdQt7_7Hz5DA6Q-7vS_nZegQxrk25zxjO0QXAMrqHP7I_-sv$>, should I try this simplification elsewhere in the pipeline? It is only used for pretty printing at the moment, and it relies much on list traversals. — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/pull/741*issuecomment-2709110976__;Iw!!Mih3wA!HRkqcoiNfXqQXQdWygGsHx3hQOYYF0fOnoNP1QWYMdQt7_7Hz5DA6Q-7vS_nZegQxrk25zxjO0QXAMrqHBYauKhk$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OAOG7XEVBNPCSQ5G2L2TS763AVCNFSM6AAAAABYUXVAV2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDOMBZGEYTAOJXGY__;!!Mih3wA!HRkqcoiNfXqQXQdWygGsHx3hQOYYF0fOnoNP1QWYMdQt7_7Hz5DA6Q-7vS_nZegQxrk25zxjO0QXAMrqHN9FE17N$> . You are receiving this because you were mentioned.Message ID: ***@***.***>

facundominguez · 2025-03-09T22:52:14Z

Sure!

Sorry to be so vague :) Do you have any advice about where to insert it?

facundominguez · 2025-03-10T13:13:56Z

Here are the benchmarks. I don't regard the changes as significant, but let me know if you have any comments.

ranjitjhala · 2025-03-10T14:16:21Z

Wow - this is amazing! I had no idea there was so much redundancy! The only other place I can think of is in “Sanitize” where we do a bunch of preprocessing steps? - Ranjit.

…

facundominguez · 2025-03-10T14:23:51Z

If you mean this sanitize, it returns an SInfo. Does it have KVar solutions to simplify anywhere inside?

ranjitjhala · 2025-03-10T14:56:56Z

Good point at that stage (sanitize) there are no kvars (solution) really I was just thinking of places there may be redundant binders… - Ranjit.

…

On Mon, Mar 10, 2025 at 7:24 AM Facundo Domínguez ***@***.***> wrote: If you mean this sanitize <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/blob/d81852c18acdcc109454ee73b090966610cd186f/src/Language/Fixpoint/Solver/Sanitize.hs*L42__;Iw!!Mih3wA!Dbf7c1U7r83ZkTA2dqx9khL_AkKXLRF9t-E-pc8RVqhGmQcYu_LcQzSrX5WUNWBGvmcyzaXJg2a9viE7T71_3qJp$>, it returns an SInfo. Does it have KVar solutions to simplify anywhere inside? — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/pull/741*issuecomment-2710779015__;Iw!!Mih3wA!Dbf7c1U7r83ZkTA2dqx9khL_AkKXLRF9t-E-pc8RVqhGmQcYu_LcQzSrX5WUNWBGvmcyzaXJg2a9viE7T2mNjrDo$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OBKH3MWUKLU2T7X6LD2TWOA3AVCNFSM6AAAAABYUXVAV2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDOMJQG43TSMBRGU__;!!Mih3wA!Dbf7c1U7r83ZkTA2dqx9khL_AkKXLRF9t-E-pc8RVqhGmQcYu_LcQzSrX5WUNWBGvmcyzaXJg2a9viE7T--3V3Di$> . You are receiving this because you were mentioned.Message ID: ***@***.***> [image: facundominguez]*facundominguez* left a comment (ucsd-progsys/liquid-fixpoint#741) <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/pull/741*issuecomment-2710779015__;Iw!!Mih3wA!Dbf7c1U7r83ZkTA2dqx9khL_AkKXLRF9t-E-pc8RVqhGmQcYu_LcQzSrX5WUNWBGvmcyzaXJg2a9viE7T2mNjrDo$> If you mean this sanitize <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/blob/d81852c18acdcc109454ee73b090966610cd186f/src/Language/Fixpoint/Solver/Sanitize.hs*L42__;Iw!!Mih3wA!Dbf7c1U7r83ZkTA2dqx9khL_AkKXLRF9t-E-pc8RVqhGmQcYu_LcQzSrX5WUNWBGvmcyzaXJg2a9viE7T71_3qJp$>, it returns an SInfo. Does it have KVar solutions to simplify anywhere inside? — Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/pull/741*issuecomment-2710779015__;Iw!!Mih3wA!Dbf7c1U7r83ZkTA2dqx9khL_AkKXLRF9t-E-pc8RVqhGmQcYu_LcQzSrX5WUNWBGvmcyzaXJg2a9viE7T2mNjrDo$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OBKH3MWUKLU2T7X6LD2TWOA3AVCNFSM6AAAAABYUXVAV2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDOMJQG43TSMBRGU__;!!Mih3wA!Dbf7c1U7r83ZkTA2dqx9khL_AkKXLRF9t-E-pc8RVqhGmQcYu_LcQzSrX5WUNWBGvmcyzaXJg2a9viE7T--3V3Di$> . You are receiving this because you were mentioned.Message ID: ***@***.***>

facundominguez added 2 commits March 9, 2025 22:47

Simplify kvar solutions in fqout files

523406a

Update CI configuration for stan

1e9d6be

facundominguez force-pushed the fd/simplify-fqout branch from 518ed68 to 1e9d6be Compare March 9, 2025 22:50

Move kvar simplification to the end of solving

feddce7

facundominguez merged commit e19e17b into develop Mar 10, 2025

facundominguez deleted the fd/simplify-fqout branch March 10, 2025 16:02

facundominguez mentioned this pull request Mar 10, 2025

Update liquid-fixpoint to include simplification of fqout files ucsd-progsys/liquidhaskell#2494

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Simplify kvar solutions in fqout files#741

Simplify kvar solutions in fqout files#741
facundominguez merged 3 commits into
developfrom
fd/simplify-fqout

facundominguez commented Mar 9, 2025

Uh oh!

facundominguez commented Mar 9, 2025

Uh oh!

ranjitjhala commented Mar 9, 2025 via email

Uh oh!

facundominguez commented Mar 9, 2025 •

edited

Loading

Uh oh!

facundominguez commented Mar 10, 2025

Uh oh!

ranjitjhala commented Mar 10, 2025 via email

Uh oh!

facundominguez commented Mar 10, 2025

Uh oh!

ranjitjhala commented Mar 10, 2025 via email

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

facundominguez commented Mar 9, 2025

Uh oh!

facundominguez commented Mar 9, 2025

Uh oh!

ranjitjhala commented Mar 9, 2025 via email

Uh oh!

facundominguez commented Mar 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

facundominguez commented Mar 10, 2025

Uh oh!

ranjitjhala commented Mar 10, 2025 via email

Uh oh!

facundominguez commented Mar 10, 2025

Uh oh!

ranjitjhala commented Mar 10, 2025 via email

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

facundominguez commented Mar 9, 2025 •

edited

Loading