Facundo Domínguez
Facundo Domínguez
In the .fq files generated from running LH, there are sometimes deeply indented expressions that span multiple lines and which are not particularly easy to read. Improving the formatting is...
LF produces a file `.fq.ple` with the equations discovered by the PLE algorithm that uses an smt solver. It would be nice to get there the equations that come from...
We have a few dumps from different parts of liquid-fixpoint. There is ``` .liquid/.fq .liquid/.fq.pretiffied .liquid/.fq.ple .liquid/.fq.out ``` `.fq` and `.fq.prettified` show the initial input to LF. They contain liquid...
While LH continues to interface with LF using the `Fixpoint.FInfo` type, people debugging LH will need to understand `.fq` files which are the textual representation of `FInfo`. The README provides...
The README says this much > This package implements a Horn-Clause/Logical Implication constraint solver used for various Liquid Types. The solver uses SMTLIB2 to implement an algorithm similar to: ......
These functions are used to encode and decode higher-order functions into a form where all function arguments are replaced with integers. They are in `Language.Fixpoint.SortCheck`. This transformation is necessary because...
These functions add explicit casts (type annotations) to expressions, since the SMT solver doesn't know about polymorphic types, neither does it have an inference algorithm. They are in `Language.Fixpoint.SortCheck` and...
Verification of the following example succeeds when constraints 1 and 3 are actually unsafe. ``` // test.fq define f(lq1:a) : a = { lq1 } expand [1 : True; 2...
AmericanFlag.hs takes near 20 seconds to verify, while `z3 AmericanFlag.hs.smt2` takes only 2 seconds. It turns out most of the time is spent in `Language.Fixpoint.Smt.Interface.command` which is called 280000 times!...
In order to reproduce, edit `pleBoolC.fq` as follows ``` diff --git a/tests/proof/pleBoolC.fq b/tests/proof/pleBoolC.fq index 2efb3cfc..5161d4e9 100644 --- a/tests/proof/pleBoolC.fq +++ b/tests/proof/pleBoolC.fq @@ -27,8 +27,8 @@ constant tail: (func(1, [Vec @(0); Vec...