diff options
author | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-05 03:32:48 -0400 |
---|---|---|
committer | ArenBabikian <aren.babikian@mail.mcgill.ca> | 2019-04-05 03:32:48 -0400 |
commit | 46995a62387aa07a6421a5546f466951f58c168c (patch) | |
tree | af284e3c21317784b2fc15334d19a292288c3e67 /Solvers | |
parent | test push (diff) | |
download | VIATRA-Generator-46995a62387aa07a6421a5546f466951f58c168c.tar.gz VIATRA-Generator-46995a62387aa07a6421a5546f466951f58c168c.tar.zst VIATRA-Generator-46995a62387aa07a6421a5546f466951f58c168c.zip |
Implement containment circularity avoidance #20
Diffstat (limited to 'Solvers')
22 files changed, 145 insertions, 29 deletions
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml index 2381b84f..beaf5498 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/plugin.xml | |||
@@ -1 +1,17 @@ | |||
1 | <?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.4"?><plugin/> | 1 | <?xml version="1.0" encoding="UTF-8"?><?eclipse version="3.4"?><plugin> |
2 | <extension id="ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries" point="org.eclipse.viatra.query.runtime.queryspecification"> | ||
3 | <group group="org.eclipse.viatra.query.runtime.extensibility.SingletonExtensionFactory:ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries" id="ca.mcgill.ecse.dslreasoner.vampire.queries.VampireQueries"> | ||
4 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSComment"/> | ||
5 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSFofFormula"/> | ||
6 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSAnnotation"/> | ||
7 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSOr"/> | ||
8 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSAnd"/> | ||
9 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSEquivalent"/> | ||
10 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSFunction"/> | ||
11 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSExistentialQuantifier"/> | ||
12 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSUniversalQuantifier"/> | ||
13 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSUnaryNegation"/> | ||
14 | <query-specification fqn="ca.mcgill.ecse.dslreasoner.vampire.queries.VLSInequality"/> | ||
15 | </group> | ||
16 | </extension> | ||
17 | </plugin> | ||
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql index 2bc22f9e..ef61e4d1 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.queries/src/ca/mcgill/ecse/dslreasoner/vampire/queries/vampireQueries.vql | |||
@@ -48,9 +48,9 @@ pattern VLSInequality(term: VLSInequality){ | |||
48 | VLSInequality(term); | 48 | VLSInequality(term); |
49 | } | 49 | } |
50 | 50 | ||
51 | pattern VLSFunctionFof(term: VLSFunctionFof){ | 51 | //pattern VLSFunctionFof(term: VLSFunctionFof){ |
52 | VLSFunctionFof(term); | 52 | // VLSFunctionFof(term); |
53 | } | 53 | //} |
54 | 54 | ||
55 | //pattern VLSFofTerm(term: VLSFofTerm){ | 55 | //pattern VLSFofTerm(term: VLSFofTerm){ |
56 | // VLSFofTerm(term); | 56 | // VLSFofTerm(term); |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend index 618980a3..98967181 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/VampireAnalyzerConfiguration.xtend | |||
@@ -4,7 +4,8 @@ import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | |||
4 | 4 | ||
5 | class VampireSolverConfiguration extends LogicSolverConfiguration { | 5 | class VampireSolverConfiguration extends LogicSolverConfiguration { |
6 | 6 | ||
7 | //public var int symmetry = 0 // by default | 7 | public var int contCycleLevel = 0 |
8 | public var boolean uniquenessDuplicates = false | ||
8 | //choose needed backend solver | 9 | //choose needed backend solver |
9 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J | 10 | // public var VampireBackendSolver solver = VampireBackendSolver.SAT4J |
10 | } | 11 | } |
diff --git a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend index b7ad8f3d..2be6c093 100644 --- a/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend +++ b/Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/src/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper.xtend | |||
@@ -87,7 +87,7 @@ class Logic2VampireLanguageMapper { | |||
87 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] | 87 | problem.relations.forEach[this.relationMapper.transformRelation(it, trace)] |
88 | 88 | ||
89 | // CONTAINMENT MAPPER | 89 | // CONTAINMENT MAPPER |
90 | containmentMapper.transformContainment(problem.containmentHierarchies, trace) | 90 | containmentMapper.transformContainment(config,problem.containmentHierarchies, trace) |
91 | 91 | ||
92 | // CONSTANT MAPPER | 92 | // CONSTANT MAPPER |
93 | // only transforms definitions | 93 | // only transforms definitions |
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 48ee8789..395b4305 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 | |||
@@ -1,6 +1,6 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm |
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
@@ -25,9 +25,9 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
25 | this.base = base | 25 | this.base = base |
26 | } | 26 | } |
27 | 27 | ||
28 | def public void transformContainment(List<ContainmentHierarchy> hierarchies, | 28 | def public void transformContainment(VampireSolverConfiguration config, List<ContainmentHierarchy> hierarchies, |
29 | Logic2VampireLanguageMapperTrace trace) { | 29 | Logic2VampireLanguageMapperTrace trace) { |
30 | //TODO throw error is there exists a circular containment that does not involve hierarchy | 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) |
@@ -94,7 +94,6 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
94 | // for (c : support.listSubtypes(toType)) { | 94 | // for (c : support.listSubtypes(toType)) { |
95 | // addToMap(type2cont, toFunc, rel) | 95 | // addToMap(type2cont, toFunc, rel) |
96 | // } | 96 | // } |
97 | |||
98 | // val listForAnd = newArrayList | 97 | // val listForAnd = newArrayList |
99 | //// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) | 98 | //// listForAnd.add(support.duplicate(fromType.lookup(trace.type2Predicate), varB)) |
100 | // listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)) | 99 | // listForAnd.add(support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), varList)) |
@@ -111,7 +110,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
111 | // STEP 3 | 110 | // STEP 3 |
112 | // Ensure that an objct only has 1 parent | 111 | // Ensure that an objct only has 1 parent |
113 | val relFormula = createVLSFofFormula => [ | 112 | val relFormula = createVLSFofFormula => [ |
114 | it.name = support.toIDMultiple("noDupCont", rel.constant.toString) | 113 | it.name = support.toIDMultiple("containment_noDup", rel.constant.toString) |
115 | it.fofRole = "axiom" | 114 | it.fofRole = "axiom" |
116 | it.fofFormula = createVLSExistentialQuantifier => [ | 115 | it.fofFormula = createVLSExistentialQuantifier => [ |
117 | it.variables += support.duplicate(varA) | 116 | it.variables += support.duplicate(varA) |
@@ -133,7 +132,7 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
133 | 132 | ||
134 | } | 133 | } |
135 | 134 | ||
136 | // STEP CONT'D | 135 | // STEP 2 CONT'D |
137 | for (e : type2cont.entrySet) { | 136 | for (e : type2cont.entrySet) { |
138 | val relFormula = createVLSFofFormula => [ | 137 | val relFormula = createVLSFofFormula => [ |
139 | it.name = support.toIDMultiple("containment", e.key.constant.toString) | 138 | it.name = support.toIDMultiple("containment", e.key.constant.toString) |
@@ -159,8 +158,39 @@ class Logic2VampireLanguageMapper_ContainmentMapper { | |||
159 | 158 | ||
160 | } | 159 | } |
161 | 160 | ||
162 | // STEP 4 | 161 | // STEP 4 |
163 | // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) | 162 | // Ensure that there are no cycles in the hierarchy (maybe same as for step3?) |
163 | // Attempt 1: all possibilities, even the impossible one, based on MM constraints, are listed | ||
164 | |||
165 | |||
166 | val variables = newArrayList | ||
167 | val disjunctionList = newArrayList | ||
168 | val conjunctionList = newArrayList | ||
169 | for (var i = 1; i <= config.contCycleLevel; i++) { | ||
170 | val ind = i | ||
171 | variables.add(createVLSVariable => [it.name = ("V"+Integer.toString(ind))]) | ||
172 | for ( var j = 0; j < i;j++){ | ||
173 | for (l : relationsList) { | ||
174 | val rel = support.duplicate((l as RelationDeclaration).lookup(trace.rel2Predicate), newArrayList(variables.get(j), variables.get((j+1)%i))) | ||
175 | disjunctionList.add(rel) | ||
176 | } | ||
177 | conjunctionList.add(support.unfoldOr(disjunctionList)) | ||
178 | disjunctionList.clear | ||
179 | } | ||
180 | |||
181 | val contCycleForm = createVLSFofFormula => [ | ||
182 | it.name = support.toIDMultiple("containment_noCycle", Integer.toString(ind)) | ||
183 | it.fofRole = "axiom" | ||
184 | it.fofFormula = createVLSUnaryNegation => [ | ||
185 | it.operand = createVLSExistentialQuantifier => [ | ||
186 | it.variables += support.duplicate(variables) | ||
187 | it.operand = support.unfoldAnd(conjunctionList) | ||
188 | ] | ||
189 | ] | ||
190 | ] | ||
191 | trace.specification.formulas += contCycleForm | ||
192 | conjunctionList.clear | ||
193 | } | ||
164 | } | 194 | } |
165 | 195 | ||
166 | protected def VLSTerm makeUnique(List<VLSFunction> list) { | 196 | protected def VLSTerm makeUnique(List<VLSFunction> list) { |
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 0d0be576..0a8812e4 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 | |||
@@ -1,17 +1,15 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction | 3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration |
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
4 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable | 5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable |
5 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | 7 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type |
8 | import java.util.ArrayList | 8 | import java.util.ArrayList |
9 | import java.util.HashMap | ||
9 | import java.util.Map | 10 | import java.util.Map |
10 | 11 | ||
11 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 12 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
12 | import java.util.HashMap | ||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm | ||
14 | import java.util.List | ||
15 | 13 | ||
16 | class Logic2VampireLanguageMapper_ScopeMapper { | 14 | class Logic2VampireLanguageMapper_ScopeMapper { |
17 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE | 15 | private val extension VampireLanguageFactory factory = VampireLanguageFactory.eINSTANCE |
@@ -23,7 +21,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
23 | this.base = base | 21 | this.base = base |
24 | } | 22 | } |
25 | 23 | ||
26 | def dispatch public void transformScope(LogicSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { | 24 | def dispatch public void transformScope(VampireSolverConfiguration config, Logic2VampireLanguageMapperTrace trace) { |
27 | val ABSOLUTE_MIN = 0 | 25 | val ABSOLUTE_MIN = 0 |
28 | val ABSOLUTE_MAX = Integer.MAX_VALUE | 26 | val ABSOLUTE_MAX = Integer.MAX_VALUE |
29 | 27 | ||
@@ -40,7 +38,6 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
40 | 38 | ||
41 | // Handling Minimum_General | 39 | // Handling Minimum_General |
42 | if (GLOBAL_MIN != ABSOLUTE_MIN) { | 40 | if (GLOBAL_MIN != ABSOLUTE_MIN) { |
43 | // * | ||
44 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant) | 41 | getInstanceConstants(GLOBAL_MIN, 0, localInstances, trace, true, !consistant) |
45 | if (consistant) { | 42 | if (consistant) { |
46 | for (i : trace.uniqueInstances) { | 43 | for (i : trace.uniqueInstances) { |
@@ -94,7 +91,7 @@ class Logic2VampireLanguageMapper_ScopeMapper { | |||
94 | 91 | ||
95 | // 3. Specify uniqueness of elements | 92 | // 3. Specify uniqueness of elements |
96 | // TEMP | 93 | // TEMP |
97 | val DUPLICATES = false | 94 | val DUPLICATES = config.uniquenessDuplicates |
98 | 95 | ||
99 | val numInst = trace.uniqueInstances.length | 96 | val numInst = trace.uniqueInstances.length |
100 | var ind = 1 | 97 | var ind = 1 |
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 dd88a53a..195b89bb 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 | |||
@@ -77,6 +77,14 @@ class Logic2VampireLanguageMapper_Support { | |||
77 | it.terms += duplicate(v) | 77 | it.terms += duplicate(v) |
78 | ] | 78 | ] |
79 | } | 79 | } |
80 | |||
81 | def protected List<VLSVariable> duplicate(List<VLSVariable> vars) { | ||
82 | var newList = newArrayList | ||
83 | for (v : vars) { | ||
84 | newList.add(duplicate(v)) | ||
85 | } | ||
86 | return newList | ||
87 | } | ||
80 | 88 | ||
81 | def protected VLSConstant toConstant(VLSFunctionAsTerm term) { | 89 | def protected VLSConstant toConstant(VLSFunctionAsTerm term) { |
82 | return createVLSConstant => [ | 90 | return createVLSConstant => [ |
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 --- 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 0714f36d..d328dcf2 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/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; | |||
4 | 4 | ||
5 | @SuppressWarnings("all") | 5 | @SuppressWarnings("all") |
6 | public class VampireSolverConfiguration extends LogicSolverConfiguration { | 6 | public class VampireSolverConfiguration extends LogicSolverConfiguration { |
7 | public int contCycleLevel = 0; | ||
8 | |||
9 | public boolean uniquenessDuplicates = false; | ||
7 | } | 10 | } |
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 --- 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_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 --- 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 cf049bd5..44b06208 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 7bc04e7b..4cab8309 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 a97c7186..ccddb430 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 a473c586..a069a62f 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 4e7796fe..46cd58fb 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/.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 --- 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/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 { | |||
123 | this.relationMapper.transformRelation(it, trace); | 123 | this.relationMapper.transformRelation(it, trace); |
124 | }; | 124 | }; |
125 | problem.getRelations().forEach(_function_3); | 125 | problem.getRelations().forEach(_function_3); |
126 | this.containmentMapper.transformContainment(problem.getContainmentHierarchies(), trace); | 126 | this.containmentMapper.transformContainment(config, problem.getContainmentHierarchies(), trace); |
127 | trace.constantDefinitions = this.collectConstantDefinitions(problem); | 127 | trace.constantDefinitions = this.collectConstantDefinitions(problem); |
128 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { | 128 | final Consumer<ConstantDefinition> _function_4 = (ConstantDefinition it) -> { |
129 | this.constantMapper.transformConstantDefinitionSpecification(it, trace); | 129 | 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
@@ -16,6 +17,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | |||
16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
17 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 18 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
18 | import com.google.common.base.Objects; | 19 | import com.google.common.base.Objects; |
20 | import com.google.common.collect.Iterables; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; | 21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ComplexTypeReference; |
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | 22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; |
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; | 23 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDeclaration; |
@@ -52,7 +54,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
52 | this.base = base; | 54 | this.base = base; |
53 | } | 55 | } |
54 | 56 | ||
55 | public void transformContainment(final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) { | 57 | public void transformContainment(final VampireSolverConfiguration config, final List<ContainmentHierarchy> hierarchies, final Logic2VampireLanguageMapperTrace trace) { |
56 | final ContainmentHierarchy hierarchy = hierarchies.get(0); | 58 | final ContainmentHierarchy hierarchy = hierarchies.get(0); |
57 | final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); | 59 | final EList<Type> containmentListCopy = hierarchy.getTypesOrderedInHierarchy(); |
58 | final EList<Relation> relationsList = hierarchy.getContainmentRelations(); | 60 | final EList<Relation> relationsList = hierarchy.getContainmentRelations(); |
@@ -135,7 +137,7 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
135 | } | 137 | } |
136 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | 138 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); |
137 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { | 139 | final Procedure1<VLSFofFormula> _function_4 = (VLSFofFormula it) -> { |
138 | it.setName(this.support.toIDMultiple("noDupCont", rel.getConstant().toString())); | 140 | it.setName(this.support.toIDMultiple("containment_noDup", rel.getConstant().toString())); |
139 | it.setFofRole("axiom"); | 141 | it.setFofRole("axiom"); |
140 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | 142 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); |
141 | final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> { | 143 | final Procedure1<VLSExistentialQuantifier> _function_5 = (VLSExistentialQuantifier it_1) -> { |
@@ -219,6 +221,57 @@ public class Logic2VampireLanguageMapper_ContainmentMapper { | |||
219 | _formulas_1.add(relFormula); | 221 | _formulas_1.add(relFormula); |
220 | } | 222 | } |
221 | } | 223 | } |
224 | final ArrayList<VLSVariable> variables = CollectionLiterals.<VLSVariable>newArrayList(); | ||
225 | final ArrayList<VLSFunction> disjunctionList = CollectionLiterals.<VLSFunction>newArrayList(); | ||
226 | final ArrayList<VLSTerm> conjunctionList = CollectionLiterals.<VLSTerm>newArrayList(); | ||
227 | for (int i = 1; (i <= config.contCycleLevel); i++) { | ||
228 | { | ||
229 | final int ind = i; | ||
230 | VLSVariable _createVLSVariable_3 = this.factory.createVLSVariable(); | ||
231 | final Procedure1<VLSVariable> _function_4 = (VLSVariable it) -> { | ||
232 | String _string = Integer.toString(ind); | ||
233 | String _plus = ("V" + _string); | ||
234 | it.setName(_plus); | ||
235 | }; | ||
236 | VLSVariable _doubleArrow = ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable_3, _function_4); | ||
237 | variables.add(_doubleArrow); | ||
238 | for (int j = 0; (j < i); j++) { | ||
239 | { | ||
240 | for (final Relation l_2 : relationsList) { | ||
241 | { | ||
242 | final VLSFunction rel = this.support.duplicate(CollectionsUtil.<RelationDeclaration, VLSFunction>lookup(((RelationDeclaration) l_2), trace.rel2Predicate), CollectionLiterals.<VLSVariable>newArrayList(variables.get(j), variables.get(((j + 1) % i)))); | ||
243 | disjunctionList.add(rel); | ||
244 | } | ||
245 | } | ||
246 | conjunctionList.add(this.support.unfoldOr(disjunctionList)); | ||
247 | disjunctionList.clear(); | ||
248 | } | ||
249 | } | ||
250 | VLSFofFormula _createVLSFofFormula_1 = this.factory.createVLSFofFormula(); | ||
251 | final Procedure1<VLSFofFormula> _function_5 = (VLSFofFormula it) -> { | ||
252 | it.setName(this.support.toIDMultiple("containment_noCycle", Integer.toString(ind))); | ||
253 | it.setFofRole("axiom"); | ||
254 | VLSUnaryNegation _createVLSUnaryNegation = this.factory.createVLSUnaryNegation(); | ||
255 | final Procedure1<VLSUnaryNegation> _function_6 = (VLSUnaryNegation it_1) -> { | ||
256 | VLSExistentialQuantifier _createVLSExistentialQuantifier = this.factory.createVLSExistentialQuantifier(); | ||
257 | final Procedure1<VLSExistentialQuantifier> _function_7 = (VLSExistentialQuantifier it_2) -> { | ||
258 | EList<VLSVariable> _variables = it_2.getVariables(); | ||
259 | List<VLSVariable> _duplicate = this.support.duplicate(variables); | ||
260 | Iterables.<VLSVariable>addAll(_variables, _duplicate); | ||
261 | it_2.setOperand(this.support.unfoldAnd(conjunctionList)); | ||
262 | }; | ||
263 | VLSExistentialQuantifier _doubleArrow_1 = ObjectExtensions.<VLSExistentialQuantifier>operator_doubleArrow(_createVLSExistentialQuantifier, _function_7); | ||
264 | it_1.setOperand(_doubleArrow_1); | ||
265 | }; | ||
266 | VLSUnaryNegation _doubleArrow_1 = ObjectExtensions.<VLSUnaryNegation>operator_doubleArrow(_createVLSUnaryNegation, _function_6); | ||
267 | it.setFofFormula(_doubleArrow_1); | ||
268 | }; | ||
269 | final VLSFofFormula contCycleForm = ObjectExtensions.<VLSFofFormula>operator_doubleArrow(_createVLSFofFormula_1, _function_5); | ||
270 | EList<VLSFofFormula> _formulas_1 = trace.specification.getFormulas(); | ||
271 | _formulas_1.add(contCycleForm); | ||
272 | conjunctionList.clear(); | ||
273 | } | ||
274 | } | ||
222 | } | 275 | } |
223 | 276 | ||
224 | protected VLSTerm makeUnique(final List<VLSFunction> list) { | 277 | protected VLSTerm makeUnique(final List<VLSFunction> 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 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; | 1 | package ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder; |
2 | 2 | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
3 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; | 4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper; |
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; | 5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapperTrace; |
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; | 6 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.builder.Logic2VampireLanguageMapper_Support; |
@@ -13,7 +14,6 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSTerm; | |||
13 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; | 14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSUniversalQuantifier; |
14 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; | 15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSVariable; |
15 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; | 16 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VampireLanguageFactory; |
16 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicSolverConfiguration; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | 17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; |
18 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; | 18 | import hu.bme.mit.inf.dslreasoner.util.CollectionsUtil; |
19 | import java.util.ArrayList; | 19 | import java.util.ArrayList; |
@@ -47,7 +47,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
47 | this.base = base; | 47 | this.base = base; |
48 | } | 48 | } |
49 | 49 | ||
50 | public void _transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 50 | public void _transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
51 | final int ABSOLUTE_MIN = 0; | 51 | final int ABSOLUTE_MIN = 0; |
52 | final int ABSOLUTE_MAX = Integer.MAX_VALUE; | 52 | final int ABSOLUTE_MAX = Integer.MAX_VALUE; |
53 | final int GLOBAL_MIN = config.typeScopes.minNewElements; | 53 | final int GLOBAL_MIN = config.typeScopes.minNewElements; |
@@ -105,7 +105,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
105 | } | 105 | } |
106 | } | 106 | } |
107 | } | 107 | } |
108 | final boolean DUPLICATES = false; | 108 | final boolean DUPLICATES = config.uniquenessDuplicates; |
109 | final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; | 109 | final int numInst = ((Object[])Conversions.unwrapArray(trace.uniqueInstances, Object.class)).length; |
110 | int ind = 1; | 110 | int ind = 1; |
111 | if ((numInst != 0)) { | 111 | if ((numInst != 0)) { |
@@ -246,7 +246,7 @@ public class Logic2VampireLanguageMapper_ScopeMapper { | |||
246 | _formulas.add(cstDec); | 246 | _formulas.add(cstDec); |
247 | } | 247 | } |
248 | 248 | ||
249 | public void transformScope(final LogicSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { | 249 | public void transformScope(final VampireSolverConfiguration config, final Logic2VampireLanguageMapperTrace trace) { |
250 | _transformScope(config, trace); | 250 | _transformScope(config, trace); |
251 | return; | 251 | return; |
252 | } | 252 | } |
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 { | |||
129 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 129 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
130 | } | 130 | } |
131 | 131 | ||
132 | protected List<VLSVariable> duplicate(final List<VLSVariable> vars) { | ||
133 | ArrayList<VLSVariable> newList = CollectionLiterals.<VLSVariable>newArrayList(); | ||
134 | for (final VLSVariable v : vars) { | ||
135 | newList.add(this.duplicate(v)); | ||
136 | } | ||
137 | return newList; | ||
138 | } | ||
139 | |||
132 | protected VLSConstant toConstant(final VLSFunctionAsTerm term) { | 140 | protected VLSConstant toConstant(final VLSFunctionAsTerm term) { |
133 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | 141 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); |
134 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | 142 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { |