Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Static Public Member Functions
Log Class Reference

Static Public Member Functions

static boolean open (String filename)
static void close ()
static void append (String s) throws Z3Exception
static boolean isOpen ()

Detailed Description

Interaction logging for Z3. Note that this is a global, static log and if multiple Context objects are created, it logs the interaction with all of them.

Definition at line 25 of file Log.java.


Member Function Documentation

static void append ( String  s) throws Z3Exception [inline, static]

Appends the user-provided string s to the interaction log.

Exceptions:
Z3Exception

Definition at line 55 of file Log.java.

    {
        if (!m_is_open)
            throw new Z3Exception("Log cannot be closed.");
        Native.appendLog(s);
    }
static void close ( ) [inline, static]

Closes the interaction log.

Definition at line 44 of file Log.java.

    {
        m_is_open = false;
        Native.closeLog();
    }
static boolean isOpen ( ) [inline, static]

Checks whether the interaction log is opened.

Returns:
True if the interaction log is open, false otherwise.

Definition at line 67 of file Log.java.

    {
        return m_is_open;
    }
static boolean open ( String  filename) [inline, static]

Open an interaction log file.

Parameters:
filenamethe name of the file to open
Returns:
True if opening the log file succeeds, false otherwise.

Definition at line 35 of file Log.java.

    {
        m_is_open = true;
        return Native.openLog(filename) == 1;
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines