From d7730cb0d684d6324622021a310d9b4a53e7531c Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 14 Mar 2019 03:45:46 -0400 Subject: Implement Containment mapping (partially) and revisit enum mapping --- .../builder/Logic2VampireLanguageMapper.xtend | 16 ++- ...c2VampireLanguageMapper_ContainmentMapper.xtend | 123 +++++++++++++++++++++ .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 25 +++-- .../Logic2VampireLanguageMapper_Support.xtend | 30 ++++- .../Logic2VampireLanguageMapper_TypeMapper.xtend | 104 +++++++++-------- 5 files changed, 233 insertions(+), 65 deletions(-) create mode 100644 Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index 1dbc0055..b7ad8f3d 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend @@ -47,6 +47,8 @@ class Logic2VampireLanguageMapper { private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support; @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ConstantMapper constantMapper = new Logic2VampireLanguageMapper_ConstantMapper( this) + @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ContainmentMapper containmentMapper = new Logic2VampireLanguageMapper_ContainmentMapper( + this) @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_RelationMapper relationMapper = new Logic2VampireLanguageMapper_RelationMapper( this) @Accessors(PUBLIC_GETTER) private val Logic2VampireLanguageMapper_ScopeMapper scopeMapper = new Logic2VampireLanguageMapper_ScopeMapper( @@ -80,24 +82,26 @@ class Logic2VampireLanguageMapper { // SCOPE MAPPER scopeMapper.transformScope(config, trace) - trace.constantDefinitions = problem.collectConstantDefinitions + // RELATION MAPPER trace.relationDefinitions = problem.collectRelationDefinitions - problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] + + // CONTAINMENT MAPPER + containmentMapper.transformContainment(problem.containmentHierarchies, trace) + // CONSTANT MAPPER // only transforms definitions + trace.constantDefinitions = problem.collectConstantDefinitions // problem.constants.filter(ConstantDefinition).forEach[this.constantMapper.transformConstant(it, trace)] problem.constants.filter(ConstantDefinition).forEach [ this.constantMapper.transformConstantDefinitionSpecification(it, trace) ] - // ////////////////// - // Transform Assertions - // ////////////////// + // ASSERTION MAPPER for (assertion : problem.assertions) { transformAssertion(assertion, trace) } - + // OUTPUT return new TracedOutput(specification, trace) } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend new file mode 100644 index 00000000..0820f47d --- /dev/null +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.xtend @@ -0,0 +1,123 @@ +package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder + +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.ContainmentHierarchy +import java.util.List +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type + +import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeReference + +class Logic2VampireLanguageMapper_ContainmentMapper { + private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE + private val Logic2VampireLanguageMapper_Support support = new Logic2VampireLanguageMapper_Support + val Logic2VampireLanguageMapper base + private val VLSVariable variable = createVLSVariable => [it.name = "A"] + + public new(Logic2VampireLanguageMapper base) { + this.base = base + } + + def public void transformContainment(List hierarchies, + Logic2VampireLanguageMapperTrace trace) { + + // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST + // TEMP + val hierarchy = hierarchies.get(0) + + val containmentListCopy = hierarchy.typesOrderedInHierarchy + val relationsList = hierarchy.containmentRelations + // STEP 1 + // Find root element + for (l : relationsList) { + var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type + containmentListCopy.remove(pointingTo) + for (c : pointingTo.subtypes) { + containmentListCopy.remove(c) + } + } + + // State that there must exist 1 and only 1 root element + val topName = containmentListCopy.get(0).lookup(trace.type2Predicate).constant.toString + val topTerm = support.duplicate(containmentListCopy.get(0).lookup(trace.type2Predicate)) + + val contTop = createVLSFofFormula => [ + it.name = support.toIDMultiple("containment_topLevel", topName) + it.fofRole = "axiom" + + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += support.duplicate(variable) + it.operand = createVLSEquivalent => [ + it.left = topTerm + it.right = createVLSEquality => [ + it.left = support.duplicate(variable) + it.right = createVLSConstant => [ + it.name = "o1" + ] + ] + ] + ] +// it.fofFormula = support.duplicate( +// topTerm, +// createVLSFunctionAsTerm => [ +// it.functor = "o1" +// ] +// ) + ] + trace.specification.formulas += contTop + + // STEP 2 + // for each edge, if the pointedTo element exists,the edge must exist also + val varA = createVLSVariable => [it.name = "A"] + val varB = createVLSVariable => [it.name = "B"] + val varList = newArrayList(varB, varA) + + for (l : relationsList) { + val relName = (l as RelationDeclaration).lookup(trace.rel2Predicate).constant.toString + val fromType = (l.parameters.get(0) as ComplexTypeReference).referred as Type + val toType = (l.parameters.get(1) as ComplexTypeReference).referred as Type + + val relFormula = createVLSFofFormula => [ + it.name = support.toIDMultiple("containment", relName) + it.fofRole = "axiom" + + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += support.duplicate(varA) + it.operand = createVLSImplies => [ + it.left = support.duplicate(toType.lookup(trace.type2Predicate), varA) + it.right = createVLSExistentialQuantifier => [ + it.variables += support.duplicate(varB) + it.operand = createVLSAnd => [ + it.left = support.duplicate(fromType.lookup(trace.type2Predicate), varB) + it.right = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), + varList) + ] + ] + + createVLSEquality => [ + it.left = support.duplicate(variable) + it.right = createVLSConstant => [ + it.name = "o1" + ] + ] + ] + ] + ] + trace.specification.formulas += relFormula + var pointingTo = (l.parameters.get(1) as ComplexTypeReference).referred as Type + containmentListCopy.remove(pointingTo) + for (c : pointingTo.subtypes) { + containmentListCopy.remove(c) + } + } + + // STEP 3 + // Ensure that an objct only has 1 parent + // STEP 4 + // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) + } +} diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend index 5c5eaff3..548deda4 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.xtend @@ -10,6 +10,8 @@ import java.util.Map import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* import java.util.HashMap +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm +import java.util.List class Logic2VampireLanguageMapper_ScopeMapper { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -24,7 +26,8 @@ class Logic2VampireLanguageMapper_ScopeMapper { def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { // TODO HANDLE ERRORS RELATED TO MAX > MIN -// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES) > MAX OBJECTS +// TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS +// TODO HANDLE // TODO NOT SPECIFIED MEANS =0 ? // 1. make a list of constants equaling the min number of specified objects val GLOBAL_MIN = config.typeScopes.minNewElements @@ -34,18 +37,22 @@ class Logic2VampireLanguageMapper_ScopeMapper { // Handling Minimum_General if (GLOBAL_MIN != 0) { - getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) // fix last param + getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) + for(i : trace.uniqueInstances){ + localInstances.add(support.duplicate(i)) + } + makeFofFormula(localInstances, trace, true, null) } // Handling Maximum_General if (GLOBAL_MAX != 0) { - getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) // fix last param - makeFofFormula(localInstances, trace, false, null) + getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) + makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) } // Handling Minimum_Specific - var i = 0 + var i = 1 var minNum = -1 var Map startPoints = new HashMap for (t : config.typeScopes.minNewElementsByType.keySet) { @@ -106,13 +113,17 @@ class Logic2VampireLanguageMapper_ScopeMapper { def protected void makeFofFormula(ArrayList list, Logic2VampireLanguageMapperTrace trace, boolean minimum, Type type) { var nm = "" - var VLSFunction tm = null + var VLSTerm tm = null if (type === null) { nm = "object" tm = support.topLevelTypeFunc } else { nm = type.lookup(trace.type2Predicate).constant.toString - tm = support.duplicate(type.lookup(trace.type2Predicate)) + tm = createVLSAnd => [ + it.left = support.duplicate(type.lookup(trace.type2Predicate)) + it.right = support.topLevelTypeFunc + ] +// tm = support.duplicate(type.lookup(trace.type2Predicate)) } val name = nm val term = tm diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend index 021cb0ea..8d00d3e7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.xtend @@ -37,11 +37,11 @@ class Logic2VampireLanguageMapper_Support { def protected VLSVariable duplicate(VLSVariable term) { return createVLSVariable => [it.name = term.name] } - + def protected VLSFunctionAsTerm duplicate(VLSFunctionAsTerm term) { return createVLSFunctionAsTerm => [it.functor = term.functor] } - + def protected VLSConstant duplicate(VLSConstant term) { return createVLSConstant => [it.name = term.name] } @@ -61,14 +61,23 @@ class Logic2VampireLanguageMapper_Support { it.terms += duplicate(v) ] } - + + def protected VLSFunction duplicate(VLSFunction term, List vars) { + return createVLSFunction => [ + it.constant = term.constant + for (v : vars) { + it.terms += duplicate(v) + } + ] + } + def protected VLSFunction duplicate(VLSFunction term, VLSFunctionAsTerm v) { return createVLSFunction => [ it.constant = term.constant it.terms += duplicate(v) ] } - + def protected VLSConstant toConstant(VLSFunctionAsTerm term) { return createVLSConstant => [ it.name = term.functor @@ -84,6 +93,13 @@ class Logic2VampireLanguageMapper_Support { ] } + def protected VLSFunction topLevelTypeFunc(VLSVariable v) { + return createVLSFunction => [ + it.constant = "object" + it.terms += duplicate(v) + ] + } + def protected VLSFunction topLevelTypeFunc(VLSFunctionAsTerm v) { return createVLSFunction => [ it.constant = "object" @@ -173,14 +189,16 @@ class Logic2VampireLanguageMapper_Support { */ // QUANTIFIERS + VARIABLES def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, - QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables, boolean isUniversal) { + QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map variables, + boolean isUniversal) { val variableMap = expression.quantifiedVariables.toInvertedMap [ v | createVLSVariable => [it.name = toIDMultiple("V", v.name)] ] val typedefs = new ArrayList for (variable : expression.quantifiedVariables) { - val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), variable.lookup(variableMap)) + val eq = duplicate((variable.range as ComplexTypeReference).referred.lookup(trace.type2Predicate), + variable.lookup(variableMap)) typedefs.add(eq) } if (isUniversal) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend index e12180fa..4c4247ce 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_TypeMapper.xtend @@ -1,12 +1,12 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder +import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDeclaration import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TypeDefinition import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage import java.util.ArrayList @@ -14,7 +14,6 @@ import java.util.Collection import java.util.List import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* -import java.util.Collections class Logic2VampireLanguageMapper_TypeMapper { private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE @@ -28,10 +27,8 @@ class Logic2VampireLanguageMapper_TypeMapper { def protected transformTypes(Collection types, Collection elements, Logic2VampireLanguageMapper mapper, Logic2VampireLanguageMapperTrace trace) { - -// val typeTrace = new Logic2VampireLanguageMapper_TypeMapperTrace_FilteredTypes -// trace.typeMapperTrace = typeTrace val VLSVariable variable = createVLSVariable => [it.name = "A"] + var globalCounter = 0 // 1. Each type (class) is a predicate with a single variable as input for (type : types) { @@ -39,94 +36,109 @@ class Logic2VampireLanguageMapper_TypeMapper { it.constant = support.toIDMultiple("t", type.name.split(" ").get(0)) it.terms += support.duplicate(variable) ] -// typeTrace.type2Predicate.put(type, typePred) trace.type2Predicate.put(type, typePred) } // 2. Map each ENUM type definition to fof formula for (type : types.filter(TypeDefinition)) { + + // Create a VLSFunction for each Enum Element val List orElems = newArrayList for (e : type.elements) { val enumElemPred = createVLSFunction => [ val splitName = e.name.split(" ") - if( splitName.length > 2) { + if (splitName.length > 2) { it.constant = support.toIDMultiple("e", splitName.get(0), splitName.get(2)) - } - else { + } else { it.constant = support.toIDMultiple("e", splitName.get(0)) } it.terms += support.duplicate(variable) ] -// typeTrace.element2Predicate.put(e, enumElemPred) trace.element2Predicate.put(e, enumElemPred) - orElems.add(enumElemPred) } + // Similar to InheritanceHierarchy for the Enum + val List possibleNots = newArrayList + val List typeDefs = newArrayList + + for (t1 : type.elements) { + for (t2 : type.elements) { + if (t1 == t2) { + val fct = support.duplicate(t2.lookup(trace.element2Predicate), variable) + possibleNots.add(fct) + } else { + val op = support.duplicate(t2.lookup(trace.element2Predicate), variable) + val negFct = createVLSUnaryNegation => [ + it.operand = op + ] + possibleNots.add(negFct) + } + } + typeDefs.add(support.unfoldAnd(possibleNots)) + possibleNots.clear + } + + // Implement Enum Inheritence Hierarchy val res = createVLSFofFormula => [ it.name = support.toIDMultiple("typeDef", type.name.split(" ").get(0)) - // below is temporary solution it.fofRole = "axiom" it.fofFormula = createVLSUniversalQuantifier => [ it.variables += support.duplicate(variable) it.operand = createVLSEquivalent => [ it.left = type.lookup(trace.type2Predicate) - it.right = support.unfoldOr(orElems) + it.right = createVLSAnd => [ + it.left = support.topLevelTypeFunc(variable) + it.right = support.unfoldOr(typeDefs) + ] +// it.right = support.unfoldOr((typeDefs)) + ] ] - ] trace.specification.formulas += res - // Create objects for the enum elements - val List enumScopeElems = newArrayList - for (var i = 0; i < type.elements.length; i++) { + for (var i = globalCounter; i < globalCounter+type.elements.length; i++) { + // Create objects for the enum elements val num = i + 1 val cstTerm = createVLSFunctionAsTerm => [ it.functor = "eo" + num ] val cst = support.toConstant(cstTerm) trace.uniqueInstances.add(cst) - val fct = support.duplicate(type.elements.get(i).lookup(trace.element2Predicate), cstTerm) - enumScopeElems.add(fct) - - //For paradox Only - for (var j = 0; j < type.elements.length; j++) { - if(j != i) { - val op = support.duplicate(type.elements.get(j).lookup(trace.element2Predicate), cstTerm) - val negFct = createVLSUnaryNegation => [ - it.operand = op + + val index = i + val enumScope = createVLSFofFormula => [ + it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0), + type.elements.get(index).name.split(" ").get(0)) + it.fofRole = "axiom" + it.fofFormula = createVLSUniversalQuantifier => [ + it.variables += support.duplicate(variable) + it.operand = createVLSEquivalent => [ + it.left = createVLSEquality => [ + it.left = support.duplicate(variable) + it.right = support.duplicate(support.toConstant(cstTerm)) + ] + it.right = support.duplicate(type.elements.get(index).lookup(trace.element2Predicate), + variable) ] - enumScopeElems.add(negFct) - } - } - //End Paradox -// enumScopeElems.add(support.topLevelTypeFunc(cstTerm)) + ] + ] + + trace.specification.formulas += enumScope + } - - - - val enumScope = createVLSFofFormula => [ - it.name = support.toIDMultiple("enumScope", type.name.split(" ").get(0)) - // below is temporary solution - it.fofRole = "axiom" - it.fofFormula = support.unfoldAnd(enumScopeElems) - ] - - trace.specification.formulas += enumScope + globalCounter+=type.elements.size } // HIERARCHY HANDLER // 3. For each non-abstract type, create an and sequence containing all typedeclaration predicates // and store in a map -// println(types.filter[!isIsAbstract]) - for (t1 : types.filter[!isIsAbstract].filter(TypeDeclaration)) { + for (t1 : types.filter[!isIsAbstract]) { for (t2 : types) { // possible improvement: check all supertypes and decide if negated or not based on negations/not negations of supertypes if (t1 == t2 || support.dfsSupertypeCheck(t1, t2)) { -// typeTrace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(typeTrace.type2Predicate))) trace.type2PossibleNot.put(t2, support.duplicate(t2.lookup(trace.type2Predicate))) } else { -// typeTrace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ trace.type2PossibleNot.put(t2, createVLSUnaryNegation => [ it.operand = support.duplicate(t2.lookup(trace.type2Predicate)) ]) -- cgit v1.2.3-54-g00ecf