blob: 71cfd0e006586ceae7276269acbd50a084c391c1 (
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
37
38
|
package hu.bme.mit.inf.dslreasoner.smt.reasoner
import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm
import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTypeReference
import java.util.List
import org.eclipse.emf.ecore.util.EcoreUtil
import org.eclipse.xtend.lib.annotations.Data
import org.eclipse.xtext.xbase.lib.Functions.Function1
interface Logic2Smt_TypeMapper {
def void transformTypes(
SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes)
def List<TypeConstraint> transformTypeReference(Type type, Logic2SmtMapperTrace trace)
def TransformedSubterm transformSymbolicReference(DefinedElement referred, Logic2SmtMapperTrace trace)
def Logic2SMT_TypeMapperInterpretation getTypeInterpretation(LogicProblem problem,SMTDocument document,SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace)
}
@Data
class TypeConstraint {
SMTTypeReference type
Function1<SMTSortedVariable,SMTTerm> constraint
def public copy() {
return new TypeConstraint(EcoreUtil.copy(this.type),this.constraint)
}
}
interface Logic2Smt_TypeMapperTrace{
def Logic2Smt_TypeMapperTrace copy(SMTInput newModel)
}
|
