diff options
author | OszkarSemerath <oszka@SEMERATH-LAPTOP> | 2017-08-16 17:18:54 +0200 |
---|---|---|
committer | OszkarSemerath <oszka@SEMERATH-LAPTOP> | 2017-08-16 17:18:54 +0200 |
commit | 54f93b02b69f83054111d6388d01b95bf96a48e7 (patch) | |
tree | c1e598c5ed867cb5d66a500298018f5e2359d92d /Solvers/SMT-Solver | |
parent | Mapping of primitive types in patterns (diff) | |
download | VIATRA-Generator-54f93b02b69f83054111d6388d01b95bf96a48e7.tar.gz VIATRA-Generator-54f93b02b69f83054111d6388d01b95bf96a48e7.tar.zst VIATRA-Generator-54f93b02b69f83054111d6388d01b95bf96a48e7.zip |
SMT support for primitive types
Diffstat (limited to 'Solvers/SMT-Solver')
-rw-r--r-- | Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend | 31 |
1 files changed, 24 insertions, 7 deletions
diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend index fb0739ab..1dde2333 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend | |||
@@ -17,6 +17,9 @@ import org.eclipse.xtend.lib.annotations.Data | |||
17 | 17 | ||
18 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 18 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
19 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration | 19 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration |
20 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral | ||
21 | import java.util.TreeSet | ||
22 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealLiteral | ||
20 | 23 | ||
21 | @Data | 24 | @Data |
22 | class ValueType { | 25 | class ValueType { |
@@ -29,6 +32,7 @@ class SmtModelInterpretation implements LogicModelInterpretation { | |||
29 | @Accessors(PUBLIC_GETTER) val SmtModelQueryEngine queryEngine; | 32 | @Accessors(PUBLIC_GETTER) val SmtModelQueryEngine queryEngine; |
30 | 33 | ||
31 | // Trace info | 34 | // Trace info |
35 | val SMTDocument document | ||
32 | val Logic2SmtMapperTrace newTrace; | 36 | val Logic2SmtMapperTrace newTrace; |
33 | val Logic2SMT_TypeMapperInterpretation typeInterpretation | 37 | val Logic2SMT_TypeMapperInterpretation typeInterpretation |
34 | 38 | ||
@@ -39,7 +43,7 @@ class SmtModelInterpretation implements LogicModelInterpretation { | |||
39 | */ | 43 | */ |
40 | new(LogicProblem problem, SMTDocument document, Logic2SmtMapper forwardMapper, Logic2SmtMapperTrace forwardTrace) { | 44 | new(LogicProblem problem, SMTDocument document, Logic2SmtMapper forwardMapper, Logic2SmtMapperTrace forwardTrace) { |
41 | //document.input.typeDeclarations.forEach[typeNames.put(it.name,it)] | 45 | //document.input.typeDeclarations.forEach[typeNames.put(it.name,it)] |
42 | 46 | this.document = document | |
43 | this.queryEngine = new SmtModelQueryEngine(document) | 47 | this.queryEngine = new SmtModelQueryEngine(document) |
44 | this.newTrace = initialiseNewTrace(document,forwardTrace) | 48 | this.newTrace = initialiseNewTrace(document,forwardTrace) |
45 | this.typeInterpretation = forwardMapper.typeMapper.getTypeInterpretation(problem,document,this,newTrace) | 49 | this.typeInterpretation = forwardMapper.typeMapper.getTypeInterpretation(problem,document,this,newTrace) |
@@ -155,13 +159,26 @@ class SmtModelInterpretation implements LogicModelInterpretation { | |||
155 | throw new UnsupportedOperationException | 159 | throw new UnsupportedOperationException |
156 | } | 160 | } |
157 | 161 | ||
158 | override getMaximalInteger() { | 162 | override getAllIntegersInStructure() { |
159 | 100 | 163 | val res = new TreeSet |
160 | //throw new UnsupportedOperationException("TODO: auto-generated method stub") | 164 | for(literal : document.eAllContents.filter(SMTIntLiteral).toIterable) { |
165 | res += literal.value | ||
166 | res += -literal.value | ||
167 | } | ||
168 | res | ||
169 | } | ||
170 | |||
171 | override getAllRealsInStructure() { | ||
172 | val res = new TreeSet | ||
173 | for(literal : document.eAllContents.filter(SMTRealLiteral).toIterable) { | ||
174 | res += literal.value | ||
175 | res += -literal.value | ||
176 | } | ||
177 | res | ||
161 | } | 178 | } |
162 | 179 | ||
163 | override getMinimalInteger() { | 180 | override getAllStringsInStructure() { |
164 | -100 | 181 | new TreeSet |
165 | //throw new UnsupportedOperationException("TODO: auto-generated method stub") | ||
166 | } | 182 | } |
183 | |||
167 | } \ No newline at end of file | 184 | } \ No newline at end of file |