From 9a770703c17e1c758b71091fd364dcda1cefacc4 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 4 Apr 2019 19:55:10 -0400 Subject: Facilitate #31, close #36 --- .../builder/.Logic2VampireLanguageMapper.xtendbin | Bin 18128 -> 18129 bytes ...ogic2VampireLanguageMapper_ScopeMapper.xtendbin | Bin 9370 -> 9570 bytes .../.Logic2VampireLanguageMapper_Support.xtendbin | Bin 12892 -> 12892 bytes .../Logic2VampireLanguageMapper_ScopeMapper.java | 29 ++++++++++++++------- 4 files changed, 20 insertions(+), 9 deletions(-) (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca') 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 6c46d2e3..2cc60591 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_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 e5600049..1108945f 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 f9813a92..a473c586 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_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 d40b0dd2..24b46e3e 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 @@ -52,16 +52,25 @@ public class Logic2VampireLanguageMapper_ScopeMapper { final int GLOBAL_MIN = config.typeScopes.minNewElements; final int GLOBAL_MAX = config.typeScopes.maxNewElements; final ArrayList localInstances = CollectionLiterals.newArrayList(); + final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); if ((GLOBAL_MIN != ABSOLUTE_MIN)) { - this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); - for (final VLSConstant i : trace.uniqueInstances) { - localInstances.add(this.support.duplicate(i)); + this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant)); + if (consistant) { + for (final VLSConstant i : trace.uniqueInstances) { + localInstances.add(this.support.duplicate(i)); + } + this.makeFofFormula(localInstances, trace, true, null); + } else { + this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, true, null); } - this.makeFofFormula(localInstances, trace, true, null); } if ((GLOBAL_MAX != ABSOLUTE_MAX)) { - this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); - this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); + this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant); + if (consistant) { + this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); + } else { + this.makeFofFormula(localInstances, trace, false, null); + } } int i_1 = 1; int minNum = (-1); @@ -95,11 +104,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper { } } } - int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; - boolean _notEquals = (_length != 0); - if (_notEquals) { + final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; + int ind = 1; + if ((numInst != 0)) { for (final VLSConstant e : trace.uniqueInstances) { { + final int x = ind; VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); final Procedure1 _function = (VLSFofFormula it) -> { it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); @@ -109,6 +119,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { final VLSFofFormula uniqueness = ObjectExtensions.operator_doubleArrow(_createVLSFofFormula, _function); EList _formulas = trace.specification.getFormulas(); _formulas.add(uniqueness); + ind++; } } } -- cgit v1.2.3-54-g00ecf