diff options
author | 2019-04-04 19:55:10 -0400 | |
---|---|---|
committer | 2019-04-04 19:55:10 -0400 | |
commit | 4829f58fb56e9f7a5f86d422e126a4a65cdeae5e (patch) | |
tree | 6339eac4eee54e788755147e5f7aa22fb73fabd9 /Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen | |
parent | Closes #34, adds code to test cases where minScope>maxScope. (diff) | |
download | VIATRA-Generator-4829f58fb56e9f7a5f86d422e126a4a65cdeae5e.tar.gz VIATRA-Generator-4829f58fb56e9f7a5f86d422e126a4a65cdeae5e.tar.zst VIATRA-Generator-4829f58fb56e9f7a5f86d422e126a4a65cdeae5e.zip |
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen')
4 files changed, 20 insertions, 9 deletions
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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 --- 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 | |||
Binary files 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 { | |||
52 | final int GLOBAL_MIN = config.typeScopes.minNewElements; | 52 | final int GLOBAL_MIN = config.typeScopes.minNewElements; |
53 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; | 53 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; |
54 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); | 54 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); |
55 | final boolean consistant = (GLOBAL_MAX > GLOBAL_MIN); | ||
55 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { | 56 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { |
56 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); | 57 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, (!consistant)); |
57 | for (final VLSConstant i : trace.uniqueInstances) { | 58 | if (consistant) { |
58 | localInstances.add(this.support.duplicate(i)); | 59 | for (final VLSConstant i : trace.uniqueInstances) { |
60 | localInstances.add(this.support.duplicate(i)); | ||
61 | } | ||
62 | this.makeFofFormula(localInstances, trace, true, null); | ||
63 | } else { | ||
64 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, true, null); | ||
59 | } | 65 | } |
60 | this.makeFofFormula(localInstances, trace, true, null); | ||
61 | } | 66 | } |
62 | if ((GLOBAL_MAX != ABSOLUTE_MAX)) { | 67 | if ((GLOBAL_MAX != ABSOLUTE_MAX)) { |
63 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); | 68 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, consistant); |
64 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); | 69 | if (consistant) { |
70 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); | ||
71 | } else { | ||
72 | this.makeFofFormula(localInstances, trace, false, null); | ||
73 | } | ||
65 | } | 74 | } |
66 | int i_1 = 1; | 75 | int i_1 = 1; |
67 | int minNum = (-1); | 76 | int minNum = (-1); |
@@ -95,11 +104,12 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
95 | } | 104 | } |
96 | } | 105 | } |
97 | } | 106 | } |
98 | int _length = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; | 107 | final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; |
99 | boolean _notEquals = (_length != 0); | 108 | int ind = 1; |
100 | if (_notEquals) { | 109 | if ((numInst != 0)) { |
101 | for (final VLSConstant e : trace.uniqueInstances) { | 110 | for (final VLSConstant e : trace.uniqueInstances) { |
102 | { | 111 | { |
112 | final int x = ind; | ||
103 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); | 113 | VLSFofFormula _createVLSFofFormula = this.factory.createVLSFofFormula(); |
104 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { | 114 | final Procedure1<VLSFofFormula> _function = (VLSFofFormula it) -> { |
105 | it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); | 115 | it.setName(this.support.toIDMultiple("t_uniqueness", e.getName())); |
@@ -109,6 +119,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
109 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); | 119 | final VLSFofFormula uniqueness = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula, _function); |
110 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); | 120 | EList<VLSFofFormula> _formulas = trace.specification.getFormulas(); |
111 | _formulas.add(uniqueness); | 121 | _formulas.add(uniqueness); |
122 | ind++; | ||
112 | } | 123 | } |
113 | } | 124 | } |
114 | } | 125 | } |