public abstract class AbstractSolverSocket
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
protected static int |
FINISH
Indicates that the solver already sent a sat/unsat/unknown result.
|
protected static int |
WAIT_FOR_DETAILS
Indicates that the socket waits for more details (a model or a proof).
|
protected static int |
WAIT_FOR_MODEL
Indicates that the socket waits for a model to be produced by the solver.
|
protected static int |
WAIT_FOR_QUERY
Indicates that the socket waits for the result to a query (used by CE generator).
|
protected static int |
WAIT_FOR_RESULT
Indicates that the solver has not yet sent a sat/unsat/unknown result.
|
Modifier | Constructor and Description |
---|---|
protected |
AbstractSolverSocket(java.lang.String name,
ModelExtractor query)
Creates a new solver socket with given solver name and ModelExtractor.
|
Modifier and Type | Method and Description |
---|---|
static AbstractSolverSocket |
createSocket(SolverType type,
ModelExtractor query)
Creates a new solver socket that can handle the communication for the given solver type.
|
protected java.lang.String |
getName() |
ModelExtractor |
getQuery() |
abstract void |
messageIncoming(Pipe pipe,
java.lang.String msg)
Invoked when the solver has sent a new message to its stdout or stderr.
|
void |
setQuery(ModelExtractor query) |
protected static final int WAIT_FOR_RESULT
protected static final int WAIT_FOR_DETAILS
protected static final int WAIT_FOR_QUERY
protected static final int WAIT_FOR_MODEL
protected static final int FINISH
protected AbstractSolverSocket(@Nonnull java.lang.String name, ModelExtractor query)
name
- the name of the solver in usequery
- the ModelExtractor used to extract a counterexamplepublic ModelExtractor getQuery()
public void setQuery(ModelExtractor query)
protected java.lang.String getName()
public abstract void messageIncoming(@Nonnull Pipe pipe, @Nonnull java.lang.String msg) throws java.io.IOException
pipe
- the Pipe that received the messagemsg
- the message as Stringjava.io.IOException
- if an I/O error occurspublic static AbstractSolverSocket createSocket(@Nonnull SolverType type, ModelExtractor query)
type
- the SolverType to create the socket forquery
- the ModelExtractor that can be used to extract a counterexample (for non-CE
solvers this can be null)Copyright © 2003-2019 The KeY-Project.