From b1bbb821c0e5a3f721de211826dab19c7d9dca4f Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Fri, 5 Apr 2019 03:32:48 -0400 Subject: Implement containment circularity avoidance #20 --- .../.VampireAnalyzerConfiguration.xtendbin | Bin 2399 -> 2691 bytes .../vampire/reasoner/.VampireSolver.xtendbin | Bin 5892 -> 5892 bytes .../reasoner/VampireSolverConfiguration.java | 3 ++ .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18129 -> 18157 bytes ...c2VampireLanguageMapper_ConstantMapper.xtendbin | Bin 3164 -> 3164 bytes ...ampireLanguageMapper_ContainmentMapper.xtendbin | Bin 9493 -> 10551 bytes ...c2VampireLanguageMapper_RelationMapper.xtendbin | Bin 8210 -> 8209 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 9828 -> 9839 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 12892 -> 13092 bytes ...Logic2VampireLanguageMapper_TypeMapper.xtendbin | Bin 10704 -> 10705 bytes .../reasoner/builder/.VampireHandler.xtendbin | Bin 4908 -> 4908 bytes .../builder/Logic2VampireLanguageMapper.java | 2 +- ...ic2VampireLanguageMapper_ContainmentMapper.java | 57 ++++++++++++++++++++- .../Logic2VampireLanguageMapper_ScopeMapper.java | 8 +-- .../Logic2VampireLanguageMapper_Support.java | 8 +++ 15 files changed, 71 insertions(+), 7 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill') diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin index b5e03979..7394b24e 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireAnalyzerConfiguration.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin index 0714f36d..d328dcf2 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/.VampireSolver.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java index 1f6b3d42..ac55ebd7 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireSolverConfiguration.java @@ -4,4 +4,7 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; @SuppressWarnings("all") public class VampireSolverConfiguration extends LogicSolverConfiguration { + public int contCycleLevel = 0; + + public boolean uniquenessDuplicates = false; } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 2cc60591..968a2df8 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin index 01b0a351..48756fcc 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ConstantMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin index cf049bd5..44b06208 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ContainmentMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin index 7bc04e7b..4cab8309 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_RelationMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin index a97c7186..ccddb430 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_ScopeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin index a473c586..a069a62f 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_Support.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin index 4e7796fe..46cd58fb 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper_TypeMapper.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 84d6c63a..1b5e4d0b 100644 Binary files a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin and b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin differ diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java index 36a727b2..f04bd7dc 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.java @@ -123,7 +123,7 @@ public class Logic2VampireLanguageMapper { this.relationMapper.transformRelation(it, trace); }; problem.getRelations().forEach(_function_3); - this.containmentMapper.transformContainment(problem.getContainmentHierarchies(), trace); + this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); trace.constantDefinitions = this.collectConstantDefinitions(problem); final Consumer _function_4 = (ConstantDefinition it) -> { this.constantMapper.transformConstantDefinitionSpecification(it, trace); diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java index 7bc70e9d..4cdc7e6a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ContainmentMapper.java @@ -1,5 +1,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; @@ -16,6 +17,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; import com.google.common.base.Objects; +import com.google.common.collect.Iterables; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; @@ -52,7 +54,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { this.base = base; } - public void transformContainment(final List hierarchies, final Logic2VampireLanguageMapperTrace trace) { + public void transformContainment(final VampireSolverConfiguration config, final List hierarchies, final Logic2VampireLanguageMapperTrace trace) { final ContainmentHierarchy hierarchy = hierarchies.get(0); final EList containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); final EList relationsList = hierarchy.getContainmentRelations(); @@ -135,7 +137,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { } VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); final Procedure1 _function_4 = (VLSFofFormula it) -> { - it.setName(this.support.toIDMultiple("noDupCont", rel.getConstant().toString())); + it.setName(this.support.toIDMultiple("containment_noDup", rel.getConstant().toString())); it.setFofRole("axiom"); VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); final Procedure1 _function_5 = (VLSExistentialQuantifier it_1) -> { @@ -219,6 +221,57 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { _formulas_1.add(relFormula); } } + final ArrayList variables = CollectionLiterals.newArrayList(); + final ArrayList disjunctionList = CollectionLiterals.newArrayList(); + final ArrayList conjunctionList = CollectionLiterals.newArrayList(); + for (int i = 1; (i <= config.contCycleLevel); i++) { + { + final int ind = i; + VLSVariable _createVLSVariable_3 = this.factory.createVLSVariable(); + final Procedure1 _function_4 = (VLSVariable it) -> { + String _string = Integer.toString(ind); + String _plus = ("V" + _string); + it.setName(_plus); + }; + VLSVariable _doubleArrow = ObjectExtensions.operator_doubleArrow(_createVLSVariable_3, _function_4); + variables.add(_doubleArrow); + for (int j = 0; (j < i); j++) { + { + for (final Relation l_2 : relationsList) { + { + final VLSFunction rel = this.support.duplicate(CollectionsUtil.lookup(((RelationDeclaration) l_2), trace.rel2Predicate), CollectionLiterals.newArrayList(variables.get(j), variables.get(((j + 1) % i)))); + disjunctionList.add(rel); + } + } + conjunctionList.add(this.support.unfoldOr(disjunctionList)); + disjunctionList.clear(); + } + } + VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); + final Procedure1 _function_5 = (VLSFofFormula it) -> { + it.setName(this.support.toIDMultiple("containment_noCycle", Integer.toString(ind))); + it.setFofRole("axiom"); + VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); + final Procedure1 _function_6 = (VLSUnaryNegation it_1) -> { + VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); + final Procedure1 _function_7 = (VLSExistentialQuantifier it_2) -> { + EList _variables = it_2.getVariables(); + List _duplicate = this.support.duplicate(variables); + Iterables.addAll(_variables, _duplicate); + it_2.setOperand(this.support.unfoldAnd(conjunctionList)); + }; + VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); + it_1.setOperand(_doubleArrow_1); + }; + VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.operator_doubleArrow(_createVLSUnaryNegation, _function_6); + it.setFofFormula(_doubleArrow_1); + }; + final VLSFofFormula contCycleForm = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula_1, _function_5); + EList _formulas_1 = trace.specification.getFormulas(); + _formulas_1.add(contCycleForm); + conjunctionList.clear(); + } + } } protected VLSTerm makeUnique(final List list) { diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java index 83543c92..f5d35b28 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_ScopeMapper.java @@ -1,5 +1,6 @@ package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; @@ -13,7 +14,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; -import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; import java.util.ArrayList; @@ -47,7 +47,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { this.base = base; } - public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { + public void _transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { final int ABSOLUTE_MIN = 0; final int ABSOLUTE_MAX = Integer.MAX_VALUE; final int GLOBAL_MIN = config.typeScopes.minNewElements; @@ -105,7 +105,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { } } } - final boolean DUPLICATES = false; + final boolean DUPLICATES = config.uniquenessDuplicates; final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; int ind = 1; if ((numInst != 0)) { @@ -246,7 +246,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { _formulas.add(cstDec); } - public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { + public void transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { _transformScope(config, trace); return; } diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java index 513618a9..89633ca1 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java @@ -129,6 +129,14 @@ public class Logic2VampireLanguageMapper_Support { return ObjectExtensions.operator_doubleArrow(_createVLSFunction, _function); } + protected List duplicate(final List vars) { + ArrayList newList = CollectionLiterals.newArrayList(); + for (final VLSVariable v : vars) { + newList.add(this.duplicate(v)); + } + return newList; + } + protected VLSConstant toConstant(final VLSFunctionAsTerm term) { VLSConstant _createVLSConstant = this.factory.createVLSConstant(); final Procedure1 _function = (VLSConstant it) -> { -- cgit v1.2.3-70-g09d2