diff options
Diffstat (limited to 'Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java')
-rw-r--r-- | Solvers/Vampire-Solver/ca.mcgill.ecse.dslreasoner.vampire.reasoner/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/reasoner/builder/Logic2VampireLanguageMapper_Support.java | 47 |
1 files changed, 47 insertions, 0 deletions
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 72ca44e9..e2ff7a0e 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 | |||
@@ -6,6 +6,7 @@ import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSAnd; | |||
6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; | 6 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSConstant; |
7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; | 7 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSExistentialQuantifier; |
8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; | 8 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunction; |
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSFunctionAsTerm; | ||
9 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; | 10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSImplies; |
10 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; | 11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSInequality; |
11 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; | 12 | import ca.mcgill.ecse.dslreasoner.vampireLanguage.VLSOr; |
@@ -62,6 +63,22 @@ public class Logic2VampireLanguageMapper_Support { | |||
62 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); | 63 | return ObjectExtensions.<VLSVariable>operator_doubleArrow(_createVLSVariable, _function); |
63 | } | 64 | } |
64 | 65 | ||
66 | protected VLSFunctionAsTerm duplicate(final VLSFunctionAsTerm term) { | ||
67 | VLSFunctionAsTerm _createVLSFunctionAsTerm = this.factory.createVLSFunctionAsTerm(); | ||
68 | final Procedure1<VLSFunctionAsTerm> _function = (VLSFunctionAsTerm it) -> { | ||
69 | it.setFunctor(term.getFunctor()); | ||
70 | }; | ||
71 | return ObjectExtensions.<VLSFunctionAsTerm>operator_doubleArrow(_createVLSFunctionAsTerm, _function); | ||
72 | } | ||
73 | |||
74 | protected VLSConstant duplicate(final VLSConstant term) { | ||
75 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
76 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
77 | it.setName(term.getName()); | ||
78 | }; | ||
79 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
80 | } | ||
81 | |||
65 | protected VLSFunction duplicate(final VLSFunction term) { | 82 | protected VLSFunction duplicate(final VLSFunction term) { |
66 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 83 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
67 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 84 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
@@ -87,6 +104,25 @@ public class Logic2VampireLanguageMapper_Support { | |||
87 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 104 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
88 | } | 105 | } |
89 | 106 | ||
107 | protected VLSFunction duplicate(final VLSFunction term, final VLSFunctionAsTerm v) { | ||
108 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
109 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
110 | it.setConstant(term.getConstant()); | ||
111 | EList<VLSTerm> _terms = it.getTerms(); | ||
112 | VLSFunctionAsTerm _duplicate = this.duplicate(v); | ||
113 | _terms.add(_duplicate); | ||
114 | }; | ||
115 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
116 | } | ||
117 | |||
118 | protected VLSConstant toConstant(final VLSFunctionAsTerm term) { | ||
119 | VLSConstant _createVLSConstant = this.factory.createVLSConstant(); | ||
120 | final Procedure1<VLSConstant> _function = (VLSConstant it) -> { | ||
121 | it.setName(term.getFunctor()); | ||
122 | }; | ||
123 | return ObjectExtensions.<VLSConstant>operator_doubleArrow(_createVLSConstant, _function); | ||
124 | } | ||
125 | |||
90 | protected VLSFunction topLevelTypeFunc() { | 126 | protected VLSFunction topLevelTypeFunc() { |
91 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | 127 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); |
92 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | 128 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { |
@@ -102,6 +138,17 @@ public class Logic2VampireLanguageMapper_Support { | |||
102 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | 138 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); |
103 | } | 139 | } |
104 | 140 | ||
141 | protected VLSFunction topLevelTypeFunc(final VLSFunctionAsTerm v) { | ||
142 | VLSFunction _createVLSFunction = this.factory.createVLSFunction(); | ||
143 | final Procedure1<VLSFunction> _function = (VLSFunction it) -> { | ||
144 | it.setConstant("object"); | ||
145 | EList<VLSTerm> _terms = it.getTerms(); | ||
146 | VLSFunctionAsTerm _duplicate = this.duplicate(v); | ||
147 | _terms.add(_duplicate); | ||
148 | }; | ||
149 | return ObjectExtensions.<VLSFunction>operator_doubleArrow(_createVLSFunction, _function); | ||
150 | } | ||
151 | |||
105 | public VLSTerm establishUniqueness(final List<VLSConstant> terms) { | 152 | public VLSTerm establishUniqueness(final List<VLSConstant> terms) { |
106 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); | 153 | final List<VLSInequality> eqs = CollectionLiterals.<VLSInequality>newArrayList(); |
107 | List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); | 154 | List<VLSConstant> _subList = terms.subList(1, ((Object[])Conversions.unwrapArray(terms, Object.class)).length); |