z3/Z3-AGENT.md

# Z3 Agent

A Copilot agent for the Z3 theorem prover. It wraps 9 skills that cover
SMT solving and code quality analysis.

## What it does

The agent handles two kinds of requests:

1. **SMT solving**: formulate constraints, check satisfiability, prove
   properties, optimize objectives, simplify expressions.
2. **Code quality**: run sanitizers (ASan, UBSan) and Clang Static Analyzer
   against the Z3 codebase to catch memory bugs and logic errors.

## Prerequisites

You need a built Z3 binary. The scripts look for it in this order:

1. Explicit `--z3 path/to/z3`
2. `build/z3`, `build/release/z3`, `build/debug/z3` (relative to repo root)
3. `z3` on your PATH

For code quality skills you also need:

- **memory-safety**: cmake, make, and a compiler with sanitizer support
  (gcc or clang). The script checks at startup and tells you what is missing.
- **static-analysis**: scan-build (part of clang-tools). Same early check
  with install instructions if absent.

## Using the agent in Copilot Chat

Mention `@z3` and describe what you want in plain language.
The agent figures out which skill to use, builds the formula if needed,
runs Z3, and gives you the result.

### solve: check satisfiability

```
@z3 is (x > 0 and y > 0 and x + y < 5) satisfiable over the integers?
```

Expected response: **sat** with a model like `x = 1, y = 1`.

```
@z3 can x + y = 10 and x - y = 4 both hold at the same time?
```

Expected response: **sat** with `x = 7, y = 3`.

```
@z3 is there an integer x where x > 0, x < 0?
```

Expected response: **unsat** (no such integer exists).

### prove: check if something is always true

```
@z3 prove that x * x >= 0 for all integers x
```

Expected response: **valid** (the negation is unsatisfiable, so the property holds).

```
@z3 is it true that (a + b)^2 >= 0 for all real a and b?
```

Expected response: **valid**.

```
@z3 prove that if x > y and y > z then x > z, for integers
```

Expected response: **valid** (transitivity of >).

### optimize: find the best value

```
@z3 maximize 3x + 2y where x >= 1, y >= 1, and x + y <= 20
```

Expected response: **sat** with `x = 19, y = 1` (objective = 59).

```
@z3 minimize x + y where x >= 5, y >= 3, and x + y >= 10
```

Expected response: **sat** with `x = 5, y = 5` or similar (objective = 10).

### simplify: reduce an expression

```
@z3 simplify x + 0 + 1*x
```

Expected response: `2*x`.

```
@z3 simplify (a and true) or (a and false)
```

Expected response: `a`.

### encode: translate a problem to SMT-LIB2

```
@z3 encode this as SMT-LIB2: find integers x and y where x + y = 10 and x > y
```

Expected response: the SMT-LIB2 formula:
```
(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
(assert (> x y))
(check-sat)
(get-model)
```

### explain: interpret Z3 output

```
@z3 what does this Z3 output mean?
sat
(
  (define-fun x () Int 7)
  (define-fun y () Int 3)
)
```

Expected response: a readable summary like "satisfying assignment: x = 7, y = 3".

```
@z3 Z3 returned unknown, what does that mean?
```

Expected response: an explanation of common causes (timeout, incomplete theory, quantifiers).

### benchmark: measure performance

```
@z3 how fast can Z3 solve (x > 0 and y > 0 and x + y < 100)? run it 5 times
```

Expected response: timing stats like min/median/max in milliseconds and the result.

### memory-safety: find memory bugs in Z3

```
@z3 run AddressSanitizer on the Z3 test suite
```

Expected response: builds Z3 with ASan, runs the tests, reports any findings
with category, file, and line number. If clean, reports no findings.

```
@z3 check for undefined behavior in Z3
```

Expected response: runs UBSan, same format.

```
@z3 run both sanitizers
```

Expected response: runs ASan and UBSan, aggregates findings from both.

### static-analysis: find bugs without running the code

```
@z3 run static analysis on the Z3 source
```

Expected response: runs Clang Static Analyzer, reports findings grouped by
category (null dereference, dead store, memory leak, etc.) with file and line.

### multi-skill: the agent chains skills when needed

```
@z3 prove that for all integers, if x^2 is even then x is even
```

The agent uses **encode** to formalize and negate the statement, then
**prove** to check it, then **explain** to present the result.

```
@z3 full verification pass before the release
```

The agent runs **memory-safety** (ASan + UBSan) and **static-analysis**
in parallel, then aggregates and deduplicates findings sorted by severity.

## Using the scripts directly

Every skill lives under `.github/skills/<name>/scripts/`. All scripts
accept `--debug` for full tracing and `--db path` to specify where the
SQLite log goes (defaults to `z3agent.db` in the current directory).

### solve

Check whether a set of constraints has a solution.

```
python3 .github/skills/solve/scripts/solve.py \
  --z3 build/release/z3 \
  --formula '
(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (> y 0))
(assert (< (+ x y) 5))
(check-sat)
(get-model)'
```

Output:

```
sat
  x = 1
  y = 1
```

### prove

Check whether a property holds for all values. The script negates your
conjecture and asks Z3 if the negation is satisfiable. If it is not,
the property is valid.

```
python3 .github/skills/prove/scripts/prove.py \
  --z3 build/release/z3 \
  --conjecture '(>= (* x x) 0)' \
  --vars 'x:Int'
```

