Add support for Algebraic Datatypes in js bindings

[NikolajBjorner]

Algebraic datatypes constructors and sort and expression wrappers are not available in the js/ts bindings. Including these, and other features such as Sequence/String/Regex allows bypassing using lower-level APIs or creating strings.

[bakkot]

Do you have links to the Python code for those? It's usually fairly straightforward to port from Python.

[NikolajBjorner]

We first have to create constructors and associate with an object.

https://github.com/Z3Prover/z3/blob/81f10912ae32f2e341fcf60627bd4de68d7a8b42/src/api/python/z3/z3.py#L5136

Then the datatype is created for z3 using an API call. At this point the Datatype sort is available and associated constructor/accessor/tester functions.

https://github.com/Z3Prover/z3/blob/81f10912ae32f2e341fcf60627bd4de68d7a8b42/src/api/python/z3/z3.py#L5344

I started poking at this yesterday to figure out what is involved in the ts side. The naive AI query didn't do the trick and was bound to break things, coupled with my entry-level ts grasp, a terrible combination.

[bakkot]

Getting good types for those is going to be tricky.

It looks like the design in Python is what you might call the builder pattern: you create the builder (List = Datatype('List')), repeatedly call a method which defines part of the final thing (List.declare('nil')), and then finalize (List = List.create()).

It's possible to do roughly the same pattern in JavaScript, but it would have to be a singe expression in order to get good types: const List = (new DataType('List')).declare('nil').declare(etc).create(). And that doesn't let you have recursive ADTs, because you can't refer to the class that you're building while you're building it.

The easiest solution would be to let you specify the (string) name of the DataType you're building, instead of referring to the object itself. So you could have sort: IntSort or sort: 'List'. And then the createDatatypes function would be responsible for assembling those. It should be possible to correctly infer the types for those cases as long as everything is inline, although it would be pretty gnarly, and I think we'd probably want to only expose createDatatypes and not new DataType.

I'm imagining something like this:

const { Tree, TreeList } = createDatatypes({
  Tree: {
    leaf: [{ name: 'val', sort: IntSort }],
    node: [{ name: 'children', sort: 'TreeList' }],
  },
  TreeList: {
    nil: [],
    cons: [{ name: 'car', sort: 'Tree' }, { name: 'cdr', sort: 'TreeList' }],
  },
});

Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil))) // works

Writing TypeScript types to make this work is going to require someone who is very good at TypeScript, probably better than current AIs. I might be able to make it work but no promises.

[bakkot]

Actually, Gemini 2.5 appears to have one-shot this, which is kind of astonishing.

prompt

I have some very complicated TypeScript types I want you to write.

The basic usage looks like this:

const { Tree, TreeList } = createDatatypes({
  Tree: {
    leaf: [{ name: 'val', sort: IntSort }],
    node: [{ name: 'children', sort: 'TreeList' }],
  },
  TreeList: {
    nil: [],
    cons: [{ name: 'car', sort: 'Tree' }, { name: 'cdr', sort: 'TreeList' }],
  },
});

// the above results in Tree and TreeList objects equivalent to the following:
class Tree {
  static leaf(val: IntSort): Tree;
  static node(children: TreeList): Tree;
  get val: IntSort;
  get children: TreeList;
}
class TreeList {
  static nil(): TreeList;
  static cons(car: Tree, cdr: TreeList): TreeList;
  get car: Tree;
  get cdr: TreeList;
}

Calling createDatatypes and passing it an object literal should return a value whose keys correspond to the keys of the provided object literal and whose values are classes, where the classes have a static member for each declared item in the object provided to createDatatypes as above.

I don't want an implementation in JS. I just want the TypeScript types for the createDatatypes function.

It gives me these types, which appear to be correct. Needs some minor tweaking to handle details like having a sort: IntSort argument result in a type which expects a number, but that's doable. Probably also needs tweaking to handle providing previously-defined data types although that's probably not strictly necessary.

Edit: better types after thinking more (these ensure properties are present only on the values which have them).

[NikolajBjorner]

I don't doubt the models generate pretty good code, but the last step is quality control. Overall, chores like these are now easier asks, but still an ask and a context switch.

[NikolajBjorner]

The other thing I read from your comment: A good ts native wrapper shouldn't have to be tied to what the Python bindings do. Right.

[bakkot]

Looking into this a bit more, the docs have this example:

; declare a mutually recursive parametric datatype
(declare-datatypes (T) ((Tree leaf (node (value T) (children TreeList)))
                        (TreeList nil (cons (car Tree) (cdr TreeList)))))
(declare-const t1 (Tree Int))
(declare-const t2 (Tree Bool))
; we must use the 'as' construct to distinguish the leaf (Tree Int) from leaf (Tree Bool)
(assert (not (= t1 (as leaf (Tree Int)))))
(assert (< (value t1) 20))
(assert (not (is-leaf t2)))
(assert (not (value t2)))
(check-sat)
(get-model)

How would you do the equivalent of declare-const and as in Python?

[NikolajBjorner]

from z3 import *

# Define the Tree and TreeList datatypes
def mk_tree(s):
    Tree = Datatype(f"{s}" + 'Tree')
    TreeList = Datatype(f"{s}" + 'TreeList')

    Tree.declare('leaf')
    Tree.declare('node', ('value', s), ('children', TreeList))
    TreeList.declare('nil')
    TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))

    return CreateDatatypes(Tree, TreeList)

IntTree, IntTreeList = mk_tree(IntSort())
BoolTree, BoolTreeList = mk_tree(BoolSort())

# Declare constants t1 and t2
t1 = Const('t1', IntTree)
t2 = Const('t2', BoolTree)

# Create the solver
s = Solver()

# Add assertions
s.add(t1 != IntTree.leaf)
s.add(IntTree.value(t1) < 20)
s.add(t2 != BoolTree.leaf)
s.add(Not(BoolTree.value(t2)))

# Check satisfiability and get model
if s.check() == sat:
    print(s.model())
else:
    print("Unsatisfiable")

The construct "as" is for the parser to disambiguate types. SHould not be necessary with the API.

[NikolajBjorner]

@bakkot - tried copilot. A PR is ready. What do you think?