From 98e29d396c1489b327dff09a23f0353e028498d9 Mon Sep 17 00:00:00 2001 From: RipplB Date: Fri, 28 Jun 2024 16:26:28 +0200 Subject: [PATCH] fix smtlib installers --- .../solver/smtlib/SmtLibSolverManager.java | 99 +++++++++---------- 1 file changed, 48 insertions(+), 51 deletions(-) diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/SmtLibSolverManager.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/SmtLibSolverManager.java index b51b7f4765..44c2400d7c 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/SmtLibSolverManager.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/SmtLibSolverManager.java @@ -48,17 +48,6 @@ public final class SmtLibSolverManager extends SolverManager { private static final Map> installerDeclarations = new HashMap<>(); private static Tuple2> genericInstallerDeclaration; - public static void registerInstaller(final String name, - final Class decl) { - installerDeclarations.put(name, decl); - } - - public static void registerGenericInstaller( - final String name, final Class decl) { - checkState(genericInstallerDeclaration == null); - genericInstallerDeclaration = Tuple2.of(name, decl); - } - static { registerInstaller("z3", Z3SmtLibSolverInstaller.class); registerInstaller("cvc4", CVC4SmtLibSolverInstaller.class); @@ -71,43 +60,12 @@ public static 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 installers; private final Tuple2 genericInstaller; - - private boolean closed = false; private final Set instantiatedSolvers; - + private boolean closed = false; private SmtLibSolverManager(final Path home, final Logger logger) { this.logger = logger; checkNotNull(home); @@ -144,12 +102,58 @@ private SmtLibSolverManager(final Path home, final Logger logger) { this.instantiatedSolvers = new HashSet<>(); } + public static void registerInstaller(final String name, + final Class decl) { + installerDeclarations.put(name, decl); + } + + public static void registerGenericInstaller( + final String name, final Class 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(); } @@ -305,7 +309,7 @@ public List 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 { @@ -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) {