From 48b83f69fba64f2846651ad470269cc01ad7fd65 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Thu, 26 Nov 2020 13:55:37 +0100 Subject: Fix Z3 dependency --- .../hu.bme.mit.inf.dslreasoner.viatra2logic/.classpath | 11 +++++------ .../META-INF/MANIFEST.MF | 8 ++++---- .../lib/.gitignore | 0 .../dslreasoner/viatra2logic/NumericProblemSolver.java | 10 +--------- .../dslreasoner/viatra2logic/NumericTranslator.xtend | 18 ++++++++---------- 5 files changed, 18 insertions(+), 29 deletions(-) delete mode 100644 Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/lib/.gitignore (limited to 'Framework') diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/.classpath b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/.classpath index 849e2a7b..2a747353 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/.classpath +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/.classpath @@ -1,14 +1,13 @@ - - - - - + - + + + + diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF index c7242106..23fba304 100644 --- a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF +++ b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/META-INF/MANIFEST.MF @@ -20,11 +20,11 @@ Require-Bundle: com.google.guava, org.eclipse.viatra.query.patternlanguage.emf;bundle-version="2.0.0", org.eclipse.xtext, org.eclipse.xtext.xbase;bundle-version="2.18.0", - hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0" + hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage;bundle-version="1.0.0", + com.microsoft.z3 Bundle-ActivationPolicy: lazy -Export-Package: hu.bme.mit.inf.dslreasoner.viatra2logic, +Export-Package: + hu.bme.mit.inf.dslreasoner.viatra2logic, hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations, hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.impl, hu.bme.mit.inf.dslreasoner.viatra2logic.viatra2logicannotations.util -Automatic-Module-Name: hu.bme.mit.inf.dslreasoner.viatra2logic - diff --git a/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/lib/.gitignore b/Framework/hu.bme.mit.inf.dslreasoner.viatra2logic/lib/.gitignore deleted file mode 100644 index e69de29b..00000000 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 @@ package hu.bme.mit.inf.dslreasoner.viatra2logic; -import java.math.BigDecimal; import java.util.ArrayList; import java.util.HashMap; -import java.util.HashSet; import java.util.List; import java.util.Map; -import java.util.Map.Entry; -import java.util.Random; -import java.util.Set; -import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint; -import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation; import org.eclipse.xtext.common.types.JvmIdentifiableElement; import org.eclipse.xtext.xbase.XBinaryOperation; import org.eclipse.xtext.xbase.XExpression; @@ -29,10 +22,9 @@ import com.microsoft.z3.Solver; import com.microsoft.z3.Status; import com.microsoft.z3.enumerations.Z3_ast_print_mode; -import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Term; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.IntegerElement; -import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement; +import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.RealElement; 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 @@ package hu.bme.mit.inf.dslreasoner.viatra2logic -import org.eclipse.xtext.xbase.XExpression -import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation -import org.eclipse.xtext.common.types.JvmIdentifiableElement -import java.util.Set import hu.bme.mit.inf.dslreasoner.viatrasolver.partialinterpretationlanguage.partialinterpretation.PrimitiveElement -import java.util.Map -import com.microsoft.z3.BoolExpr -import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint -import java.util.Map.Entry -import org.eclipse.xtext.xbase.XFeatureCall -import java.util.Comparator import java.util.ArrayList +import java.util.Comparator import java.util.HashMap import java.util.List +import java.util.Map +import java.util.Map.Entry +import org.eclipse.viatra.query.runtime.matchers.psystem.PConstraint +import org.eclipse.viatra.query.runtime.matchers.psystem.basicdeferred.ExpressionEvaluation +import org.eclipse.xtext.common.types.JvmIdentifiableElement +import org.eclipse.xtext.xbase.XExpression +import org.eclipse.xtext.xbase.XFeatureCall class NumericTranslator { -- cgit v1.2.3-54-g00ecf