Processing of Vampire output now correctly detecting Proofs

macleod/Process.py

@@ -53,7 +53,7 @@ def update_cputime (self, pid):
         #print "total CPU time of " + self.args[0] + " = " + str(self.cputime)
 
     def enforce_limits (self, pid):
-        limit = 1536 # each reasoning process is not allowed to use up more than 1.5GB of memory
+        limit = int(filemgt.read_config('system', 'memory_limit')) # each reasoning process is not allowed to use up more than 1.5GB of memory
         memory = get_memory(pid)
         #enforce memory limit
         if memory>limit:
@@ -94,7 +94,7 @@ def run (self):
         # finished normally, i.e., sp.poll() determined the subprocess has terminated by itself
         self.update_cputime(sp.pid)
         self.result_queue.put((self.args[0], sp.returncode, None))
-        logging.getLogger(__name__).info("REASONER FINISHED: "  + self.name + ", command = " + self.args[0])
+        logging.getLogger(__name__).info("REASONER FINISHED: "  + self.name + ", exit code " + str(sp.returncode) + ", command = " + self.args[0])
         out_file.flush()
         out_file.close()
         self.writeHeader()

macleod/Reasoner.py

@@ -93,14 +93,29 @@ def isProver (self):
     def terminatedSuccessfully (self):
         from macleod.ClifModuleSet import ClifModuleSet
         mapping = {
+            ClifModuleSet.PROOF: True,
+            ClifModuleSet.COUNTEREXAMPLE: True,
             ClifModuleSet.CONSISTENT: True,
             ClifModuleSet.INCONSISTENT : True,
             ClifModuleSet.UNKNOWN : False,
             None: False
         }
 
-        def szs_status(line):
+        def paradox_status(line):
             if 'Theorem' in line:
+                #print "PARADOX SZS status found: THEOREM"
+                return ClifModuleSet.PROOF
+            elif 'Unsatisfiable' in line:
+                return ClifModuleSet.INCONSISTENT
+            elif 'CounterSatisfiable' in line:
+                return ClifModuleSet.COUNTEREXAMPLE
+            elif 'Satisfiable' in line:
+                return ClifModuleSet.CONSISTENT
+            else: # Timeout, GaveUp, Error
+                return ClifModuleSet.UNKNOWN
+
+        def vampire_status(line):
+            if 'Refutation' in line:
                 #print "VAMPIRE SZS status found: THEOREM"
                 return ClifModuleSet.PROOF
             elif 'Unsatisfiable' in line:
@@ -126,14 +141,15 @@ def success_vampire (self):
             out_file = open(self.output_file, 'r')
             lines = out_file.readlines()
             out_file.close()
-            output_lines = [x for x in lines if x.startswith('% SZS status')]
-            if len(output_lines)!=1:
+            output_lines = [x for x in lines if x.startswith('Termination reason:')]
+            l = len(output_lines)
+            if l==0:
                 if not self.return_code:
                     self.output = None
                 else:
                     self.output = ClifModuleSet.UNKNOWN                    
             else:
-                self.output = szs_status(output_lines[0])
+                self.output = vampire_status(output_lines[l-1])
 
             return mapping[self.output]
 
@@ -149,7 +165,7 @@ def success_paradox (self):
                 else:
                     self.output = ClifModuleSet.UNKNOWN                    
             else:
-                self.output = szs_status(output_lines[0])
+                self.output = paradox_status(output_lines[0])
                 #logging.getLogger(self.__module__ + "." + self.__class__.__name__).debug('Paradox terminated successfully : ' + str(self.output))