From f87b4233437f0900c19f462b5e443a3c81b27b6e Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Tue, 15 Jan 2019 12:44:33 -0500 Subject: Initial workspace setup --- .../dslreasoner/vampire/test/.SimpleRun.xtendbin | Bin 0 -> 687 bytes .../dslreasoner/vampire/test/.VampireTest.xtendbin | Bin 0 -> 6302 bytes .../ecse/dslreasoner/vampire/test/.gitignore | 2 + .../ecse/dslreasoner/vampire/test/VampireTest.java | 140 +++++++++++++++++++++ 4 files changed, 142 insertions(+) create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.gitignore create mode 100644 Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/VampireTest.java (limited to 'Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca') 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 Binary files /dev/null and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.SimpleRun.xtendbin 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 Binary files /dev/null and b/Tests/ca.mcgill.ecse.dslreasoner.vampire.test/xtend-gen/ca/mcgill/ecse/dslreasoner/vampire/test/.VampireTest.xtendbin 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 @@ +/.VampireTest.java._trace +/.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 @@ +package ca.mcgill.ecse.dslreasoner.vampire.test; + +import ca.mcgill.ecse.dslreasoner.VampireLanguageStandaloneSetup; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolver; +import ca.mcgill.ecse.dslreasoner.vampire.reasoner.VampireSolverConfiguration; +import hu.bme.mit.inf.dslreasoner.ecore2logic.ecore2logicannotations.Ecore2logicannotationsPackage; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicProblemBuilder; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.LogicReasoner; +import hu.bme.mit.inf.dslreasoner.logic.model.builder.VariableContext; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.And; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDeclaration; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Exists; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Iff; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Not; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Or; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Relation; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.TermDescription; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type; +import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable; +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem; +import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicproblemPackage; +import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult; +import hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.Viatra2LogicAnnotationsPackage; +import hu.bme.mit.inf.dslreasoner.workspace.FileSystemWorkspace; +import java.util.Collections; +import java.util.Map; +import org.eclipse.emf.common.util.EList; +import org.eclipse.emf.common.util.URI; +import org.eclipse.emf.ecore.resource.Resource; +import org.eclipse.emf.ecore.resource.impl.ResourceSetImpl; +import org.eclipse.emf.ecore.xmi.impl.XMIResourceFactoryImpl; +import org.eclipse.xtend2.lib.StringConcatenation; +import org.eclipse.xtext.xbase.lib.Exceptions; +import org.eclipse.xtext.xbase.lib.Extension; +import org.eclipse.xtext.xbase.lib.Functions.Function1; +import org.eclipse.xtext.xbase.lib.InputOutput; +import org.eclipse.xtext.xbase.lib.ObjectExtensions; +import org.eclipse.xtext.xbase.lib.Procedures.Procedure1; + +@SuppressWarnings("all") +public class VampireTest { + @Extension + private final static LogicProblemBuilder builder = new LogicProblemBuilder(); + + public static void main(final String[] args) { + try { + LogicproblemPackage.eINSTANCE.eClass(); + Ecore2logicannotationsPackage.eINSTANCE.eClass(); + Viatra2LogicAnnotationsPackage.eINSTANCE.eClass(); + final Resource.Factory.Registry reg = Resource.Factory.Registry.INSTANCE; + final Map map = reg.getExtensionToFactoryMap(); + XMIResourceFactoryImpl _xMIResourceFactoryImpl = new XMIResourceFactoryImpl(); + map.put("logicproblem", _xMIResourceFactoryImpl); + VampireLanguageStandaloneSetup.doSetup(); + StringConcatenation _builder = new StringConcatenation(); + _builder.append("output/models/"); + final FileSystemWorkspace workspace = new FileSystemWorkspace(_builder.toString(), ""); + workspace.initAndClear(); + final ResourceSetImpl rs = new ResourceSetImpl(); + final URI logicURI = URI.createFileURI("output/files/logProb.logicproblem"); + final Resource logRes = rs.createResource(logicURI); + LogicProblem problem = VampireTest.builder.createProblem(); + VampireTest.deMorgan(problem); + logRes.getContents().add(problem); + logRes.save(Collections.EMPTY_MAP); + InputOutput.println("Problem Created"); + LogicResult solution = null; + LogicReasoner reasoner = null; + VampireSolver _vampireSolver = new VampireSolver(); + reasoner = _vampireSolver; + VampireSolverConfiguration _vampireSolverConfiguration = new VampireSolverConfiguration(); + final Procedure1 _function = (VampireSolverConfiguration it) -> { + it.writeToFile = false; + }; + final VampireSolverConfiguration vampireConfig = ObjectExtensions.operator_doubleArrow(_vampireSolverConfiguration, _function); + solution = reasoner.solve(problem, vampireConfig, workspace); + InputOutput.println("Problem Solved"); + } catch (Throwable _e) { + throw Exceptions.sneakyThrow(_e); + } + } + + public static Assertion deMorgan(final LogicProblem problem) { + Assertion _xblockexpression = null; + { + ConstantDeclaration X = VampireTest.builder.ConstantDeclaration(VampireTest.builder.LogicBool()); + ConstantDeclaration Y = VampireTest.builder.ConstantDeclaration(VampireTest.builder.LogicBool()); + VampireTest.builder.add(problem, X); + VampireTest.builder.add(problem, Y); + And _and = VampireTest.builder.operator_and(X, Y); + Not _not = VampireTest.builder.operator_not(_and); + Not _not_1 = VampireTest.builder.operator_not(X); + Not _not_2 = VampireTest.builder.operator_not(Y); + Or _or = VampireTest.builder.operator_or(_not_1, _not_2); + Iff _spaceship = VampireTest.builder.operator_spaceship(_not, _or); + _xblockexpression = VampireTest.builder.add(problem, VampireTest.builder.Assertion(_spaceship)); + } + return _xblockexpression; + } + + public static Assertion rockPaperScisors(final LogicProblem problem) { + Assertion _xblockexpression = null; + { + final DefinedElement rock = VampireTest.builder.Element("Rock"); + final DefinedElement paper = VampireTest.builder.Element("Paper"); + final DefinedElement scissor = VampireTest.builder.Element("Scissor"); + EList _elements = problem.getElements(); + _elements.add(rock); + EList _elements_1 = problem.getElements(); + _elements_1.add(paper); + EList _elements_2 = problem.getElements(); + _elements_2.add(scissor); + final Type oldRPS = VampireTest.builder.add(problem, VampireTest.builder.TypeDefinition("oldRPS", false, rock, paper, scissor)); + final Relation beats2 = VampireTest.builder.add(problem, VampireTest.builder.RelationDeclaration("beats2", oldRPS, oldRPS)); + final Function1 _function = (VariableContext it) -> { + Exists _xblockexpression_1 = null; + { + final Variable x = it.addVar("x", oldRPS); + final Function1 _function_1 = (VariableContext it_1) -> { + SymbolicValue _xblockexpression_2 = null; + { + final Variable y = it_1.addVar("y", oldRPS); + _xblockexpression_2 = VampireTest.builder.call(beats2, x, y); + } + return _xblockexpression_2; + }; + _xblockexpression_1 = VampireTest.builder.Exists(_function_1); + } + return _xblockexpression_1; + }; + _xblockexpression = VampireTest.builder.add(problem, + VampireTest.builder.Assertion( + VampireTest.builder.Forall(_function))); + } + return _xblockexpression; + } +} -- cgit v1.2.3-70-g09d2