From 9323c0736434c6c1ec02a41652112eb4c3296010 Mon Sep 17 00:00:00 2001 From: oszkarsemerath Date: Mon, 3 May 2021 23:24:39 +0200 Subject: fixed bigdecimal <-> double casting error --- .../hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend | 3 ++- .../mit/inf/dslreasoner/smt/reasoner/SmtModelInterpretation.xtend | 7 ++++--- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend index 6f20b956..194eba37 100644 --- a/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend +++ b/Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme/mit/inf/dslreasoner/smt/reasoner/Logic2SmtMapper.xtend @@ -80,6 +80,7 @@ import org.eclipse.xtext.xbase.lib.Functions.Function1 import org.eclipse.xtext.xbase.lib.Functions.Function2 import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* +import java.math.BigDecimal class Logic2SmtMapper{ val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE @@ -525,7 +526,7 @@ class Logic2SmtMapper{ if(literal.value>=0) { new NumericSubterm(#[],#[],createSMTIntLiteral => [value = literal.value])} else {new NumericSubterm(#[],#[],createSMTMinus => [ leftOperand = (createSMTIntLiteral => [value = - (literal.value) ] ) ]) } } def dispatch protected TransformedSubterm transformTerm(RealLiteral literal, Logic2SmtMapperTrace trace, Map variables) { - new NumericSubterm(#[],#[],createSMTRealLiteral => [value = literal.value]) } + new NumericSubterm(#[],#[],createSMTRealLiteral => [value = BigDecimal.valueOf(literal.value)]) } /////////////////////////////////////////////////////// // NumericOperators 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 1dde2333..aa8579b1 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 @@ -20,6 +20,7 @@ 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 +import java.math.BigDecimal @Data class ValueType { @@ -124,7 +125,7 @@ class SmtModelInterpretation implements LogicModelInterpretation { // } override getElements(Type type) { - return this.typeInterpretation.getElements(type) + return this.typeInterpretation.getElements(type) } override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { @@ -171,8 +172,8 @@ class SmtModelInterpretation implements LogicModelInterpretation { override getAllRealsInStructure() { val res = new TreeSet for(literal : document.eAllContents.filter(SMTRealLiteral).toIterable) { - res += literal.value - res += -literal.value + res += literal.value.doubleValue + res += -literal.value.doubleValue } res } -- cgit v1.2.3-54-g00ecf