diff options
Diffstat (limited to 'Solvers/VIATRA-Solver/hu.bme.mit.inf.dslreasoner.viatrasolver.logic2viatra/src/hu/bme/mit/inf/dslreasoner/viatrasolver/logic2viatra/formulacanonization')
2 files changed, 27 insertions, 11 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 index e511a961..fd4374f5 100644 --- 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 | |||
@@ -11,7 +11,5 @@ import org.eclipse.xtend.lib.annotations.Data | |||
11 | class CanonisedFormulae { | 11 | class CanonisedFormulae { |
12 | CharSequence viatraCode | 12 | CharSequence viatraCode |
13 | Map<Assertion,String> assertion2ConstraintPattern | 13 | Map<Assertion,String> assertion2ConstraintPattern |
14 | Map<ConstantDefinition,String> constant2ValuePattern | ||
15 | Map<RelationDefinition,String> relation2ValuePattern | 14 | Map<RelationDefinition,String> relation2ValuePattern |
16 | Map<FunctionDefinition,String> function2ValuePattern | ||
17 | } \ No newline at end of file | 15 | } \ 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 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 | |||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition | 5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.FunctionDefinition |
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition | 6 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.RelationDefinition |
7 | import java.util.List | 7 | import java.util.List |
8 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term | ||
9 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.SymbolicValue | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Variable | ||
8 | 11 | ||
9 | /** | 12 | /** |
10 | * Translates a set of assertions and definitions to viatra patterns. | 13 | * Translates a Terms into format |
14 | * <P(x1,...,xn)> := Bodies(x1,...,xn) | ||
15 | * <Bodies(x1,...,xn)> := <Body(x1,...,xn)> | <Body(x1,...,xn)> or <Bodies(x1,...,xn)> | ||
16 | * <Body(x1,...,xn)> := Exists y1,...,ym : <Constraints(x1,...,xn,y1,....,ym)> | ||
17 | * <Constraints(x1,...,xn)> := Constraint(x1,...xn) | Constraint(x1,...,xn) and <Constraints(x1,...,xn)> | ||
11 | */ | 18 | */ |
12 | class FormulaCanoniser { | 19 | class FormulaCanoniser { |
13 | def canonise( | 20 | // def canonise( |
14 | List<Assertion> assertions, | 21 | // List<Assertion> assertions, |
15 | List<RelationDefinition> relations, | 22 | // List<RelationDefinition> relations) |
16 | List<ConstantDefinition> constants, | 23 | // { |
17 | List<FunctionDefinition> functions) | 24 | // |
18 | { | 25 | // } |
19 | 26 | // | |
20 | } | 27 | // |
28 | // def canoniseToConstraintBlock(Term predicate, List<Variable> variables) { | ||
29 | // val | ||
30 | // } | ||
31 | // | ||
32 | // def freeVariables(Term t) { | ||
33 | // val subterms = #[t]+t.eAllContents.toList | ||
34 | // val variables = subterms.filter(Variable).toSet | ||
35 | // val variableReferences = subterms.filter(SymbolicValue).filter[it.symbolicReference instanceof Variable] | ||
36 | // val freeVariables = variableReferences.filter[!variables.contains(it.symbolicReference)] | ||
37 | // return freeVariables.map | ||
38 | // } | ||
21 | } \ No newline at end of file | 39 | } \ No newline at end of file |