Code

Introducing NewVMC#147

Code

Merged

stefan-aws merged 26 commits intomaindafny-lang/Dafny-VMC:mainfrom newvmcdafny-lang/Dafny-VMC:newvmcCopy head branch name to clipboardFeb 14, 2024

+339-2,330

Commits

Commits on Feb 13, 2024

• Tests simplification: rng always of type DafnyVMC.Random

  jtristan

  committed
  1c4b1f4

  Copy full SHA for 1c4b1f4

• New test for Bernoulli negative exponential less or equal to 1

  jtristan

  committed
  70eb6e1

  Copy full SHA for 70eb6e1

• Plugging in new vmc and adapting test to lack of Rationals

  jtristan

  committed
  8be6cbb

  Copy full SHA for 8be6cbb

• Set formatting of code generated from Lean

  jtristan

  committed
  c7cd36e

  Copy full SHA for c7cd36e

• Filtering NewVMC from auditor

  jtristan

  committed
  c398bbd

  Copy full SHA for c398bbd

• Redefining Uniform interface for pos

  jtristan

  committed
  a54cacd

  Copy full SHA for a54cacd

• Pos module

  jtristan

  committed
  8508c89

  Copy full SHA for 8508c89

• rm: Gaussian

  jtristan

  committed
  eb75800

  Copy full SHA for eb75800

• rm: DafnyVNCTrait

  jtristan

  committed
  4701a41

  Copy full SHA for 4701a41

• reusing old name for java build and tests

  jtristan

  committed
  835f241

  Copy full SHA for 835f241

• Generating with Dafny old name

  jtristan

  committed
  e30a246

  Copy full SHA for e30a246

• fixed mess with files in wrong directories

  jtristan

  committed
  8368ef3

  Copy full SHA for 8368ef3

• More names fixes

  jtristan

  committed
  b6a9896

  Copy full SHA for b6a9896

• fixed API

  jtristan

  committed
  6a026ed

  Copy full SHA for 6a026ed

• fixed build

  jtristan

  committed
  60fbc69

  Copy full SHA for 60fbc69

• fixed build

  jtristan

  committed
  27c5e25

  Copy full SHA for 27c5e25

• fixed build

  jtristan

  committed
  6396a6a

  Copy full SHA for 6396a6a

• rm: Laplace

  jtristan

  committed
  20761b7

  Copy full SHA for 20761b7

• update audit

  jtristan

  committed
  7239fde

  Copy full SHA for 7239fde

• rm: bern and bern en

  jtristan

  committed
  bfc3aba

  Copy full SHA for bfc3aba

• edit audit

  jtristan

  committed
  d7e5b65

  Copy full SHA for d7e5b65

• Trying to rm some termination axioms

  jtristan

  committed
  0dc43d6

  Copy full SHA for 0dc43d6

• Cleaning up unused math

  jtristan

  committed
  d19aca0

  Copy full SHA for d19aca0

• Cleaned up unused math

  jtristan

  committed
  3fe2946

  Copy full SHA for 3fe2946

• rm: dead implementation and equivalence of uniform

  jtristan

  committed
  429a74b

  Copy full SHA for 429a74b

• spurious code commented

  jtristan

  committed
  25b2c28

  Copy full SHA for 25b2c28