z3-solver Z3.String() is not a function angular implementation

[MargeKh]

Hello everyone! I recently added the 'z3-solver' npm package to my Angular app, updated all the necessary dependencies, and conducted some tests with numeric values. Working with numeric values went smoothly; I created a variable using 'Z3.Int('x')' and performed various operations. However, when attempting to work with string data, I encountered an error in the console: "ERROR Error: Uncaught (in promise): TypeError: V0.Z3.String is not a function." The error appeared when I tried to create a string value using 'Z3.String('x')'. Does anyone have any advice on how to resolve this issue? Thank you in advance!

Angular CLI: 14.2.13 Node: 16.14.2 Package Manager: npm 8.5.0 and in package.json: "z3-solver": "^4.10.1"

upd: "z3-solver": "^4.12.2" Updated version to the latest but got the same issue

[NikolajBjorner]

There is currently no js API support for strings. You can find the wrapper for "Int" here: https://github.com/Z3Prover/z3/blob/d5fe4b0d78ef109582e9562adb9a67d33a8871ea/src/api/js/src/high-level/high-level.ts#L668 There are no corresponding wrappers for strings (or sequences).

[MargeKh]

There is currently no js API support for strings. You can find the wrapper for "Int" here:

https://github.com/Z3Prover/z3/blob/d5fe4b0d78ef109582e9562adb9a67d33a8871ea/src/api/js/src/high-level/high-level.ts#L668

There are no corresponding wrappers for strings (or sequences).

I attempted to access strings using a low-level API and was able to create a string successfully. I also managed to manipulate the string using _'mkeq' without encountering any errors. However, when I added _'solverassert', I encountered the following error: "core.mjs:6736 ERROR Error: Uncaught (in promise): 17743752".

I believe there must be a way to work with different variable types, and I'm hopeful that there's a small trick to resolve this issue. If it's not possible to work with both integers and strings in this version, please let me know.

Here's my test example:

let test1 = 'olleH';
let test2 = 'Hello';
const strVar1 = Z3.mk_string(ctx, test1);
const strVar2 = Z3.mk_string(ctx, test2);
const isEquals = Z3.mk_eq(ctx, strVar1, strVar2);
const solver = Z3.mk_solver(ctx);
Z3.solver_assert(ctx, solver, isEquals);

In the stable version of Z3, is there built-in support for handling strings, or do I need to include a separate library for string manipulation in my project? I noticed references to string operations in the (C API documentation ). Moreover, there are code snippets that suggest we can interact with strings, but there appears to be no integration with the solver. You can find an example at this GitHub link