From 54f93b02b69f83054111d6388d01b95bf96a48e7 Mon Sep 17 00:00:00 2001 From: OszkarSemerath Date: Wed, 16 Aug 2017 17:18:54 +0200 Subject: SMT support for primitive types --- .../smt/reasoner/SmtModelInterpretation.xtend | 31 +++++++++++++++++----- 1 file changed, 24 insertions(+), 7 deletions(-) (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner') 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 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTFunctionDeclaration +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral +import java.util.TreeSet +import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealLiteral @Data class ValueType { @@ -29,6 +32,7 @@ class SmtModelInterpretation implements LogicModelInterpretation { @Accessors(PUBLIC_GETTER) val SmtModelQueryEngine queryEngine; // Trace info + val SMTDocument document val Logic2SmtMapperTrace newTrace; val Logic2SMT_TypeMapperInterpretation typeInterpretation @@ -39,7 +43,7 @@ class SmtModelInterpretation implements LogicModelInterpretation { */ new(LogicProblem problem, SMTDocument document, Logic2SmtMapper forwardMapper, Logic2SmtMapperTrace forwardTrace) { //document.input.typeDeclarations.forEach[typeNames.put(it.name,it)] - + this.document = document this.queryEngine = new SmtModelQueryEngine(document) this.newTrace = initialiseNewTrace(document,forwardTrace) this.typeInterpretation = forwardMapper.typeMapper.getTypeInterpretation(problem,document,this,newTrace) @@ -155,13 +159,26 @@ class SmtModelInterpretation implements LogicModelInterpretation { throw new UnsupportedOperationException } - override getMaximalInteger() { - 100 - //throw new UnsupportedOperationException("TODO: auto-generated method stub") + override getAllIntegersInStructure() { + val res = new TreeSet + for(literal : document.eAllContents.filter(SMTIntLiteral).toIterable) { + res += literal.value + res += -literal.value + } + res + } + + override getAllRealsInStructure() { + val res = new TreeSet + for(literal : document.eAllContents.filter(SMTRealLiteral).toIterable) { + res += literal.value + res += -literal.value + } + res } - override getMinimalInteger() { - -100 - //throw new UnsupportedOperationException("TODO: auto-generated method stub") + override getAllStringsInStructure() { + new TreeSet } + } \ No newline at end of file -- cgit v1.2.3-70-g09d2