fixed bigdecimal <-> double casting error

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<Variable, SMTSortedVariable> 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

         }