Add data constant support

4 files changed, 100 insertions, 40 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 466988d8..7e253ef5 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,7 @@ Problem:
         statements+=Statement*;
 
 Statement:
-        ClassDeclaration | EnumDeclaration | PredicateDefinition | Assertion | ScopeDeclaration;
+        ClassDeclaration | EnumDeclaration | PredicateDefinition | Assertion | NodeValueAssertion | ScopeDeclaration;
 
 ClassDeclaration:
         abstract?="abstract"? "class"
@@ -56,23 +56,53 @@ Atom:
         "(" (arguments+=Argument ("," arguments+=Argument)*)? ")";
 
 Argument:
+        VariableOrNodeArgument | ConstantArgument;
+
+VariableOrNodeArgument:
         variableOrNode=[VariableOrNode|QualifiedName];
 
+ConstantArgument:
+        constant=Constant;
+
 Assertion:
         (relation=[Relation|QualifiedName]
-        "(" (arguments+=[Node|QualifiedName] ("," arguments+=[Node|QualifiedName])*)? ")"
+        "(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")"
         ":" value=LogicValue |
         value=ShortLogicValue?
         relation=[Relation|QualifiedName]
-        "(" (arguments+=[Node|QualifiedName] ("," arguments+=[Node|QualifiedName])*)? ")")
+        "(" (arguments+=AssertionArgument ("," arguments+=AssertionArgument)*)? ")")
         ".";
 
+AssertionArgument:
+        NodeAssertionArgument | ConstantAssertionArgument;
+
+NodeAssertionArgument:
+        node=[Node|QualifiedName];
+
+ConstantAssertionArgument:
+        constant=Constant;
+
 enum LogicValue:
         TRUE="true" | FALSE="false" | UNKNOWN="unknown";
 
 enum ShortLogicValue returns LogicValue:
         FALSE="!" | UNKNOWN="?";
 
+NodeValueAssertion:
+        node=[Node|QualifiedName] ":" value=Constant ".";
+
+Constant:
+        IntConstant | RealConstant | StringConstant;
+
+IntConstant:
+        intValue=Integer;
+
+RealConstant:
+        realValue=Real;
+
+StringConstant:
+        stringValue=STRING;
+
 ScopeDeclaration:
         "scope" typeScopes+=TypeScope ("," typeScopes+=TypeScope)* ".";
 
@@ -102,11 +132,21 @@ UpperBound returns ecore::EInt:
 QuotedOrUnquotedId:
         QUOTED_ID | Identifier;
 
-QualifiedName:
+QualifiedName hidden():
         QUOTED_ID | Identifier ("::" Identifier)* ("::" QUOTED_ID)?;
 
 Identifier:
-        ID | "true" | "false";
+        ID | "true" | "false" | "e" | "E";
+
+Integer returns ecore::EInt hidden():
+        "-"? INT;
+
+Real returns ecore::EDouble hidden():
+        "-"? INT ("." INT | ("." INT)? ("e" | "E") ("-" | "+")? INT);
+
+@Override
+terminal ID:
+        ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'_'|'0'..'9')*;
 
 @Override
 terminal STRING:
@@ -117,4 +157,4 @@ terminal QUOTED_ID:
 
 @Override
 terminal SL_COMMENT:
