Package org.smtlib

Class SolverResolver

java.lang.Object

org.smtlib.SolverResolver

public final class SolverResolver
extends Object

For internal use only (public so that the tests can reach it); not part of the API. Resolves a solver name, from the merged jsmtlib.properties, to the adapter class and the executable or command that SMT.Configuration.createSolver(java.lang.String, java.lang.String) constructs it with (#123). The platform, solver directory and class lookup are passed in, so that the rules can be tested with no solver installed.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static final record	SolverResolver.Resolution	The result of resolve(java.util.Properties, java.lang.String, java.lang.String, java.lang.String, java.lang.String, java.util.function.Function<java.lang.String, java.lang.Class<?>>): the adapter class (and its name, for messages), and the executable, or the command array if the properties give one

Method Summary

Modifier and Type	Method	Description
static String	configuredExecutable(Properties props, String solvername, String platform)	The executable the properties configure for the solver: .exec.<platform>, then .exec; null if neither is given, or it is blank.
static Class<?>	forName(String name)	Class.forName(String), or null if there is no such class: the production class lookup
static SolverResolver.Resolution	resolve(Properties props, String solvername, String executable, String platform, String solverDir, Function<String,Class<?>> classLookup)	Resolves the solver: the adapter: a .adapter.<platform> property, then .adapter (an error if the class it names is not found); else the class Solver_<name> (with - and .

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Details

forName

public static Class<?> forName(String name)

Class.forName(String), or null if there is no such class: the production class lookup

resolve

public static SolverResolver.Resolution resolve(Properties props,
 String solvername,
 String executable,
 String platform,
 String solverDir,
 Function<String,Class<?>> classLookup)
                                         throws ISolver.CreationException

Resolves the solver:

1. the adapter: a .adapter.<platform> property, then .adapter (an error if the class it names is not found); else the class Solver_<name> (with - and . in the name as _); else, for a z3 name, Solver_z3_recent; else Solver_smt;
2. a .command property, split at commas, if given and not blank;
3. the executable: the one given, else .exec.<platform>, then .exec; resolved by SMT.resolveExecutablePath(java.lang.String, java.lang.String), and put in the command in place of %exec%, or as its first element if there is no %exec%; with neither a command nor an executable, the solver name itself, resolved the same way.

The test pseudo-solver is Solver_test, with the executable as given.

Parameters:

props - the merged properties, or null for none

solvername - the name of the solver

executable - the caller's executable, or null to resolve one

platform - the platform name, as SMT.platformName() gives it

solverDir - the solver directory (SMT_SOLVER_DIR), or null

classLookup - the class with a given name, or null if there is none

Throws:

ISolver.CreationException - if a configured adapter class is not found or the .command property is only commas

configuredExecutable

public static String configuredExecutable(Properties props,
 String solvername,
 String platform)

The executable the properties configure for the solver: .exec.<platform>, then .exec; null if neither is given, or it is blank. A platform-specific override is for solvers whose executable filename itself differs by platform (e.g. z3-4.3 ships as z3-4.3.1 on Unix/macOS but z3-4.3.2 on Windows). Not resolved to a path.