From 7e50434905cbb7f5d03636033b698e17a9075e9d Mon Sep 17 00:00:00 2001
From: OszkarSemerath <oszka@SEMERATH-LAPTOP>
Date: Sat, 13 Jan 2018 19:33:26 +0100
Subject: Initial commit of the configuration language and application

---
 .../formulacanonization/CanonisedFormulae.xtend    | 17 ++++++++++
 .../formulacanonization/FormulaCanoniser.xtend     | 21 +++++++++++++
 .../formulacanonization/FormulaRewriter.xtend      | 36 ++++++++++++++++++++++
 3 files changed, 74 insertions(+)
 create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/CanonisedFormulae.xtend
 create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaCanoniser.xtend
 create mode 100644 Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization/FormulaRewriter.xtend

(limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf')

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
-- 
cgit v1.2.3-70-g09d2