mirror of
https://github.com/Z3Prover/z3
synced 2026-03-15 17:49:59 +00:00
move agent readme to repo root as Z3-AGENT.md
This commit is contained in:
Angelica Moreira
parent
4e0a41252a
commit
68ea8d3a43
1 changed files with 0 additions and 0 deletions
312
.github/agents/README.md
vendored
312
.github/agents/README.md
vendored
|
|
@ -1,312 +0,0 @@
|
|||
# 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:
|
||||
|
||||
```
|
||||
@z3 is (x + y > 10) satisfiable?
|
||||
@z3 prove that x*x >= 0 for all integers
|
||||
@z3 run memory-safety checks on the test suite
|
||||
```
|
||||
|
||||
The agent picks the right skill and runs it.
|
||||
|
||||
## 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 |
|
||||
Loading…
Add table
Add a link
Reference in a new issue