6 files changed, 28 insertions, 77 deletions

diff --git a/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext b/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext
index 9e032a13..d4fa6f35 100644
--- a/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext
+++ b/language/src/main/java/org/eclipse/viatra/solver/language/Problem.xtext
@@ -8,7 +8,8 @@ Problem:
         statements+=Statement*;
 
 Statement:
-        ClassDeclaration | EnumDeclaration | PredicateDefinition | Assertion | NodeValueAssertion | ScopeDeclaration;
+        ClassDeclaration | EnumDeclaration | PredicateDefinition | Assertion | NodeValueAssertion | ScopeDeclaration |
+        UniqueDeclaration;
 
 ClassDeclaration:
         abstract?="abstract"? "class"
@@ -25,7 +26,7 @@ EnumLiteral returns Node:
         name=Identifier;
 
 ReferenceDeclaration:
-        (containment?="contains" | "refers")?
+        (-> (containment?="contains" | "refers"))?
         referenceType=[Relation|QualifiedName]
         ("[" multiplicity=Multiplicity "]")?
         name=Identifier
@@ -35,7 +36,7 @@ PredicateDefinition:
         (error?="error" "pred"? | "pred")
         name=Identifier
         "(" (parameters+=Parameter ("," parameters+=Parameter)*)? ")"
-        ("<=>" bodies+=Conjunction (";" bodies+=Conjunction)*)?
+        ("<->" bodies+=Conjunction (";" bodies+=Conjunction)*)?
         ".";
 
 Parameter:
@@ -65,6 +66,7 @@ ConstantArgument:
         constant=Constant;
 
 Assertion:
+        default?="default"?
         (relation=[Relation|QualifiedName]
         "(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")"
         ":" value=LogicValue |
@@ -74,16 +76,19 @@ Assertion:
         ".";
 
 AssertionArgument:
-        NodeAssertionArgument | ConstantAssertionArgument;
+        NodeAssertionArgument | WildcardAssertionArgument | ConstantAssertionArgument;
 
 NodeAssertionArgument:
         node=[Node|QualifiedName];
 
+WildcardAssertionArgument:
+        {WildcardAssertionArgument} "*";
+
 ConstantAssertionArgument:
         constant=Constant;
 
 enum LogicValue:
-        TRUE="true" | FALSE="false" | UNKNOWN="unknown";
+        TRUE="true" | FALSE="false" | UNKNOWN="unknown" | ERROR="error";
 
 enum ShortLogicValue returns LogicValue:
         FALSE="!" | UNKNOWN="?";
@@ -126,14 +131,18 @@ RangeMultiplicity:
 ExactMultiplicity:
         exactValue=INT;
 
+UniqueDeclaration:
+        "unique" nodes+=EnumLiteral ("," nodes+=EnumLiteral)* ".";
+
 UpperBound returns ecore::EInt:
         INT | "*";
 
 QualifiedName hidden():
-        QUOTED_ID | Identifier ("::" Identifier)*;
+        Identifier ("::" Identifier)*;
 
 Identifier:
-        ID | "true" | "false";
+        ID | "true" | "false" | "unknown" | "error" | "class" | "abstract" | "extends" | "enum" | "pred" | "scope" |
+        "unique" | "default" | "problem" | "contains" | "refers";
 
 Integer returns ecore::EInt hidden():
         "-"? INT;
@@ -143,18 +152,11 @@ Real returns ecore::EDouble:
 
 @Override
 terminal ID:
-        ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'0'..'9')*;
+        ('a'..'z' | 'A'..'Z' | '_') ('a'..'z' | 'A'..'Z' | '_' | '0'..'9')*;
 
 terminal EXPONENTIAL:
         INT ("e" | "E") ("+" | "-")? INT;
 
 @Override
-terminal STRING:
-        '"' ('\\' . /* 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' */ | !('\\' | '"'))* '"';
-
-terminal QUOTED_ID:
-        "'" ('\\' . /* 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'\\' */ | !('\\' | "'"))* "'";
-
-@Override
 terminal SL_COMMENT:
         ('%' | '//') !('\n' | '\r')* ('\r'? '\n')?;
diff --git a/language/src/main/java/org/eclipse/viatra/solver/language/ProblemUtil.java b/language/src/main/java/org/eclipse/viatra/solver/language/ProblemUtil.java
index 2d7fede6..1581186c 100644
--- a/language/src/main/java/org/eclipse/viatra/solver/language/ProblemUtil.java
+++ b/language/src/main/java/org/eclipse/viatra/solver/language/ProblemUtil.java
@@ -16,7 +16,6 @@ import org.eclipse.viatra.solver.language.model.problem.ProblemPackage;
 import org.eclipse.viatra.solver.language.model.problem.ReferenceDeclaration;
 import org.eclipse.viatra.solver.language.model.problem.Relation;
 import org.eclipse.viatra.solver.language.model.problem.Variable;
