1 files changed, 27 insertions, 9 deletions

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