mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 08:30:50 +00:00
Code Activity

Fix duplicate example in advanced_example.go and add silent markers for unused vars

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-16 21:46:23 +00:00 • committed by Nikolaj Bjorner
parent d1dd539519
commit 42c783ac98
1 changed files with 9 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

52
examples/go/advanced_example.go
View file

@ -91,6 +91,8 @@ func main() {
intSort := ctx.MkIntSort() intSort := ctx.MkIntSort()
listSort, nilDecl, consDecl, isNilDecl, isConsDecl, headDecl, tailDecl := listSort, nilDecl, consDecl, isNilDecl, isConsDecl, headDecl, tailDecl :=
ctx.MkListSort("IntList", intSort) ctx.MkListSort("IntList", intSort)
// Silence unused warnings (these constructors may be needed in more complex examples)
_, _, _ = isNilDecl, isConsDecl, tailDecl
// Create list: cons(1, cons(2, nil)) // Create list: cons(1, cons(2, nil))
nilList := ctx.MkApp(nilDecl) nilList := ctx.MkApp(nilDecl)
@ -140,10 +142,12 @@ func main() {
"Color", "Color",
[]string{"Red", "Green", "Blue"}, []string{"Red", "Green", "Blue"},
) )
_ = colorTesters // Silence unused warning
red := ctx.MkApp(colorConsts[0]) red := ctx.MkApp(colorConsts[0])
green := ctx.MkApp(colorConsts[1]) green := ctx.MkApp(colorConsts[1])
blue := ctx.MkApp(colorConsts[2]) blue := ctx.MkApp(colorConsts[2])
_, _ = green, blue // Silence unused warning
c1 := ctx.MkConst(ctx.MkStringSymbol("c1"), colorSort) c1 := ctx.MkConst(ctx.MkStringSymbol("c1"), colorSort)
c2 := ctx.MkConst(ctx.MkStringSymbol("c2"), colorSort) c2 := ctx.MkConst(ctx.MkStringSymbol("c2"), colorSort)
@ -201,18 +205,18 @@ func main() {
str := ctx.MkConst(ctx.MkStringSymbol("str"), ctx.MkStringSort()) str := ctx.MkConst(ctx.MkStringSymbol("str"), ctx.MkStringSort())
// Create regex: (a|b)*c+ (zero or more 'a' or 'b', followed by one or more 'c') // Create regex: (a|b)*c+ (zero or more 'a' or 'b', followed by one or more 'c')
a := ctx.MkToRe(ctx.MkString("a")) reA := ctx.MkToRe(ctx.MkString("a"))
b := ctx.MkToRe(ctx.MkString("b")) reB := ctx.MkToRe(ctx.MkString("b"))
c := ctx.MkToRe(ctx.MkString("c")) reC := ctx.MkToRe(ctx.MkString("c"))
// (a|b) // (a|b)
aOrB := ctx.MkReUnion(a, b) aOrB := ctx.MkReUnion(reA, reB)
// (a|b)* // (a|b)*
aOrBStar := ctx.MkReStar(aOrB) aOrBStar := ctx.MkReStar(aOrB)
// c+ // c+
cPlus := ctx.MkRePlus(c) cPlus := ctx.MkRePlus(reC)
// (a|b)*c+ // (a|b)*c+
regex := ctx.MkReConcat(aOrBStar, cPlus) regex := ctx.MkReConcat(aOrBStar, cPlus)
@ -233,44 +237,6 @@ func main() {
} }
} }
// Example 8: Regular expressions
fmt.Println("\nExample 8: Regular expressions")
solver.Reset()
// Create a string variable
str := ctx.MkConst(ctx.MkStringSymbol("str"), ctx.MkStringSort())
// Create regex: (a|b)*c+ (zero or more 'a' or 'b', followed by one or more 'c')
a := ctx.MkToRe(ctx.MkString("a"))
b := ctx.MkToRe(ctx.MkString("b"))
c := ctx.MkToRe(ctx.MkString("c"))
// (a|b)*
aOrB := ctx.MkReUnion(a, b)
aOrBStar := ctx.MkReStar(aOrB)
// c+
cPlus := ctx.MkRePlus(c)
// (a|b)*c+
regex := ctx.MkReConcat(aOrBStar, cPlus)
// Assert that string matches the regex
solver.Assert(ctx.MkInRe(str, regex))
// Also assert that length is less than 10
strLen := ctx.MkSeqLength(str)
tenStr := ctx.MkInt(10, ctx.MkIntSort())
solver.Assert(ctx.MkLt(strLen, tenStr))
if solver.Check() == z3.Satisfiable {
model := solver.Model()
fmt.Println("Satisfiable!")
if strVal, ok := model.Eval(str, true); ok {
fmt.Println("String matching (a|b)*c+:", strVal.String())
}
}
// Example 9: Optimization // Example 9: Optimization
fmt.Println("\nExample 9: Optimization (maximize/minimize)") fmt.Println("\nExample 9: Optimization (maximize/minimize)")