-import org.eclipse.viatra.solver.language.naming.NamingUtil;
 import org.eclipse.viatra.solver.language.scoping.ProblemGlobalScopeProvider;
 
 import com.google.common.collect.ImmutableList;
@@ -32,12 +31,10 @@ public final class ProblemUtil {
                 return variable.eContainingFeature() == ProblemPackage.Literals.VARIABLE_OR_NODE_ARGUMENT__SINGLETON_VARIABLE;
         }
 
-        public static boolean isEnumLiteral(Node node) {
-                return node.eContainingFeature() == ProblemPackage.Literals.ENUM_DECLARATION__LITERALS;
-        }
-
-        public static boolean isEnumNode(Node node) {
-                return NamingUtil.isQuotedName(node.getName()) || isEnumLiteral(node);
+        public static boolean isUniqueNode(Node node) {
+                var containingFeature = node.eContainingFeature();
+                return containingFeature == ProblemPackage.Literals.UNIQUE_DECLARATION__NODES
+                                || containingFeature == ProblemPackage.Literals.ENUM_DECLARATION__LITERALS;
         }
 
         public static boolean isNewNode(Node node) {
diff --git a/language/src/main/java/org/eclipse/viatra/solver/language/naming/NamingUtil.java b/language/src/main/java/org/eclipse/viatra/solver/language/naming/NamingUtil.java
index decc014a..edd455bb 100644
--- a/language/src/main/java/org/eclipse/viatra/solver/language/naming/NamingUtil.java
+++ b/language/src/main/java/org/eclipse/viatra/solver/language/naming/NamingUtil.java
@@ -4,8 +4,6 @@ import java.util.regex.Pattern;
 
 public final class NamingUtil {
         private static final String SINGLETON_VARIABLE_PREFIX = "_";
-
-        private static final String ENUM_NODE_NAME_QUOTE = "'";
         
         private static final Pattern ID_REGEX = Pattern.compile("[_a-zA-Z][_0-9a-zA-Z]*");
 
@@ -20,16 +18,8 @@ public final class NamingUtil {
         public static boolean isSingletonVariableName(String name) {
                 return name != null && name.startsWith(SINGLETON_VARIABLE_PREFIX);
         }
-
-        public static boolean isQuotedName(String name) {
-                return name != null && name.startsWith(ENUM_NODE_NAME_QUOTE) && name.endsWith(ENUM_NODE_NAME_QUOTE);
-        }
         
         public static boolean isValidId(String name) {
                 return name != null && ID_REGEX.matcher(name).matches();
         }
-        
-        public static boolean isValidNodeName(String name) {
-                return isValidId(name) || isQuotedName(name);
-        }
 }
diff --git a/language/src/main/java/org/eclipse/viatra/solver/language/resource/NodeNameCollector.java b/language/src/main/java/org/eclipse/viatra/solver/language/resource/NodeNameCollector.java
index 597dd92d..e9533c25 100644
--- a/language/src/main/java/org/eclipse/viatra/solver/language/resource/NodeNameCollector.java
+++ b/language/src/main/java/org/eclipse/viatra/solver/language/resource/NodeNameCollector.java
@@ -2,24 +2,16 @@ package org.eclipse.viatra.solver.language.resource;
 
 import java.util.List;
 import java.util.Set;
-import java.util.function.Predicate;
 
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.EStructuralFeature;
-import org.eclipse.viatra.solver.language.model.problem.Argument;
 import org.eclipse.viatra.solver.language.model.problem.Assertion;
 import org.eclipse.viatra.solver.language.model.problem.AssertionArgument;
-import org.eclipse.viatra.solver.language.model.problem.Atom;
-import org.eclipse.viatra.solver.language.model.problem.Conjunction;
-import org.eclipse.viatra.solver.language.model.problem.Literal;
-import org.eclipse.viatra.solver.language.model.problem.NegativeLiteral;
 import org.eclipse.viatra.solver.language.model.problem.NodeAssertionArgument;
 import org.eclipse.viatra.solver.language.model.problem.NodeValueAssertion;
-import org.eclipse.viatra.solver.language.model.problem.PredicateDefinition;
 import org.eclipse.viatra.solver.language.model.problem.Problem;
 import org.eclipse.viatra.solver.language.model.problem.ProblemPackage;
 import org.eclipse.viatra.solver.language.model.problem.Statement;
-import org.eclipse.viatra.solver.language.model.problem.VariableOrNodeArgument;
 import org.eclipse.viatra.solver.language.naming.NamingUtil;
 import org.eclipse.xtext.linking.impl.LinkingHelper;
 import org.eclipse.xtext.naming.IQualifiedNameConverter;
@@ -64,57 +56,26 @@ public class NodeNameCollector {
                         collectAssertionNodeNames((Assertion) statement);
                 } else if (statement instanceof NodeValueAssertion) {
                         collectNodeValueAssertionNodeNames((NodeValueAssertion) statement);
-                } else if (statement instanceof PredicateDefinition) {
-                        collectPredicateDefinitionNodeNames((PredicateDefinition) statement);
                 }
         }
 
         protected void collectAssertionNodeNames(Assertion assertion) {
                 for (AssertionArgument argument : assertion.getArguments()) {
                         if (argument instanceof NodeAssertionArgument) {
-                                collectNodeNames(argument, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE,
-                                                NamingUtil::isValidNodeName);
+                                collectNodeNames(argument, ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE);
                         }
                 }
         }
 
         protected void collectNodeValueAssertionNodeNames(NodeValueAssertion nodeValueAssertion) {
-                collectNodeNames(nodeValueAssertion, ProblemPackage.Literals.NODE_VALUE_ASSERTION__NODE,
-                                NamingUtil::isValidNodeName);
+                collectNodeNames(nodeValueAssertion, ProblemPackage.Literals.NODE_VALUE_ASSERTION__NODE);
         }
 
-        protected void collectPredicateDefinitionNodeNames(PredicateDefinition predicateDefinition) {
-                for (Conjunction body : predicateDefinition.getBodies()) {
-                        for (Literal literal : body.getLiterals()) {
-                                collectLiteralNodeNames(literal);
-                        }
-                }
-        }
-
-        protected void collectLiteralNodeNames(Literal literal) {
-                Atom atom = null;
-                if (literal instanceof Atom) {
-                        atom = (Atom) literal;
-                } else if (literal instanceof NegativeLiteral) {
-                        var negativeLiteral = (NegativeLiteral) literal;
-                        atom = negativeLiteral.getAtom();
-                }
-                if (atom == null) {
-                        return;
-                }
-                for (Argument argument : atom.getArguments()) {
-                        if (argument instanceof VariableOrNodeArgument) {
-                                collectNodeNames(argument, ProblemPackage.Literals.VARIABLE_OR_NODE_ARGUMENT__VARIABLE_OR_NODE,
-                                                NamingUtil::isQuotedName);
-                        }
-                }
-        }
-
-        private void collectNodeNames(EObject eObject, EStructuralFeature feature, Predicate<String> condition) {
+        private void collectNodeNames(EObject eObject, EStructuralFeature feature) {
                 List<INode> nodes = NodeModelUtils.findNodesForFeature(eObject, feature);
                 for (INode node : nodes) {
                         var nodeName = linkingHelper.getCrossRefNodeAsString(node, true);
-                        if (!condition.test(nodeName)) {
+                        if (!NamingUtil.isValidId(nodeName)) {
                                 continue;
                         }
                         var qualifiedName = qualifiedNameConverter.toQualifiedName(nodeName);
diff --git a/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemLocationInFileProvider.java b/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemLocationInFileProvider.java
index 94dbdfee..80bbdb0f 100644
--- a/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemLocationInFileProvider.java
+++ b/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemLocationInFileProvider.java
@@ -20,7 +20,7 @@ public class ProblemLocationInFileProvider extends DefaultLocationInFileProvider
         }
 
         protected ITextRegion getNodeTextRegion(Node node, RegionDescription query) {
-                if (ProblemUtil.isEnumLiteral(node)) {
+                if (ProblemUtil.isUniqueNode(node)) {
                         return super.doGetTextRegion(node, query);
                 }
                 if (ProblemUtil.isNewNode(node)) {
diff --git a/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemResourceDescriptionStrategy.java b/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemResourceDescriptionStrategy.java
index da737e3d..012606d6 100644
--- a/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemResourceDescriptionStrategy.java
+++ b/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemResourceDescriptionStrategy.java
@@ -45,6 +45,7 @@ public class ProblemResourceDescriptionStrategy extends DefaultResourceDescripti
                 while (parent != null && parent != problem) {
                         var parentQualifiedName = getNameAsQualifiedName(parent);
                         if (parentQualifiedName == null) {
+                                parent = parent.eContainer();
                                 continue;
                         }
                         qualifiedName = parentQualifiedName.append(qualifiedName);
@@ -82,7 +83,7 @@ public class ProblemResourceDescriptionStrategy extends DefaultResourceDescripti
                 if (eObject instanceof Node) {
                         var node = (Node) eObject;
                         // Only enum literals and new nodes are visible across problem files.
-                        return ProblemUtil.isEnumLiteral(node) || ProblemUtil.isNewNode(node);
+                        return ProblemUtil.isUniqueNode(node) || ProblemUtil.isNewNode(node);
                 }
                 return true;
         }