diff options
| author |  Kristóf Marussy <marussy@mit.bme.hu> | 2020-11-26 13:55:37 +0100 |
|---|---|---|
| committer | Kristóf Marussy <marussy@mit.bme.hu> | 2020-11-26 13:55:37 +0100 |
| commit | 48b83f69fba64f2846651ad470269cc01ad7fd65 (patch) | |
| tree | bce325b21d5183951e1fa83c96870b375ee4d92f /Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src | |
| parent | Optimizing generator with linear objective functions (diff) | |
| download | VIATRA-Generator-48b83f69fba64f2846651ad470269cc01ad7fd65.tar.gz VIATRA-Generator-48b83f69fba64f2846651ad470269cc01ad7fd65.tar.zst VIATRA-Generator-48b83f69fba64f2846651ad470269cc01ad7fd65.zip | |
Fix Z3 dependency
Diffstat (limited to 'Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src')
2 files changed, 9 insertions, 19 deletions
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java index 0b249962..f1314925 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericProblemSolver.java | |||
| @@ -1,17 +1,10 @@ | |||
| 1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; | 1 | package hu.bme.mit.inf.dslreasoner.viatra2logic; |
| 2 | 2 | ||
| 3 | import java.math.BigDecimal; | ||
| 4 | import java.util.ArrayList; | 3 | import java.util.ArrayList; |
| 5 | import java.util.HashMap; | 4 | import java.util.HashMap; |
| 6 | import java.util.HashSet; | ||
| 7 | import java.util.List; | 5 | import java.util.List; |
| 8 | import java.util.Map; | 6 | import java.util.Map; |
| 9 | import java.util.Map.Entry; | ||
| 10 | import java.util.Random; | ||
| 11 | import java.util.Set; | ||
| 12 | 7 | ||
| 13 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint; | ||
| 14 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation; | ||
| 15 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; | 8 | import org.eclipse.xtext.common.types.JvmIdentifiableElement; |
| 16 | import org.eclipse.xtext.xbase.XBinaryOperation; | 9 | import org.eclipse.xtext.xbase.XBinaryOperation; |
| 17 | import org.eclipse.xtext.xbase.XExpression; | 10 | import org.eclipse.xtext.xbase.XExpression; |
| @@ -29,10 +22,9 @@ import com.microsoft.z3.Solver; | |||
| 29 | import com.microsoft.z3.Status; | 22 | import com.microsoft.z3.Status; |
| 30 | import com.microsoft.z3.enumerations.Z3_ast_print_mode; | 23 | import com.microsoft.z3.enumerations.Z3_ast_print_mode; |
| 31 | 24 | ||
| 32 | import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; | ||
| 33 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; | 25 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; |
| 34 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; | ||
| 35 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; | 26 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; |
| 27 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; | ||
| 36 | 28 | ||
| 37 | 29 | ||
| 38 | public class NumericProblemSolver { | 30 | public class NumericProblemSolver { |
diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend index 81bc1796..b9eda7b3 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/src/hu/bme/mit/inf/dslreasoner/viatra2logic/NumericTranslator.xtend | |||
| @@ -1,19 +1,17 @@ | |||
| 1 | package hu.bme.mit.inf.dslreasoner.viatra2logic | 1 | package hu.bme.mit.inf.dslreasoner.viatra2logic |
| 2 | 2 | ||
| 3 | import org.eclipse.xtext.xbase.XExpression | ||
| 4 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
| 5 | import org.eclipse.xtext.common.types.JvmIdentifiableElement | ||
| 6 | import java.util.Set | ||
| 7 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement | 3 | import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement |
| 8 | import java.util.Map | ||
| 9 | import com.microsoft.z3.BoolExpr | ||
| 10 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
| 11 | import java.util.Map.Entry | ||
| 12 | import org.eclipse.xtext.xbase.XFeatureCall | ||
| 13 | import java.util.Comparator | ||
| 14 | import java.util.ArrayList | 4 | import java.util.ArrayList |
| 5 | import java.util.Comparator | ||
| 15 | import java.util.HashMap | 6 | import java.util.HashMap |
| 16 | import java.util.List | 7 | import java.util.List |
| 8 | import java.util.Map | ||
| 9 | import java.util.Map.Entry | ||
| 10 | import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint | ||
| 11 | import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation | ||
| 12 | import org.eclipse.xtext.common.types.JvmIdentifiableElement | ||
| 13 | import org.eclipse.xtext.xbase.XExpression | ||
| 14 | import org.eclipse.xtext.xbase.XFeatureCall | ||
| 17 | 15 | ||
| 18 | class NumericTranslator { | 16 | class NumericTranslator { |
| 19 | 17 | ||