Skip to content

Commit

Permalink
fix smtlib installers
Browse files Browse the repository at this point in the history
  • Loading branch information
RipplB committed Jun 28, 2024
1 parent 0c01e98 commit 98e29d3
Showing 1 changed file with 48 additions and 51 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -48,17 +48,6 @@ public final class SmtLibSolverManager extends SolverManager {
private static final Map<String, Class<? extends SmtLibSolverInstaller>> installerDeclarations = new HashMap<>();
private static Tuple2<String, Class<? extends GenericSmtLibSolverInstaller>> genericInstallerDeclaration;

public static <T extends SmtLibSolverInstaller> void registerInstaller(final String name,
final Class<T> decl) {
installerDeclarations.put(name, decl);
}

public static <T extends GenericSmtLibSolverInstaller> void registerGenericInstaller(
final String name, final Class<T> decl) {
checkState(genericInstallerDeclaration == null);
genericInstallerDeclaration = Tuple2.of(name, decl);
}

static {
registerInstaller("z3", Z3SmtLibSolverInstaller.class);
registerInstaller("cvc4", CVC4SmtLibSolverInstaller.class);
Expand All @@ -71,43 +60,12 @@ public static <T extends GenericSmtLibSolverInstaller> void registerGenericInsta
registerGenericInstaller("generic", GenericSmtLibSolverInstaller.class);
}

public static String getSolverName(final String name) {
final var solverName = decodeSolverName(name, 0);
if (solverName != null) {
return solverName;
} else {
throw new IllegalArgumentException("Invalid version string: " + name);
}
}

public static String getSolverVersion(final String name) {
final var solverVersion = decodeSolverName(name, 1);
if (solverVersion != null) {
return solverVersion;
} else {
throw new IllegalArgumentException("Invalid version string: " + name);
}
}

private static String decodeSolverName(final String name, final int part) {
final var versionArr = name.split(":");

if (versionArr.length != 2) {
return null;
}

return versionArr[part];
}

private final Path home;
private final Logger logger;

private final Map<String, SmtLibSolverInstaller> installers;
private final Tuple2<String, GenericSmtLibSolverInstaller> genericInstaller;

private boolean closed = false;
private final Set<SolverBase> instantiatedSolvers;

private boolean closed = false;
private SmtLibSolverManager(final Path home, final Logger logger) {
this.logger = logger;
checkNotNull(home);
Expand Down Expand Up @@ -144,12 +102,58 @@ private SmtLibSolverManager(final Path home, final Logger logger) {
this.instantiatedSolvers = new HashSet<>();
}

public static <T extends SmtLibSolverInstaller> void registerInstaller(final String name,
final Class<T> decl) {
installerDeclarations.put(name, decl);
}

public static <T extends GenericSmtLibSolverInstaller> void registerGenericInstaller(
final String name, final Class<T> decl) {
checkState(genericInstallerDeclaration == null);
genericInstallerDeclaration = Tuple2.of(name, decl);
}

public static String getSolverName(final String name) {
final var solverName = decodeSolverName(name, 0);
if (solverName != null) {
return solverName;
} else {
throw new IllegalArgumentException("Invalid version string: " + name);
}
}

public static String getSolverVersion(final String name) {
final var solverVersion = decodeSolverName(name, 1);
if (solverVersion != null) {
return solverVersion;
} else {
throw new IllegalArgumentException("Invalid version string: " + name);
}
}

private static String decodeSolverName(final String name, final int part) {
final var versionArr = name.split(":");

if (versionArr.length != 2) {
return null;
}

return versionArr[part];
}

public static SmtLibSolverManager create(final Path home, final Logger logger)
throws IOException {
createIfNotExists(home);
return new SmtLibSolverManager(home, logger);
}

private static Path createIfNotExists(final Path path) throws IOException {
if (!Files.exists(path)) {
Files.createDirectory(path);
}
return path;
}

public String getGenericInstallerName() {
return genericInstaller.get1();
}
Expand Down Expand Up @@ -305,7 +309,7 @@ public List<String> getInstalledVersions(final String solver)
}

public String getVersionString(final String solver, final String version,
final boolean installed) throws SmtLibSolverInstallerException {
final boolean installed) throws SmtLibSolverInstallerException {
if (!version.equals("latest")) {
return version;
} else {
Expand All @@ -323,13 +327,6 @@ public String getVersionString(final String solver, final String version,
}
}

private static Path createIfNotExists(final Path path) throws IOException {
if (!Files.exists(path)) {
Files.createDirectory(path);
}
return path;
}

@Override
public void close() throws Exception {
for (final var solver : instantiatedSolvers) {
Expand Down

0 comments on commit 98e29d3

Please sign in to comment.