allow warnings and java interop

dafny-lang · Jul 26, 2024 · d4c7d61 · d4c7d61
1 parent 72276c7
commit d4c7d61
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 6 deletions.
diff --git a/scripts/build.sh b/scripts/build.sh
@@ -16,7 +16,7 @@ fi
 
 if [ "$TARGET_LANG" = "java" ]
 then
-  $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify
+  $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify --allow-warnings
 else
-  $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify
+  $DAFNY build --target:$TARGET_LANG src/interop/$TARGET_LANG/Full/Random.$TARGET_LANG src/interop/$TARGET_LANG/Part/Random.$TARGET_LANG -o build/$TARGET_LANG/DafnyVMC dfyconfig.toml --no-verify --allow-warnings
 fi
diff --git a/src/interop/java/Full/Random.java b/src/interop/java/Full/Random.java
@@ -78,12 +78,20 @@ public boolean BernoulliExpNegSample(java.math.BigInteger num, java.math.BigInte
     return DafnyVMCTrait._Companion_RandomTrait.BernoulliExpNegSample(this, num, den);
   }
 
-  public dafny.Tuple2<java.math.BigInteger, Boolean> DiscreteGaussianSampleLoop(java.math.BigInteger num, java.math.BigInteger den, java.math.BigInteger t) {
-    return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSampleLoop(this, num, den, t);
+  public dafny.Tuple2<java.math.BigInteger, Boolean> DiscreteGaussianSampleLoop(java.math.BigInteger num, java.math.BigInteger den, java.math.BigInteger t, java.math.BigInteger mix) {
+    return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSampleLoop(this, num, den, t, mix);
   }
 
-  public java.math.BigInteger DiscreteGaussianSample(java.math.BigInteger num, java.math.BigInteger den) {
-    return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSample(this, num, den);
+  public java.math.BigInteger DiscreteGaussianSample(java.math.BigInteger num, java.math.BigInteger den, java.math.BigInteger mix) {
+    return DafnyVMCTrait._Companion_RandomTrait.DiscreteGaussianSample(this, num, den, mix);
+  }
+
+  public java.math.BigInteger DiscreteLaplaceSampleMixed(java.math.BigInteger num, java.math.BigInteger den, java.math.BigInteger mix) {
+    return DafnyVMCTrait._Companion_RandomTrait.DiscreteLaplaceSampleMixed(this, num, den, mix);
+  }
+
+  public java.math.BigInteger DiscreteLaplaceSampleOptimized(java.math.BigInteger num, java.math.BigInteger den) {
+    return DafnyVMCTrait._Companion_RandomTrait.DiscreteLaplaceSampleOptimized(this, num, den);
   }
 
   public dafny.Tuple2<java.math.BigInteger, Boolean> DiscreteLaplaceSampleLoopIn1Aux(java.math.BigInteger t) {