mirror of
https://github.com/Z3Prover/z3
synced 2026-02-22 08:17:37 +00:00
74 lines
1.8 KiB
Go
74 lines
1.8 KiB
Go
package main
|
|
|
|
import (
|
|
"fmt"
|
|
"os"
|
|
"path/filepath"
|
|
|
|
"github.com/Z3Prover/z3/src/api/go"
|
|
)
|
|
|
|
func main() {
|
|
// Test SetInitialValue
|
|
fmt.Println("\nTesting Solver.SetInitialValue()...")
|
|
ctx2 := z3.NewContext()
|
|
solver2 := ctx2.NewSolver()
|
|
|
|
x := ctx2.MkIntConst("x")
|
|
y := ctx2.MkIntConst("y")
|
|
|
|
// Set initial values to guide the solver
|
|
solver2.SetInitialValue(x, ctx2.MkInt(5, ctx2.MkIntSort()))
|
|
solver2.SetInitialValue(y, ctx2.MkInt(10, ctx2.MkIntSort()))
|
|
|
|
// Add constraints
|
|
solver2.Assert(ctx2.MkGt(x, ctx2.MkInt(0, ctx2.MkIntSort())))
|
|
solver2.Assert(ctx2.MkGt(y, ctx2.MkInt(0, ctx2.MkIntSort())))
|
|
|
|
if solver2.Check() == z3.Satisfiable {
|
|
fmt.Println(" ✓ SetInitialValue works (solver found solution)")
|
|
} else {
|
|
fmt.Println(" ✗ SetInitialValue failed")
|
|
os.Exit(1)
|
|
}
|
|
|
|
// Test FromString
|
|
fmt.Println("\nTesting Solver.FromString()...")
|
|
ctx3 := z3.NewContext()
|
|
solver3 := ctx3.NewSolver()
|
|
|
|
smtString := "(declare-const z Int)(assert (> z 42))"
|
|
solver3.FromString(smtString)
|
|
|
|
if solver3.Check() == z3.Satisfiable {
|
|
fmt.Println(" ✓ FromString works correctly")
|
|
} else {
|
|
fmt.Println(" ✗ FromString failed")
|
|
os.Exit(1)
|
|
}
|
|
|
|
// Test FromFile
|
|
fmt.Println("\nTesting Solver.FromFile()...")
|
|
ctx4 := z3.NewContext()
|
|
solver4 := ctx4.NewSolver()
|
|
|
|
// Create a temporary SMT file
|
|
tmpDir := os.TempDir()
|
|
smtFile := filepath.Join(tmpDir, "test.smt2")
|
|
err := os.WriteFile(smtFile, []byte("(declare-const w Int)\n(assert (< w 100))\n"), 0644)
|
|
if err != nil {
|
|
fmt.Printf(" ✗ Failed to create test file: %v\n", err)
|
|
os.Exit(1)
|
|
}
|
|
defer os.Remove(smtFile)
|
|
|
|
solver4.FromFile(smtFile)
|
|
if solver4.Check() == z3.Satisfiable {
|
|
fmt.Println(" ✓ FromFile works correctly")
|
|
} else {
|
|
fmt.Println(" ✗ FromFile failed")
|
|
os.Exit(1)
|
|
}
|
|
|
|
fmt.Println("\nAll tests passed! ✓")
|
|
}
|