public class ModelExtractor extends java.lang.Object implements PipeListener<SolverCommunication>
Modifier and Type | Field and Description |
---|---|
static int |
ARRAYFIELDS |
private java.util.List<SMTFunction> |
bools |
private int |
currentQuery |
static int |
DEFAULT |
private java.util.List<SMTFunction> |
fields |
static int |
FINISHED |
private java.util.List<SMTFunction> |
heaps |
private int |
intBound |
private java.util.List<SMTFunction> |
ints |
private java.util.List<SMTFunction> |
locsets |
private Model |
model |
private java.util.List<SMTFunction> |
objects |
private java.util.Map<java.lang.String,Sort> |
objectSorts |
private java.util.Map<java.lang.String,SMTSort> |
objFunctions |
private java.util.List<Query> |
queries |
static int |
SEQ |
private java.util.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 java.util.List<SMTFunction> heaps
private java.util.List<SMTFunction> objects
private java.util.List<SMTFunction> fields
private java.util.List<SMTFunction> locsets
private java.util.List<SMTFunction> ints
private java.util.List<SMTFunction> bools
private java.util.List<SMTFunction> seqs
private java.util.Map<java.lang.String,SMTSort> objFunctions
private ProblemTypeInformation types
private java.util.Map<java.lang.String,Sort> objectSorts
private java.util.List<Query> queries
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 java.util.List<java.lang.String> getAllIDs(int size)
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, java.lang.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, java.lang.Throwable exception)
exceptionOccurred
in interface PipeListener<SolverCommunication>