From 7e50434905cbb7f5d03636033b698e17a9075e9d Mon Sep 17 00:00:00 2001
From: OszkarSemerath
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 assertion2ConstraintPattern
+ Map constant2ValuePattern
+ Map relation2ValuePattern
+ Map 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 assertions,
+ List relations,
+ List constants,
+ List 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 atomicExpressions
+}
+
+/**
+ * Rewrites a term to a first order CNF, where F
+ *
+ * Symbol | -> | expression |
+ * F | -> | Quantified (∨ Quantified)* |
+ * Quantified | -> | (∃x Quantified) | Clause |
+ * Clause | -> | Atomic (∧ Atomic)* |
+ * Atomic | -> | Type(x) | Path (x,y) | x==y | x!=y | F | ¬F |
+ *
+ */
+class FormulaRewriter {
+ public def rewriteExpression(Term expression) {
+ val termToRewrite = EcoreUtil.copy(expression
+ )
+ }
+
+ public def internalRewriteExpression(Term expression) {
+ val List quantifiedVariables = new LinkedList
+ val List clauses = new LinkedList
+ }
+}
\ No newline at end of file
--
cgit v1.2.3-70-g09d2