ucsd-progsys / liquid-fixpoint

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

Copy over the HOF configuraration options in hornFInfo #684

Closed ranjitjhala closed 6 months ago

ranjitjhala commented 6 months ago

So that the below works, for example:

(fixpoint "--allowho")
(fixpoint "--allowhoqs")

(qualif MyQual ((v @(0)) (p @(1))) (p v))

(var $k0 (Int (func 0 (Int) bool)))

(constraint
  (and
    (forall ((p0 (func 0 (Int) bool)) (true))
      (and
        (forall ((x Int) ((p0 x)))
          ($k0 x p0))
        (forall ((y Int) ($k0 y p0))
          (forall ((v Int) ((= v y)))
            ($k0 v p0)))
        (forall ((z Int) ($k0 z p0))
          ((p0 z)))))))
ranjitjhala commented 6 months ago

@facundominguez, this tickled the first failure I've seen in the computes a fixpoint test copied over from the CI logs in case you want to investigate; but looks like it has to do with a divide-by-zero so pretty exotic?

computes a fixpoint:                       FAIL (4.40s)
      *** Failed! Falsified (after 1779 tests):
      POr [POr [ESym (SL "dymkjhhxgd"),ECon (L "emurwzzckkgx" (FTC (TC "Stcdlfq" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False}))))],EBin Div (ECon (I 0)) (ECon (R 0.0))]
      POr [POr [ESym (SL "dymkjhhxgd"),ECon (L "emurwzzckkgx" (FTC (TC "Stcdlfq" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False}))))],ECon (R NaN)] /= POr [POr [ESym (SL "dymkjhhxgd"),ECon (L "emurwzzckkgx" (FTC (TC "Stcdlfq" (dummyLoc) (TCInfo {tc_isNum = False, tc_isReal = False, tc_isString = False}))))],ECon (R NaN)]
      Use --quickcheck-replay=204453 --quickcheck-max-size=25 to reproduce.