Output:

```
valid
```

If Z3 finds a counterexample, it prints `invalid` followed by the
counterexample values.

### optimize

Find the best value of an objective subject to constraints.

```
python3 .github/skills/optimize/scripts/optimize.py \
  --z3 build/release/z3 \
  --formula '
(declare-const x Int)
(declare-const y Int)
(assert (>= x 1))
(assert (>= y 1))
(assert (<= (+ x y) 20))
(maximize (+ (* 3 x) (* 2 y)))
(check-sat)
(get-model)'
```

Output:

```
sat
  x = 19
  y = 1
```

Here Z3 maximizes `3x + 2y` under the constraint `x + y <= 20`, so it
pushes x as high as possible (19) and keeps y at its minimum (1),
giving `3*19 + 2*1 = 59`.

### simplify

Reduce expressions using Z3 tactic chains.

```
python3 .github/skills/simplify/scripts/simplify.py \
  --z3 build/release/z3 \
  --formula '(declare-const x Int)(simplify (+ x 0 (* 1 x)))'
```

Output:

```
(* 2 x)
(goals
(goal
  :precision precise :depth 1)
)
```

Z3 simplified `x + 0 + 1*x` down to `2*x`.

### benchmark

Measure solving time over multiple runs.

```
python3 .github/skills/benchmark/scripts/benchmark.py \
  --z3 build/release/z3 \
  --runs 5 \
  --formula '
(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (> y 0))
(assert (< (+ x y) 100))
(check-sat)'
```

Output (times will vary on your machine):

```
runs: 5
min: 27ms
median: 28ms
max: 30ms
result: sat
```

### explain

Interpret Z3 output in readable form. It reads from stdin:

```
echo 'sat
(
  (define-fun x () Int
    19)
  (define-fun y () Int
    1)
)' | python3 .github/skills/explain/scripts/explain.py --stdin --type model
```

Output:

```
satisfying assignment:
  x = 19
  y = 1
```

### encode

Validate that an SMT-LIB2 file is well-formed by running it through Z3:

```
python3 .github/skills/encode/scripts/encode.py \
  --z3 build/release/z3 \
  --validate problem.smt2
```

If the file parses and runs without errors, it prints the formula back.
If there are syntax or sort errors, it prints the Z3 error message.

### memory-safety

Build Z3 with AddressSanitizer or UndefinedBehaviorSanitizer, run the
test suite, and collect any findings.

```
python3 .github/skills/memory-safety/scripts/memory_safety.py --sanitizer asan
python3 .github/skills/memory-safety/scripts/memory_safety.py --sanitizer ubsan
python3 .github/skills/memory-safety/scripts/memory_safety.py --sanitizer both
```

Use `--skip-build` to reuse a previous instrumented build. Use
`--build-dir path` to control where the build goes (defaults to
`build/sanitizer-asan` or `build/sanitizer-ubsan` under the repo root).

If cmake, make, or a C compiler is not found, the script prints what
you need to install and exits.

### static-analysis

Run Clang Static Analyzer over the Z3 source tree.

```
python3 .github/skills/static-analysis/scripts/static_analysis.py \
  --build-dir build/scan
```

Results go to `build/scan/scan-results/` by default. Findings are
printed grouped by category with file and line number.

If `scan-build` is not on your PATH, the script prints install
instructions for Ubuntu, macOS, and Fedora.

## Debug tracing

Add `--debug` to any command to see the full trace: run IDs, z3 binary
path, the exact command and stdin sent to Z3, stdout/stderr received,
timing, and database logging. Example:

```
python3 .github/skills/solve/scripts/solve.py \
  --z3 build/release/z3 --debug \
  --formula '
(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (> y 0))
(assert (< (+ x y) 5))
(check-sat)
(get-model)'
```

```
[DEBUG] started run 31 (skill=solve, hash=d64beb5a61842362)
[DEBUG] found z3: build/release/z3
[DEBUG] cmd: build/release/z3 -in
[DEBUG] stdin:
(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (> y 0))
(assert (< (+ x y) 5))
(check-sat)
(get-model)
[DEBUG] exit_code=0 duration=28ms
[DEBUG] stdout:
sat
(
  (define-fun x () Int
    1)
  (define-fun y () Int
    1)
)
[DEBUG] finished run 31: sat (28ms)
sat
  x = 1
  y = 1
```

## Logging

Every run is logged to a SQLite database (`z3agent.db` by default).
You can query it directly:

```
sqlite3 z3agent.db "SELECT id, skill, status, duration_ms FROM runs ORDER BY id DESC LIMIT 10;"
```

Use `--db /path/to/file.db` on any script to put the database somewhere
else.

## Skill list

| Skill | What it does |
|-------|-------------|
| solve | check satisfiability, extract models or unsat cores |
| prove | prove validity by negating and checking unsatisfiability |
| optimize | minimize or maximize objectives under constraints |
| simplify | reduce formulas with Z3 tactic chains |
| encode | translate problems into SMT-LIB2, validate syntax |
| explain | interpret Z3 output (models, cores, stats, errors) |
| benchmark | measure solving time, collect statistics |
| memory-safety | run ASan/UBSan on Z3 test suite |
| static-analysis | run Clang Static Analyzer on Z3 source |