From 0b03547ba8e02c4b942a4cc308607b5e9e26654e Mon Sep 17 00:00:00 2001
From: Daniel Dietsch <daniel.dietsch@gmail.com>
Date: Wed, 19 May 2021 13:01:44 +0200
Subject: [PATCH] add support for different "modes" in table definitions: first
 match and last match

---
 benchexec/tools/smtinterpol.py | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/benchexec/tools/smtinterpol.py b/benchexec/tools/smtinterpol.py
index 17eecd7b5..cd06b38b9 100644
--- a/benchexec/tools/smtinterpol.py
+++ b/benchexec/tools/smtinterpol.py
@@ -10,6 +10,7 @@
 import benchexec.util as util
 import benchexec.tools.smtlib2
 import logging
+import json
 
 class Tool(benchexec.tools.smtlib2.Smtlib2Tool):
     """
@@ -40,10 +41,29 @@ def cmdline(self, executable, options, tasks, propertyfile=None, rlimits={}):
         return [executable, "-jar", "smtinterpol.jar"] + options + tasks
 
     def get_value_from_output(self, output, identifier):
-        regex = re.compile(identifier)
+        try:
+            val = json.loads(identifier)
+        except json.decoder.JSONDecodeError as ex:
+            raise AssertionError(f'Invalid JSON: "{identifier}". Should be {{ "Type" : "<FirstMatch>|<LastMatch>", "Expr": "<regexp>" }}')
+
+        mode = val.get('Type','FirstMatch')
+        expr = val['Expr']
+        if 'FirstMatch' == mode:
+            return self._get_value_from_output_regex(mode, output, expr)
+        elif 'LastMatch' == mode:
+            return self._get_value_from_output_regex(mode, reversed(output), expr)
+        else:
+            raise AssertionError(f"Unknown column mode {mode}")
+
+    def _get_value_from_output_regex(self, mode, output, expr):
+        regex = re.compile(expr)
+        i=0
         for line in output:
+            i=i+1
             match = regex.search(line)
             if match and len(match.groups()) > 0:
                 return match.group(1)
-        logging.debug("Did not find a match with regex %s", identifier)
+        logging.debug(f"Did not find a match with regex {expr} and mode {mode} in {i} lines")
         return None
+    
+