blob: af34a5a772100a9b39d6d2fdc6fa0f59234a5f15 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
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
}
}
|
