diff options
Diffstat (limited to 'rba.tool.editor/src/rba/tool/editor/generator/z3/GeneratorConstants.java')
-rw-r--r-- | rba.tool.editor/src/rba/tool/editor/generator/z3/GeneratorConstants.java | 320 |
1 files changed, 320 insertions, 0 deletions
diff --git a/rba.tool.editor/src/rba/tool/editor/generator/z3/GeneratorConstants.java b/rba.tool.editor/src/rba/tool/editor/generator/z3/GeneratorConstants.java new file mode 100644 index 0000000..7ca3b74 --- /dev/null +++ b/rba.tool.editor/src/rba/tool/editor/generator/z3/GeneratorConstants.java @@ -0,0 +1,320 @@ +package rba.tool.editor.generator.z3; + +interface GeneratorConstants { + + static final String CMT_AREA_LIST = "// Area definition"; + + static final String CMT_AREA_VISIBILITY_LABEL_LIST = "// Visibility-constrained labeling"; + + static final String CMT_AREA_ZORDER_LABEL_LIST = "// Constraint expression labeling"; + + static final String CMT_CONTENT_STATE_LIST = "// Content definition"; + + static final String CMT_CONTENT_STATE_LABEL_LIST = "// Labeling Priority Constraint Expressions"; + + static final String CMT_CONTENT_STATE_PRIORITY_COMMENT_CONNECTOR = "Priority conditional expression"; + + static final String CMT_CONTENT_MULTI_START = "/**"; + + static final String CMT_CONTENT_MULTI_END = " */"; + + static final String CMT_CONTENT_IMPLIES_METHOD1 = " * Contradiction verification of implication partial constraints"; + + static final String CMT_CONTENT_IMPLIES_METHOD2 = " * %s == TRUE holds"; + + static final String CMT_CONTENT_IMPLIES_METHOD3 = " * target name : "; + + static final String CMT_CONTENT_IMPLIES_METHOD4 = " * expression text : "; + + static final String CMT_NAME_CLOSE = "]"; + + static final String CMT_NAME_OPEN = "["; + + static final String EX_NON = "non"; + + static final String EX_STD = "std"; + + static final String EX_MAX = "max"; + + static final String EX_MIN = "min"; + + static final String FUNC_ALLO_LIST = "createAlloList"; + + static final String FUNC_ALLO_VIS_CONSTR = "createAlloVisConstrList"; + + static final String FUNC_ALLO_VIS_CONSTR_LBL = "createAlloVisConstrLbl"; + + static final String FUNC_AREA_LIST = "createAreaList"; + + static final String FUNC_AREA_ZORDR_CONSTR = "createAreaZorderConstrList"; + + static final String FUNC_AREA_ZORDR_CONSTR_LBL = "createAreaZorderConstrLbl"; + + static final String FUNC_CST_LIST = "createContentList"; + + static final String FUNC_CST_CONSTR = "createConstrList"; + + static final String FUNC_CST_CONSTR_LBL = "createConstrLabelList"; + + static final String EX_CTX_MK_EQ = "ctx.mkEq"; + + static final String EX_CTX_MK_GT = "ctx.mkGt"; + + static final String EX_CTX_MK_LT = "ctx.mkLt"; + + static final String EX_CTX_MK_AND = "ctx.mkAnd"; + + static final String EX_CTX_MK_ADD = "ctx.mkAdd"; + + static final String EX_CTX_MK_INT = "ctx.mkInt"; + + static final String EX_CTX_MK_OR = "ctx.mkOr"; + + static final String EX_CTX_MK_XOR = "ctx.mkXor"; + + static final String EX_CTX_MK_NOT = "ctx.mkNot"; + + static final String EX_CTX_MK_IMPLIES = "ctx.mkImplies"; + + static final String EX_CTX_MK_GE = "ctx.mkGe"; + + static final String EX_CTX_MK_LE = "ctx.mkLe"; + + static final String EX_CTX_MK_SELECT = "ctx.mkSelect"; + + static final String EX_CTX_MK_STORE = "ctx.mkStore"; + + static final String EX_CTX_MK_EXISTS = "ctx.mkExists"; + + static final String EX_CTX_MK_FORALL = "ctx.mkForall"; + + static final String EX_CTX_MK_SYMBOL = "ctx.mkSymbol"; + + static final String EX_CTX_MK_ITE = "ctx.mkITE"; + + static final String EX_CTX_MK_TRUE = "ctx.mkTrue()"; + + static final String EX_CTX_MK_FALSE = "ctx.mkFalse()"; + + static final String EX_INT_EXPR = "(IntExpr) "; + + static final String EX_BOOL_EXPR = "(BoolExpr) "; + + static final String EX_ARITH_EXPR = "(ArithExpr) "; + + static final String EX_ARRAY_EXPR_CATS = "(ArrayExpr) "; + + static final String EX_CTX_MK_BOOL_CONST = "ctx.mkBoolConst"; + + static final String EX_CTX_MK_INT_CONST = "ctx.mkIntConst"; + + static final String EX_CTX_MK_ARRAY_CONST = "ctx.mkArrayConst"; + + static final String AREA_LIST_NAME = "areaList"; + + static final String CONSTR_LIST_NAME = "constrList"; + + static final String CONSTR_LABEL_LIST_NAME = "constrLabelList"; + + static final String CONTENT_LIST_NAME = "contentList"; + + static final String CONTENT_LIST_ADD = "contentList.add"; + + static final String CONSTR_LIST_ADD = "constrList.add"; + + static final String AREA_LIST_ADD = "areaList.add"; + + static final String CONSTR_LABEL_LIST_ADD = "constrLabelList.add"; + + static final String VISIBILITY = " Visibility : "; + + static final String ZORDER = " Zorder : "; + + static final String GET = ".get"; + + static final String CONST_ADDED_VALUE = "10"; + + static final String STR_QUOTE = "\""; + + static final String _4SPACES = " "; + + static final String _8SPACES = " "; + + static final String OPEN = "("; + + static final String CLOSE = ")"; + + static final String NAME_SEPARATOR = "_"; + + static final String COMMA = ", "; + + static final String DOT = "."; + + static final String NULL_STRING = "null"; + + static final String SL_COMMENT = "//"; + + static final String NL = "\r\n"; + + static final String END = ";"; + + static final String NUMBER = "#"; + + static final String NUMBER_ZERO = "#0:"; + + static final String VARIABLE_CMT = "// Variable "; + + static final String VARIABLE_DEFINE = "Expr[] %s = new Expr[1];"; + + static final String VARIABLE_VAR_NAME = "variable_"; + + static final String AREASET_VAR_NAME = "areaSet_"; + + static final String ZONESET_VAR_NAME = "zoneSet_"; + + static final String VIEW_CONTENTSET_VAR_NAME = "vcontentSet_"; + + static final String SOUND_CONTENTSET_VAR_NAME = "scontentSet_"; + + static final String SETOF_OP_VAR_NAME = "setOfOperator_"; + + static final String ARRAY_TOP = "[0]"; + + static final String SET_VARIABLE_VALUE = " = ctx.mkConst(ctx.mkSymbol(\"%s\"), ctx.getIntSort());"; + + static final String OP_IS_DISPLAYED = "isDisplayed"; + + static final String OP_DISPLAYING_CONTENT = "displayingContent"; + + static final String OP_ALLOCATED_CONTENT = "allocatedContent"; + + static final String OP_CONTENTS_LIST = "contentsList"; + + static final String OP_IS_HIDDEN = "isHidden"; + + static final String OP_IS_ACTIVE = "isActive"; + + static final String OP_IS_VISIBLE = "isVisible"; + + static final String OP_ALLOCATABLE = "allocatable"; + + static final String OP_CONTENT_VALUE = "contentValue"; + + static final String OP_PRE_IS_DISPLAYED = "preIsDisplayed"; + + static final String OP_PRE_DISPLAYING_CONTENT = "preDisplayingContent"; + + static final String OP_PRE_ALLOCATED_CONTENT = "preAllocatedContent"; + + static final String OP_PRE_CONTENTS_LIST = "preContentsList"; + + static final String OP_PRE_IS_HIDDEN = "preIsHidden"; + + static final String OP_PRE_IS_ACTIVE = "preIsActive"; + + static final String OP_PRE_IS_VISIBLE = "preIsVisible"; + + static final String OP_PRE_ALLOCATABLE = "preAllocatable"; + + static final String OP_PRE_CONTENT_VALUE = "preContentValue"; + + static final String OP_IS_MUTED = "isMuted"; + + static final String OP_PRE_IS_MUTED = "preIsMuted"; + + static final String OP_IS_ATTENUATED = "isAttenuated"; + + static final String OP_PRE_IS_ATTENUATED = "preIsAttenuated"; + + static final String OP_IS_SOUNDING = "isSounding"; + + static final String OP_PRE_IS_SOUNDING = "preIsSounding"; + + static final String OP_OUTPUTTING_SOUND = "outputtingSound"; + + static final String OP_PRE_OUTPUTTING_SOUND = "preOutputtingSound"; + + static final String OP_IS_OUTPUTTED = "isOutputted"; + + static final String OP_PRE_IS_OUTPUTTED = "preIsOutputted"; + + static final String OP_GET_PROPERTY = "getProperty"; + + static final String OP_PRE_GET_PROPERTY = "preGetProperty"; + + static final String OP_IS_ON = "isOn"; + + static final String OP_PRE_IS_ON = "preIsOn"; + + static final String OP_IS_DEFEATED_BY = "isDefeatedBy"; + + static final String OP_PRE_IS_DEFEATED_BY = "preIsDefeatedBy\""; + + static final String OP_DEFEATS = "defeats"; + + static final String OP_PRE_DEFEATS = "preDefeats"; + + static final String OP_IS_DISAPPEARED = "isDisappeared"; + + static final String OP_PRE_IS_DISAPPEARED = "preIsDisappeared"; + + static final String OP_IS_CANCELED = "isCanceled"; + + static final String OP_PRE_IS_CANCELED = "preIsCanceled"; + + static final String OP_HAS_BEEN_DISPLAYED = "hasBeenDisplayed"; + + static final String OP_PRE_HAS_BEEN_DISPLAYED = "preHasBeenDisplayed"; + + static final String OP_HAS_COME_EARLIER_THAN = "hasComeEarlierThan"; + + static final String OP_HAS_COME_LATER_THAN = "hasComeLaterThan"; + + static final String OP_ACTIVE_CONTENTS = "activeContents"; + + static final String OP_PRE_ACTIVE_CONTENTS = "preActiveContents"; + + static final String EMP_ARRAY_CONST = "empArrayConst"; + + static final String ALL_AREA_CONST = "allInstanceOfAreaConst"; + + static final String ALL_ZONE_CONST = "allInstanceOfZoneConst"; + + static final String ALL_SOUNDCONTENT_CONST = "allInstanceOfSoundContentConst"; + + static final String ALL_VIEWCONTENT_CONST = "allInstanceOfViewContentConst"; + + static final String ALLOCATABLE_SIZE = "allocatableSize"; + + static final String CONTENT_SIZE = "contentSize"; + + static final String ARRAY_EXPR_SORT = "ArrayExpr "; + + static final String CONSTRAINT_PREFIX = "Constraint:"; + + static final String EQUAL = " = "; + + static final String INT_TYPE = "int_type"; + + static final String BOOL_TYPE = "bool_type"; + + static final String IMPLIES_CONSTRAINT_METHOD_NAME = "doCalculateImpliesConstraint_%s()"; + + static final String IMPLIES_CONSTRAINT_METHOD = "private List<String> %s {"; + + static final String IMPLIES_CONSTRAINT_METHOD_DETAIL1 = "List<String> constraint_%s" + EQUAL; + + static final String IMPLIES_CONSTRAINT_METHOD_DETAIL2 = "if(!constraint_%s.isEmpty() && !constraint_%s.get(0).equals(\"SAT\")) {"; + + static final String IMPLIES_CONSTRAINT_METHOD_DETAIL3 = "map.put(\"#%s:%s\", constraint_%s)"; + + static final String IMPLIES_CONSTRAINT_METHOD_DETAIL4 = "if(constraint_%s.get(0).equals(\"UNSAT\")) {"; + + static final String IMPLIES_CONSTRAINT_METHOD_DETAIL5 = "return map"; + + static final String BLOCK_CLOSE = "}"; + + static final String IF_OFFLINE = "if(!onlyOnline) {"; + + static final String STORE_TEMPLATE = EX_CTX_MK_STORE + OPEN + "%s" + COMMA + EX_CTX_MK_INT + OPEN + "%s" + CLOSE + COMMA + EX_CTX_MK_TRUE + CLOSE;; +} |