Package org.sosy_lab.java_smt.delegate.trace

Class TraceSolverContext

java.lang.Object

org.sosy_lab.java_smt.delegate.trace.TraceSolverContext

All Implemented Interfaces:

AutoCloseable, SolverContext

public class TraceSolverContext
extends Object
implements SolverContext

Nested Class Summary

Nested classes/interfaces inherited from interface org.sosy_lab.java_smt.api.SolverContext

SolverContext.ProverOptions

Constructor Summary

Constructors

Constructor	Description
TraceSolverContext(SolverContextFactory.Solvers pSolver, Configuration config, SolverContext pDelegate, LogManager pLogManager)

Method Summary

Modifier and Type	Method	Description
void	close()	Close the solver context.
FormulaManager	getFormulaManager()	Get the formula manager, which is used for formula manipulation.
SolverContextFactory.Solvers	getSolverName()	Get solver name (MATHSAT5/Z3/etc...).
String	getVersion()	Get version information out of the solver.
OptimizationProverEnvironment	newOptimizationProverEnvironment(SolverContext.ProverOptions... options)	Create a fresh new OptimizationProverEnvironment which encapsulates an assertion stack and allows solving optimization queries.
ProverEnvironment	newProverEnvironment(SolverContext.ProverOptions... options)	Create a fresh new ProverEnvironment which encapsulates an assertion stack and can be used to check formulas for unsatisfiability.
InterpolatingProverEnvironment<?>	newProverEnvironmentWithInterpolation(SolverContext.ProverOptions... options)	Create a fresh new InterpolatingProverEnvironment which encapsulates an assertion stack and allows generating and retrieve interpolants for unsatisfiable formulas.

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.sosy_lab.java_smt.api.SolverContext

getStatistics

Constructor Details

TraceSolverContext

public TraceSolverContext(SolverContextFactory.Solvers pSolver,
 Configuration config,
 SolverContext pDelegate,
 LogManager pLogManager)
                   throws InvalidConfigurationException

Throws:

InvalidConfigurationException

Method Details

getFormulaManager

public FormulaManager getFormulaManager()

Description copied from interface: SolverContext

Get the formula manager, which is used for formula manipulation.

Specified by:

getFormulaManager in interface SolverContext

newProverEnvironment

public ProverEnvironment newProverEnvironment(SolverContext.ProverOptions... options)

Description copied from interface: SolverContext

Create a fresh new ProverEnvironment which encapsulates an assertion stack and can be used to check formulas for unsatisfiability.

Specified by:

newProverEnvironment in interface SolverContext

Parameters:

options - Options specified for the prover environment. All the options specified in SolverContext.ProverOptions are turned off by default.

newProverEnvironmentWithInterpolation

public InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation(SolverContext.ProverOptions... options)

Description copied from interface: SolverContext

Create a fresh new InterpolatingProverEnvironment which encapsulates an assertion stack and allows generating and retrieve interpolants for unsatisfiable formulas. If the SMT solver is able to handle satisfiability tests with assumptions please consider implementing the InterpolatingProverEnvironment interface, and return an Object of this type here.

Specified by:

newProverEnvironmentWithInterpolation in interface SolverContext

Parameters:

options - Options specified for the prover environment. All the options specified in SolverContext.ProverOptions are turned off by default.

newOptimizationProverEnvironment

public OptimizationProverEnvironment newOptimizationProverEnvironment(SolverContext.ProverOptions... options)

Description copied from interface: SolverContext

Create a fresh new OptimizationProverEnvironment which encapsulates an assertion stack and allows solving optimization queries.

Specified by:

newOptimizationProverEnvironment in interface SolverContext

Parameters:

options - Options specified for the prover environment. All the options specified in SolverContext.ProverOptions are turned off by default.

getVersion

public String getVersion()

Description copied from interface: SolverContext

Get version information out of the solver.

In most cases, the version contains the name of the solver followed by some numbers and additional info about the version, e.g., "SMTInterpol 2.5-12-g3d15a15c".

Specified by:

getVersion in interface SolverContext

getSolverName

public SolverContextFactory.Solvers getSolverName()

Description copied from interface: SolverContext

Get solver name (MATHSAT5/Z3/etc...).

This is an uppercase String matching the enum identifier from SolverContextFactory.Solvers

Specified by:

getSolverName in interface SolverContext

close

public void close()

Description copied from interface: SolverContext

Close the solver context.

After calling this method, further access to any object that had been returned from this context is not wanted, i.e., it depends on the solver. Java-based solvers might wait for the next garbage collection with any cleanup operation. Native solvers might even reference invalid memory and cause segmentation faults.

Necessary for the solvers implemented in native code, frees the associated memory.

Specified by:

close in interface AutoCloseable

Specified by:

close in interface SolverContext