From 4829f58fb56e9f7a5f86d422e126a4a65cdeae5e Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Thu, 4 Apr 2019 19:55:10 -0400 Subject: Facilitate #31, close #36 --- .../Logic2VampireLanguageMapper_ScopeMapper.xtend | 53 +++++++++++++-------- .../Logic2VampireLanguageMapper_Support.xtend | 4 ++ .../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 +++++++---- 6 files changed, 58 insertions(+), 28 deletions(-) (limited to 'Solvers') 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 54fcdc86..5e8819a6 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 @@ -36,31 +36,30 @@ class Logic2VampireLanguageMapper_ScopeMapper { val localInstances = newArrayList + val consistant = GLOBAL_MAX > GLOBAL_MIN + // Handling Minimum_General if (GLOBAL_MIN != ABSOLUTE_MIN) { - getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) - for (i : trace.uniqueInstances) { - localInstances.add(support.duplicate(i)) + // * + getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant) + if (consistant) { + for (i : trace.uniqueInstances) { + localInstances.add(support.duplicate(i)) + } + makeFofFormula(localInstances, trace, true, null) + } else { + makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null) } - - makeFofFormula(localInstances, trace, true, null) - -// //For testing Min>Max scope -// getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, true) -// makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null) -// //end for testing - } // Handling Maximum_General if (GLOBAL_MAX != ABSOLUTE_MAX) { - getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) - makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) - -// //For testing Min>Max scope -// getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, false) -// makeFofFormula(localInstances, trace, false, null) -// //end for testing + getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant) + if (consistant) { + makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) + } else { + makeFofFormula(localInstances, trace, false, null) + } } // Handling Minimum_Specific @@ -94,14 +93,30 @@ class Logic2VampireLanguageMapper_ScopeMapper { } // 3. Specify uniqueness of elements - if (trace.uniqueInstances.length != 0) { + val numInst = trace.uniqueInstances.length + var ind = 1 + if (numInst != 0) { + /* + * // SHORTER + * for (e : trace.uniqueInstances.subList(0, numInst-1)) { + /*/ + // LONGER for (e : trace.uniqueInstances) { + // */ + val x = ind val uniqueness = createVLSFofFormula => [ it.name = support.toIDMultiple("t_uniqueness", e.name) it.fofRole = "axiom" + /* + * // SHORTER + * it.fofFormula = support.establishUniqueness(trace.uniqueInstances.subList(x, numInst), e) + /*/ + // LONGER it.fofFormula = support.establishUniqueness(trace.uniqueInstances, e) + // */ ] trace.specification.formulas += uniqueness + ind++ } } } 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 b00dad42..dd88a53a 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 @@ -109,6 +109,8 @@ class Logic2VampireLanguageMapper_Support { // TODO Make more general def establishUniqueness(List terms, VLSConstant t2) { + +// OLD // val List eqs = newArrayList // for (t1 : terms.subList(1, terms.length)) { // for (t2 : terms.subList(0, terms.indexOf(t1))) { @@ -122,6 +124,8 @@ class Logic2VampireLanguageMapper_Support { // } // } // return unfoldAnd(eqs) +// END OLD + val List eqs = newArrayList for (t1 : terms) { if (t1 != t2) { 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