diff --git a/examples/go/test_new_api_additions.go b/examples/go/test_new_api_additions.go new file mode 100644 index 000000000..9a3549c13 --- /dev/null +++ b/examples/go/test_new_api_additions.go @@ -0,0 +1,74 @@ +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! ✓") +}