diff options
Diffstat (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill')
4 files changed, 142 insertions, 0 deletions
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin new file mode 100644 index 00000000..b60ffe4c --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin new file mode 100644 index 00000000..881f927c --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin | |||
Binary files differ | |||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore new file mode 100644 index 00000000..f3c47b99 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore | |||
@@ -0,0 +1,2 @@ | |||
1 | /.VampireTest.java._trace | ||
2 | /.SimpleRun.java._trace | ||
diff --git a/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java new file mode 100644 index 00000000..73c413b3 --- /dev/null +++ b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java | |||
@@ -0,0 +1,140 @@ | |||
1 | package ca.mcgill.ecse.dslreasoner.vampire.test; | ||
2 | |||
3 | import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup; | ||
4 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; | ||
5 | import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; | ||
6 | import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage; | ||
7 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder; | ||
8 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.VariableContext; | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; | ||
12 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; | ||
13 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; | ||
14 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists; | ||
15 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff; | ||
16 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; | ||
17 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; | ||
18 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; | ||
19 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; | ||
20 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription; | ||
21 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; | ||
22 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; | ||
23 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; | ||
24 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; | ||
25 | import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; | ||
26 | import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage; | ||
27 | import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; | ||
28 | import java.util.Collections; | ||
29 | import java.util.Map; | ||
30 | import org.eclipse.emf.common.util.EList; | ||
31 | import org.eclipse.emf.common.util.URI; | ||
32 | import org.eclipse.emf.ecore.resource.Resource; | ||
33 | import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl; | ||
34 | import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; | ||
35 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
36 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
37 | import org.eclipse.xtext.xbase.lib.Extension; | ||
38 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
39 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
40 | import org.eclipse.xtext.xbase.lib.ObjectExtensions; | ||
41 | import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; | ||
42 | |||
43 | @SuppressWarnings("all") | ||
44 | public class VampireTest { | ||
45 | @Extension | ||
46 | private final static LogicProblemBuilder builder = new LogicProblemBuilder(); | ||
47 | |||
48 | public static void main(final String[] args) { | ||
49 | try { | ||
50 | LogicproblemPackage.eINSTANCE.eClass(); | ||
51 | Ecore2logicannotationsPackage.eINSTANCE.eClass(); | ||
52 | Viatra2LogicAnnotationsPackage.eINSTANCE.eClass(); | ||
53 | final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; | ||
54 | final Map<String, Object> map = reg.getExtensionToFactoryMap(); | ||
55 | XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); | ||
56 | map.put("logicproblem", _xMIResourceFactoryImpl); | ||
57 | VampireLanguageStandaloneSetup.doSetup(); | ||
58 | StringConcatenation _builder = new StringConcatenation(); | ||
59 | _builder.append("output/models/"); | ||
60 | final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder.toString(), ""); | ||
61 | workspace.initAndClear(); | ||
62 | final ResourceSetImpl rs = new ResourceSetImpl(); | ||
63 | final URI logicURI = URI.createFileURI("output/files/logProb.logicproblem"); | ||
64 | final Resource logRes = rs.createResource(logicURI); | ||
65 | LogicProblem problem = VampireTest.builder.createProblem(); | ||
66 | VampireTest.deMorgan(problem); | ||
67 | logRes.getContents().add(problem); | ||
68 | logRes.save(Collections.EMPTY_MAP); | ||
69 | InputOutput.<String>println("Problem Created"); | ||
70 | LogicResult solution = null; | ||
71 | LogicReasoner reasoner = null; | ||
72 | VampireSolver _vampireSolver = new VampireSolver(); | ||
73 | reasoner = _vampireSolver; | ||
74 | VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); | ||
75 | final Procedure1<VampireSolverConfiguration> _function = (VampireSolverConfiguration it) -> { | ||
76 | it.writeToFile = false; | ||
77 | }; | ||
78 | final VampireSolverConfiguration vampireConfig = ObjectExtensions.<VampireSolverConfiguration>operator_doubleArrow(_vampireSolverConfiguration, _function); | ||
79 | solution = reasoner.solve(problem, vampireConfig, workspace); | ||
80 | InputOutput.<String>println("Problem Solved"); | ||
81 | } catch (Throwable _e) { | ||
82 | throw Exceptions.sneakyThrow(_e); | ||
83 | } | ||
84 | } | ||
85 | |||
86 | public static Assertion deMorgan(final LogicProblem problem) { | ||
87 | Assertion _xblockexpression = null; | ||
88 | { | ||
89 | ConstantDeclaration X = VampireTest.builder.ConstantDeclaration(VampireTest.builder.LogicBool()); | ||
90 | ConstantDeclaration Y = VampireTest.builder.ConstantDeclaration(VampireTest.builder.LogicBool()); | ||
91 | VampireTest.builder.add(problem, X); | ||
92 | VampireTest.builder.add(problem, Y); | ||
93 | And _and = VampireTest.builder.operator_and(X, Y); | ||
94 | Not _not = VampireTest.builder.operator_not(_and); | ||
95 | Not _not_1 = VampireTest.builder.operator_not(X); | ||
96 | Not _not_2 = VampireTest.builder.operator_not(Y); | ||
97 | Or _or = VampireTest.builder.operator_or(_not_1, _not_2); | ||
98 | Iff _spaceship = VampireTest.builder.operator_spaceship(_not, _or); | ||
99 | _xblockexpression = VampireTest.builder.add(problem, VampireTest.builder.Assertion(_spaceship)); | ||
100 | } | ||
101 | return _xblockexpression; | ||
102 | } | ||
103 | |||
104 | public static Assertion rockPaperScisors(final LogicProblem problem) { | ||
105 | Assertion _xblockexpression = null; | ||
106 | { | ||
107 | final DefinedElement rock = VampireTest.builder.Element("Rock"); | ||
108 | final DefinedElement paper = VampireTest.builder.Element("Paper"); | ||
109 | final DefinedElement scissor = VampireTest.builder.Element("Scissor"); | ||
110 | EList<DefinedElement> _elements = problem.getElements(); | ||
111 | _elements.add(rock); | ||
112 | EList<DefinedElement> _elements_1 = problem.getElements(); | ||
113 | _elements_1.add(paper); | ||
114 | EList<DefinedElement> _elements_2 = problem.getElements(); | ||
115 | _elements_2.add(scissor); | ||
116 | final Type oldRPS = VampireTest.builder.add(problem, VampireTest.builder.TypeDefinition("oldRPS", false, rock, paper, scissor)); | ||
117 | final Relation beats2 = VampireTest.builder.add(problem, VampireTest.builder.RelationDeclaration("beats2", oldRPS, oldRPS)); | ||
118 | final Function1<VariableContext, TermDescription> _function = (VariableContext it) -> { | ||
119 | Exists _xblockexpression_1 = null; | ||
120 | { | ||
121 | final Variable x = it.addVar("x", oldRPS); | ||
122 | final Function1<VariableContext, TermDescription> _function_1 = (VariableContext it_1) -> { | ||
123 | SymbolicValue _xblockexpression_2 = null; | ||
124 | { | ||
125 | final Variable y = it_1.addVar("y", oldRPS); | ||
126 | _xblockexpression_2 = VampireTest.builder.call(beats2, x, y); | ||
127 | } | ||
128 | return _xblockexpression_2; | ||
129 | }; | ||
130 | _xblockexpression_1 = VampireTest.builder.Exists(_function_1); | ||
131 | } | ||
132 | return _xblockexpression_1; | ||
133 | }; | ||
134 | _xblockexpression = VampireTest.builder.add(problem, | ||
135 | VampireTest.builder.Assertion( | ||
136 | VampireTest.builder.Forall(_function))); | ||
137 | } | ||
138 | return _xblockexpression; | ||
139 | } | ||
140 | } | ||