<commit_before>Liquid Fixpoint
===============

This package is a Haskell wrapper to the SMT (Z3) Based Horn-Clause/
Logical Implication constraint solver used for Liquid Types. The solver
itself is written in Ocaml. The Haskell Library contains

1. Types for representing Expressions, Predicates, Constraints, Solutions
2. Code for serializing the above 
3. Code for parsing the results from the fixpoint.native binary

Requirements
------------

The package include the Ocaml fixpoint code, as well as the z3 binaries

In addition to the .cabal dependencies, to build you must have

- the GNU multiprecision library 
- a recent OCaml compiler
- the CamlIDL library

Due to the Z3 dependency, LiquidHaskell can **only be compiled on Linux** at the moment.

The above can be carried out in one shot on a recent Linux by

    sudo apt-get install haskell-platform ocaml camlidl g++ libgmp3c2


How to Clone
------------

To clone liquidhaskell:

    git clone <EMAIL>@github.com:ucsd-progsys/liquid-fixpoint.git

How To Build and Install
------------------------

    cabal install


Using SMTLIB-based SMT Solvers
------------------------------

You can use one of several SMTLIB2 compliant solvers, by:

    liquid --smtsolver=z3 path/to/file.hs

Currently, we support
    
    * z3

1. command line option to fixpoint.native
    
    fixpoint.native -smtsolver z3      foo.fq
    fixpoint.native -smtsolver cvc4    foo.fq
    fixpoint.native -smtsolver mathsat foo.fq

2. liquid-fixpoint check if solver exists

3. Install cvc4 
    - run benchmarks

4. Install mathsat5
    - run benchmarks

5. Add set axioms
    - redo 5,6,7

9. MERGE

10. Find clean platform-independent BUILD.

    DELETE z3bind (easy build on macOS) 
   



Failed 18 tests:
 
  Broken:
    , SS.hs, cont.hs, ptr.hs, ptr2.hs, ptr3.hs
   
  Sets:
    , deepmeas0.hs
    , ListConcat.hs
    , ListElem.hs
    , listSet.hs
    , listSetDemo.hs
    , stacks0.hs
    , zipper.hs
    , zipper0.hs
    , meas9.hs
    , meas10.hs
    , meas11.hs
 




<commit_msg>asdasd<commit_after>Liquid Fixpoint
===============

This package is a Haskell wrapper to the SMT (Z3) Based Horn-Clause/
Logical Implication constraint solver used for Liquid Types. The solver
itself is written in Ocaml. The Haskell Library contains

1. Types for representing Expressions, Predicates, Constraints, Solutions
2. Code for serializing the above 
3. Code for parsing the results from the fixpoint.native binary

Requirements
------------

The package include the Ocaml fixpoint code, as well as the z3 binaries

In addition to the .cabal dependencies, to build you must have

- the GNU multiprecision library 
- a recent OCaml compiler
- the CamlIDL library

Due to the Z3 dependency, LiquidHaskell can **only be compiled on Linux** at the moment.

The above can be carried out in one shot on a recent Linux by

    sudo apt-get install haskell-platform ocaml camlidl g++ libgmp3c2


How to Clone
------------

To clone liquidhaskell:

    git clone <EMAIL>:ucsd-progsys/liquid-fixpoint.git

How To Build and Install
------------------------

    cabal install


Using SMTLIB-based SMT Solvers
------------------------------

You can use one of several SMTLIB2 compliant solvers, by:

    fixpoint --smtsolver=z3 path/to/file.hs

Currently, we support
    
    * z3

1. command line option to fixpoint.native
2. merge 
3. Find clean platform-independent BUILD.

{'fraction_non_alphanumeric': 0.10510863182618908, 'fraction_numerical': 0.015560775102759836, 'mean_word_length': 2.6832432432432434, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '158709', 'n_tokens_mistral': 1109, 'n_tokens_neox': 1030, 'n_words': 421}