creation smtlog

Author: Your Name

backends/smt2/smtbmc.py

@@ -236,7 +236,7 @@ def usage():
     elif so.handle(o, a):
         pass
     elif o == "--dump-log-lines":
-        sl.write_log = True
+        sl.toggle_on_log()
         if(len(a)>0):
             sl.filename = a
     else:
@@ -390,7 +390,7 @@ def replace_netref(match):
     return "(and %s)" % " ".join(expr_list)
 
 
-smt = SmtIo(opts=so)
+smt = SmtIo(opts=so, logs=sl)
 
 if noinfo and vcdfile is None and vlogtbfile is None and outconstr is None:
     smt.produce_models = False

backends/smt2/smtio.py

@@ -106,7 +106,7 @@ def __init__(self):
 
 
 class SmtIo:
-    def __init__(self, opts=None):
+    def __init__(self, opts=None, logs=None):
         global solvers_index
 
         self.logic = None
@@ -147,6 +147,12 @@ def __init__(self, opts=None):
             self.info_stmts = list()
             self.nocomments = False
 
+        if logs is None:
+            self.smtlog = SmtLog()
+        
+        else:
+            self.smtlog = logs
+
         self.start_time = time()
 
         self.modinfo = dict()
@@ -347,6 +353,7 @@ def p_close(self):
         self.p_thread = None
 
     def write(self, stmt, unroll=True):
+        self.smtlog.write_line(stmt) # Write log
         if stmt.startswith(";"):
             self.info(stmt)
             if not self.setup_done:

backends/smt2/smtlog.py

@@ -21,18 +21,18 @@
 class SmtLog:
     def __init__(self):
         self.filename = "log"
-        self.ext = ".log"
+        self.ext = ".smtlog"
         self.prefix = "pre_"
 
         self.show_err = True
-        self.write_log = False
+        self.write_allowed = False
 
         self.depth = 0
         self.refine = 0
 
         self.logfile = None
 
-    #SETTERS
+    # GETTERS / SETTERS
     def set_filename(self, filename="log"):
         if(filename != ""):
             self.filename = filename
@@ -43,6 +43,16 @@ def set_depth(self, depth=0):
     def set_refine(self, refine=0):
         self.refine = refine
 
+    def toggle_log(self):
+        self.write_allowed = not self.write_allowed
+    
+    def toggle_on_log(self):
+        self.write_allowed = True
+
+    def toggle_off_log(self):
+        self.write_allowed = False
+
+    # -----------------
 
     # Open <logfile> if not already open and set <filename> if given
     def open_file(self, filename=""):
@@ -60,20 +70,21 @@ def close_file(self):
             self.logfile = None
 
     # Write a text in <logfile> if it is open
-    def write(self, text):
+    def write_log(self, text):
         if(self.logfile != None and not self.logfile.closed):
             self.logfile.write(text)
         elif(self.show_err):
             sys.stderr.write("Can't write line:\n{}in file {}".format(text, self.filename))
 
     # Write a line in <logfile> if it is open
     def write_line(self, text):
-        if(not text.endswith("\n")):
-            text = text+"\n"
-        self.write(text)
+        if(self.write_allowed):
+            if(not text.endswith("\n")):
+                text = text+"\n"
+            self.write_log(text)
 
 
-    
     def show_depth(self, depth=-1):
         if(depth != -1):
             self.set_depth(depth)
+        self.write_line("\n=== \tDepth \t{} \t===".format(self.depth))