diff options
Diffstat (limited to 'Solvers/Vampire-Solver')
34 files changed, 104 insertions, 21 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin index 31f46622..fe8f0b3b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin index cc4fa425..a59f4b57 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ide/xtend-gen/ca/mcgill/ecse/dslreasoner/ide/.VampireLanguageIdeSetup.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin index 23c27b9f..c9bdec6a 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/.VampireLanguageUiModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin index c0b6798a..ada1dc0f 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/contentassist/.VampireLanguageProposalProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin index f8684dcf..b92abb22 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageDescriptionLabelProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin index 34cde9c6..d381aa93 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/labeling/.VampireLanguageLabelProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin index 794a6799..94d70495 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/outline/.VampireLanguageOutlineTreeProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin index fca8ea98..50e8edbf 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language.ui/xtend-gen/ca/mcgill/ecse/dslreasoner/ui/quickfix/.VampireLanguageQuickfixProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin index 690743f8..0886858b 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageRuntimeModule.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin index ac507dd4..fb078be1 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/.VampireLanguageStandaloneSetup.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin index b9d659a5..7febb8b9 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/formatting2/.VampireLanguageFormatter.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin index 0f24f135..a790245e 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/generator/.VampireLanguageGenerator.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin index 46e4ff65..19d74808 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/scoping/.VampireLanguageScopeProvider.xtendbin | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin index feb807fe..ab5c8cfa 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.language/xtend-gen/ca/mcgill/ecse/dslreasoner/validation/.VampireLanguageValidator.xtendbin | |||
Binary files differ | |||
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 index 820d0db2..48ee8789 100644 --- 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 | |||
@@ -27,7 +27,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
27 | 27 | ||
28 | def public void transformContainment(List<ContainmentHierarchy> hierarchies, | 28 | def public void transformContainment(List<ContainmentHierarchy> hierarchies, |
29 | Logic2VampireLanguageMapperTrace trace) { | 29 | Logic2VampireLanguageMapperTrace trace) { |
30 | 30 | //TODO throw error is there exists a circular containment that does not involve hierarchy | |
31 | // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST | 31 | // TODO CONSIDER CASE WHERE MULTIPLE CONTAINMMENT HIERARCHIES EXIST |
32 | // TEMP | 32 | // TEMP |
33 | val hierarchy = hierarchies.get(0) | 33 | val hierarchy = hierarchies.get(0) |
@@ -91,6 +91,9 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
91 | for (c : toType.subtypes) { | 91 | for (c : toType.subtypes) { |
92 | addToMap(type2cont, toFunc, rel) | 92 | addToMap(type2cont, toFunc, rel) |
93 | } | 93 | } |
94 | // for (c : support.listSubtypes(toType)) { | ||
95 | // addToMap(type2cont, toFunc, rel) | ||
96 | // } | ||
94 | 97 | ||
95 | // val listForAnd = newArrayList | 98 | // val listForAnd = newArrayList |
96 | //// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) | 99 | //// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) |
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 bc87d3b7..54fcdc86 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 | |||
@@ -24,11 +24,12 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
24 | } | 24 | } |
25 | 25 | ||
26 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { | 26 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { |
27 | val ABSOLUTE_MIN = 0 | ||
28 | val ABSOLUTE_MAX = Integer.MAX_VALUE | ||
27 | 29 | ||
28 | // TODO HANDLE ERRORS RELATED TO MAX > MIN | 30 | // TODO HANDLE ERRORS RELATED TO MAX > MIN |
29 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS | 31 | // TODO HANDLE ERROR RELATED TO SUM(MIN TYPES)+1(for root) > MAX OBJECTS |
30 | // TODO HANDLE | 32 | // TODO HANDLE |
31 | // TODO NOT SPECIFIED MEANS =0 ? | ||
32 | // 1. make a list of constants equaling the min number of specified objects | 33 | // 1. make a list of constants equaling the min number of specified objects |
33 | val GLOBAL_MIN = config.typeScopes.minNewElements | 34 | val GLOBAL_MIN = config.typeScopes.minNewElements |
34 | val GLOBAL_MAX = config.typeScopes.maxNewElements | 35 | val GLOBAL_MAX = config.typeScopes.maxNewElements |
@@ -36,19 +37,30 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
36 | val localInstances = newArrayList | 37 | val localInstances = newArrayList |
37 | 38 | ||
38 | // Handling Minimum_General | 39 | // Handling Minimum_General |
39 | if (GLOBAL_MIN != 0) { | 40 | if (GLOBAL_MIN != ABSOLUTE_MIN) { |
40 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) | 41 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false) |
41 | for (i : trace.uniqueInstances) { | 42 | for (i : trace.uniqueInstances) { |
42 | localInstances.add(support.duplicate(i)) | 43 | localInstances.add(support.duplicate(i)) |
43 | } | 44 | } |
44 | 45 | ||
45 | makeFofFormula(localInstances, trace, true, null) | 46 | makeFofFormula(localInstances, trace, true, null) |
47 | |||
48 | // //For testing Min>Max scope | ||
49 | // getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, true) | ||
50 | // makeFofFormula(trace.uniqueInstances as ArrayList, trace, true, null) | ||
51 | // //end for testing | ||
52 | |||
46 | } | 53 | } |
47 | 54 | ||
48 | // Handling Maximum_General | 55 | // Handling Maximum_General |
49 | if (GLOBAL_MAX != 0) { | 56 | if (GLOBAL_MAX != ABSOLUTE_MAX) { |
50 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) | 57 | getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true) |
51 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) | 58 | makeFofFormula(trace.uniqueInstances as ArrayList, trace, false, null) |
59 | |||
60 | // //For testing Min>Max scope | ||
61 | // getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, false) | ||
62 | // makeFofFormula(localInstances, trace, false, null) | ||
63 | // //end for testing | ||
52 | } | 64 | } |
53 | 65 | ||
54 | // Handling Minimum_Specific | 66 | // Handling Minimum_Specific |
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 d1ea2a15..b00dad42 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 | |||
@@ -23,7 +23,7 @@ import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | |||
23 | class Logic2VampireLanguageMapper_Support { | 23 | class Logic2VampireLanguageMapper_Support { |
24 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 24 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
25 | 25 | ||
26 | // ID Handler | 26 | // ID Handler |
27 | def protected String toIDMultiple(String... ids) { | 27 | def protected String toIDMultiple(String... ids) { |
28 | ids.map[it.split("\\s+").join("_")].join("_") | 28 | ids.map[it.split("\\s+").join("_")].join("_") |
29 | } | 29 | } |
@@ -32,8 +32,8 @@ class Logic2VampireLanguageMapper_Support { | |||
32 | ids.split("\\s+").join("_") | 32 | ids.split("\\s+").join("_") |
33 | } | 33 | } |
34 | 34 | ||
35 | // Term Handling | 35 | // Term Handling |
36 | // TODO Make more general | 36 | // TODO Make more general |
37 | def protected VLSVariable duplicate(VLSVariable term) { | 37 | def protected VLSVariable duplicate(VLSVariable term) { |
38 | return createVLSVariable => [it.name = term.name] | 38 | return createVLSVariable => [it.name = term.name] |
39 | } | 39 | } |
@@ -107,7 +107,7 @@ class Logic2VampireLanguageMapper_Support { | |||
107 | ] | 107 | ] |
108 | } | 108 | } |
109 | 109 | ||
110 | // TODO Make more general | 110 | // TODO Make more general |
111 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { | 111 | def establishUniqueness(List<VLSConstant> terms, VLSConstant t2) { |
112 | // val List<VLSInequality> eqs = newArrayList | 112 | // val List<VLSInequality> eqs = newArrayList |
113 | // for (t1 : terms.subList(1, terms.length)) { | 113 | // for (t1 : terms.subList(1, terms.length)) { |
@@ -135,9 +135,9 @@ class Logic2VampireLanguageMapper_Support { | |||
135 | return unfoldAnd(eqs) | 135 | return unfoldAnd(eqs) |
136 | } | 136 | } |
137 | 137 | ||
138 | // Support Functions | 138 | // Support Functions |
139 | // booleans | 139 | // booleans |
140 | // AND and OR | 140 | // AND and OR |
141 | def protected VLSTerm unfoldAnd(List<? extends VLSTerm> operands) { | 141 | def protected VLSTerm unfoldAnd(List<? extends VLSTerm> operands) { |
142 | if (operands.size == 1) { | 142 | if (operands.size == 1) { |
143 | return operands.head | 143 | return operands.head |
@@ -163,7 +163,7 @@ class Logic2VampireLanguageMapper_Support { | |||
163 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP | 163 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') // TEMP |
164 | } | 164 | } |
165 | 165 | ||
166 | // can delete below | 166 | // can delete below |
167 | def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands, | 167 | def protected VLSTerm unfoldDistinctTerms(Logic2VampireLanguageMapper m, EList<Term> operands, |
168 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { | 168 | Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables) { |
169 | if (operands.size == 1) { | 169 | if (operands.size == 1) { |
@@ -183,8 +183,8 @@ class Logic2VampireLanguageMapper_Support { | |||
183 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') | 183 | throw new UnsupportedOperationException('''Logic operator with 0 operands!''') |
184 | } | 184 | } |
185 | 185 | ||
186 | // Symbolic | 186 | // Symbolic |
187 | // def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) { | 187 | // def postprocessResultOfSymbolicReference(TypeReference type, VLSTerm term, Logic2VampireLanguageMapperTrace trace) { |
188 | // if(type instanceof BoolTypeReference) { | 188 | // if(type instanceof BoolTypeReference) { |
189 | // return booleanToLogicValue(term ,trace) | 189 | // return booleanToLogicValue(term ,trace) |
190 | // } | 190 | // } |
@@ -198,7 +198,7 @@ class Logic2VampireLanguageMapper_Support { | |||
198 | * ids.map[it.split("\\s+").join("'")].join("'") | 198 | * ids.map[it.split("\\s+").join("'")].join("'") |
199 | * } | 199 | * } |
200 | */ | 200 | */ |
201 | // QUANTIFIERS + VARIABLES | 201 | // QUANTIFIERS + VARIABLES |
202 | def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, | 202 | def protected VLSTerm createQuantifiedExpression(Logic2VampireLanguageMapper mapper, |
203 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables, | 203 | QuantifiedExpression expression, Logic2VampireLanguageMapperTrace trace, Map<Variable, VLSVariable> variables, |
204 | boolean isUniversal) { | 204 | boolean isUniversal) { |
@@ -245,6 +245,32 @@ class Logic2VampireLanguageMapper_Support { | |||
245 | } | 245 | } |
246 | } | 246 | } |
247 | } | 247 | } |
248 | //TODO rewrite such that it uses "listSubTypes" | ||
249 | def protected boolean dfsSubtypeCheck(Type type, Type type2) { | ||
250 | // There is surely a better way to do this | ||
251 | if (type.subtypes.isEmpty) | ||
252 | return false | ||
253 | else { | ||
254 | if (type.subtypes.contains(type2)) | ||
255 | return true | ||
256 | else { | ||
257 | for (subtype : type.subtypes) { | ||
258 | if(dfsSubtypeCheck(subtype, type2)) return true | ||
259 | } | ||
260 | } | ||
261 | } | ||
262 | } | ||
263 | |||
264 | def protected List<Type> listSubtypes(Type t) { | ||
265 | var List<Type> allSubtypes = newArrayList | ||
266 | if (!t.subtypes.isEmpty) { | ||
267 | for (subt : t.subtypes) { | ||
268 | allSubtypes.add(subt) | ||
269 | allSubtypes = listSubtypes(subt) | ||
270 | } | ||
271 | } | ||
272 | return allSubtypes | ||
273 | } | ||
248 | 274 | ||
249 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { | 275 | def protected withAddition(Map<Variable, VLSVariable> map1, Map<Variable, VLSVariable> map2) { |
250 | new HashMap(map1) => [putAll(map2)] | 276 | new HashMap(map1) => [putAll(map2)] |
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 1719bbcc..3bc945df 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 | |||
@@ -150,10 +150,10 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
150 | 150 | ||
151 | } | 151 | } |
152 | 152 | ||
153 | // 4. case where an object is not an object | 153 | // 3.5: case where an object is not an object |
154 | val List<VLSTerm> type2Not = newArrayList | 154 | val List<VLSTerm> type2Not = newArrayList |
155 | 155 | ||
156 | for(t : types) { | 156 | for (t : types) { |
157 | type2Not.add(createVLSUnaryNegation => [ | 157 | type2Not.add(createVLSUnaryNegation => [ |
158 | it.operand = support.duplicate(t.lookup(trace.type2Predicate)) | 158 | it.operand = support.duplicate(t.lookup(trace.type2Predicate)) |
159 | ]) | 159 | ]) |
@@ -174,7 +174,7 @@ class Logic2VampireLanguageMapper_TypeMapper { | |||
174 | ] | 174 | ] |
175 | 175 | ||
176 | trace.specification.formulas += notObj | 176 | trace.specification.formulas += notObj |
177 | 177 | // End 3.5 | |
178 | // 4. create fof function that is an or with all the elements in map | 178 | // 4. create fof function that is an or with all the elements in map |
179 | val hierarch = createVLSFofFormula => [ | 179 | val hierarch = createVLSFofFormula => [ |
180 | it.name = "inheritanceHierarchyHandler" | 180 | it.name = "inheritanceHierarchyHandler" |
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 b2e83781..b5e03979 100644 --- 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 | |||
Binary files 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 ec4554da..0714f36d 100644 --- 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 | |||
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.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapper.xtendbin index 85d288b2..6c46d2e3 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/.Logic2VampireLanguageMapperTrace.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin index f43d3267..346daf52 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Logic2VampireLanguageMapperTrace.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_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 a49422be..01b0a351 100644 --- 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 | |||
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_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 e9060301..cf049bd5 100644 --- 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 | |||
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_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 ca19d1c9..7bc04e7b 100644 --- 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 | |||
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 bd348286..e5600049 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 274a1261..f9813a92 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_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 2e16b79c..4e7796fe 100644 --- 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 | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin index b363474f..8725e6b1 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.Vampire2LogicMapper.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/.VampireHandler.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireHandler.xtendbin index 82ee023c..84d6c63a 100644 --- 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 | |||
Binary files differ | |||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin index e378eda2..ca749be9 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation.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/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin index 427ec9c1..1c910cc9 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.xtendbin +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/.VampireModelInterpretation_TypeInterpretation_FilteredTypes.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 7aca7633..d40b0dd2 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 | |||
@@ -47,17 +47,19 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
47 | } | 47 | } |
48 | 48 | ||
49 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 49 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
50 | final int ABSOLUTE_MIN = 0; | ||
51 | final int ABSOLUTE_MAX = Integer.MAX_VALUE; | ||
50 | final int GLOBAL_MIN = config.typeScopes.minNewElements; | 52 | final int GLOBAL_MIN = config.typeScopes.minNewElements; |
51 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; | 53 | final int GLOBAL_MAX = config.typeScopes.maxNewElements; |
52 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); | 54 | final ArrayList<VLSConstant> localInstances = CollectionLiterals.<VLSConstant>newArrayList(); |
53 | if ((GLOBAL_MIN != 0)) { | 55 | if ((GLOBAL_MIN != ABSOLUTE_MIN)) { |
54 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); | 56 | this.getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, false); |
55 | for (final VLSConstant i : trace.uniqueInstances) { | 57 | for (final VLSConstant i : trace.uniqueInstances) { |
56 | localInstances.add(this.support.duplicate(i)); | 58 | localInstances.add(this.support.duplicate(i)); |
57 | } | 59 | } |
58 | this.makeFofFormula(localInstances, trace, true, null); | 60 | this.makeFofFormula(localInstances, trace, true, null); |
59 | } | 61 | } |
60 | if ((GLOBAL_MAX != 0)) { | 62 | if ((GLOBAL_MAX != ABSOLUTE_MAX)) { |
61 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); | 63 | this.getInstanceConstants(GLOBAL_MAX, 0, localInstances, trace, true, true); |
62 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); | 64 | this.makeFofFormula(((ArrayList) trace.uniqueInstances), trace, false, null); |
63 | } | 65 | } |
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 64129bf3..513618a9 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 | |||
@@ -371,6 +371,46 @@ public class Logic2VampireLanguageMapper_Support { | |||
371 | return _xifexpression; | 371 | return _xifexpression; |
372 | } | 372 | } |
373 | 373 | ||
374 | protected boolean dfsSubtypeCheck(final Type type, final Type type2) { | ||
375 | boolean _xifexpression = false; | ||
376 | boolean _isEmpty = type.getSubtypes().isEmpty(); | ||
377 | if (_isEmpty) { | ||
378 | return false; | ||
379 | } else { | ||
380 | boolean _xifexpression_1 = false; | ||
381 | boolean _contains = type.getSubtypes().contains(type2); | ||
382 | if (_contains) { | ||
383 | return true; | ||
384 | } else { | ||
385 | EList<Type> _subtypes = type.getSubtypes(); | ||
386 | for (final Type subtype : _subtypes) { | ||
387 | boolean _dfsSubtypeCheck = this.dfsSubtypeCheck(subtype, type2); | ||
388 | if (_dfsSubtypeCheck) { | ||
389 | return true; | ||
390 | } | ||
391 | } | ||
392 | } | ||
393 | _xifexpression = _xifexpression_1; | ||
394 | } | ||
395 | return _xifexpression; | ||
396 | } | ||
397 | |||
398 | protected List<Type> listSubtypes(final Type t) { | ||
399 | List<Type> allSubtypes = CollectionLiterals.<Type>newArrayList(); | ||
400 | boolean _isEmpty = t.getSubtypes().isEmpty(); | ||
401 | boolean _not = (!_isEmpty); | ||
402 | if (_not) { | ||
403 | EList<Type> _subtypes = t.getSubtypes(); | ||
404 | for (final Type subt : _subtypes) { | ||
405 | { | ||
406 | allSubtypes.add(subt); | ||
407 | allSubtypes = this.listSubtypes(subt); | ||
408 | } | ||
409 | } | ||
410 | } | ||
411 | return allSubtypes; | ||
412 | } | ||
413 | |||
374 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { | 414 | protected HashMap<Variable, VLSVariable> withAddition(final Map<Variable, VLSVariable> map1, final Map<Variable, VLSVariable> map2) { |
375 | HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1); | 415 | HashMap<Variable, VLSVariable> _hashMap = new HashMap<Variable, VLSVariable>(map1); |
376 | final Procedure1<HashMap<Variable, VLSVariable>> _function = (HashMap<Variable, VLSVariable> it) -> { | 416 | final Procedure1<HashMap<Variable, VLSVariable>> _function = (HashMap<Variable, VLSVariable> it) -> { |