Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Diagnostics.Contracts;
00022
00023 namespace Microsoft.Z3
00024 {
00032 [ContractVerification(true)]
00033 public static class Log
00034 {
00035 private static bool m_is_open = false;
00036
00042 public static bool Open(string filename)
00043 {
00044 m_is_open = true;
00045 return Native.Z3_open_log(filename) == 1;
00046 }
00047
00051 public static void Close()
00052 {
00053 m_is_open = false;
00054 Native.Z3_close_log();
00055 }
00056
00060 public static void Append(string s)
00061 {
00062 Contract.Requires(isOpen());
00063
00064 if (!m_is_open)
00065 throw new Z3Exception("Log cannot be closed.");
00066 Native.Z3_append_log(s);
00067 }
00068
00073 [Pure]
00074 public static bool isOpen()
00075 {
00076 return m_is_open;
00077 }
00078 }
00079 }