search

ucsd-progsys / liquid-fixpoint

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

SMTLIB2 Interface not alive #395

Open nikivazou opened 5 years ago

nikivazou commented 5 years ago

The following in the README does not seem to exist anymore, should we delete it https://github.com/ucsd-progsys/liquid-fixpoint#smtlib2-interface ?

@gridaphobe

philderbeast commented 2 years ago

@nikivazou I was able to run the command line examples with little change but the following, I cannot find.

## SMTLIB2 Interface

There is a new SMTLIB2 interface directly from Haskell:

+ Language.Fixpoint.SmtLib2

See `tests/smt2/{Smt.hs, foo.smt2}` for an example of how to use it.
philderbeast commented 2 years ago

The file tests/smt2/Smt.hs is liquid-fixpoint-ocaml/tests/smt2/Smt.hs isn't it?

nikivazou commented 2 years ago

Yes! If you cannot run it just delete and update the README. The comment and code is quite old (and outdated). Thanks!