-        ('%' | '//') !('\n'|'\r')* ('\r'? '\n')?;
+        ('%' | '//') !('\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 09f062f5..e0a72687 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
@@ -38,13 +38,13 @@ public final class ProblemUtil {
         }
 
         public static boolean isSingletonVariable(Variable variable) {
-                return variable.eContainingFeature() == ProblemPackage.Literals.ARGUMENT__SINGLETON_VARIABLE;
+                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) {
                 String name = node.getName();
                 boolean isNameQuoted = name != null && name.startsWith(ENUM_NODE_NAME_QUOTE)
diff --git a/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemDerivedStateComputer.java b/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemDerivedStateComputer.java
index b885ce0e..fc03fa87 100644
--- a/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemDerivedStateComputer.java
+++ b/language/src/main/java/org/eclipse/viatra/solver/language/resource/ProblemDerivedStateComputer.java
@@ -11,6 +11,7 @@ import org.eclipse.emf.ecore.EStructuralFeature;
 import org.eclipse.viatra.solver.language.ProblemUtil;
 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.ClassDeclaration;
 import org.eclipse.viatra.solver.language.model.problem.Conjunction;
@@ -19,12 +20,15 @@ import org.eclipse.viatra.solver.language.model.problem.ImplicitVariable;
 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.Node;
+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.Parameter;
 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.ProblemFactory;
 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.xtext.linking.impl.LinkingHelper;
 import org.eclipse.xtext.naming.IQualifiedNameConverter;
 import org.eclipse.xtext.naming.QualifiedName;
@@ -97,7 +101,16 @@ public class ProblemDerivedStateComputer implements IDerivedStateComputer {
                 Set<String> nodeNames = new HashSet<>();
                 for (Statement statement : problem.getStatements()) {
                         if (statement instanceof Assertion) {
-                                addNodeNames(nodeNames, nodeScope, statement, ProblemPackage.Literals.ASSERTION__ARGUMENTS,
+                                Assertion assertion = (Assertion) statement;
+                                for (AssertionArgument argument : assertion.getArguments()) {
+                                        if (argument instanceof NodeAssertionArgument) {
+                                                addNodeNames(nodeNames, nodeScope, argument,
+                                                                ProblemPackage.Literals.NODE_ASSERTION_ARGUMENT__NODE,
+                                                                ProblemDerivedStateComputer::validNodeName);
+                                        }
+                                }
+                        } else if (statement instanceof NodeValueAssertion) {
+                                addNodeNames(nodeNames, nodeScope, statement, ProblemPackage.Literals.NODE_VALUE_ASSERTION__NODE,
                                                 ProblemDerivedStateComputer::validNodeName);
                         } else if (statement instanceof PredicateDefinition) {
                                 PredicateDefinition predicateDefinition = (PredicateDefinition) statement;
@@ -114,9 +127,11 @@ public class ProblemDerivedStateComputer implements IDerivedStateComputer {
                                                         continue;
                                                 }
                                                 for (Argument argument : atom.getArguments()) {
-                                                        addNodeNames(nodeNames, nodeScope, argument,
-                                                                        ProblemPackage.Literals.ARGUMENT__VARIABLE_OR_NODE,
-                                                                        ProblemDerivedStateComputer::validQuotedId);
+                                                        if (argument instanceof VariableOrNodeArgument) {
+                                                                addNodeNames(nodeNames, nodeScope, argument,
+                                                                                ProblemPackage.Literals.VARIABLE_OR_NODE_ARGUMENT__VARIABLE_OR_NODE,
+                                                                                ProblemDerivedStateComputer::validQuotedId);
+                                                        }
                                                 }
                                         }
                                 }
@@ -189,29 +204,31 @@ public class ProblemDerivedStateComputer implements IDerivedStateComputer {
 
         protected void createSigletonVariablesAndCollectVariables(Atom atom, Set<String> knownVariables,
                         Set<String> newVariables) {
-                IScope scope = scopeProvider.getScope(atom, ProblemPackage.Literals.ARGUMENT__VARIABLE_OR_NODE);
-                List<INode> nodes = NodeModelUtils.findNodesForFeature(atom, ProblemPackage.Literals.ATOM__ARGUMENTS);
-                int nodesSize = nodes.size();
-                List<Argument> arguments = atom.getArguments();
-                int argumentsSize = arguments.size();
-                for (int i = 0; i < nodesSize; i++) {
-                        INode node = nodes.get(i);
-                        String variableName = linkingHelper.getCrossRefNodeAsString(node, true);
-                        if (!validId(variableName)) {
-                                continue;
-                        }
-                        QualifiedName qualifiedName = qualifiedNameConverter.toQualifiedName(variableName);
-                        if (scope.getSingleElement(qualifiedName) != null) {
-                                continue;
-                        }
-                        if (ProblemUtil.isSingletonVariableName(variableName)) {
-                                if (i < argumentsSize) {
-                                        createSingletonVariable(arguments.get(i), variableName);
+                for (Argument argument : atom.getArguments()) {
+                        if (argument instanceof VariableOrNodeArgument) {
+                                VariableOrNodeArgument variableOrNodeArgument = (VariableOrNodeArgument) argument;
+                                IScope scope = scopeProvider.getScope(variableOrNodeArgument,
+                                                ProblemPackage.Literals.VARIABLE_OR_NODE_ARGUMENT__VARIABLE_OR_NODE);
+                                List<INode> nodes = NodeModelUtils.findNodesForFeature(variableOrNodeArgument,
+                                                ProblemPackage.Literals.VARIABLE_OR_NODE_ARGUMENT__VARIABLE_OR_NODE);
+                                for (INode node : nodes) {
+                                        String variableName = linkingHelper.getCrossRefNodeAsString(node, true);
+                                        if (!validId(variableName)) {
+                                                continue;
+                                        }
+                                        QualifiedName qualifiedName = qualifiedNameConverter.toQualifiedName(variableName);
+                                        if (scope.getSingleElement(qualifiedName) != null) {
+                                                continue;
+                                        }
+                                        if (ProblemUtil.isSingletonVariableName(variableName)) {
+                                                createSingletonVariable(variableOrNodeArgument, variableName);
+                                                break;
+                                        }
+                                        if (!knownVariables.contains(variableName)) {
+                                                newVariables.add(variableName);
+                                                break;
+                                        }
                                 }
-                                continue;
-                        }
-                        if (!knownVariables.contains(variableName)) {
-                                newVariables.add(variableName);
                         }
                 }
         }
@@ -229,7 +246,7 @@ public class ProblemDerivedStateComputer implements IDerivedStateComputer {
                 }
         }
 
-        protected void createSingletonVariable(Argument argument, String variableName) {
+        protected void createSingletonVariable(VariableOrNodeArgument argument, String variableName) {
                 if (validId(variableName)) {
                         ImplicitVariable variable = createNamedVariable(variableName);
                         argument.setSingletonVariable(variable);
@@ -281,7 +298,10 @@ public class ProblemDerivedStateComputer implements IDerivedStateComputer {
                         return;
                 }
                 for (Argument argument : atom.getArguments()) {
-                        argument.setSingletonVariable(null);
+                        if (argument instanceof VariableOrNodeArgument) {
+                                VariableOrNodeArgument variableOrNodeArgument = (VariableOrNodeArgument) argument;
+                                variableOrNodeArgument.setSingletonVariable(null);
+                        }
                 }
         }
 
diff --git a/language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemScopeProvider.java b/language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemScopeProvider.java
index fc4034ae..3748e81d 100644
--- a/language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemScopeProvider.java
+++ b/language/src/main/java/org/eclipse/viatra/solver/language/scoping/ProblemScopeProvider.java
@@ -10,7 +10,6 @@ import java.util.List;
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.EReference;
 import org.eclipse.viatra.solver.language.ProblemUtil;
-import org.eclipse.viatra.solver.language.model.problem.Argument;
 import org.eclipse.viatra.solver.language.model.problem.ClassDeclaration;
 import org.eclipse.viatra.solver.language.model.problem.ExistentialQuantifier;
 import org.eclipse.viatra.solver.language.model.problem.PredicateDefinition;
@@ -18,6 +17,7 @@ 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.model.problem.VariableOrNodeArgument;
 import org.eclipse.xtext.EcoreUtil2;
 import org.eclipse.xtext.scoping.IScope;
 import org.eclipse.xtext.scoping.Scopes;
@@ -34,7 +34,7 @@ public class ProblemScopeProvider extends AbstractProblemScopeProvider {
         @Override
         public IScope getScope(EObject context, EReference reference) {
                 IScope scope = super.getScope(context, reference);
-                if (reference == ProblemPackage.Literals.ARGUMENT__VARIABLE_OR_NODE) {
+                if (reference == ProblemPackage.Literals.VARIABLE_OR_NODE_ARGUMENT__VARIABLE_OR_NODE) {
                         return getVariableScope(context, scope);
                 } else if (reference == ProblemPackage.Literals.REFERENCE_DECLARATION__OPPOSITE) {
                         return getOppositeScope(context, scope);
@@ -45,8 +45,8 @@ public class ProblemScopeProvider extends AbstractProblemScopeProvider {
         protected IScope getVariableScope(EObject context, IScope delegateScope) {
                 List<Variable> variables = new ArrayList<>();
                 EObject currentContext = context;
-                if (context instanceof Argument) {
-                        Argument argument = (Argument) context;
+                if (context instanceof VariableOrNodeArgument) {
+                        VariableOrNodeArgument argument = (VariableOrNodeArgument) context;
                         Variable singletonVariable = argument.getSingletonVariable();
                         if (singletonVariable != null) {
                                 variables.add(singletonVariable);