public class ModelExtractor extends Object implements PipeListener<SolverCommunication>
Modifier and Type | Field and Description |
---|---|
static int |
ARRAYFIELDS |
private List<SMTFunction> |
bools |
private int |
currentQuery |
static int |
DEFAULT |
private List<SMTFunction> |
fields |
static int |
FINISHED |
private List<SMTFunction> |
heaps |
private int |
intBound |
private List<SMTFunction> |
ints |
private List<SMTFunction> |
locsets |
private Model |
model |
private List<SMTFunction> |
objects |
private Map<String,Sort> |
objectSorts |
private Map<String,SMTSort> |
objFunctions |
private List<Query> |
queries |
static int |
SEQ |
private List<SMTFunction> |
seqs |
private int |
state |
private ProblemTypeInformation |
types |
static int |
TYPES |
static int |
WORKING |
Constructor and Description |
---|
ModelExtractor() |
public static final int DEFAULT
public static final int TYPES
public static final int WORKING
public static final int ARRAYFIELDS
public static final int FINISHED
public static final int SEQ
private Model model
private int state
private List<SMTFunction> heaps
private List<SMTFunction> objects
private List<SMTFunction> fields
private List<SMTFunction> locsets
private List<SMTFunction> ints
private List<SMTFunction> bools
private List<SMTFunction> seqs
private ProblemTypeInformation types
private int currentQuery
private int intBound
public void addFunction(SMTFunction f)
public Model getModel()
private void generateTypeQueries()
private void generateBasicQueries()
private void generateArrayQueries()
private void generateSeqQueries()
public int getIntBound()
public void setIntBound(int intBound)
public ProblemTypeInformation getTypes()
public void setTypes(ProblemTypeInformation types)
public int getState()
private void finishBasicQueries(Pipe<SolverCommunication> pipe)
private void processBasicQueries()
public void messageIncoming(Pipe<SolverCommunication> pipe, String message, int type)
PipeListener
messageIncoming
in interface PipeListener<SolverCommunication>
private void finishTypesQueries(Pipe<SolverCommunication> pipe)
private void finishSeqQueries(Pipe<SolverCommunication> pipe)
private void startBasicQueries(Pipe<SolverCommunication> pipe)
private void processTypesQueries()
private void finishArrayQueries(Pipe<SolverCommunication> pipe)
private void processArrayQueries()
private void processSeqQueries()
public void start(Pipe<SolverCommunication> pipe)
public boolean isWorking()
public void exceptionOccurred(Pipe<SolverCommunication> pipe, Throwable exception)
exceptionOccurred
in interface PipeListener<SolverCommunication>