Provide JavaSMT main to execute as solver for SMT-COMP

javasmt

@@ -0,0 +1,132 @@
+#!/usr/bin/env bash
+
+# This file is part of JavaSMT,
+# an API wrapper for a collection of SMT solvers:
+# https://github.com/sosy-lab/java-smt
+#
+# SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+# Launcher for the command-line interface of JavaSMT. Benchmarking frameworks such
+# as BenchExec need a single executable inside the project directory, so that the
+# tool can be located and transferred via that path. The classpath is assembled the
+# same way as in runExamples.sh.
+#
+# This script sets no JVM option that influences what is measured, so that every
+# solver runs under the same conditions. The heap size comes from the memory limit
+# of the run and is passed by the tool-info module.
+
+# the location of the java command
+[ -z "$JAVA" ] && JAVA=java
+
+java_version="`"$JAVA" -XX:-UsePerfData -Xmx5m -version 2>&1`"
+result=$?
+if [ $result -eq 127 ]; then
+  echo "Java not found, please install Java 17 or newer." 1>&2
+  echo "For Ubuntu: sudo apt-get install openjdk-17-jre" 1>&2
+  echo "If you have installed Java 17, but it is not in your PATH," 1>&2
+  echo "let the environment variable JAVA point to the \"java\" binary." 1>&2
+  exit 1
+fi
+if [ $result -ne 0 ]; then
+  echo "Failed to execute Java VM, return code was $result and output was" 1>&2
+  echo "$java_version" 1>&2
+  echo "Please make sure you are able to execute Java processes by running \"$JAVA\"." 1>&2
+  exit 1
+fi
+java_version="`echo "$java_version" | grep -e "^\(java\|openjdk\) version" | cut -f2 -d\\\" | cut -f1 -d. | cut -f1 -d-`"
+if [ -z "$java_version" ] || [ "$java_version" -lt 17 ] ; then
+  echo "Your Java version is too old, please install Java 17 or newer." 1>&2
+  echo "For Ubuntu: sudo apt-get install openjdk-17-jre" 1>&2
+  echo "If you have installed Java 17, but it is not in your PATH," 1>&2
+  echo "let the environment variable JAVA point to the \"java\" binary." 1>&2
+  exit 1
+fi
+
+platform="`uname -s`"
+SEP=":"
+
+# where the project directory is, relative to the location of this script
+case "$platform" in
+  Linux|CYGWIN*)
+    SCRIPT="$(readlink -f "$0")"
+    [ -n "$PATH_TO_JAVASMT" ] || PATH_TO_JAVASMT="$(readlink -f "$(dirname "$SCRIPT")")"
+    ;;
+  MINGW64*)
+	PATH_TO_JAVASMT="." # assume working directory is the current directory
+	SEP=";"
+    ;;
+  # other platforms like Mac don't support readlink -f
+  *)
+    [ -n "$PATH_TO_JAVASMT" ] || PATH_TO_JAVASMT="$(dirname "$0")"
+    ;;
+esac
+
+# JavaSMT can be present either as the JAR that "ant jar" produces, which takes precedence, or as
+# compiled classes below bin/. The JARs with the sources and the documentation carry no classes
+# to run, so they are skipped. Several JARs would make it ambiguous which version runs, so this
+# is refused.
+JAVASMT_CLASSES=""
+for jar in "$PATH_TO_JAVASMT"/java-smt-*.jar; do
+  case "$jar" in
+    *-sources.jar | *-javadoc.jar) continue ;;
+  esac
+  if [ -e "$jar" ]; then
+    if [ -n "$JAVASMT_CLASSES" ]; then
+      echo "Found several JavaSMT JARs, please remove all but one: $JAVASMT_CLASSES $jar" 1>&2
+      exit 1
+    fi
+    JAVASMT_CLASSES="$jar"
+  fi
+done
+if [ -z "$JAVASMT_CLASSES" ]; then
+  if [ -e "$PATH_TO_JAVASMT/bin/org/sosy_lab/java_smt/cmdline/JavaSMTMain.class" ]; then
+    JAVASMT_CLASSES="$PATH_TO_JAVASMT/bin"
+  else
+    echo "Could not find JavaSMT binary, please check path to project directory" 1>&2
+    exit 1
+  fi
+fi
+
+# the classpath contains the classes of JavaSMT, the core JARs, and every solver present
+CLASSPATH="$JAVASMT_CLASSES$SEP$PATH_TO_JAVASMT/lib/java/core/*"
+for solver_dir in "$PATH_TO_JAVASMT"/lib/java/runtime-*; do
+  [ -d "$solver_dir" ] && CLASSPATH="$CLASSPATH$SEP$solver_dir/*"
+done
+
+# loop over all input parameters and parse them
+declare -a OPTIONS
+declare -a JAVA_VM_ARGUMENTS
+while [ $# -gt 0 ]; do
+
+  case $1 in
+   -X*) # params starting with "-X" are used for JVM, this includes -Xmx
+       JAVA_VM_ARGUMENTS+=("$1")
+       ;;
+   *) # other params are only for JavaSMT
+       OPTIONS+=("$1")
+       ;;
+  esac
+
+  shift
+done
+
+# Determine temp dir to use for JVM
+if [ -n "$TMPDIR" ]; then
+  JAVA_VM_ARGUMENTS+=("-Djava.io.tmpdir=$TMPDIR")
+elif [ -n "$TEMP" ]; then
+  JAVA_VM_ARGUMENTS+=("-Djava.io.tmpdir=$TEMP")
+elif [ -n "$TMP" ]; then
+  JAVA_VM_ARGUMENTS+=("-Djava.io.tmpdir=$TMP")
+fi
+
+# Run JavaSMT. Everything given here comes before the arguments from the command
+# line, so that a benchmark definition can override any of it.
+exec "$JAVA" \
+    -XX:+PerfDisableSharedMem \
+    -Djava.awt.headless=true \
+    "${JAVA_VM_ARGUMENTS[@]}" \
+    -cp "$CLASSPATH" \
+    org.sosy_lab.java_smt.cmdline.JavaSMTMain \
+    "${OPTIONS[@]}"

