Z3
 
Loading...
Searching...
No Matches
log.go
Go to the documentation of this file.
1// Copyright (c) Microsoft Corporation 2025
2// Z3 Go API: Logging functionality
3
4package z3
5
6/*
7#include "z3.h"
8#include <stdlib.h>
9*/
10import "C"
11import (
12 "sync"
13 "unsafe"
14)
15
16var (
17 logMutex sync.Mutex
18 isLogOpen bool
19)
20
21// OpenLog opens an interaction log file
22// Returns true if successful, false otherwise
23func OpenLog(filename string) bool {
24 logMutex.Lock()
25 defer logMutex.Unlock()
26
27 cFilename := C.CString(filename)
28 defer C.free(unsafe.Pointer(cFilename))
29
30 result := C.Z3_open_log(cFilename)
31 if bool(result) {
32 isLogOpen = true
33 return true
34 }
35 return false
36}
37
38// CloseLog closes the interaction log
39func CloseLog() {
40 logMutex.Lock()
41 defer logMutex.Unlock()
42
43 C.Z3_close_log()
44 isLogOpen = false
45}
46
47// AppendLog appends a user-provided string to the interaction log
48// Panics if the log is not open
49func AppendLog(s string) {
50 logMutex.Lock()
51 defer logMutex.Unlock()
52
53 if !isLogOpen {
54 panic("Log is not open")
55 }
56
57 cStr := C.CString(s)
58 defer C.free(unsafe.Pointer(cStr))
59 C.Z3_append_log(cStr)
60}
61
62// IsLogOpen returns true if the interaction log is open
63func IsLogOpen() bool {
64 logMutex.Lock()
65 defer logMutex.Unlock()
66 return isLogOpen
67}