From be4f78978faba3d3ceb88df02a7f93a2e09ff1e0 Mon Sep 17 00:00:00 2001 From: Kenji Hosokawa Date: Tue, 3 Aug 2021 18:42:39 +0900 Subject: Initial commit Bug-AGL: SPEC-4033 Signed-off-by: Kenji Hosokawa --- rba.tool.core/src/rba/tool/core/Activator.java | 49 +++ .../src/rba/tool/core/console/ConsoleManager.java | 96 ++++++ .../src/rba/tool/core/console/IConsoleHook.java | 8 + .../src/rba/tool/core/console/IConsoleManager.java | 14 + .../core/constraint/IConstraintCalculation.java | 14 + .../src/rba/tool/core/marker/MarkerManager.java | 142 ++++++++ .../rba/tool/core/sort/ComparisonAndEvaluator.java | 49 +++ .../core/sort/ComparisonOperatorEvaluator.java | 49 +++ .../src/rba/tool/core/sort/EObjectDecorator.java | 118 +++++++ .../tool/core/sort/EqualToOperatorEvaluator.java | 52 +++ .../rba/tool/core/sort/ExpressionEvaluator.java | 55 ++++ .../core/sort/GreaterThanOperatorEvaluator.java | 64 ++++ .../rba/tool/core/sort/ISortValueCalculation.java | 15 + .../sort/MuchGreaterThanOperatorEvaluator.java | 67 ++++ .../src/rba/tool/core/sort/SortValue.java | 45 +++ .../src/rba/tool/core/sort/SortValueManager.java | 56 ++++ .../src/rba/tool/core/sort/ValueGroup.java | 35 ++ .../src/rba/tool/core/sort/ValueSortedList.java | 168 ++++++++++ .../tool/core/ui/BasicTableViewerColumnFilter.java | 72 +++++ .../src/rba/tool/core/ui/CommonValueValidator.java | 51 +++ .../src/rba/tool/core/util/EmptyToolLogger.java | 20 ++ .../src/rba/tool/core/util/IToolLogger.java | 8 + .../src/rba/tool/core/util/ModelUtil.java | 29 ++ .../src/rba/tool/core/util/ResourceUtil.java | 72 +++++ .../src/rba/tool/core/util/SelectionTester.java | 53 +++ .../src/rba/tool/core/util/SelectionUtil.java | 167 ++++++++++ .../src/rba/tool/core/util/SortResult.java | 38 +++ .../src/rba/tool/core/util/SortResultSet.java | 25 ++ .../src/rba/tool/core/util/ToolLogger.java | 79 +++++ .../src/rba/tool/core/util/ValueSort.java | 152 +++++++++ .../src/rba/tool/core/util/data/ExCommentInfo.java | 32 ++ .../rba/tool/core/util/data/ExCommentLabel.java | 21 ++ .../src/rba/tool/core/z3/Z3CodeManager.java | 360 +++++++++++++++++++++ .../src/rba/tool/core/z3/Z3Constants.java | 18 ++ 34 files changed, 2293 insertions(+) create mode 100644 rba.tool.core/src/rba/tool/core/Activator.java create mode 100644 rba.tool.core/src/rba/tool/core/console/ConsoleManager.java create mode 100644 rba.tool.core/src/rba/tool/core/console/IConsoleHook.java create mode 100644 rba.tool.core/src/rba/tool/core/console/IConsoleManager.java create mode 100644 rba.tool.core/src/rba/tool/core/constraint/IConstraintCalculation.java create mode 100644 rba.tool.core/src/rba/tool/core/marker/MarkerManager.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/ComparisonAndEvaluator.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/ComparisonOperatorEvaluator.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/EObjectDecorator.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/EqualToOperatorEvaluator.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/ExpressionEvaluator.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/GreaterThanOperatorEvaluator.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/ISortValueCalculation.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/MuchGreaterThanOperatorEvaluator.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/SortValue.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/SortValueManager.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/ValueGroup.java create mode 100644 rba.tool.core/src/rba/tool/core/sort/ValueSortedList.java create mode 100644 rba.tool.core/src/rba/tool/core/ui/BasicTableViewerColumnFilter.java create mode 100644 rba.tool.core/src/rba/tool/core/ui/CommonValueValidator.java create mode 100644 rba.tool.core/src/rba/tool/core/util/EmptyToolLogger.java create mode 100644 rba.tool.core/src/rba/tool/core/util/IToolLogger.java create mode 100644 rba.tool.core/src/rba/tool/core/util/ModelUtil.java create mode 100644 rba.tool.core/src/rba/tool/core/util/ResourceUtil.java create mode 100644 rba.tool.core/src/rba/tool/core/util/SelectionTester.java create mode 100644 rba.tool.core/src/rba/tool/core/util/SelectionUtil.java create mode 100644 rba.tool.core/src/rba/tool/core/util/SortResult.java create mode 100644 rba.tool.core/src/rba/tool/core/util/SortResultSet.java create mode 100644 rba.tool.core/src/rba/tool/core/util/ToolLogger.java create mode 100644 rba.tool.core/src/rba/tool/core/util/ValueSort.java create mode 100644 rba.tool.core/src/rba/tool/core/util/data/ExCommentInfo.java create mode 100644 rba.tool.core/src/rba/tool/core/util/data/ExCommentLabel.java create mode 100644 rba.tool.core/src/rba/tool/core/z3/Z3CodeManager.java create mode 100644 rba.tool.core/src/rba/tool/core/z3/Z3Constants.java (limited to 'rba.tool.core/src/rba') diff --git a/rba.tool.core/src/rba/tool/core/Activator.java b/rba.tool.core/src/rba/tool/core/Activator.java new file mode 100644 index 0000000..e316252 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/Activator.java @@ -0,0 +1,49 @@ +package rba.tool.core; + +import org.eclipse.ui.plugin.AbstractUIPlugin; +import org.osgi.framework.BundleContext; + +/** + * The activator class controls the plug-in life cycle + */ +public class Activator extends AbstractUIPlugin { + + // The plug-in ID + public static final String PLUGIN_ID = "rba.tool.core"; //$NON-NLS-1$ + + // The shared instance + private static Activator plugin; + + /** + * The constructor + */ + public Activator() { + } + + /* + * (non-Javadoc) + * @see org.eclipse.ui.plugin.AbstractUIPlugin#start(org.osgi.framework.BundleContext) + */ + public void start(BundleContext context) throws Exception { + super.start(context); + plugin = this; + } + + /* + * (non-Javadoc) + * @see org.eclipse.ui.plugin.AbstractUIPlugin#stop(org.osgi.framework.BundleContext) + */ + public void stop(BundleContext context) throws Exception { + plugin = null; + super.stop(context); + } + + /** + * Returns the shared instance + * @return the shared instance + */ + public static Activator getDefault() { + return plugin; + } + +} diff --git a/rba.tool.core/src/rba/tool/core/console/ConsoleManager.java b/rba.tool.core/src/rba/tool/core/console/ConsoleManager.java new file mode 100644 index 0000000..823d3dd --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/console/ConsoleManager.java @@ -0,0 +1,96 @@ +package rba.tool.core.console; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +import org.eclipse.swt.SWT; +import org.eclipse.swt.graphics.Color; +import org.eclipse.ui.console.ConsolePlugin; +import org.eclipse.ui.console.MessageConsole; +import org.eclipse.ui.console.MessageConsoleStream; + +public class ConsoleManager implements IConsoleManager { + + public static ConsoleManager INSTANCE = new ConsoleManager(); + + org.eclipse.ui.console.IConsoleManager consoleManager; + + MessageConsole console; + + MessageConsoleStream consoleStream; + + MessageConsoleStream consoleWarnStream; + + String title = "RBA Tool Console"; + + Map> hook_notifierIdMap = new HashMap>(); + + private ConsoleManager() { + consoleManager = ConsolePlugin.getDefault().getConsoleManager(); + console = new MessageConsole(title, null); + consoleManager.addConsoles(new MessageConsole[] { console }); + + consoleStream = console.newMessageStream(); + + consoleWarnStream = console.newMessageStream(); + consoleWarnStream.setColor(new Color(null, 255, 0, 0)); // red + consoleWarnStream.setFontStyle(SWT.BOLD); + } + + public void clearConsole() { + console.clearConsole(); + } + + @Override + public void output(String message, String notifierId) { + preNotify(message, notifierId); + // original output message + consoleManager.showConsoleView(console); + consoleStream.println(message); + postNotify(message, notifierId); + } + + @Override + public void warning(String message, String notifierId) { + preNotify(message, notifierId); + // original warning message + consoleManager.showConsoleView(console); + consoleWarnStream.println(message); + postNotify(message, notifierId); + } + + @Override + public void addHook(IConsoleHook hook, String targetNotifierId) { + List hookList = hook_notifierIdMap.get(targetNotifierId); + if (hookList == null) { + hookList = new ArrayList(); + hook_notifierIdMap.put(targetNotifierId, hookList); + } + hookList.add(hook); + } + + @Override + public void removeHook(IConsoleHook hook, String targetNotifierId) { + List hookList = hook_notifierIdMap.get(targetNotifierId); + if (hookList == null) { + return; + } + hookList.remove(hook); + } + + public void preNotify(String message, String notifierId) { + List hookList = hook_notifierIdMap.get(notifierId); + if (hookList != null && !hookList.isEmpty()) { + hookList.forEach(hook -> hook.preNotify(message, notifierId)); + } + } + + public void postNotify(String message, String notifierId) { + List hookList = hook_notifierIdMap.get(notifierId); + if (hookList != null && !hookList.isEmpty()) { + hookList.forEach(hook -> hook.postNotify(message, notifierId)); + } + } +} diff --git a/rba.tool.core/src/rba/tool/core/console/IConsoleHook.java b/rba.tool.core/src/rba/tool/core/console/IConsoleHook.java new file mode 100644 index 0000000..8fbbd12 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/console/IConsoleHook.java @@ -0,0 +1,8 @@ +package rba.tool.core.console; + +public interface IConsoleHook { + + void preNotify(String message, String notifierId); + + void postNotify(String message, String notifierId); +} diff --git a/rba.tool.core/src/rba/tool/core/console/IConsoleManager.java b/rba.tool.core/src/rba/tool/core/console/IConsoleManager.java new file mode 100644 index 0000000..821e6f9 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/console/IConsoleManager.java @@ -0,0 +1,14 @@ +package rba.tool.core.console; + +public interface IConsoleManager { + + void output(String message, String notifierId); + + void clearConsole(); + + void warning(String message, String notifierId); + + void addHook(IConsoleHook hook, String targetNotifierId); + + void removeHook(IConsoleHook hook, String targetNotifierId); +} diff --git a/rba.tool.core/src/rba/tool/core/constraint/IConstraintCalculation.java b/rba.tool.core/src/rba/tool/core/constraint/IConstraintCalculation.java new file mode 100644 index 0000000..5066767 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/constraint/IConstraintCalculation.java @@ -0,0 +1,14 @@ +package rba.tool.core.constraint; + +import java.util.List; +import java.util.Map; + +public interface IConstraintCalculation { + List calculateAllConstraint(); + + Map> calculateImpliesConstraints(); + + void setUp(boolean onlyOnline); + + void close(); +} diff --git a/rba.tool.core/src/rba/tool/core/marker/MarkerManager.java b/rba.tool.core/src/rba/tool/core/marker/MarkerManager.java new file mode 100644 index 0000000..b04809f --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/marker/MarkerManager.java @@ -0,0 +1,142 @@ +package rba.tool.core.marker; + +import java.net.URI; +import java.util.HashMap; +import java.util.Map; + +import org.eclipse.core.resources.IFile; +import org.eclipse.core.resources.IFolder; +import org.eclipse.core.resources.IMarker; +import org.eclipse.core.resources.IProject; +import org.eclipse.core.resources.IResource; +import org.eclipse.core.resources.ResourcesPlugin; +import org.eclipse.core.runtime.CoreException; +import org.eclipse.core.runtime.IPath; +import org.eclipse.emf.ecore.EObject; +import org.eclipse.emf.ecore.resource.Resource; +import org.eclipse.emf.workspace.util.WorkspaceSynchronizer; +import org.eclipse.xtext.resource.ILocationInFileProvider; +import org.eclipse.xtext.util.TextRegionWithLineInformation; + +import com.google.inject.Injector; + +import rba.tool.editor.ui.activator.ExtensionEditorActivator; +import rba.tool.editor.util.RBAModelEditorNameUtil; + +public class MarkerManager { + public static MarkerManager INSTANCE = new MarkerManager(); + + public static String MARKER_ID_MODEL_EX = "rba.tool.core.model.ex"; //$NON-NLS-1$ + + public static String MARKER_ID_SORT_VALUE = "rba.tool.core.sort"; //$NON-NLS-1$ + + public static String MARKER_ID_CONSTRAINT = "rba.tool.core.constraint"; //$NON-NLS-1$ + + public void createMarker(EObject element, String message, int errorLevel, String id) { + Resource resource = element.eResource(); + IFile file = WorkspaceSynchronizer.getFile(resource); + + if (existInBuildFolder(file.getParent())) { + IFolder fol = file.getProject().getFolder(RBAModelEditorNameUtil.MODEL_FOLDER_NAME); + String path = getPath(file.getParent(), ""); + if (!path.equals("")) { + file = fol.getFile(path + "//" + file.getName()); + } else { + file = fol.getFile(file.getName()); + } + } + if (file != null && file.exists()) { + String location = file.getFullPath().toString(); + + Injector injector = ExtensionEditorActivator.getInstance().getInjector("rba.tool.editor.RBAModel"); + ILocationInFileProvider locationInFileProvider = injector.getInstance(ILocationInFileProvider.class); + + TextRegionWithLineInformation fullTextRegion = (TextRegionWithLineInformation) locationInFileProvider.getFullTextRegion(element); + int lineNumber = fullTextRegion.getLineNumber() + 1; + + Map attributes = new HashMap(); + attributes.put(IMarker.LINE_NUMBER, lineNumber); + + attributes.put(IMarker.SEVERITY, errorLevel); + attributes.put(IMarker.MESSAGE, message); + attributes.put(IMarker.LOCATION, location); + + try { + IMarker marker = file.createMarker(id); + marker.setAttributes(attributes); + } catch (CoreException e) { + e.printStackTrace(); + } + } + } + + public void clearMarkers(Resource resource, String id) { + IFile ifile = WorkspaceSynchronizer.getFile(resource); + if (ifile == null) { + return; + } + if (existInBuildFolder(ifile.getParent())) { + IFolder fol = ifile.getProject().getFolder(RBAModelEditorNameUtil.MODEL_FOLDER_NAME); + String path = getPath(ifile.getParent(), ""); + if (!path.equals("")) { + ifile = fol.getFile(path + "//" + ifile.getName()); + } else { + ifile = fol.getFile(ifile.getName()); + } + } + if (ifile != null && ifile.exists()) { + try { + for (IMarker marker : ResourcesPlugin.getWorkspace().getRoot().findMarkers(id, true, IResource.DEPTH_INFINITE)) { + if (ifile.equals(marker.getResource())) { + marker.delete(); + } + } + } catch (CoreException e) { + throw new RuntimeException(e); + } + } + } + + public void clearMarkers(IProject project, String id) { + + try { + for (IMarker marker : ResourcesPlugin.getWorkspace().getRoot().findMarkers(id, true, IResource.DEPTH_INFINITE)) { + + IResource resource = marker.getResource(); + if (project == resource.getProject()) { + marker.delete(); + } + } + } catch (CoreException e) { + throw new RuntimeException(e); + } + } + + private boolean existInBuildFolder(IResource res) { + if (res instanceof IFolder) { + if (res.getName().equals(RBAModelEditorNameUtil.BUILD_FOLDER_NAME)) { + return true; + } else { + return existInBuildFolder(res.getParent()); + } + } + return false; + } + + private String getPath(IResource res, String path) { + if (res instanceof IFolder) { + if (res.getName().equals(RBAModelEditorNameUtil.BUILD_FOLDER_NAME)) { + return path; + } else { + String p; + if (!path.equals("")) { + p = res.getName() + "//" + path; + } else { + p = res.getName(); + } + return getPath(res.getParent(), p); + } + } + return ""; + } +} diff --git a/rba.tool.core/src/rba/tool/core/sort/ComparisonAndEvaluator.java b/rba.tool.core/src/rba/tool/core/sort/ComparisonAndEvaluator.java new file mode 100644 index 0000000..5a4b1b2 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/ComparisonAndEvaluator.java @@ -0,0 +1,49 @@ +package rba.tool.core.sort; + +import org.eclipse.emf.common.util.EList; + +import rba.core.ComparisonAnd; +import rba.core.ComparisonOperator; +import rba.core.Expression; +import rba.core.GreaterThanOperator; +import rba.core.LetStatement; +import rba.core.MuchGreaterThanOperator; +import rba.core.RuleObject; + +public class ComparisonAndEvaluator extends ComparisonOperatorEvaluator implements ComparisonAnd { + + public ComparisonAndEvaluator(ComparisonAnd o) { + super(o); + } + + @Override + public boolean evaluate(ValueSortedList list) { + // TODO Auto-generated method stub + return false; + } + + @Override + public int suggestIndex(ValueSortedList list) { + int max = 9999; + int min = -1; + + for (Expression operand : operator.getOperand()) { + if (operand instanceof GreaterThanOperator || operand instanceof MuchGreaterThanOperator) { + int i = list.createEvaluator((ComparisonOperator) operand).suggestIndex(list); + if (i > min && i >= 0) { + min = i; + } + } else { + throw new RuntimeException("Unsupported expression [" + operator.getExpression() + "]"); + } + } + return Math.min(min, max); + } + + @Override + public EList getLetStatements() { + // TODO Auto-generated method stub + return null; + } + +} diff --git a/rba.tool.core/src/rba/tool/core/sort/ComparisonOperatorEvaluator.java b/rba.tool.core/src/rba/tool/core/sort/ComparisonOperatorEvaluator.java new file mode 100644 index 0000000..d0bc3dd --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/ComparisonOperatorEvaluator.java @@ -0,0 +1,49 @@ +package rba.tool.core.sort; + +import org.eclipse.emf.common.util.EList; +import org.eclipse.emf.ecore.EObject; + +import rba.core.ComparisonOperator; +import rba.core.Expression; +import rba.core.RuleObject; + +public abstract class ComparisonOperatorEvaluator extends ExpressionEvaluator implements ComparisonOperator { + + protected ComparisonOperator operator; + + protected T subject; + + @SuppressWarnings("unchecked") + protected ComparisonOperatorEvaluator(ComparisonOperator o) { + super(o); + operator = o; + EObject container = o.eContainer(); + while (!(container instanceof RuleObject)) { + container = container.eContainer(); + if (container == null) + break; + } + if (container != null) { + subject = (T) container; + } + } + + abstract public boolean evaluate(ValueSortedList list); + + /** + * @param list + * @return -1 if it has no suggestion 9999 implies MAX group (last index) + */ + abstract public int suggestIndex(ValueSortedList list); + + @Override + public EList getOperand() { + return operator.getOperand(); + } + + @Override + public String getSymbol() { + return operator.getSymbol(); + } + +} diff --git a/rba.tool.core/src/rba/tool/core/sort/EObjectDecorator.java b/rba.tool.core/src/rba/tool/core/sort/EObjectDecorator.java new file mode 100644 index 0000000..58aae87 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/EObjectDecorator.java @@ -0,0 +1,118 @@ +package rba.tool.core.sort; + +import java.lang.reflect.InvocationTargetException; + +import org.eclipse.emf.common.notify.Adapter; +import org.eclipse.emf.common.notify.Notification; +import org.eclipse.emf.common.util.EList; +import org.eclipse.emf.common.util.TreeIterator; +import org.eclipse.emf.ecore.EClass; +import org.eclipse.emf.ecore.EObject; +import org.eclipse.emf.ecore.EOperation; +import org.eclipse.emf.ecore.EReference; +import org.eclipse.emf.ecore.EStructuralFeature; +import org.eclipse.emf.ecore.resource.Resource; + +abstract public class EObjectDecorator implements EObject { + private EObject object; + + protected EObjectDecorator(EObject o) { + object = o; + } + + @Override + public EList eAdapters() { + return object.eAdapters(); + } + + @Override + public boolean eDeliver() { + return object.eDeliver(); + } + + @Override + public void eSetDeliver(boolean deliver) { + object.eSetDeliver(deliver); + } + + @Override + public void eNotify(Notification notification) { + object.eNotify(notification); + } + + @Override + public EClass eClass() { + return object.eClass(); + } + + @Override + public Resource eResource() { + return object.eResource(); + } + + @Override + public EObject eContainer() { + return object.eContainer(); + } + + @Override + public EStructuralFeature eContainingFeature() { + return object.eContainingFeature(); + } + + @Override + public EReference eContainmentFeature() { + return object.eContainmentFeature(); + } + + @Override + public EList eContents() { + return object.eContents(); + } + + @Override + public TreeIterator eAllContents() { + return object.eAllContents(); + } + + @Override + public boolean eIsProxy() { + return object.eIsProxy(); + } + + @Override + public EList eCrossReferences() { + return object.eCrossReferences(); + } + + @Override + public Object eGet(EStructuralFeature feature) { + return object.eGet(feature); + } + + @Override + public Object eGet(EStructuralFeature feature, boolean resolve) { + return object.eGet(feature, resolve); + } + + @Override + public void eSet(EStructuralFeature feature, Object newValue) { + object.eSet(feature, newValue); + } + + @Override + public boolean eIsSet(EStructuralFeature feature) { + return object.eIsSet(feature); + } + + @Override + public void eUnset(EStructuralFeature feature) { + object.eUnset(feature); + } + + @Override + public Object eInvoke(EOperation operation, EList arguments) throws InvocationTargetException { + return object.eInvoke(operation, arguments); + } + +} diff --git a/rba.tool.core/src/rba/tool/core/sort/EqualToOperatorEvaluator.java b/rba.tool.core/src/rba/tool/core/sort/EqualToOperatorEvaluator.java new file mode 100644 index 0000000..81b668a --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/EqualToOperatorEvaluator.java @@ -0,0 +1,52 @@ +package rba.tool.core.sort; + +import org.eclipse.emf.common.util.EList; + +import rba.core.ComparisonOperator; +import rba.core.EqualToOperator; +import rba.core.Expression; +import rba.core.LetStatement; +import rba.core.ObjectReference; +import rba.core.RuleObject; +import rba.core.ThatOfOperator; +import rba.core.ValueExpression; + +public class EqualToOperatorEvaluator extends ComparisonOperatorEvaluator implements EqualToOperator { + + protected EqualToOperatorEvaluator(ComparisonOperator o) { + super(o); + } + + @Override + public boolean evaluate(ValueSortedList list) { + // TODO Auto-generated method stub + return false; + } + + @Override + public int suggestIndex(ValueSortedList list) { + Expression operand = operator.getOperand().get(0); + if (operand instanceof ThatOfOperator) { + Expression target = ((ThatOfOperator) operand).getOperand().get(0); + + if (target instanceof ObjectReference) { + @SuppressWarnings("unchecked") + T object = (T) ((ObjectReference) target).getRefObject(); + return list.getGroupIndexOf(object); + } + + } else if (operand instanceof ValueExpression) { + int i = list.getGroupIndexOf(((ValueExpression) operand).getExpression()); + return i; + } + + throw new RuntimeException("Unsupported expression [" + operator.getExpression() + "]"); + } + + @Override + public EList getLetStatements() { + // TODO Auto-generated method stub + return null; + } + +} diff --git a/rba.tool.core/src/rba/tool/core/sort/ExpressionEvaluator.java b/rba.tool.core/src/rba/tool/core/sort/ExpressionEvaluator.java new file mode 100644 index 0000000..e0ac109 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/ExpressionEvaluator.java @@ -0,0 +1,55 @@ +package rba.tool.core.sort; + +import rba.core.Expression; +import rba.core.ExpressionType; + +abstract public class ExpressionEvaluator extends EObjectDecorator implements Expression { + + private Expression expression; + + protected ExpressionEvaluator(Expression o) { + super(o); + expression = o; + } + + @Override + public ExpressionType getType() { + return expression.getType(); + } + + @Override + public boolean isSetType() { + return expression.isSetType(); + } + + @Override + public String getExpression() { + return expression.getExpression(); + } + + @Override + public void setExpression(String value) { + expression.setExpression(value); + } + + @Override + public void unsetExpression() { + expression.unsetExpression(); + } + + @Override + public boolean isSetExpression() { + return expression.isSetExpression(); + } + + @Override + public String getExpressionText() { + return expression.getExpressionText(); + } + + @Override + public ExpressionType getUnderlyingType() { + return expression.getUnderlyingType(); + } + +} diff --git a/rba.tool.core/src/rba/tool/core/sort/GreaterThanOperatorEvaluator.java b/rba.tool.core/src/rba/tool/core/sort/GreaterThanOperatorEvaluator.java new file mode 100644 index 0000000..686fa54 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/GreaterThanOperatorEvaluator.java @@ -0,0 +1,64 @@ +package rba.tool.core.sort; + +import org.eclipse.emf.common.util.EList; + +import rba.core.Expression; +import rba.core.GreaterThanOperator; +import rba.core.LetStatement; +import rba.core.ObjectReference; +import rba.core.RuleObject; +import rba.core.ThatOfOperator; +import rba.core.ValueExpression; + +public class GreaterThanOperatorEvaluator extends ComparisonOperatorEvaluator implements GreaterThanOperator { + + protected GreaterThanOperatorEvaluator(GreaterThanOperator o) { + super(o); + } + + @Override + public boolean evaluate(ValueSortedList list) { + Expression operand = operator.getOperand().get(0); + if (operand instanceof ObjectReference) { + @SuppressWarnings("unchecked") + T object = (T) ((ObjectReference) operand).getRefObject(); + return (list.getGroupIndexOf(subject) > list.getGroupIndexOf(object)); + } + + return false; + } + + @Override + public int suggestIndex(ValueSortedList list) { + Expression operand = operator.getOperand().get(0); + if (operand instanceof ThatOfOperator) { + Expression target = ((ThatOfOperator) operand).getOperand().get(0); + + if (target instanceof ObjectReference) { + @SuppressWarnings("unchecked") + T object = (T) ((ObjectReference) target).getRefObject(); + if (list.getGroupIndexOf(subject) > list.getGroupIndexOf(object)) { + return -1; + } else { + return list.getGroupIndexOf(object) + 1; + } + } + + } else if (operand instanceof ValueExpression) { + int i = ((ValueExpression) operand).getExpressionValue(); + if (list.getGroupIndexOf(subject) > i) { + return -1; + } else { + return i + 1; + } + } + + throw new RuntimeException("Unsupported expression [" + operator.getExpression() + "]"); + } + + @Override + public EList getLetStatements() { + // TODO Auto-generated method stub + return null; + } +} diff --git a/rba.tool.core/src/rba/tool/core/sort/ISortValueCalculation.java b/rba.tool.core/src/rba/tool/core/sort/ISortValueCalculation.java new file mode 100644 index 0000000..5d4a544 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/ISortValueCalculation.java @@ -0,0 +1,15 @@ +package rba.tool.core.sort; + +import java.util.Map; + +public interface ISortValueCalculation { + Map calculateArea_zorder(); + + Map calculateAllocatable_visibility(); + + Map calculateContentState_priority(); + + void setUp(); + + void close(); +} diff --git a/rba.tool.core/src/rba/tool/core/sort/MuchGreaterThanOperatorEvaluator.java b/rba.tool.core/src/rba/tool/core/sort/MuchGreaterThanOperatorEvaluator.java new file mode 100644 index 0000000..5eb6ade --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/MuchGreaterThanOperatorEvaluator.java @@ -0,0 +1,67 @@ +package rba.tool.core.sort; + +import org.eclipse.emf.common.util.EList; + +import rba.core.Expression; +import rba.core.LetStatement; +import rba.core.MuchGreaterThanOperator; +import rba.core.ObjectReference; +import rba.core.RuleObject; +import rba.core.ThatOfOperator; +import rba.core.ValueExpression; + +public class MuchGreaterThanOperatorEvaluator extends ComparisonOperatorEvaluator implements MuchGreaterThanOperator { + + static int MUCH_GAP = 10; + + public MuchGreaterThanOperatorEvaluator(MuchGreaterThanOperator o) { + super(o); + } + + @Override + public boolean evaluate(ValueSortedList list) { + Expression operand = operator.getOperand().get(0); + if (operand instanceof ObjectReference) { + @SuppressWarnings("unchecked") + T object = (T) ((ObjectReference) operand).getRefObject(); + return (list.getGroupIndexOf(subject) >= list.getGroupIndexOf(object) + MUCH_GAP); + } + + return false; + } + + @Override + public int suggestIndex(ValueSortedList list) { + Expression operand = operator.getOperand().get(0); + if (operand instanceof ThatOfOperator) { + Expression target = ((ThatOfOperator) operand).getOperand().get(0); + + if (target instanceof ObjectReference) { + @SuppressWarnings("unchecked") + T object = (T) ((ObjectReference) target).getRefObject(); + if (list.getGroupIndexOf(subject) >= list.getGroupIndexOf(object) + MUCH_GAP) { + return -1; + } else { + return list.getGroupIndexOf(object) + MUCH_GAP; + } + } + + } else if (operand instanceof ValueExpression) { + int i = ((ValueExpression) operand).getExpressionValue(); + if (list.getGroupIndexOf(subject) > i) { + return -1; + } else { + return i + 1; + } + } + + throw new RuntimeException("Unsupported expression [" + operator.getExpression() + "]"); + } + + @Override + public EList getLetStatements() { + // TODO Auto-generated method stub + return null; + } + +} diff --git a/rba.tool.core/src/rba/tool/core/sort/SortValue.java b/rba.tool.core/src/rba/tool/core/sort/SortValue.java new file mode 100644 index 0000000..61ceaa9 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/SortValue.java @@ -0,0 +1,45 @@ +package rba.tool.core.sort; + +import java.util.HashMap; +import java.util.Map; + +import rba.tool.core.z3.Z3Constants; + +public class SortValue { + private Map sortMap = new HashMap(); + + private boolean unsat = false; + + public void setSortValue(Map map) { + if (map == null) { + clear(); + return; + } + + sortMap = map; + Integer result = map.get(Z3Constants.TOTAL_RESULT); + if (result == Z3Constants.UNSAT_VAL) { + unsat = true; + } + } + + public boolean isUnsat() { + return unsat; + } + + public Integer getValue(String name) { + if (!sortMap.isEmpty()) { + Integer integer = sortMap.get(name); + if (integer != null) { + return integer; + } + } + + return Z3Constants.UNKNOWN_VAL; + } + + public void clear() { + sortMap.clear(); + unsat = false; + } +} diff --git a/rba.tool.core/src/rba/tool/core/sort/SortValueManager.java b/rba.tool.core/src/rba/tool/core/sort/SortValueManager.java new file mode 100644 index 0000000..17fbb37 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/SortValueManager.java @@ -0,0 +1,56 @@ +package rba.tool.core.sort; + +import org.eclipse.core.resources.IProject; + +import rba.tool.core.console.ConsoleManager; +import rba.tool.core.z3.Z3CodeManager; + +public class SortValueManager { + + public static SortValueManager INSTANCE = new SortValueManager(); + + private static final String CONSOLE_TITLE = "#### Execution of Constraint ####"; + + private SortValue areaZorderSortValue = new SortValue(); + + private SortValue visibilitySortValue = new SortValue();; + + private SortValue csPrioritySortValue = new SortValue();; + + private static final String NOTIFIER_ID = "rba.tool.core.CalculateSortValue"; + + public boolean updateSortValue(IProject project) { + + try { + ISortValueCalculation calc = Z3CodeManager.INSTNACE.getSortCaluculator(project); + calc.setUp(); + areaZorderSortValue.setSortValue(calc.calculateArea_zorder()); + visibilitySortValue.setSortValue(calc.calculateAllocatable_visibility()); + csPrioritySortValue.setSortValue(calc.calculateContentState_priority()); + calc.close(); + + } catch (RuntimeException e) { + ConsoleManager.INSTANCE.output(CONSOLE_TITLE, NOTIFIER_ID); + ConsoleManager.INSTANCE.output(e.getMessage(), NOTIFIER_ID); + ConsoleManager.INSTANCE.output("##################", NOTIFIER_ID); + + areaZorderSortValue.clear(); + visibilitySortValue.clear(); + csPrioritySortValue.clear(); + return false; + } + return true; + } + + public SortValue getAreaZorderSortValue() { + return areaZorderSortValue; + } + + public SortValue getAllocatableVisibilitySortValue() { + return visibilitySortValue; + } + + public SortValue getCsPrioritySortValue() { + return csPrioritySortValue; + } +} diff --git a/rba.tool.core/src/rba/tool/core/sort/ValueGroup.java b/rba.tool.core/src/rba/tool/core/sort/ValueGroup.java new file mode 100644 index 0000000..86c8e63 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/ValueGroup.java @@ -0,0 +1,35 @@ +package rba.tool.core.sort; + +import java.util.ArrayList; +import java.util.Collection; + +public class ValueGroup { + private String name; + + private Collection member; + + public ValueGroup(String name) { + this.name = name; + member = new ArrayList(); + } + + public void setName(String name) { + this.name = name; + } + + public String getName() { + return name; + } + + public void add(T e) { + member.add(e); + } + + public void remove(T e) { + member.remove(e); + } + + public Collection getMember() { + return member; + } +} diff --git a/rba.tool.core/src/rba/tool/core/sort/ValueSortedList.java b/rba.tool.core/src/rba/tool/core/sort/ValueSortedList.java new file mode 100644 index 0000000..25ab560 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/sort/ValueSortedList.java @@ -0,0 +1,168 @@ +package rba.tool.core.sort; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; + +import rba.core.ComparisonAnd; +import rba.core.ComparisonOperator; +import rba.core.EqualToOperator; +import rba.core.Expression; +import rba.core.GreaterThanOperator; +import rba.core.MuchGreaterThanOperator; +import rba.core.RuleObject; +import rba.core.ValueExpression; + +abstract public class ValueSortedList { + private List> list; + + private Collection unsorted; + + public ValueSortedList(Collection originalList) { + list = new ArrayList>(); + list.add(new ValueGroup("MIN")); + list.add(new ValueGroup("1")); + list.add(new ValueGroup("MAX")); + unsorted = new ArrayList(originalList); + sort(); + } + + public void add(T o) { + unsorted.add(o); + sort(); + } + + public void addAll(Collection list) { + unsorted.addAll(list); + sort(); + } + + public void sort() { + list.get(0).getMember().addAll(unsorted); + unsorted.clear(); + boolean trysort = true; + int retry = 0; + while (trysort) { + trysort = false; + retry = retry + 1; + if (retry > 100) { + throw new RuntimeException("Could not sort value [" + list + "]"); + } + for (T i : sortedList()) { + int currentIndex = this.getGroupIndexOf(i); + Expression e = this.getValueExpression(i); + if (e == null) + continue; + if (e instanceof ValueExpression) { + int index = this.getGroupIndexOf(e.getExpression()); + if (index == -1) { + index = ((ValueExpression) e).getExpressionValue(); + + if (index == -1) { + index = 0; + } + if (index >= list.size() - 1) { + list.get(currentIndex).remove(i); + addGroupAt(index, i); + trysort = true; + continue; + } + } + if (index != currentIndex) { + list.get(currentIndex).remove(i); + list.get(index).add(i); + trysort = true; + } else { + } + } else if (e instanceof ComparisonOperator) { + ComparisonOperatorEvaluator evaluator = createEvaluator((ComparisonOperator) e); + int index = evaluator.suggestIndex(this); + if (index < 0) + continue; + if (index >= list.size() - 1) { + list.get(currentIndex).remove(i); + addGroupAt(index, i); + trysort = true; + } else if (index != currentIndex) { + list.get(currentIndex).remove(i); + list.get(index).add(i); + trysort = true; + } else { + } + } else { + throw new RuntimeException("Unsupported expression [" + e.getExpression() + "]"); + } + } + } + } + + private void addGroupAt(int index, T e) { + + if (index >= list.size() - 1) { + for (int i = list.size() - 1; i <= index; ++i) { + ValueGroup newGroup = new ValueGroup(Integer.toString(i)); + list.add(i, newGroup); + } + } + + list.get(index).add(e); + + } + + public List sortedList() { + List result = new ArrayList(); + for (ValueGroup i : list) { + result.addAll(i.getMember()); + } + return result; + } + + public List> getGroupList() { + return list; + } + + public List sortedListByBig() { + List result = new ArrayList(); + for (int index = list.size() - 1; index >= 0; index--) { + ValueGroup i = list.get(index); + result.addAll(i.getMember()); + } + return result; + } + + abstract protected Expression getValueExpression(T e); + + public int getGroupIndexOf(T e) { + for (ValueGroup i : list) { + if (i.getMember().contains(e)) { + return list.indexOf(i); + } + } + return -1; + } + + public int getGroupIndexOf(String groupName) { + for (ValueGroup i : list) { + if (i.getName().contentEquals(groupName)) { + return list.indexOf(i); + } + } + return -1; + } + + public ComparisonOperatorEvaluator createEvaluator(ComparisonOperator e) { + ComparisonOperatorEvaluator evaluator; + if (e instanceof GreaterThanOperator) { + evaluator = new GreaterThanOperatorEvaluator((GreaterThanOperator) e); + } else if (e instanceof MuchGreaterThanOperator) { + evaluator = new MuchGreaterThanOperatorEvaluator((MuchGreaterThanOperator) e); + } else if (e instanceof ComparisonAnd) { + evaluator = new ComparisonAndEvaluator((ComparisonAnd) e); + } else if (e instanceof EqualToOperator) { + evaluator = new EqualToOperatorEvaluator((EqualToOperator) e); + } else { + throw new RuntimeException("Unsupported expression [" + e.getExpression() + "]"); + } + return evaluator; + } +} diff --git a/rba.tool.core/src/rba/tool/core/ui/BasicTableViewerColumnFilter.java b/rba.tool.core/src/rba/tool/core/ui/BasicTableViewerColumnFilter.java new file mode 100644 index 0000000..4eb07a5 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/ui/BasicTableViewerColumnFilter.java @@ -0,0 +1,72 @@ +package rba.tool.core.ui; + +import java.util.regex.Pattern; + +import org.apache.commons.lang3.StringUtils; +import org.eclipse.jface.viewers.ITableLabelProvider; +import org.eclipse.jface.viewers.TableViewer; +import org.eclipse.jface.viewers.Viewer; +import org.eclipse.jface.viewers.ViewerFilter; + +public class BasicTableViewerColumnFilter extends ViewerFilter { + + private String filterString; + + private final int[] filterColumns; + + public BasicTableViewerColumnFilter(String filterString, int[] filterColumns) { + this.filterString = filterString; + this.filterColumns = filterColumns; + } + + @Override + public boolean select(Viewer viewer, Object parentElement, Object element) { + if ((null == filterString) || (StringUtils.isEmpty(filterString))) { + return true; + } + + Pattern pattern = Pattern.compile(createRegexFromGlob(filterString), Pattern.CASE_INSENSITIVE); + + for (int i : this.filterColumns) { + + ITableLabelProvider labelProvider = (ITableLabelProvider) ((TableViewer) viewer).getLabelProvider(); + + String cellLabel = labelProvider.getColumnText(element, i); + + if (pattern.matcher(cellLabel).find()) { + return true; + } else if (cellLabel.toLowerCase().contains(filterString.toLowerCase())) { + return true; + } + } + return false; + } + + /** + * Create Regular Expression for filter string + * @param glob + * @return + */ + private String createRegexFromGlob(String glob) { + String out = "^"; + for (int i = 0; i < glob.length(); ++i) { + final char c = glob.charAt(i); + switch (c) { + case '*': + out += ".*"; + break; + case '?': + out += '.'; + break; + default: + out += c; + } + } + out += '$'; + return out; + } + + public void setFilterString(String filterString) { + this.filterString = filterString; + } +} diff --git a/rba.tool.core/src/rba/tool/core/ui/CommonValueValidator.java b/rba.tool.core/src/rba/tool/core/ui/CommonValueValidator.java new file mode 100644 index 0000000..c724760 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/ui/CommonValueValidator.java @@ -0,0 +1,51 @@ +package rba.tool.core.ui; + +import java.nio.file.Files; +import java.nio.file.Paths; + +import org.apache.commons.lang3.StringUtils; + +public class CommonValueValidator { + + public static boolean isExistFilePath(String folderPath, String fileName) { + if (StringUtils.isEmpty(folderPath) || StringUtils.isEmpty(fileName)) + return false; + return Files.exists(Paths.get(folderPath, fileName)); + } + + public static boolean isExistFilePath(String filePath) { + if (StringUtils.isEmpty(filePath)) + return false; + return Files.exists(Paths.get(filePath)); + } + + public static boolean isValidFileName(String target) { + if (StringUtils.isEmpty(target)) { + return false; + } + if (target.length() > 250) { + return false; + } + if (target.contains("¥") || target.contains("/") || target.contains(":") || target.contains("*") || target.contains("?") || target.contains("\"") || target.contains("|") + || target.contains("<") || target.contains(">")) { + return false; + } + + return true; + } + + public static boolean isValidFolderName(String target) { + if (StringUtils.isEmpty(target)) { + return false; + } + if (target.length() > 250) { + return false; + } + if (target.contains("¥") || target.contains("/") || target.contains(":") || target.contains("*") || target.contains("?") || target.contains("\"") || target.contains("|") + || target.contains("<") || target.contains(">") || target.contains(".") || target.contains(",")) { + return false; + } + + return true; + } +} diff --git a/rba.tool.core/src/rba/tool/core/util/EmptyToolLogger.java b/rba.tool.core/src/rba/tool/core/util/EmptyToolLogger.java new file mode 100644 index 0000000..cf2280d --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/EmptyToolLogger.java @@ -0,0 +1,20 @@ +package rba.tool.core.util; + +/** + * @author kousuke_morishima + */ +public class EmptyToolLogger implements IToolLogger { + + public EmptyToolLogger() { + } + + @Override + public void logging(Throwable e) { + // nothing to do + } + + @Override + public void logging(String message) { + // nothing to do + } +} diff --git a/rba.tool.core/src/rba/tool/core/util/IToolLogger.java b/rba.tool.core/src/rba/tool/core/util/IToolLogger.java new file mode 100644 index 0000000..b53cf8c --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/IToolLogger.java @@ -0,0 +1,8 @@ +package rba.tool.core.util; + +public interface IToolLogger { + + void logging(Throwable e); + + void logging(String message); +} diff --git a/rba.tool.core/src/rba/tool/core/util/ModelUtil.java b/rba.tool.core/src/rba/tool/core/util/ModelUtil.java new file mode 100644 index 0000000..b6b34a7 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/ModelUtil.java @@ -0,0 +1,29 @@ +package rba.tool.core.util; + +import org.eclipse.emf.ecore.EObject; + +import rba.core.NamedElement; +import rba.core.Package; + +public class ModelUtil { + + public static final String SEPARATOR = "/"; + + public static String getRBAModelHierarchicalName(NamedElement target) { + return getRBAModelHierarchicalName(target, SEPARATOR); + } + + public static String getRBAModelHierarchicalName(NamedElement target, String separator) { + EObject parent = target.eContainer(); + if (parent == null || !(parent instanceof NamedElement) || parent instanceof Package) { + return target.getName(); + } else { + return getRBAModelHierarchicalName((NamedElement) parent, separator) + separator + target.getName(); + } + } + + public static String convertModelName2ArbitrateName(String modelName) { + if (modelName == null) return modelName; + return modelName.replace(".", "/"); + } +} diff --git a/rba.tool.core/src/rba/tool/core/util/ResourceUtil.java b/rba.tool.core/src/rba/tool/core/util/ResourceUtil.java new file mode 100644 index 0000000..751f308 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/ResourceUtil.java @@ -0,0 +1,72 @@ +package rba.tool.core.util; + +import java.io.BufferedReader; +import java.io.BufferedWriter; +import java.io.File; +import java.io.FileInputStream; +import java.io.FileOutputStream; +import java.io.IOException; +import java.io.InputStreamReader; +import java.io.OutputStreamWriter; + +public class ResourceUtil { + public static BufferedReader getReader(File file) { + FileInputStream fis = null; + InputStreamReader isr = null; + BufferedReader reader = null; + + try { + fis = new FileInputStream(file); + isr = new InputStreamReader(fis, "UTF-8"); + reader = new BufferedReader(isr); + } catch (Throwable e) { + e.printStackTrace(); + try { + if (reader != null) { + reader.close(); + } + if (isr != null) { + isr.close(); + } + if (fis != null) { + fis.close(); + } + } catch (IOException e1) { + e1.printStackTrace(); + } + + throw new RuntimeException(e); + } + return reader; + } + + public static BufferedWriter getWriter(File file) { + FileOutputStream fos = null; + OutputStreamWriter osw = null; + BufferedWriter writer = null; + + try { + fos = new FileOutputStream(file); + osw = new OutputStreamWriter(fos, "UTF-8"); + writer = new BufferedWriter(osw); + } catch (Throwable e) { + e.printStackTrace(); + try { + if (writer != null) { + writer.close(); + } + if (osw != null) { + osw.close(); + } + if (fos != null) { + fos.close(); + } + } catch (IOException e1) { + e1.printStackTrace(); + } + + throw new RuntimeException(e); + } + return writer; + } +} diff --git a/rba.tool.core/src/rba/tool/core/util/SelectionTester.java b/rba.tool.core/src/rba/tool/core/util/SelectionTester.java new file mode 100644 index 0000000..b1bec63 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/SelectionTester.java @@ -0,0 +1,53 @@ +package rba.tool.core.util; + +import org.eclipse.core.expressions.PropertyTester; +import org.eclipse.core.resources.IFolder; +import org.eclipse.core.resources.IResource; + +public class SelectionTester extends PropertyTester { + + @Override + public boolean test(Object receiver, String property, Object[] args, Object expectedValue) { + if (property.equals("IsTestRev")) { + IFolder folder = SelectionUtil.getRevFolder(receiver); + return folder != null; + } + if (property.equals("IsResource")) { + return receiver instanceof IResource; + } + if (property.equals("IsMultiSelect")) { + IFolder folder = SelectionUtil.getRevFolder(receiver); + return folder != null; + } + if (property.equals("IsTestCompare")) { + IFolder folder = SelectionUtil.getRevCompareFolder(receiver); + return folder != null; + } + return false; + } + // + // protected boolean isEnableProject(Object receiver) { + // IResource resource = null; + // + // if (receiver instanceof EObject) { + // EObject eObject = (EObject) receiver; + // if (eObject.eResource() != null) { + // resource = WorkspaceSynchronizer.getFile(eObject.eResource()); + // } + // } else if (receiver instanceof IResource) { + // resource = (IResource) receiver; + // } + // + // if (resource != null) { + // IProject project = resource.getProject(); + // if (project != null) { + // // if (ZIPCProjectNature.hasNature(project)) { + // if (ZIPCProjectNature.hasNature(project) && DesignProjectNature.hasNature(project)) { + // return true; + // } + // } + // } + // return false; + // } + +} diff --git a/rba.tool.core/src/rba/tool/core/util/SelectionUtil.java b/rba.tool.core/src/rba/tool/core/util/SelectionUtil.java new file mode 100644 index 0000000..e6093b7 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/SelectionUtil.java @@ -0,0 +1,167 @@ +package rba.tool.core.util; + +import org.eclipse.core.resources.IFile; +import org.eclipse.core.resources.IFolder; +import org.eclipse.core.resources.IProject; +import org.eclipse.core.resources.IResource; +import org.eclipse.core.runtime.CoreException; +import org.eclipse.jface.viewers.ISelection; +import org.eclipse.jface.viewers.IStructuredSelection; + +public class SelectionUtil { + + public static final String TEST_FILE_NAME = "testinformation"; + + public static final String TEST_CASE_FOLDER_NAME = "testcase"; + + public static final String TEST_COVERAGE_FOLDER_NAME = "coverage"; + + public static final String TEST_LOG_FOLDER_NAME = "testlog"; + + public static final String TEST_RESULT_FOLDER_NAME = "testresult"; + + /** + * get testresult folder in revision folder from selected item + * @param file + * @return testcase folder + */ + public static IFolder getRevResultFolder(Object object) { + return getAndCreateFolderInTestRevFolder(object, TEST_RESULT_FOLDER_NAME); + } + + /** + * get testlog folder in revision folder from selected item + * @param file + * @return testcase folder + */ + public static IFolder getRevLogFolder(Object object) { + return getAndCreateFolderInTestRevFolder(object, TEST_LOG_FOLDER_NAME); + } + + /** + * get coverage folder in revision folder from selected item + * @param file + * @return testcase folder + */ + public static IFolder getRevCoverageFolder(Object object) { + return getAndCreateFolderInTestRevFolder(object, TEST_COVERAGE_FOLDER_NAME); + } + + /** + * get testcase folder in revision folder from selected item + * @param file + * @return testcase folder + */ + public static IFolder getRevTestcaseFolder(Object object) { + return getAndCreateFolderInTestRevFolder(object, TEST_CASE_FOLDER_NAME); + } + + public static IFolder getAndCreateFolderInTestRevFolder(Object object, String foldername) { + IFolder folder = getRevFolder(object); + if (folder != null) { + IFolder testcase = folder.getFolder(foldername); + if (!testcase.exists()) { + try { + testcase.create(true, true, null); + } catch (CoreException e) { + throw new RuntimeException(e); + } + } + return testcase; + } + return null; + } + + /** + * get revision folder of selected file + * @param file + * @return + */ + public static IFolder getRevFolder(Object object) { + try { + if (object instanceof ISelection) { + ISelection selection = (ISelection) object; + if (selection instanceof IStructuredSelection) { + IStructuredSelection structuredSelection = (IStructuredSelection) selection; + Object element = structuredSelection.getFirstElement(); + if (element instanceof IResource) { + return getRevFolder((IResource) element); + } + } + } else if (object instanceof IResource) { + if (object instanceof IFolder) { + IFolder f = (IFolder) object; + IResource[] resources = f.members(); + for (IResource res : resources) { + if (res instanceof IFile) { + IFile file = (IFile) res; + if (file.getName().equals(TEST_FILE_NAME)) { + return f; + } + } + } + } else if (object instanceof IFile) { + IFolder parent = (IFolder) ((IFile) object).getParent(); + return getRevFolder(parent); + } + IResource r = (IResource) object; + return getRevFolder(r.getParent()); + + // + // IFolder f = null; + // if (object instanceof IFile) { + // IContainer parent = ((IFile) object).getParent(); + // if (parent instanceof IFolder) { + // f = (IFolder) parent; + // } + // } else + // + // if (f.getParent() instanceof IFolder) { + // return getRevFolder((IFolder) f.getParent()); + // } + } + } catch (CoreException e) { + e.printStackTrace(); + } + return null; + } + + /** + * to get only 2 selected revision file + * @param object + * @return + */ + public static IFolder getRevCompareFolder(Object object) { + try { + if (object instanceof ISelection) { + ISelection selection = (ISelection) object; + if (selection instanceof IStructuredSelection) { + IStructuredSelection structuredSelection = (IStructuredSelection) selection; + if (structuredSelection.size() == 2) { + Object element = structuredSelection.getFirstElement(); + if (element instanceof IResource) { + return getRevCompareFolder((IResource) element); + } + } + } + } else if (object instanceof IResource) { + if (object instanceof IFolder) { + IFolder f = (IFolder) object; + IResource[] resources = f.members(); + for (IResource res : resources) { + if (res instanceof IFile) { + IFile file = (IFile) res; + if (file.getName().equals(TEST_FILE_NAME)) { + return f; + } + } + } + } + + } + } catch (CoreException e) { + e.printStackTrace(); + } + return null; + } +} diff --git a/rba.tool.core/src/rba/tool/core/util/SortResult.java b/rba.tool.core/src/rba/tool/core/util/SortResult.java new file mode 100644 index 0000000..838a325 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/SortResult.java @@ -0,0 +1,38 @@ +package rba.tool.core.util; + +import java.util.ArrayList; +import java.util.List; + +import rba.core.RuleObject; + +public class SortResult { + private List> sortResults = new ArrayList>(); + + private boolean isUnsat; + + public List> getSortResults() { + return sortResults; + } + + public boolean addSortResult(SortResultSet sortResult) { + return sortResults.add(sortResult); + } + + public SortResultSet getSortResultSet(RuleObject obj) { + for (SortResultSet sortResult : sortResults) { + T element = sortResult.getElement(); + if (element.equals(obj)) { + return sortResult; + } + } + return null; + } + + public boolean isUnsat() { + return isUnsat; + } + + public void setUnsat(boolean isUnsat) { + this.isUnsat = isUnsat; + } +} diff --git a/rba.tool.core/src/rba/tool/core/util/SortResultSet.java b/rba.tool.core/src/rba/tool/core/util/SortResultSet.java new file mode 100644 index 0000000..93e18f0 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/SortResultSet.java @@ -0,0 +1,25 @@ +package rba.tool.core.util; + +import rba.core.RuleObject; + +public class SortResultSet { + private T element; + + private int value; + + public T getElement() { + return element; + } + + public void setElement(T element) { + this.element = element; + } + + public int getValue() { + return value; + } + + public void setValue(int value) { + this.value = value; + } +} diff --git a/rba.tool.core/src/rba/tool/core/util/ToolLogger.java b/rba.tool.core/src/rba/tool/core/util/ToolLogger.java new file mode 100644 index 0000000..0907eb6 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/ToolLogger.java @@ -0,0 +1,79 @@ +package rba.tool.core.util; + +import java.io.File; +import java.io.IOException; +import java.util.logging.FileHandler; +import java.util.logging.Handler; +import java.util.logging.Level; +import java.util.logging.Logger; +import java.util.logging.SimpleFormatter; +import java.util.stream.Stream; + +public class ToolLogger implements IToolLogger { + + private Logger logger; + + /** + * @param name logger name + * @param logFile File name + * @param append + * @throws SecurityException + * @throws IOException + */ + public ToolLogger(String name, String logFile, boolean append) throws SecurityException, IOException { + this(Logger.getLogger(name), logFile, append); + } + + /** + * @param logger logger name + * @param logFile + * @param append + * @throws SecurityException + * @throws IOException + * @throws NullPointerException + */ + public ToolLogger(Logger logger, String logFile, boolean append) throws SecurityException, IOException { + if (logger == null) { + throw new NullPointerException("logger must be not null."); //$NON-NLS-1$ + } + this.logger = logger; + String path = "log/" + logFile; //$NON-NLS-1$ + createParent(path); + FileHandler h = new FileHandler(path, append); + h.setFormatter(new SimpleFormatter()); + this.logger.addHandler(h); + this.logger.setLevel(Level.ALL); + } + + public ToolLogger(Logger logger, Handler handler) { + if (logger == null) { + throw new NullPointerException("logger must be not null."); //$NON-NLS-1$ + } + this.logger = logger; + this.logger.addHandler(handler); + this.logger.setLevel(Level.ALL); + } + + static void createParent(String path) { + File logPath = new File(path); + if (!logPath.getParentFile().exists()) { + logPath.getParentFile().mkdirs(); + } + } + + /** + * Logging when handle to occurred error + * @param e + */ + public void logging(Throwable e) { + StringBuilder message = new StringBuilder(e.toString() + "\n"); //$NON-NLS-1$ + Stream.of(e.getStackTrace()).forEach(t -> message.append("\t").append(t.toString()).append("\n")); //$NON-NLS-1$ //$NON-NLS-2$ + logger.warning(message.toString()); + } + + @Override + public void logging(String message) { + logger.warning(message); + } + +} diff --git a/rba.tool.core/src/rba/tool/core/util/ValueSort.java b/rba.tool.core/src/rba/tool/core/util/ValueSort.java new file mode 100644 index 0000000..7182667 --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/ValueSort.java @@ -0,0 +1,152 @@ +package rba.tool.core.util; + +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +import rba.core.ContentState; +import rba.core.Expression; +import rba.core.RBACoreFactory; +import rba.tool.core.sort.ValueGroup; +import rba.tool.core.sort.ValueSortedList; +import rba.view.Area; + +public class ValueSort { + public static ValueSort INSTANCE = new ValueSort(); + + public SortResult sortVisibility(List areas) { + SortResult sortResult = new SortResult(); + + try { + sortResult = doSortVisibility(areas); + sortResult.setUnsat(false); + } catch (RuntimeException e) { + sortResult.setUnsat(true); + } + + return sortResult; + } + + private SortResult doSortVisibility(List areas) { + SortResult sortResult = new SortResult(); + + Map> map = new HashMap>(); + for (Area area : areas) { + SortResultSet set = new SortResultSet(); + set.setElement(area); + sortResult.addSortResult(set); + map.put(area, set); + } + + ValueSortedList sortedElement = new ValueSortedList(areas) { + protected Expression getValueExpression(Area e) { + return e.getVisibility(); + } + }; + + for (ValueGroup valueGroup : sortedElement.getGroupList()) { + int value = convertValue(valueGroup.getName()); + for (Area member : valueGroup.getMember()) { + SortResultSet set = map.get(member); + set.setValue(value); + } + } + + return sortResult; + } + + public SortResult sortZorder(List areas) { + SortResult sortResult = new SortResult(); + + try { + sortResult = doSortZorder(areas); + sortResult.setUnsat(false); + } catch (RuntimeException e) { + sortResult.setUnsat(true); + } + + return sortResult; + } + + private SortResult doSortZorder(List areas) { + + SortResult sortResult = new SortResult(); + + Map> map = new HashMap>(); + for (Area area : areas) { + SortResultSet set = new SortResultSet(); + set.setElement(area); + sortResult.addSortResult(set); + map.put(area, set); + } + + ValueSortedList sortedElement = new ValueSortedList(areas) { + protected Expression getValueExpression(Area e) { + return e.getZorder(); + } + }; + + for (ValueGroup valueGroup : sortedElement.getGroupList()) { + int value = convertValue(valueGroup.getName()); + for (Area member : valueGroup.getMember()) { + SortResultSet set = map.get(member); + set.setValue(value); + } + } + return sortResult; + } + + public SortResult sortPriority(List contentStates) { + SortResult sortResult = new SortResult(); + + try { + sortResult = doSortPriority(contentStates); + sortResult.setUnsat(false); + } catch (RuntimeException e) { + sortResult.setUnsat(true); + } + + return sortResult; + } + + public SortResult doSortPriority(List contentStates) { + SortResult sortResult = new SortResult(); + + Map> map = new HashMap>(); + for (ContentState contentState : contentStates) { + SortResultSet set = new SortResultSet(); + set.setElement(contentState); + sortResult.addSortResult(set); + map.put(contentState, set); + } + + ValueSortedList sortedElement = new ValueSortedList(contentStates) { + protected Expression getValueExpression(ContentState e) { + return e.getValue(); + } + }; + + for (ValueGroup valueGroup : sortedElement.getGroupList()) { + int value = convertValue(valueGroup.getName()); + for (ContentState member : valueGroup.getMember()) { + SortResultSet set = map.get(member); + set.setValue(value); + } + } + + return sortResult; + } + + private int convertValue(String valueString) { + int value; + if (valueString.equals("MIN")) { + value = RBACoreFactory.eINSTANCE.createMinValue().getExpressionValue(); + } else if (valueString.equals("MAX")) { + value = RBACoreFactory.eINSTANCE.createMaxValue().getExpressionValue(); + } else { + value = Integer.parseInt(valueString); + } + return value; + } + +} diff --git a/rba.tool.core/src/rba/tool/core/util/data/ExCommentInfo.java b/rba.tool.core/src/rba/tool/core/util/data/ExCommentInfo.java new file mode 100644 index 0000000..936d8ae --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/data/ExCommentInfo.java @@ -0,0 +1,32 @@ +package rba.tool.core.util.data; + +import java.util.ArrayList; +import java.util.List; + +public class ExCommentInfo { + + private String fileName; + + private List info = new ArrayList(); + + public String getFileName() { + return fileName; + } + + public void setFileName(String fileName) { + this.fileName = fileName; + } + + public List getInfo() { + return info; + } + + public void setInfo(List info) { + this.info = info; + } + + public void addInfo(String info) { + this.info.add(info); + } + +} diff --git a/rba.tool.core/src/rba/tool/core/util/data/ExCommentLabel.java b/rba.tool.core/src/rba/tool/core/util/data/ExCommentLabel.java new file mode 100644 index 0000000..c83f03a --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/util/data/ExCommentLabel.java @@ -0,0 +1,21 @@ +package rba.tool.core.util.data; + +public class ExCommentLabel { + + private final String label; + + private final int columnWidth; + + public ExCommentLabel(String label, int columnWidth) { + this.label = label; + this.columnWidth = columnWidth; + } + + public String getLabel() { + return label; + } + + public int getColumnWidth() { + return columnWidth; + } +} diff --git a/rba.tool.core/src/rba/tool/core/z3/Z3CodeManager.java b/rba.tool.core/src/rba/tool/core/z3/Z3CodeManager.java new file mode 100644 index 0000000..7f9da9c --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/z3/Z3CodeManager.java @@ -0,0 +1,360 @@ +package rba.tool.core.z3; + +import java.io.IOException; +import java.lang.reflect.Field; +import java.net.URL; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +import org.eclipse.core.resources.IContainer; +import org.eclipse.core.resources.IFile; +import org.eclipse.core.resources.IProject; +import org.eclipse.core.resources.IResource; +import org.eclipse.core.runtime.CoreException; +import org.eclipse.core.runtime.FileLocator; +import org.eclipse.core.runtime.Platform; + +import com.microsoft.z3.ApplyResult; +import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.Context; +import com.microsoft.z3.Expr; +import com.microsoft.z3.Goal; +import com.microsoft.z3.Solver; +import com.microsoft.z3.Status; +import com.microsoft.z3.Tactic; + +import groovy.util.GroovyScriptEngine; +import rba.tool.core.Activator; +import rba.tool.core.constraint.IConstraintCalculation; +import rba.tool.core.sort.ISortValueCalculation; + +public class Z3CodeManager { + + public static Z3CodeManager INSTNACE = new Z3CodeManager(); + + private static final String ERROR_ENV_PATH = "The Z3 storage path cannot be found. Area and content parameters are not derived correctly. \r\nSet the environment variable of the storage path of Z3."; + + private static final String ERROR_SCRIPT = "Z3 execution failed. There is an error in the script."; + + private static final String SORT_SCRIPT_NAME = "SortValueCalculation.java"; + + private static final String CONST_SCRIPT_NAME = "ConstraintCalculation.java"; + + private static final String ERROR_NOT_FOUND_SCRIPT = "Z3 execution failed. Failed to generate %s in the %s project."; + + private Z3CodeManager() { + } + + public boolean loadZ3Lib() { + String z3Path = ""; + try { + z3Path = getPath(); + } catch (Exception e1) { + e1.printStackTrace(); + return false; + } + if (null == z3Path || z3Path.isEmpty()) { + return false; + } + try { + // load necessary z3 DLLs + loadDLLs(z3Path); + // add z3 path to java.library.path + addLibraryPath(z3Path); + return true; + } catch (Exception e) { + e.printStackTrace(); + return false; + } + } + + private String getPath() throws IOException { + String path = ""; + String jvmBitMode = System.getProperty("sun.arch.data.model"); + // Check JVM 32 Bit. + if (jvmBitMode != null && jvmBitMode.contains("32")) { + URL bundleEntryUrl = Platform.getBundle(Activator.PLUGIN_ID).getEntry("lib32/z3"); + URL fileUrl = FileLocator.toFileURL(bundleEntryUrl); + path = fileUrl.getPath(); + } + // Check JVM 64 Bit. + if (jvmBitMode != null && jvmBitMode.contains("64")) { + URL bundleEntryUrl = Platform.getBundle(Activator.PLUGIN_ID).getEntry("lib/z3"); + URL fileUrl = FileLocator.toFileURL(bundleEntryUrl); + path = fileUrl.getPath(); + } + return path; + } + + public ISortValueCalculation getSortCaluculator(IProject project) throws RuntimeException { + + if (!loadZ3Lib()) { + String errMsg = ERROR_ENV_PATH; + throw new RuntimeException(errMsg); + } + + ISortValueCalculation calc = null; + IFile file = findFile(SORT_SCRIPT_NAME, project); + if (file != null) { + try { + String fileName = file.getName(); + String className = fileName.substring(0, fileName.lastIndexOf(".")); + + String string = file.getLocation().toString(); + String genPath = string.substring(0, string.length() - fileName.length()); + + GroovyScriptEngine e = new GroovyScriptEngine(new String[] { genPath }, getClass().getClassLoader()); + e.loadScriptByName(fileName); + Class s = e.getGroovyClassLoader().loadClass(className); + + calc = (ISortValueCalculation) s.newInstance(); + } catch (Exception e) { + String errMsg = ERROR_SCRIPT; + throw new RuntimeException(errMsg); + } + + } else { + String errMsg = String.format(ERROR_NOT_FOUND_SCRIPT, project.getName(), SORT_SCRIPT_NAME); + throw new RuntimeException(errMsg); + } + + return calc; + } + + public IFile findFile(String name, IContainer container) { + try { + IResource[] resources; + resources = container.members(); + if (resources == null || resources.length == 0) { + return null; + } + for (IResource resource : resources) { + if (resource instanceof IFile && resource.getName().equals(name)) { + return (IFile) resource; + } + if (resource instanceof IContainer) { + IFile recursive = findFile(name, (IContainer) resource); + if (recursive != null) { + return recursive; + } + } + } + } catch (CoreException e) { + } + + return null; + } + + /** + * load z3 DLLs from the path + * @param z3Path + */ + private void loadDLLs(String z3Path) throws Exception { + System.load(z3Path + "\\Microsoft.Z3.dll"); + System.load(z3Path + "\\msvcr110.dll"); + System.load(z3Path + "\\msvcp110.dll"); + System.load(z3Path + "\\vcomp110.dll"); + System.load(z3Path + "\\libz3.dll"); + System.load(z3Path + "\\libz3java.dll"); + } + + /** + * add z3 path to java.library.path + * @param pathToAdd + */ + private void addLibraryPath(String pathToAdd) throws Exception { + final Field usrPathsField = ClassLoader.class.getDeclaredField("usr_paths"); + usrPathsField.setAccessible(true); + // get array of paths + final String[] paths = (String[]) usrPathsField.get(null); + // check if the path to add is already present + for (String path : paths) { + if (path.equals(pathToAdd)) { + return; + } + } + // add the new path + final String[] newPaths = Arrays.copyOf(paths, paths.length + 1); + newPaths[newPaths.length - 1] = pathToAdd; + usrPathsField.set(null, newPaths); + } + + public Map setModel(Solver s, List contentsList, Status st) { + switch (st) { + case UNKNOWN: + System.out.println("Unknown"); + break; + + case SATISFIABLE: + return setSat(s, contentsList); + case UNSATISFIABLE: + return setUnsat(s); + } + + return null; + } + + public Map setSat(Solver s, List evaluatedExpr) { + + Map map = new HashMap(); + + map.put(Z3Constants.TOTAL_RESULT, Z3Constants.SAT_VAL); + + for (Expr i : evaluatedExpr) { + String areaName = getName(i.getSExpr()); + String expVal = s.getModel().evaluate(i, false).toString(); + + map.put(areaName, Integer.valueOf(expVal)); + } + + return map; + } + + public Map setUnsat(Solver s) { + + Map map = new HashMap(); + + map.put(Z3Constants.TOTAL_RESULT, Z3Constants.UNSAT_VAL); + + for (Expr i : s.getUnsatCore()) { + String areaName = getName(i.toString()); + map.put(areaName, Z3Constants.UNSAT_VAL); + } + return map; + } + + private String getName(String baseName) { + String name = baseName; + if (name.length() > 2 && name.startsWith("|") && name.endsWith("|")) { + name = name.substring(1, name.length() - 1); + } + + return name; + } + + public List getErrors(Solver s, Status st) { + List list = new ArrayList(); + + switch (st) { + case UNKNOWN: + + list.add(Z3Constants.UNKNOWN); + list.add(s.getReasonUnknown()); + break; + case SATISFIABLE: + list.add(Z3Constants.SAT); + break; + case UNSATISFIABLE: + list.add(Z3Constants.UNSAT); + + for (Expr i : s.getUnsatCore()) { + list.add(getName(i.toString())); + } + } + + return list; + } + + public List getErrors(Context ctx, Solver s, Status st, String constrName, List constrList, List constrLabelList) { + List list = new ArrayList(); + + switch (st) { + case UNKNOWN: + String reason = s.getReasonUnknown(); + System.out.println("*Unknown:" + constrName + " - " + reason); + + Goal g = ctx.mkGoal(false, false, false); + for (int i = 0; i < constrList.size(); i++) { + g.add(constrList.get(i), constrLabelList.get(i)); + } + + Tactic t = ctx.mkTactic("qfbv"); + try { + ApplyResult ar = t.apply(g); + if (ar.getNumSubgoals() == 1) { + if (ar.getSubgoals()[0].isDecidedSat()) { + System.out.println("=> SAT"); + list.add(Z3Constants.SAT); + break; + } + } + } catch (Exception e) { + System.out.println("2ND Check"); + + t = ctx.mkTactic("smt"); + try { + ApplyResult ar = t.apply(g); + if (ar.getNumSubgoals() == 1) { + if (ar.getSubgoals()[0].isDecidedSat()) { + System.out.println("==> SAT"); + list.add(Z3Constants.SAT); + break; + } + } + } catch (Exception e2) { + e2.printStackTrace(); + } + } + + list.add(Z3Constants.UNKNOWN); + list.add(reason); + break; + case SATISFIABLE: + list.add(Z3Constants.SAT); + break; + case UNSATISFIABLE: + list.add(Z3Constants.UNSAT); + + for (Expr i : s.getUnsatCore()) { + list.add(getName(i.toString())); + } + } + + return list; + } + + public IConstraintCalculation getConstraintCaluculator(IProject project) throws RuntimeException { + + if (!loadZ3Lib()) { + String errMsg = ERROR_ENV_PATH; + throw new RuntimeException(errMsg); + } + + IConstraintCalculation calc = null; + IFile file = findFile(CONST_SCRIPT_NAME, project); + if (file != null) { + String fileName = file.getName(); + String className = fileName.substring(0, fileName.lastIndexOf(".")); + + String string = file.getLocation().toString(); + String genPath = string.substring(0, string.length() - fileName.length()); + + calc = getConstraintCaluculator(fileName, className, genPath); + + } else { + String errMsg = String.format(ERROR_NOT_FOUND_SCRIPT, project.getName(), CONST_SCRIPT_NAME); + throw new RuntimeException(errMsg); + } + + return calc; + } + + public IConstraintCalculation getConstraintCaluculator(String fileName, String className, String genPath) throws RuntimeException { + IConstraintCalculation calc = null; + try { + GroovyScriptEngine e = new GroovyScriptEngine(new String[] { genPath }, getClass().getClassLoader()); + e.loadScriptByName(fileName); + Class s = e.getGroovyClassLoader().loadClass(className); + + calc = (IConstraintCalculation) s.newInstance(); + } catch (Exception e) { + String errMsg = ERROR_SCRIPT; + System.out.println(e.getMessage()); + throw new RuntimeException(errMsg); + } + return calc; + } +} diff --git a/rba.tool.core/src/rba/tool/core/z3/Z3Constants.java b/rba.tool.core/src/rba/tool/core/z3/Z3Constants.java new file mode 100644 index 0000000..51e726f --- /dev/null +++ b/rba.tool.core/src/rba/tool/core/z3/Z3Constants.java @@ -0,0 +1,18 @@ +package rba.tool.core.z3; + +public class Z3Constants { + + public static String TOTAL_RESULT = "Z3_CODE_TOTAL_RESULT"; + + public static String SAT = "SAT"; + + public static String UNSAT = "UNSAT"; + + public static String UNKNOWN = "UNKNOWN"; + + public static Integer SAT_VAL = 0; + + public static Integer UNSAT_VAL = -99; + + public static Integer UNKNOWN_VAL = -98; +} -- cgit 1.2.3-korg