diff --git a/benchexec/tools/btormc.py b/benchexec/tools/btormc.py new file mode 100644 index 000000000..6b5714852 --- /dev/null +++ b/benchexec/tools/btormc.py @@ -0,0 +1,47 @@ +# This file is part of BenchExec, a framework for reliable benchmarking: +# https://github.com/sosy-lab/benchexec +# +# SPDX-FileCopyrightText: 2007-2020 Dirk Beyer +# +# SPDX-License-Identifier: Apache-2.0 + +import benchexec.result as result +import benchexec.tools.template + + +class Tool(benchexec.tools.template.BaseTool2): + """ + Tool info for BtorMC -- A Bounded Model Checker for Btor2 + """ + + REQUIRED_PATHS = ["build/"] + + def executable(self, tool_locator): + return tool_locator.find_executable("btormc", subdir="build/bin") + + def name(self): + return "BtorMC" + + def project_url(self): + return "https://github.com/Boolector/boolector" + + def version(self, executable): + return self._version_from_tool(executable, stdin="") + + def cmdline(self, executable, options, task, rlimits): + return [executable] + options + [task.single_input_file] + + def determine_result(self, run): + """ + @return: status of BtorMC after executing a run + """ + if run.was_timeout: + return result.RESULT_TIMEOUT + for line in run.output[::-1]: + # BtorMC's option `--trace-gen` must be set to 1 + # such that "sat/unsat" is printed to the output + if line.startswith("unsat"): + return result.RESULT_TRUE_PROP + elif line.startswith("sat"): + return result.RESULT_FALSE_PROP + return result.RESULT_UNKNOWN diff --git a/benchexec/tools/template.py b/benchexec/tools/template.py index 2309f95dd..48a190ac7 100644 --- a/benchexec/tools/template.py +++ b/benchexec/tools/template.py @@ -137,6 +137,7 @@ def version(self, executable): def _version_from_tool( executable, arg="--version", + stdin=None, use_stderr=False, ignore_stderr=False, line_prefix=None, @@ -146,6 +147,7 @@ def _version_from_tool( and returning stdout. @param executable: the path to the executable of the tool (typically the result of executable()) @param arg: an argument to pass to the tool to let it print its version + @param stdin: this argument is passed to the tool's stdin (default: None) @param use_stderr: True if the tool prints version on stderr, False for stdout @param line_prefix: if given, search line with this prefix and return only the rest of this line @return a (possibly empty) string of output of the tool @@ -153,6 +155,7 @@ def _version_from_tool( try: process = subprocess.run( [executable, arg], + input=stdin, stdout=subprocess.PIPE, stderr=subprocess.PIPE, universal_newlines=True,