search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
132 stars 59 forks source link

[cutsolver] Sets #83

Closed BenjaminCosman closed 9 years ago

BenjaminCosman commented 9 years ago

See:

https://github.com/ucsd-progsys/liquid-fixpoint/blob/cutsolver/tests/weird/sets.fq (adapted from LH test MeasureSets.hs.fq)

It passes the Ocaml solver with or without the constant definition, but the haskell solver exhibits two distinct failure modes depending on whether you include the constant.

Related to Issue #75 ?

ranjitjhala commented 9 years ago

Notes to self @ranjitjhala:

In ocaml, dig around for SMT.mkEmptySet.

Note that

  1. set_emp(v) ===> v = smt_set_emp
  2. set_empty ===> smt_set_emp

In haskell, we only do (1) and not (2).

ranjitjhala commented 9 years ago

Commit fdf9461cd9 fixes this. However, it does not fix #75 -- but even fixpoint.native crashes with that. Can you confirm which .hs file that comes from?