diff options
Diffstat (limited to 'Solvers/SMT-Solver/hu.bme.mit.inf.dslreasoner.smt.reasoner/src/hu/bme')
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 | |||
80 | import org.eclipse.xtext.xbase.lib.Functions.Function2 | 80 | import org.eclipse.xtext.xbase.lib.Functions.Function2 |
81 | 81 | ||
82 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* | 82 | import static extension hu.bme.mit.inf.dslreasoner.util.CollectionsUtil.* |
83 | import java.math.BigDecimal | ||
83 | 84 | ||
84 | class Logic2SmtMapper{ | 85 | class Logic2SmtMapper{ |
85 | val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE | 86 | val extension SmtLanguageFactory factory = SmtLanguageFactory.eINSTANCE |
@@ -525,7 +526,7 @@ class Logic2SmtMapper{ | |||
525 | if(literal.value>=0) { new NumericSubterm(#[],#[],createSMTIntLiteral => [value = literal.value])} | 526 | if(literal.value>=0) { new NumericSubterm(#[],#[],createSMTIntLiteral => [value = literal.value])} |
526 | else {new NumericSubterm(#[],#[],createSMTMinus => [ leftOperand = (createSMTIntLiteral => [value = - (literal.value) ] ) ]) } } | 527 | else {new NumericSubterm(#[],#[],createSMTMinus => [ leftOperand = (createSMTIntLiteral => [value = - (literal.value) ] ) ]) } } |
527 | def dispatch protected TransformedSubterm transformTerm(RealLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { | 528 | def dispatch protected TransformedSubterm transformTerm(RealLiteral literal, Logic2SmtMapperTrace trace, Map<Variable, SMTSortedVariable> variables) { |
528 | new NumericSubterm(#[],#[],createSMTRealLiteral => [value = literal.value]) } | 529 | new NumericSubterm(#[],#[],createSMTRealLiteral => [value = BigDecimal.valueOf(literal.value)]) } |
529 | 530 | ||
530 | /////////////////////////////////////////////////////// | 531 | /////////////////////////////////////////////////////// |
531 | // NumericOperators | 532 | // 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 | |||
20 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral | 20 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTIntLiteral |
21 | import java.util.TreeSet | 21 | import java.util.TreeSet |
22 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealLiteral | 22 | import hu.bme.mit.inf.dslreasoner.smtLanguage.SMTRealLiteral |
23 | import java.math.BigDecimal | ||
23 | 24 | ||
24 | @Data | 25 | @Data |
25 | class ValueType { | 26 | class ValueType { |
@@ -124,7 +125,7 @@ class SmtModelInterpretation implements LogicModelInterpretation { | |||
124 | // } | 125 | // } |
125 | 126 | ||
126 | override getElements(Type type) { | 127 | override getElements(Type type) { |
127 | return this.typeInterpretation.getElements(type) | 128 | return this.typeInterpretation.getElements(type) |
128 | } | 129 | } |
129 | 130 | ||
130 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { | 131 | override getInterpretation(FunctionDeclaration function, Object[] parameterSubstitution) { |
@@ -171,8 +172,8 @@ class SmtModelInterpretation implements LogicModelInterpretation { | |||
171 | override getAllRealsInStructure() { | 172 | override getAllRealsInStructure() { |
172 | val res = new TreeSet | 173 | val res = new TreeSet |
173 | for(literal : document.eAllContents.filter(SMTRealLiteral).toIterable) { | 174 | for(literal : document.eAllContents.filter(SMTRealLiteral).toIterable) { |
174 | res += literal.value | 175 | res += literal.value.doubleValue |
175 | res += -literal.value | 176 | res += -literal.value.doubleValue |
176 | } | 177 | } |
177 | res | 178 | res |
178 | } | 179 | } |