Sum function in js library

[profanat]

Hi, i want to use Sum https://z3prover.github.io/api/html/namespacez3py.html#ae216ee811ee315ea318298314829c5d8 function to create constraints, but i cant find it in js library:
const { Context, em } = await init();
let Z3 = Context('main')
console.log(Z3.Sum)
// undefined
Where can i find it?

P.S. Link to js api from npmjs.com is not working: https://z3prover.github.io/api/html/js/index.html

[NikolajBjorner]

You could add it to the js library.
Note that @walnutwaldo has a pull request open with several features where he is adding useful functionality.

[walnutwaldo]

You could just use the + functionality between values (x + y + z) or you could install my fork/PR of z3-solver that has the Sum function builtin. The PR I opened is fully working in terms of this functionality at least.

[profanat]

How can i use + functionality? 🤔 I have something like this
this.solver.add(this.subtree_size_grid[point].eq(this.Z3.Sum(...subtree_size_terms)))
How can install PR from npm?😀 Why PR is not accepted yet?

[walnutwaldo]

Ah, sorry I forget that typescript uses a different interface from the Python API. You would actually use .add. Something like

let sum = subtree_size_terms[0];
for (let i = 1; i < subtree_size_terms.length; i++) sum = sum.add(subtree_size_terms[i]);
this.solver.add(this.subtree_size_grid[point].eq(sum))

On the note of installing the PR, which I am still adding features to relating to typing of quantifier, it would be harder for you to download and maintain than the solution above so I would suggest sticking with that for now. Hopefully, I can get the last few things polished up and merged in soon.

[NikolajBjorner]

Why PR is not accepted yet?
As soon as it is not marked draft :-)

[profanat]

It works!!! Thanks!!! I'm going to create the best puzzle website thanks to your awesome library!