# Z3 JavaScript

The Z3 distribution comes with TypeScript (and therefore JavaScript) bindings for Z3. In the following we give a few examples of using Z3 through these bindings. You can run and modify the examples locally in your browser.

The bindings do not support all features of z3. For example, you cannot (yet) create array expressions in the same way that you can create arithmetic expressions. The JavaScript bindings have the distinct advantage that they allow to use z3 directly in your browser with minimal extra dependencies.

## Warmup

We use a collection of basic examples to illustrate the bindings. The first example is a formula that establishes that there is no number both above 9 and below 10:

We note that the JavaScript bindings wrap z3 expressions into JavaScript options that support methods for building new expressions.
For example, the method `ge`

is available on an arithmetic expression `a`

. It takes one argument `b`

and returns
and expression corresponding to the predicate `a >= b`

.
The `Z3.solve`

method takes a sequence of predicates and checks if there is a solution. If there is a solution, it returns a model.

## Propositional Logic

Prove De Morgan's Law

What not to wear? It is well-known that developers of SAT solvers have difficulties looking sharp. They like to wear some combination of shirt and tie, but can't wear both. What should a SAT solver developer wear?

## Integer Arithmetic

solve `x > 2 and y < 10 and x + 2y = 7`

### Dogs, cats and mice

Given 100 dollars, the puzzle asks if it is possible to buy 100 animals based on their prices that are 15, 1, and 0.25 dollars, respectively.

## Uninterpreted Functions

The method `call`

is used to build expressions by applying the function node to arguments.

### Prove `x = y implies g(x) = g(y)`

### Disprove `x = y implies g(g(x)) = g(y)`

we illustrate the use of the `Solver`

object in the following example. Instead of calling `Z3.solve`

we here create a solver object and add assertions to it. The `solver.check()`

method is used to check
satisfiability (we expect the result to be `sat`

for this example). The method `solver.model()`

is used to retrieve a model.

### Prove `x = y implies g(x) = g(y)`

### Disprove that `x = y implies g(g(x)) = g(y)`

## Solve sudoku

The popular Sudoko can be solved.

The encoding used in the following example uses arithmetic. It works here, but is not the only possible encoding approach. You can also use bit-vectors for the cells. It is generally better to use bit-vectors for finite domain problems in z3.

## Arithmetic over Reals

You can create constants ranging over reals from strings that use fractions, decimal notation and from floating point numbers.

Z3 uses arbitrary precision arithmetic, so decimal positions are not truncated when you use strings to represent real numerals.

## Non-linear arithmetic

Z3 uses a decision procedure for non-linear arithmetic over reals.
It is based on Cylindric Algebraic Decomposition. Solutions to non-linear
arithmetic formulas are no longer necessarily rational. They are represented
as *algebraic numbers* in general and can be displayed with any number of
decimal position precision.

## Bit-vectors

Unlike in programming languages, there is no distinction between signed and unsigned bit-vectors. Instead the API supports operations that have different meaning depending on whether a bit-vector is treated as a signed or unsigned numeral. These are signed comparison and signed division, remainder operations.

In the following we illustrate the use of signed and unsigned less-than-or-equal.

It is easy to write formulas that mix bit-wise and arithmetic operations over bit-vectors.

## Using Z3 objects wrapped in JavaScript

The following example illustrates the use of AstVector