Initial commit of the configuration language and application

3 files changed, 74 insertions, 0 deletions

diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
new file mode 100644
index 00000000..e511a961
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
@@ -0,0 +1,17 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.formulacanonization

+

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion

+import java.util.Map

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition

+import org.eclipse.xtend.lib.annotations.Data

+

+@Data

+class CanonisedFormulae {

+        CharSequence viatraCode

+        Map<Assertion,String> assertion2ConstraintPattern

+        Map<ConstantDefinition,String> constant2ValuePattern

+        Map<RelationDefinition,String> relation2ValuePattern

+        Map<FunctionDefinition,String> function2ValuePattern

+}
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
new file mode 100644
index 00000000..0af0b36a
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
@@ -0,0 +1,21 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.formulacanonization

+

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Assertion

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.ConstantDefinition

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition

+import java.util.List

+

+/**

+ * Translates a set of assertions and definitions to viatra patterns.

+ */

+class FormulaCanoniser {

+        def canonise(

+                List<Assertion> assertions,

+                List<RelationDefinition> relations,

+                List<ConstantDefinition> constants,

+                List<FunctionDefinition> functions)

+        {

+                

+        }

+}
\ No newline at end of file
diff --git a/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaRewriter.xtend b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaRewriter.xtend
new file mode 100644
index 00000000..af34a5a7
--- /dev/null
+++ b/Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaRewriter.xtend
@@ -0,0 +1,36 @@
+package hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra.formulacanonization

+

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term

+import org.eclipse.emf.ecore.util.EcoreUtil

+import java.util.LinkedList

+import java.util.List

+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable

+import org.eclipse.xtend.lib.annotations.Data

+

+

+@Data

+class Clause {

+        List<Term> atomicExpressions

+}

+

+/**

+ * Rewrites a term to a first order CNF, where F

+ * <p><table>

+ * <tr><th>Symbol</th><th>-></th><th>expression</th></tr>

+ * <tr><td>F</td><td>-></td><td>Quantified (∨ Quantified)*</td></tr>

+ * <tr><td>Quantified</td><td>-></td><td>(∃x Quantified) | Clause</td></tr>

+ * <tr><td>Clause</td><td>-></td><td> Atomic (∧ Atomic)* </td></tr>

+ * <tr><td>Atomic</td><td>-></td><td> Type(x) | Path (x,y) | x==y | x!=y | F | ¬F </td></tr>

+ * </table></p>

+ */

+class FormulaRewriter {

+        public def rewriteExpression(Term expression) {

+                val termToRewrite = EcoreUtil.copy(expression

+                )

+        }

+        

+        public def internalRewriteExpression(Term expression) {

+                val List<Variable> quantifiedVariables = new LinkedList

+                val List<Clause> clauses = new LinkedList

+        }

+}
\ No newline at end of file