Skip to content

Commit

Permalink
add support for different "modes" in table definitions: first match a…
Browse files Browse the repository at this point in the history
…nd last match
  • Loading branch information
danieldietsch committed Nov 13, 2024
1 parent dd7dcad commit e5efee5
Showing 1 changed file with 22 additions and 2 deletions.
24 changes: 22 additions & 2 deletions benchexec/tools/smtinterpol.py
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
import benchexec.util as util
import benchexec.tools.smtlib2
import logging
import json

class Tool(benchexec.tools.smtlib2.Smtlib2Tool):
"""
Expand Down Expand Up @@ -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


0 comments on commit e5efee5

Please sign in to comment.