Package org.smtlib

Class SolverCapabilities

java.lang.Object

org.smtlib.SolverCapabilities

public final class SolverCapabilities
extends Object

Whether a solver supports a capability, as recorded per solver name in jsmtlib.properties (#157): org.smtlib.solver_<name>.capabilities=strings,-proofs,... -- a name records a supported capability, a -name an unsupported one. A capability the solver's entry does not mention (or every capability, if it has no entry) is taken from its family's entry, the family being the name before the first -<digit> (z3-4.12.6 uses z3). A capability neither records is SolverCapabilities.Support.UNKNOWN.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static enum	SolverCapabilities.Capability	The capabilities that can be queried; SolverCapabilities.Capability.token is the name used in the properties
static enum	SolverCapabilities.Support	The answer to a query; UNKNOWN means the solver's entry does not record the capability

Field Summary

Fields

Modifier and Type	Field	Description
static final String	PROPS_CAPABILITIES_SUFFIX	The suffix of the property that lists a solver's capabilities

Method Summary

Modifier and Type	Method	Description
static String	family(String solvername)	The family name: the solver name before the first '-' followed by a digit; null if there is none
static SolverCapabilities.Support	supports(String solvername, String capability)	As supports(String, Capability), with the capability given by its token or enum name
static SolverCapabilities.Support	supports(String solvername, SolverCapabilities.Capability capability)	Whether the solver supports the capability, according to the merged jsmtlib.properties
static SolverCapabilities.Support	supports(Properties props, String solvername, SolverCapabilities.Capability capability)	Whether the solver supports the capability, according to the given properties

Methods inherited from class java.lang.Object

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

Field Details

PROPS_CAPABILITIES_SUFFIX

public static final String PROPS_CAPABILITIES_SUFFIX

The suffix of the property that lists a solver's capabilities

See Also:

• Constant Field Values

Method Details

supports

public static SolverCapabilities.Support supports(String solvername,
 SolverCapabilities.Capability capability)

Whether the solver supports the capability, according to the merged jsmtlib.properties

Throws:

IllegalArgumentException - if the solver's entry has an unknown or contradictory token

supports

public static SolverCapabilities.Support supports(String solvername,
 String capability)

As supports(String, Capability), with the capability given by its token or enum name

Throws:

IllegalArgumentException - if there is no such capability

supports

public static SolverCapabilities.Support supports(Properties props,
 String solvername,
 SolverCapabilities.Capability capability)

Whether the solver supports the capability, according to the given properties

Throws:

IllegalArgumentException - if the solver's entry has an unknown or contradictory token

family

public static String family(String solvername)

The family name: the solver name before the first '-' followed by a digit; null if there is none