Code

reflection of quot and rem#2540

Code

Merged

facundominguez merged 33 commits intoucsd-progsys:developucsd-progsys/liquidhaskell:developfrom

ninioArtillero:reflect-quot-remninioArtillero/liquidhaskell:reflect-quot-remCopy head branch name to clipboard

May 29, 2025

Commits

Commits on Mar 29, 2025

• temp

  ranjitjhala

  committed
  69f6c27

  Copy full SHA for 69f6c27

• link lh-lf develop

  ranjitjhala

  committed
  3dba062

  Copy full SHA for 3dba062

Commits on May 19, 2025

• Merge pull request #2509 from ucsd-progsys/define-fun-new

  Show description for 01c08fe
  ranjitjhala

  authored
  01c08fe

  Copy full SHA for 01c08fe

Commits on May 20, 2025

• create neg test

  ninioArtillero

  committed
  0448369

  Copy full SHA for 0448369

• correct name of test

  ninioArtillero

  committed
  b409abb

  Copy full SHA for b409abb

Commits on May 22, 2025

• specify error

  ninioArtillero

  committed
  6675612

  Copy full SHA for 6675612

• tentative defines (no abs in the logic)

  ninioArtillero

  committed
  854c722

  Copy full SHA for 854c722

• added define for abs, test now trows no error

  ninioArtillero

  committed
  69ccef6

  Copy full SHA for 69ccef6

• move to positive test

  ninioArtillero

  committed
  cbe217f

  Copy full SHA for cbe217f

• correct refinement name and clear failure comments

  ninioArtillero

  committed
  3f08a7b

  Copy full SHA for 3f08a7b

• add test-suite to liquidhaskell with quotRem prop

  ninioArtillero

  committed
  ac46050

  Copy full SHA for ac46050

Commits on May 23, 2025

• replace with lemmas for testing but getting error

  ninioArtillero

  committed
  c3e737f

  Copy full SHA for c3e737f

• alternative quot and mod implementation test fails

  ninioArtillero

  committed
  2cc9c9c

  Copy full SHA for 2cc9c9c

Commits on May 24, 2025

• correct quot and rem implementation

  ninioArtillero

  committed
  1238028

  Copy full SHA for 1238028

• fixed logic quot and rem, tests ok, but found bug

  ninioArtillero

  committed
  9cb9a08

  Copy full SHA for 9cb9a08

Commits on May 26, 2025

• some cleanup

  ninioArtillero

  committed
  9e79205

  Copy full SHA for 9e79205

• moved examples to issue #2547

  ninioArtillero

  committed
  7913052

  Copy full SHA for 7913052

Commits on May 27, 2025

• fix implementation of logic quot and rem

  ninioArtillero

  committed
  7b648be

  Copy full SHA for 7b648be

• remove failure comments

  ninioArtillero

  committed
  ea1714a

  Copy full SHA for ea1714a

• use logic `/` here as well, avoid dependence on div

  Show description for b0e07fd
  

  ninioArtillero

  and

  facundominguez

  authored
  b0e07fd

  Copy full SHA for b0e07fd

• remove unneeded comments

  Show description for 416b679
  

  ninioArtillero

  and

  facundominguez

  authored
  416b679

  Copy full SHA for 416b679

• refactor to a clea(n | r)er definition

  Show description for dada829
  

  ninioArtillero

  and

  facundominguez

  authored
  dada829

  Copy full SHA for dada829

• add missing specs and make all monomorphic

  ninioArtillero

  committed
  95b1a0f

  Copy full SHA for 95b1a0f

Commits on May 28, 2025

• clean, improve names and verified implementation

  ninioArtillero

  committed
  54b427e

  Copy full SHA for 54b427e

• lemma is not passing verification

  ninioArtillero

  committed
  dde90b0

  Copy full SHA for dde90b0

• redundant condition

  ninioArtillero

  committed
  1000588

  Copy full SHA for 1000588

• add test for smt division

  ninioArtillero

  committed
  f8729cf

  Copy full SHA for f8729cf

• more cleanup

  ninioArtillero

  committed
  b77875e

  Copy full SHA for b77875e

• add neg test for missing unfolding bug

  ninioArtillero

  committed
  921a2d7

  Copy full SHA for 921a2d7

Commits on May 29, 2025

• Remove uses of abs from quot and rem defines

  facundominguez

  committed
  280c0e1

  Copy full SHA for 280c0e1

• Move liquidhaskell-test to the tests package

  facundominguez

  committed
  24c1275

  Copy full SHA for 24c1275

• Update tests in liquidhaskell-test/QuotRem.hs to changes in defines

  facundominguez

  committed
  b27f0fa

  Copy full SHA for b27f0fa

• Revert "add neg test for missing unfolding bug"

  Show description for 7f9e7d1
  facundominguez

  committed
  7f9e7d1

  Copy full SHA for 7f9e7d1