mirror of
https://github.com/Z3Prover/z3
synced 2026-02-18 14:44:21 +00:00
87812a99c0
- Add comment about safety of &levels[0] after n > 0 check - Improve test documentation about SimpleSolver limitations - Clarify that Units/NonUnits are more reliable for general use Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
93 lines
3 KiB
Go
93 lines
3 KiB
Go
package main
|
|
|
|
import (
|
|
"fmt"
|
|
"github.com/Z3Prover/z3/src/api/go"
|
|
)
|
|
|
|
func main() {
|
|
// Create a new Z3 context
|
|
ctx := z3.NewContext()
|
|
fmt.Println("Z3 Go Bindings - New APIs Test")
|
|
fmt.Println("================================")
|
|
|
|
// Test diagnostic APIs
|
|
fmt.Println("\nTest 1: Solver Diagnostic APIs")
|
|
solver := ctx.NewSolver()
|
|
|
|
// Create some simple constraints
|
|
x := ctx.MkIntConst("x")
|
|
y := ctx.MkIntConst("y")
|
|
zero := ctx.MkInt(0, ctx.MkIntSort())
|
|
ten := ctx.MkInt(10, ctx.MkIntSort())
|
|
|
|
solver.Assert(ctx.MkGt(x, zero))
|
|
solver.Assert(ctx.MkLt(x, ten))
|
|
solver.Assert(ctx.MkEq(ctx.MkAdd(x, y), ten))
|
|
|
|
// Check satisfiability
|
|
status := solver.Check()
|
|
fmt.Println("Status:", status.String())
|
|
|
|
if status == z3.Satisfiable {
|
|
// Test Units() - get unit clauses
|
|
units := solver.Units()
|
|
fmt.Printf("Units: %d clauses\n", len(units))
|
|
for i, unit := range units {
|
|
fmt.Printf(" Unit %d: %s\n", i, unit.String())
|
|
}
|
|
|
|
// Test NonUnits() - get non-unit clauses
|
|
nonUnits := solver.NonUnits()
|
|
fmt.Printf("NonUnits: %d clauses\n", len(nonUnits))
|
|
for i, nu := range nonUnits {
|
|
fmt.Printf(" NonUnit %d: %s\n", i, nu.String())
|
|
}
|
|
|
|
// Note: Trail() and TrailLevels() work primarily with SimpleSolver,
|
|
// which is used internally by Z3 but not directly exposed in the Go API.
|
|
// With default solvers (created with NewSolver()), they return errors like
|
|
// "cannot retrieve trail from solvers created using tactics".
|
|
// Units() and NonUnits() provide similar diagnostic information without
|
|
// this limitation and work with all solver types.
|
|
fmt.Println("\nNote: Trail() and TrailLevels() work primarily with SimpleSolver")
|
|
fmt.Println(" These functions may return errors with default solvers")
|
|
fmt.Println(" For general diagnostic purposes, Units() and NonUnits() are more reliable")
|
|
}
|
|
|
|
// Test congruence closure APIs
|
|
fmt.Println("\nTest 2: Congruence Closure APIs")
|
|
solver2 := ctx.NewSolver()
|
|
|
|
// Create expressions for congruence testing
|
|
a := ctx.MkIntConst("a")
|
|
b := ctx.MkIntConst("b")
|
|
c := ctx.MkIntConst("c")
|
|
|
|
// Assert a = b and b = c (so a should be congruent to c)
|
|
solver2.Assert(ctx.MkEq(a, b))
|
|
solver2.Assert(ctx.MkEq(b, c))
|
|
|
|
status = solver2.Check()
|
|
fmt.Println("Status:", status.String())
|
|
|
|
if status == z3.Satisfiable {
|
|
// Test CongruenceRoot() - get congruence class representative
|
|
rootA := solver2.CongruenceRoot(a)
|
|
rootB := solver2.CongruenceRoot(b)
|
|
rootC := solver2.CongruenceRoot(c)
|
|
fmt.Printf("CongruenceRoot(a): %s\n", rootA.String())
|
|
fmt.Printf("CongruenceRoot(b): %s\n", rootB.String())
|
|
fmt.Printf("CongruenceRoot(c): %s\n", rootC.String())
|
|
|
|
// Test CongruenceNext() - get next element in congruence class
|
|
nextA := solver2.CongruenceNext(a)
|
|
fmt.Printf("CongruenceNext(a): %s\n", nextA.String())
|
|
|
|
// Test CongruenceExplain() - explain why two terms are congruent
|
|
explain := solver2.CongruenceExplain(a, c)
|
|
fmt.Printf("CongruenceExplain(a, c): %s\n", explain.String())
|
|
}
|
|
|
|
fmt.Println("\nAll new API tests completed successfully!")
|
|
}
|