mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

add initial sample agent use case

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-04 18:40:06 -07:00
parent 0a3719447e
commit a5048e4563
1 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
genaisrc/agentz3.genai.ts Normal file
View file

@ -0,0 +1,12 @@
script({
tools: ["agent_z3"],
})
$`Solve the following problems using Z3:
Twenty golfers wish to play in foursomes for 5 days. Is it possible for each golfer to play no more
than once with any other golfer?
Use SMTLIB2 to formulate the problem as a quantifier free formula over linear integer arithmetic,
also known as QF_LIA. The formula should produce an assignemnt to the twenty golfers for the 5 days of foursomes. The SMTLIB2 formula must not contain forall or exists.
`