mirror of
https://github.com/Z3Prover/z3
synced 2026-02-17 06:11:44 +00:00
313 lines
8.3 KiB
Go
313 lines
8.3 KiB
Go
package main
|
|
|
|
import (
|
|
"fmt"
|
|
"github.com/Z3Prover/z3/src/api/go"
|
|
)
|
|
|
|
func main() {
|
|
ctx := z3.NewContext()
|
|
fmt.Println("Z3 Go Bindings - Advanced Features Example")
|
|
fmt.Println("==========================================")
|
|
|
|
// Example 1: Bit-vectors
|
|
fmt.Println("\nExample 1: Bit-vector operations")
|
|
x := ctx.MkBVConst("x", 8)
|
|
y := ctx.MkBVConst("y", 8)
|
|
|
|
// x + y == 255 && x > y
|
|
sum := ctx.MkBVAdd(x, y)
|
|
ff := ctx.MkBV(255, 8)
|
|
|
|
solver := ctx.NewSolver()
|
|
solver.Assert(ctx.MkEq(sum, ff))
|
|
solver.Assert(ctx.MkBVUGT(x, y))
|
|
|
|
if solver.Check() == z3.Satisfiable {
|
|
model := solver.Model()
|
|
fmt.Println("Satisfiable!")
|
|
if xVal, ok := model.Eval(x, true); ok {
|
|
fmt.Println("x =", xVal.String())
|
|
}
|
|
if yVal, ok := model.Eval(y, true); ok {
|
|
fmt.Println("y =", yVal.String())
|
|
}
|
|
}
|
|
|
|
// Example 2: Floating-point arithmetic
|
|
fmt.Println("\nExample 2: Floating-point arithmetic")
|
|
solver.Reset()
|
|
|
|
fpSort := ctx.MkFPSort32()
|
|
a := ctx.MkConst(ctx.MkStringSymbol("a"), fpSort)
|
|
b := ctx.MkConst(ctx.MkStringSymbol("b"), fpSort)
|
|
|
|
// a + b > 0.0 (with rounding mode)
|
|
rm := ctx.MkConst(ctx.MkStringSymbol("rm"), ctx.MkFPRoundingModeSort())
|
|
fpSum := ctx.MkFPAdd(rm, a, b)
|
|
zero := ctx.MkFPZero(fpSort, false)
|
|
|
|
solver.Assert(ctx.MkFPGT(fpSum, zero))
|
|
solver.Assert(ctx.MkFPGT(a, ctx.MkFPZero(fpSort, false)))
|
|
|
|
if solver.Check() == z3.Satisfiable {
|
|
fmt.Println("Satisfiable! (Floating-point constraint satisfied)")
|
|
}
|
|
|
|
// Example 3: Strings
|
|
fmt.Println("\nExample 3: String operations")
|
|
solver.Reset()
|
|
|
|
s1 := ctx.MkConst(ctx.MkStringSymbol("s1"), ctx.MkStringSort())
|
|
s2 := ctx.MkConst(ctx.MkStringSymbol("s2"), ctx.MkStringSort())
|
|
|
|
// s1 contains "hello" && length(s1) < 20
|
|
hello := ctx.MkString("hello")
|
|
solver.Assert(ctx.MkSeqContains(s1, hello))
|
|
|
|
len1 := ctx.MkSeqLength(s1)
|
|
twenty := ctx.MkInt(20, ctx.MkIntSort())
|
|
solver.Assert(ctx.MkLt(len1, twenty))
|
|
|
|
// s2 is s1 concatenated with "world"
|
|
world := ctx.MkString(" world")
|
|
solver.Assert(ctx.MkEq(s2, ctx.MkSeqConcat(s1, world)))
|
|
|
|
if solver.Check() == z3.Satisfiable {
|
|
model := solver.Model()
|
|
fmt.Println("Satisfiable!")
|
|
if s1Val, ok := model.Eval(s1, true); ok {
|
|
fmt.Println("s1 =", s1Val.String())
|
|
}
|
|
if s2Val, ok := model.Eval(s2, true); ok {
|
|
fmt.Println("s2 =", s2Val.String())
|
|
}
|
|
}
|
|
|
|
// Example 4: Datatypes (List)
|
|
fmt.Println("\nExample 4: List datatype")
|
|
solver.Reset()
|
|
|
|
intSort := ctx.MkIntSort()
|
|
listSort, nilDecl, consDecl, isNilDecl, isConsDecl, headDecl, tailDecl :=
|
|
ctx.MkListSort("IntList", intSort)
|
|
|
|
// Create list: cons(1, cons(2, nil))
|
|
nilList := ctx.MkApp(nilDecl)
|
|
one := ctx.MkInt(1, intSort)
|
|
two := ctx.MkInt(2, intSort)
|
|
list2 := ctx.MkApp(consDecl, two, nilList)
|
|
list12 := ctx.MkApp(consDecl, one, list2)
|
|
|
|
// Check that head(list12) == 1
|
|
listVar := ctx.MkConst(ctx.MkStringSymbol("mylist"), listSort)
|
|
solver.Assert(ctx.MkEq(listVar, list12))
|
|
|
|
headOfList := ctx.MkApp(headDecl, listVar)
|
|
solver.Assert(ctx.MkEq(headOfList, one))
|
|
|
|
if solver.Check() == z3.Satisfiable {
|
|
fmt.Println("Satisfiable! List head is 1")
|
|
}
|
|
|
|
// Example 5: Tactics and Goals
|
|
fmt.Println("\nExample 5: Using tactics")
|
|
|
|
goal := ctx.MkGoal(true, false, false)
|
|
p := ctx.MkIntConst("p")
|
|
q := ctx.MkIntConst("q")
|
|
|
|
// Add constraint: p > 0 && q > 0 && p + q == 10
|
|
goal.Assert(ctx.MkGt(p, ctx.MkInt(0, ctx.MkIntSort())))
|
|
goal.Assert(ctx.MkGt(q, ctx.MkInt(0, ctx.MkIntSort())))
|
|
goal.Assert(ctx.MkEq(ctx.MkAdd(p, q), ctx.MkInt(10, ctx.MkIntSort())))
|
|
|
|
// Apply simplify tactic
|
|
tactic := ctx.MkTactic("simplify")
|
|
result := tactic.Apply(goal)
|
|
|
|
fmt.Printf("Tactic produced %d subgoals\n", result.NumSubgoals())
|
|
if result.NumSubgoals() > 0 {
|
|
subgoal := result.Subgoal(0)
|
|
fmt.Println("Simplified goal:", subgoal.String())
|
|
}
|
|
|
|
// Example 6: Enumerations
|
|
fmt.Println("\nExample 6: Enumeration types")
|
|
solver.Reset()
|
|
|
|
colorSort, colorConsts, colorTesters := ctx.MkEnumSort(
|
|
"Color",
|
|
[]string{"Red", "Green", "Blue"},
|
|
)
|
|
|
|
red := ctx.MkApp(colorConsts[0])
|
|
green := ctx.MkApp(colorConsts[1])
|
|
blue := ctx.MkApp(colorConsts[2])
|
|
|
|
c1 := ctx.MkConst(ctx.MkStringSymbol("c1"), colorSort)
|
|
c2 := ctx.MkConst(ctx.MkStringSymbol("c2"), colorSort)
|
|
|
|
// c1 != c2 && c1 != Red
|
|
solver.Assert(ctx.MkDistinct(c1, c2))
|
|
solver.Assert(ctx.MkNot(ctx.MkEq(c1, red)))
|
|
|
|
if solver.Check() == z3.Satisfiable {
|
|
model := solver.Model()
|
|
fmt.Println("Satisfiable!")
|
|
if c1Val, ok := model.Eval(c1, true); ok {
|
|
fmt.Println("c1 =", c1Val.String())
|
|
}
|
|
if c2Val, ok := model.Eval(c2, true); ok {
|
|
fmt.Println("c2 =", c2Val.String())
|
|
}
|
|
}
|
|
|
|
// Example 7: Tuples
|
|
fmt.Println("\nExample 7: Tuple types")
|
|
solver.Reset()
|
|
|
|
tupleSort, mkTuple, projections := ctx.MkTupleSort(
|
|
"Point",
|
|
[]string{"x", "y"},
|
|
[]*z3.Sort{ctx.MkIntSort(), ctx.MkIntSort()},
|
|
)
|
|
|
|
// Create point (3, 4)
|
|
three := ctx.MkInt(3, ctx.MkIntSort())
|
|
four := ctx.MkInt(4, ctx.MkIntSort())
|
|
point := ctx.MkApp(mkTuple, three, four)
|
|
|
|
p1 := ctx.MkConst(ctx.MkStringSymbol("p1"), tupleSort)
|
|
solver.Assert(ctx.MkEq(p1, point))
|
|
|
|
// Extract x coordinate
|
|
xCoord := ctx.MkApp(projections[0], p1)
|
|
solver.Assert(ctx.MkEq(xCoord, three))
|
|
|
|
if solver.Check() == z3.Satisfiable {
|
|
fmt.Println("Satisfiable! Tuple point created")
|
|
model := solver.Model()
|
|
if p1Val, ok := model.Eval(p1, true); ok {
|
|
fmt.Println("p1 =", p1Val.String())
|
|
}
|
|
}
|
|
|
|
// 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)
|
|
|
|
// (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)
|
|
ten := ctx.MkInt(10, ctx.MkIntSort())
|
|
solver.Assert(ctx.MkLt(strLen, ten))
|
|
|
|
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 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
|
|
fmt.Println("\nExample 9: Optimization (maximize/minimize)")
|
|
|
|
opt := ctx.NewOptimize()
|
|
|
|
// Variables
|
|
xOpt := ctx.MkIntConst("x_opt")
|
|
yOpt := ctx.MkIntConst("y_opt")
|
|
|
|
// Constraints: x + y <= 10, x >= 0, y >= 0
|
|
tenOpt := ctx.MkInt(10, ctx.MkIntSort())
|
|
zeroOpt := ctx.MkInt(0, ctx.MkIntSort())
|
|
|
|
opt.Assert(ctx.MkLe(ctx.MkAdd(xOpt, yOpt), tenOpt))
|
|
opt.Assert(ctx.MkGe(xOpt, zeroOpt))
|
|
opt.Assert(ctx.MkGe(yOpt, zeroOpt))
|
|
|
|
// Objective: maximize x + 2*y
|
|
twoOpt := ctx.MkInt(2, ctx.MkIntSort())
|
|
objective := ctx.MkAdd(xOpt, ctx.MkMul(twoOpt, yOpt))
|
|
objHandle := opt.Maximize(objective)
|
|
|
|
if opt.Check() == z3.Satisfiable {
|
|
model := opt.Model()
|
|
fmt.Println("Optimal solution found!")
|
|
if xVal, ok := model.Eval(xOpt, true); ok {
|
|
fmt.Println("x =", xVal.String())
|
|
}
|
|
if yVal, ok := model.Eval(yOpt, true); ok {
|
|
fmt.Println("y =", yVal.String())
|
|
}
|
|
upper := opt.GetUpper(objHandle)
|
|
if upper != nil {
|
|
fmt.Println("Maximum value of x + 2*y =", upper.String())
|
|
}
|
|
}
|
|
|
|
fmt.Println("\nAll advanced examples completed successfully!")
|
|
}
|
|
|