From ed434397058fd520ad92a938eccd8f93ef378d8a Mon Sep 17 00:00:00 2001
From: Oszkar Semerath <semerath@mit.bme.hu>
Date: Tue, 14 Apr 2020 22:45:52 +0200
Subject: restructured pattern generation

---
 .../formulacanonization/FormulaCanoniser.xtend     | 36 ++++++++++++++++------
 1 file changed, 27 insertions(+), 9 deletions(-)

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

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
index 0af0b36a..182f3a3a 100644
--- 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
@@ -5,17 +5,35 @@ 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
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue
+import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable
 
 /**
- * Translates a set of assertions and definitions to viatra patterns.
+ * Translates a Terms into format
+ * <P(x1,...,xn)> := Bodies(x1,...,xn)
+ * <Bodies(x1,...,xn)> := <Body(x1,...,xn)> | <Body(x1,...,xn)> or <Bodies(x1,...,xn)>
+ * <Body(x1,...,xn)> := Exists y1,...,ym : <Constraints(x1,...,xn,y1,....,ym)>
+ * <Constraints(x1,...,xn)> := Constraint(x1,...xn) | Constraint(x1,...,xn) and <Constraints(x1,...,xn)>   
  */
 class FormulaCanoniser {
-	def canonise(
-		List<Assertion> assertions,
-		List<RelationDefinition> relations,
-		List<ConstantDefinition> constants,
-		List<FunctionDefinition> functions)
-	{
-		
-	}
+//	def canonise(
+//		List<Assertion> assertions,
+//		List<RelationDefinition> relations)
+//	{
+//		
+//	}
+//	
+//	
+//	def canoniseToConstraintBlock(Term predicate, List<Variable> variables) {
+//		val 
+//	}
+//	
+//	def freeVariables(Term t) {
+//		val subterms = #[t]+t.eAllContents.toList
+//		val variables = subterms.filter(Variable).toSet
+//		val variableReferences = subterms.filter(SymbolicValue).filter[it.symbolicReference instanceof Variable]
+//		val freeVariables = variableReferences.filter[!variables.contains(it.symbolicReference)]
+//		return freeVariables.map
+//	}
 }
\ No newline at end of file
-- 
cgit v1.2.3-54-g00ecf