diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend new file mode 100644 index 00000000..71cfd0e0 --- /dev/null +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2Smt_TypeMapper.xtend | |||
@@ -0,0 +1,38 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.smt.reasoner | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.TypeScopes | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.DefinedElement | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem | ||
7 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTDocument | ||
8 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTInput | ||
9 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTSortedVariable | ||
10 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTerm | ||
11 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTTypeReference | ||
12 | import java.util.List | ||
13 | import org.eclipse.emf.ecore.util.EcoreUtil | ||
14 | import org.eclipse.xtend.lib.annotations.Data | ||
15 | import org.eclipse.xtext.xbase.lib.Functions.Function1 | ||
16 | |||
17 | interface Logic2Smt_TypeMapper { | ||
18 | def void transformTypes( | ||
19 | SMTInput document, LogicProblem problem, Logic2SmtMapperTrace trace, TypeScopes scopes) | ||
20 | |||
21 | def List<TypeConstraint> transformTypeReference(Type type, Logic2SmtMapperTrace trace) | ||
22 | def TransformedSubterm transformSymbolicReference(DefinedElement referred, Logic2SmtMapperTrace trace) | ||
23 | def Logic2SMT_TypeMapperInterpretation getTypeInterpretation(LogicProblem problem,SMTDocument document,SmtModelInterpretation interpretation, Logic2SmtMapperTrace trace) | ||
24 | } | ||
25 | |||
26 | @Data | ||
27 | class TypeConstraint { | ||
28 | SMTTypeReference type | ||
29 | Function1<SMTSortedVariable,SMTTerm> constraint | ||
30 | |||
31 | def public copy() { | ||
32 | return new TypeConstraint(EcoreUtil.copy(this.type),this.constraint) | ||
33 | } | ||
34 | } | ||
35 | |||
36 | interface Logic2Smt_TypeMapperTrace{ | ||
37 | def Logic2Smt_TypeMapperTrace copy(SMTInput newModel) | ||
38 | } \ No newline at end of file | ||