node-compat: z3-solver

[sigmaSd]

import { init } from "npm:z3-solver";
const { Context } = await init();
const { Solver, Int, And } = new Context("main");

const x = Int.const("x");

const solver = new Solver();
solver.add(And(x.ge(0), x.le(9)));
console.log(await solver.check()); // line that fails

error:

error: Uncaught RangeError: Maximum call stack size exceeded
    this._events = Object.create(null);
                          ^
    at Function.create (<anonymous>)
    at _Worker.EventEmitter.init (https://deno.land/std@0.170.0/node/_events.mjs:176:27)
    at new EventEmitter (https://deno.land/std@0.170.0/node/_events.mjs:56:21)
    at new _Worker (https://deno.land/std@0.170.0/node/worker_threads.ts:49:5)
    at new _Worker (https://deno.land/std@0.170.0/node/worker_threads.ts:55:36)
    at new _Worker (https://deno.land/std@0.170.0/node/worker_threads.ts:55:36)
    at new _Worker (https://deno.land/std@0.170.0/node/worker_threads.ts:55:36)
    at new _Worker (https://deno.land/std@0.170.0/node/worker_threads.ts:55:36)
    at new _Worker (https://deno.land/std@0.170.0/node/worker_threads.ts:55:36)
    at new _Worker (https://deno.land/std@0.170.0/node/worker_threads.ts:55:36)

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

import { init } from "npm:z3-solver/browser";

errors

error: Unable to load /home/mrcool/.cache/deno/npm/registry.npmjs.org/z3-solver/4.11.2/browser imported from file:///home/mrcool/dev/deno/lab/qqq.ts

Caused by:

[sigmaSd]

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 ?

[sigmaSd]

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.

[scarf005]

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))))

System Info

deno 1.39.1+140e8be (canary, x86_64-unknown-linux-gnu)
v8 12.0.267.8
typescript 5.3.3

[sullrich84]

Advent of bug fixing :)

[rich-dtk]

I ran into a similar bug when trying to use the Optimize solver in deno. I was also able to reproduce the bug in #17171 (comment)
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

[sigmaSd]

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());

[sigmaSd]

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

[sigmaSd]

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