Package org.sosy_lab.java_smt

Class SolverContextFactory

java.lang.Object

org.sosy_lab.java_smt.SolverContextFactory

public class SolverContextFactory
extends Object

Factory class for loading and generating solver contexts. Generates a SolverContext corresponding to the chosen solver.

Main entry point for JavaSMT.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	SolverContextFactory.Solvers

Constructor Summary

Constructors

Constructor	Description
SolverContextFactory(Configuration pConfig, LogManager pLogger, ShutdownNotifier pShutdownNotifier)	This constructor uses the default JavaSMT loader for accessing native libraries.
SolverContextFactory(Configuration pConfig, LogManager pLogger, ShutdownNotifier pShutdownNotifier, Consumer<String> pLoader)	This constructor instantiates a factory for building solver contexts for a configured SMT solver (via the parameter pConfig).

Method Summary

Modifier and Type	Method	Description
static SolverContext	createSolverContext(Configuration config, LogManager logger, ShutdownNotifier shutdownNotifier)	Shortcut for getting a SolverContext, the solver is selected using the configuration config.
static SolverContext	createSolverContext(Configuration config, LogManager logger, ShutdownNotifier shutdownNotifier, SolverContextFactory.Solvers solver)	Shortcut for getting a SolverContext, the solver is selected using an argument.
static SolverContext	createSolverContext(Configuration config, LogManager logger, ShutdownNotifier shutdownNotifier, SolverContextFactory.Solvers solver, Consumer<String> loader)	This is the most explicit method for getting a SolverContext, the solver, the logger, the shutdownNotifier, and the libraryLoader are provided as parameters by the caller.
static SolverContext	createSolverContext(SolverContextFactory.Solvers solver)	Minimalistic shortcut for creating a solver context.
SolverContext	generateContext()	Create new context with solver chosen according to the supplied configuration.
SolverContext	generateContext(SolverContextFactory.Solvers solverToCreate)	Create new context with solver name supplied.

Methods inherited from class java.lang.Object

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

Constructor Detail

SolverContextFactory

public SolverContextFactory(Configuration pConfig,
                            LogManager pLogger,
                            ShutdownNotifier pShutdownNotifier)
                     throws InvalidConfigurationException

This constructor uses the default JavaSMT loader for accessing native libraries.

Throws:

InvalidConfigurationException

See Also:

SolverContextFactory(Configuration, LogManager, ShutdownNotifier, Consumer)

SolverContextFactory

public SolverContextFactory(Configuration pConfig,
                            LogManager pLogger,
                            ShutdownNotifier pShutdownNotifier,
                            Consumer<String> pLoader)
                     throws InvalidConfigurationException

This constructor instantiates a factory for building solver contexts for a configured SMT solver (via the parameter pConfig). Each created context is independent of other contexts and uses its own environment for building formulas and querying the solver.

Parameters:

pConfig - The configuration to be used when instantiating JavaSMT and the solvers. By default, the configuration specifies the solver to use via the option solver.solver=.... This option can be overridden when calling the method generateContext(Solvers).

pLogger - The processing of log messages from SMT solvers (or their bindings) is handled via this LogManager.

pShutdownNotifier - This central instance allows to request the termination of all operations in the created solver. Please note that the solver can decide on its own to accept the shutdown request and terminate its operation afterwards. We do not forcefully terminate any solver query eagerly. In general, a solver is of good nature, and maturely developed, and terminates accordingly.

pLoader - The loading mechanism (loading method) in this class can be injected by the user and, e.g., can be used to search for the library binaries in more directories. This makes the loading process for native solvers like Boolector, CVC4, MathSAT, Z3 more flexible. For Java-based libraries (solvers like SMTInterpol or Princess, and also other dependences), this class is irrelevant and not accessed.

Throws:

InvalidConfigurationException

Method Detail

generateContext

public SolverContext generateContext()
                              throws InvalidConfigurationException

Create new context with solver chosen according to the supplied configuration.

Throws:

InvalidConfigurationException

generateContext

public SolverContext generateContext(SolverContextFactory.Solvers solverToCreate)
                              throws InvalidConfigurationException

Create new context with solver name supplied.

Throws:

InvalidConfigurationException

See Also:

generateContext()

createSolverContext

public static SolverContext createSolverContext(Configuration config,
                                                LogManager logger,
                                                ShutdownNotifier shutdownNotifier)
                                         throws InvalidConfigurationException

Shortcut for getting a SolverContext, the solver is selected using the configuration config.

Throws:

InvalidConfigurationException

createSolverContext

public static SolverContext createSolverContext(Configuration config,
                                                LogManager logger,
                                                ShutdownNotifier shutdownNotifier,
                                                SolverContextFactory.Solvers solver)
                                         throws InvalidConfigurationException

Shortcut for getting a SolverContext, the solver is selected using an argument.

See SolverContextFactory(Configuration, LogManager, ShutdownNotifier, Consumer) for documentation of accepted parameters.

Throws:

InvalidConfigurationException

createSolverContext

public static SolverContext createSolverContext(Configuration config,
                                                LogManager logger,
                                                ShutdownNotifier shutdownNotifier,
                                                SolverContextFactory.Solvers solver,
                                                Consumer<String> loader)
                                         throws InvalidConfigurationException

This is the most explicit method for getting a SolverContext, the solver, the logger, the shutdownNotifier, and the libraryLoader are provided as parameters by the caller.

See SolverContextFactory(Configuration, LogManager, ShutdownNotifier, Consumer) for documentation of accepted parameters.

Throws:

InvalidConfigurationException

createSolverContext

public static SolverContext createSolverContext(SolverContextFactory.Solvers solver)
                                         throws InvalidConfigurationException

Minimalistic shortcut for creating a solver context. Empty default configuration, no logging, and no shutdown notifier.

Parameters:

solver - Solver to initialize

Throws:

InvalidConfigurationException