class ContextualBlock
extends java.lang.Object
ContextualBlock
is used to integrate comments to translations of AbstractSMTtranslator. A concrete instance of ContexualBlock
describes either a block of semantical connected assumptions or a block of semantical connected predicates.
How the assumptions or predicates are connected are described by the constants declared within this class.
Concrete instances of AbstractSMTTranslator which implements the function
buildCompleteText(StringBuffer formula,
ArrayList assumptions,
ArrayList assumptionBlocks,
ArrayList> functions,
ArrayList> predicates,
ArrayList predicateBlocks,
ArrayList types, SortHierarchy sortHierarchy)
assumptionBlocks
and predicateBlocks
to find out, at which position in the containers assumptions
and predicates
blocks begin and end.Modifier and Type | Field and Description |
---|---|
static int |
ASSUMPTION_DISTINCT |
static int |
ASSUMPTION_DUMMY_IMPLEMENTATION
The block contains assumptions for dummy variables.
|
static int |
ASSUMPTION_FUNCTION_DEFINTION
The block contains assumptions for function definitions.
|
static int |
ASSUMPTION_INTEGER |
static int |
ASSUMPTION_MULTIPLICATION |
static int |
ASSUMPTION_SORT_PREDICATES
The block contains assumptions for sorts which are expressed by predicates.
|
static int |
ASSUMPTION_SORTS_NOT_EMPTY |
static int |
ASSUMPTION_TACLET_TRANSLATION |
static int |
ASSUMPTION_TYPE_HIERARCHY
The block contains assumptions for the type hierarchy.
|
private int |
End |
static int |
PREDICATE_FORMULA
The block contains predicates which appear in the formula.
|
static int |
PREDICATE_TYPE
The block contains predicates which describe types.
|
private int |
Start |
private int |
Type |
Constructor and Description |
---|
ContextualBlock(int start,
int end,
int type) |
Modifier and Type | Method and Description |
---|---|
int |
getEnd() |
int |
getStart() |
int |
getType()
Returns the type of the block, that can be
- ASSUMPTION_FUNCTION_DEFINTION - ASSUMPTION_TYPE_HIERARCHY - ASSUMPTION_SORT_PREDICATES - ASSUMPTION_DUMMY_IMPLEMENTATION3 - PREDICATE_FORMULA - PREDICATE_TYPE |
public static final int ASSUMPTION_FUNCTION_DEFINTION
public static final int ASSUMPTION_TYPE_HIERARCHY
public static final int ASSUMPTION_SORT_PREDICATES
public static final int ASSUMPTION_DUMMY_IMPLEMENTATION
public static final int ASSUMPTION_TACLET_TRANSLATION
public static final int ASSUMPTION_DISTINCT
public static final int ASSUMPTION_INTEGER
public static final int ASSUMPTION_MULTIPLICATION
public static final int ASSUMPTION_SORTS_NOT_EMPTY
public static final int PREDICATE_FORMULA
public static final int PREDICATE_TYPE
private int Start
private int End
private int Type
public ContextualBlock(int start, int end, int type)
start
- first index of the blockend
- last index of the blocktype
- type of the blockpublic int getStart()
public int getEnd()
public int getType()