src/org/sosy_lab/java_smt/cmdline/CmdLineArgument.java

@@ -0,0 +1,158 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.cmdline;
+
+import static com.google.common.base.Preconditions.checkState;
+import static org.sosy_lab.java_smt.cmdline.CmdLineArguments.putIfNotExistent;
+
+import com.google.common.base.Joiner;
+import com.google.common.collect.FluentIterable;
+import com.google.common.collect.ImmutableSet;
+import com.google.errorprone.annotations.CanIgnoreReturnValue;
+import java.util.Iterator;
+import java.util.LinkedHashMap;
+import java.util.Map;
+import java.util.Map.Entry;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+/**
+ * A command-line argument with one or more names, e.g., <code>--solver</code> and <code>-solver
+ * </code>. The first name is the main name that is shown in the help message. Sorting and equality
+ * are both based on the sequence of names.
+ */
+abstract class CmdLineArgument implements Comparable<CmdLineArgument> {
+
+  private final ImmutableSet<String> names;
+  private String description = "";
+
+  CmdLineArgument(String... pNames) {
+    names = ImmutableSet.copyOf(pNames);
+  }
+
+  @CanIgnoreReturnValue
+  CmdLineArgument withDescription(String pDescription) {
+    description = pDescription;
+    return this;
+  }
+
+  /** The first name given in the constructor. */
+  String getMainName() {
+    return names.iterator().next();
+  }
+
+  @Override
+  public int compareTo(CmdLineArgument pOther) {
+    // Consistent with equals(): the string of an ImmutableSet lists the names in insertion order.
+    return names.toString().compareTo(pOther.names.toString());
+  }
+
+  @Override
+  public boolean equals(@Nullable Object pOther) {
+    if (this == pOther) {
+      return true;
+    }
+    return pOther instanceof CmdLineArgument other && names.asList().equals(other.names.asList());
+  }
+
+  @Override
+  public int hashCode() {
+    return names.asList().hashCode();
+  }
+
+  @Override
+  public String toString() {
+    String s =
+        FluentIterable.from(names)
+            .filter(pName -> !CmdLineArguments.isOldStyleArgument(pName))
+            .join(Joiner.on("/"));
+    if (description.isEmpty()) {
+      return s;
+    } else {
+      return String.format("%1$-20s %2$s", s, description);
+    }
+  }
+
+  /**
+   * Applies this argument if it matches the current argument.
+   *
+   * @return whether the current argument matched one of the names of this argument
+   */
+  boolean apply(Map<String, String> pProperties, String pCurrentArg, Iterator<String> pArgsIt)
+      throws InvalidCmdlineArgumentException {
+    if (names.contains(pCurrentArg)) {
+      apply0(pProperties, pCurrentArg, pArgsIt);
+      return true;
+    }
+    return false;
+  }
+
+  abstract void apply0(
+      Map<String, String> pProperties, String pCurrentArg, Iterator<String> pArgsIt)
+      throws InvalidCmdlineArgumentException;
+
+  /** A command-line argument with one value that is given as the next argument. */
+  static class CmdLineArgument1 extends CmdLineArgument {
+
+    private @Nullable String option;
+
+    CmdLineArgument1(String... pNames) {
+      super(pNames);
+    }
+
+    /** Sets the name of the option that receives the value of this argument. */
+    @CanIgnoreReturnValue
+    CmdLineArgument1 settingOption(String pOption) {
+      option = pOption;
+      return this;
+    }
+
+    @Override
+    final void apply0(Map<String, String> pProperties, String pCurrentArg, Iterator<String> pArgsIt)
+        throws InvalidCmdlineArgumentException {
+      if (pArgsIt.hasNext()) {
+        handleArg(pProperties, pArgsIt.next());
+      } else {
+        throw new InvalidCmdlineArgumentException(pCurrentArg + " argument missing.");
+      }
+    }
+
+    void handleArg(Map<String, String> pProperties, String pArgValue)
+        throws InvalidCmdlineArgumentException {
+      checkState(option != null, "settingOption() has to be called first");
+      putIfNotExistent(pProperties, option, pArgValue);
+    }
+  }
+
+  /** A command-line argument that sets some properties to fixed values. */
+  static class PropertyAddingCmdLineArgument extends CmdLineArgument {
+
+    // Insertion order determines which conflict is reported first.
+    private final Map<String, String> additionalIfNotExistentArgs = new LinkedHashMap<>();
+
+    PropertyAddingCmdLineArgument(String... pNames) {
+      super(pNames);
+    }
+
+    @CanIgnoreReturnValue
+    PropertyAddingCmdLineArgument settingProperty(String pName, String pValue) {
+      additionalIfNotExistentArgs.put(pName, pValue);
+      return this;
+    }
+
+    @Override
+    void apply0(Map<String, String> pProperties, String pCurrentArg, Iterator<String> pArgsIt)
+        throws InvalidCmdlineArgumentException {
+      for (Entry<String, String> e : additionalIfNotExistentArgs.entrySet()) {
+        putIfNotExistent(pProperties, e.getKey(), e.getValue());
+      }
+    }
+  }
+}