Open sigmaSd opened 1 year ago
One interesting thing though
import { init } from "npm:z3-solver";
const { Context } = await init();
Actually downloads the wasm file as part of the deno downloading dependencies part
So I didn't even need to give --allow-net, is this something I can do with my own deno modules ?
now this causes a deno panic
============================================================
Deno has panicked. This is a bug in Deno. Please report this
at https://github.com/denoland/deno/issues/new.
If you can reliably reproduce this panic, include the
reproduction steps and re-run with the RUST_BACKTRACE=1 env
var set and include the backtrace in your report.
Platform: linux x86_64
Version: 1.37.0+f0a022b
Args: ["deno", "run", "-A", "a.ts"]
thread 'main' panicked at 'Custom error class must have a builder registered: Uncaught Error: Unable to build custom error for "NotFound"
Maximum call stack size exceeded', /home/runner/.cargo/registry/src/index.crates.io-6f17d22bba15001f/deno_core-0.218.0/error.rs:132:7
stack backtrace:
0: rust_begin_unwind
at /rustc/d5c2e9c342b358556da91d61ed4133f6f50fc0c3/library/std/src/panicking.rs:593:5
1: core::panicking::panic_fmt
at /rustc/d5c2e9c342b358556da91d61ed4133f6f50fc0c3/library/core/src/panicking.rs:67:14
2: deno_core::error::to_v8_error
3: deno_node::ops::require::op_require_read_closest_package_json<P>::v8_fn_ptr
4: Builtins_CallApiCallbackGeneric
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
sorry for the necropost, but this also causes infinite hanging.
import { init } from "npm:z3-solver"
const { Context } = await init()
const { Int, And, solve } = Context("main")
const x = Int.const("x")
console.log(await solve(And(x.ge(10), x.le(9))))
deno 1.39.1+140e8be (canary, x86_64-unknown-linux-gnu) v8 12.0.267.8 typescript 5.3.3
Advent of bug fixing :)
I ran into a similar bug when trying to use the Optimize solver in deno. I was also able to reproduce the bug in https://github.com/denoland/deno/issues/17171#issuecomment-1868450461 I then tried variations (replacing solver call with equivalent create Solver and add assertions. I tried three cases as shown below:
import { init } from "npm:z3-solver";
const z3 = await init();
enum ExperimentEnum {
A,
B,
C,
}
const expirement = ExperimentEnum.A; // ExperimentEnum.A, ExperimentEnum.B, ExperimentEnum.C
const ctx = z3.Context("main");
const x = ctx.Int.const("x");
const s = ctx.Sort.declare("S");
const bs = ctx.Bool.sort();
const edge = ctx.Function.declare("edge", s, s, bs);
const a = ctx.Const("a", s);
const b = ctx.Const("b", s);
const c = ctx.Const("c", s);
async function main(expirement: ExperimentEnum) {
const solver = new ctx.Solver();
const assertions = [];
if (expirement === ExperimentEnum.A) {
assertions.push(ctx.And(x.ge(0), x.le(9)));
} else if (expirement === ExperimentEnum.B) {
assertions.push(ctx.And(x.ge(10), x.le(9)));
} else if (expirement === ExperimentEnum.C) {
assertions.push(ctx.And(x.ge(10), x.le(9)));
solver.add(edge.call(a, b));
solver.add(edge.call(b, c));
}
solver.add(...assertions);
console.log(await solver.check());
}
await main(expirement);
Case A and C work fine returning sat, and unsat respectively. However, case B gives me the error:
Deno has panicked. This is a bug in Deno. Please report this
at https://github.com/denoland/deno/issues/new.
If you can reliably reproduce this panic, include the
reproduction steps and re-run with the RUST_BACKTRACE=1 env
var set and include the backtrace in your report.
Platform: linux x86_64
Version: 1.39.4
Args: ["/root/.asdf/installs/deno/1.39.4/bin/deno", "run", "--allow-all", "--unstable", "test1.ts"]
thread 'main' panicked at /home/runner/.cargo/registry/src/index.crates.io-6f17d22bba15001f/deno_core-0.245.0/error.rs:132:7:
Custom error class must have a builder registered: Uncaught RangeError: Maximum call stack size exceeded
stack backtrace:
0: rust_begin_unwind
at /rustc/82e1608dfa6e0b5569232559e3d385fea5a93112/library/std/src/panicking.rs:645:5
1: core::panicking::panic_fmt
at /rustc/82e1608dfa6e0b5569232559e3d385fea5a93112/library/core/src/panicking.rs:72:14
2: deno_core::error::to_v8_error::panic_cold_display
3: deno_core::error::to_v8_error
4: deno_node::ops::require::op_require_read_closest_package_json<P>::v8_fn_ptr
5: Builtins_CallApiCallbackGeneric
Obviously not the same, but in the meantime, its possible to use libpython for this, here is an example of the original snippet (requires z3-python library installed)
deno run -A --unstable-ffi file.ts
import { python } from "https://deno.land/x/python@0.4.3/mod.ts";
const z3 = python.import("z3");
const x = z3.Int("x");
const solver = z3.Solver();
solver.add(z3.And(x.__ge__(0), x.__le__(9)));
console.log(solver.check());
console.log(solver.model());
The error have changed in the last version
error: Uncaught (in worker "") (in promise) TypeError: Cannot set property location of #<DedicatedWorkerGlobalScope> which has only a getter
at Function.assign (<anonymous>)
at Object.<anonymous> (file:///home/mrcool/.cache/deno/npm/registry.npmjs.org/z3-solver/4.13.0/build/z3-built.worker.js:30:10)
at Object.<anonymous> (file:///home/mrcool/.cache/deno/npm/registry.npmjs.org/z3-solver/4.13.0/build/z3-built.worker.js:208:4)
at Module._compile (node:module:718:34)
at Object.Module._extensions..js (node:module:732:10)
at Module.load (node:module:643:32)
at Function.Module._load (node:module:524:12)
at Module.require (node:module:662:19)
at require (node:module:776:16)
at data:text/javascript,import { createRequi......3-built.worker.js");:1:176
deno 1.42.0+bca0fe1
I just noticed that this issue is untagged, @satyarohith would be great if you tag this issue with npm-compat so it doesn't get lost
error:
Also there seem to be a lint issue ?
The node packagae has z3-solver/browser recomends z3-solver/browser for browsers, but I don't know how to use this with deno becasue using
errors