diff options
Diffstat (limited to 'subprojects')
-rw-r--r-- | subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java | 263 |
1 files changed, 230 insertions, 33 deletions
diff --git a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java index 59ceae3f..a86e2c47 100644 --- a/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java +++ b/subprojects/language-semantics/src/main/java/tools/refinery/language/semantics/ModelInitializer.java | |||
@@ -6,6 +6,7 @@ | |||
6 | package tools.refinery.language.semantics; | 6 | package tools.refinery.language.semantics; |
7 | 7 | ||
8 | import com.google.inject.Inject; | 8 | import com.google.inject.Inject; |
9 | import org.jetbrains.annotations.Nullable; | ||
9 | import tools.refinery.language.library.BuiltinLibrary; | 10 | import tools.refinery.language.library.BuiltinLibrary; |
10 | import tools.refinery.language.model.problem.*; | 11 | import tools.refinery.language.model.problem.*; |
11 | import tools.refinery.language.scoping.imports.ImportAdapterProvider; | 12 | import tools.refinery.language.scoping.imports.ImportAdapterProvider; |
@@ -14,6 +15,7 @@ import tools.refinery.language.semantics.internal.MutableSeed; | |||
14 | import tools.refinery.language.utils.BuiltinSymbols; | 15 | import tools.refinery.language.utils.BuiltinSymbols; |
15 | import tools.refinery.language.utils.ProblemUtil; | 16 | import tools.refinery.language.utils.ProblemUtil; |
16 | import tools.refinery.logic.Constraint; | 17 | import tools.refinery.logic.Constraint; |
18 | import tools.refinery.logic.dnf.AbstractQueryBuilder; | ||
17 | import tools.refinery.logic.dnf.InvalidClauseException; | 19 | import tools.refinery.logic.dnf.InvalidClauseException; |
18 | import tools.refinery.logic.dnf.Query; | 20 | import tools.refinery.logic.dnf.Query; |
19 | import tools.refinery.logic.dnf.RelationalQuery; | 21 | import tools.refinery.logic.dnf.RelationalQuery; |
@@ -25,8 +27,16 @@ import tools.refinery.logic.term.cardinalityinterval.CardinalityIntervals; | |||
25 | import tools.refinery.logic.term.truthvalue.TruthValue; | 27 | import tools.refinery.logic.term.truthvalue.TruthValue; |
26 | import tools.refinery.logic.term.uppercardinality.UpperCardinalities; | 28 | import tools.refinery.logic.term.uppercardinality.UpperCardinalities; |
27 | import tools.refinery.store.dse.propagation.PropagationBuilder; | 29 | import tools.refinery.store.dse.propagation.PropagationBuilder; |
30 | import tools.refinery.store.dse.transition.DesignSpaceExplorationBuilder; | ||
31 | import tools.refinery.store.dse.transition.Rule; | ||
32 | import tools.refinery.store.dse.transition.RuleBuilder; | ||
33 | import tools.refinery.store.dse.transition.actions.ActionLiteral; | ||
28 | import tools.refinery.store.model.ModelStoreBuilder; | 34 | import tools.refinery.store.model.ModelStoreBuilder; |
29 | import tools.refinery.store.reasoning.ReasoningAdapter; | 35 | import tools.refinery.store.reasoning.ReasoningAdapter; |
36 | import tools.refinery.store.reasoning.actions.PartialActionLiterals; | ||
37 | import tools.refinery.store.reasoning.literal.Concreteness; | ||
38 | import tools.refinery.store.reasoning.literal.ModalConstraint; | ||
39 | import tools.refinery.store.reasoning.literal.Modality; | ||
30 | import tools.refinery.store.reasoning.representation.PartialRelation; | 40 | import tools.refinery.store.reasoning.representation.PartialRelation; |
31 | import tools.refinery.store.reasoning.scope.ScopePropagator; | 41 | import tools.refinery.store.reasoning.scope.ScopePropagator; |
32 | import tools.refinery.store.reasoning.seed.ModelSeed; | 42 | import tools.refinery.store.reasoning.seed.ModelSeed; |
@@ -87,6 +97,8 @@ public class ModelInitializer { | |||
87 | 97 | ||
88 | private ModelSeed modelSeed; | 98 | private ModelSeed modelSeed; |
89 | 99 | ||
100 | private int ruleCount; | ||
101 | |||
90 | public void readProblem(Problem problem) { | 102 | public void readProblem(Problem problem) { |
91 | if (this.problem != null) { | 103 | if (this.problem != null) { |
92 | throw new IllegalArgumentException("Problem was already set"); | 104 | throw new IllegalArgumentException("Problem was already set"); |
@@ -174,6 +186,7 @@ public class ModelInitializer { | |||
174 | storeBuilder.with(scopePropagator); | 186 | storeBuilder.with(scopePropagator); |
175 | } | 187 | } |
176 | collectPredicates(storeBuilder); | 188 | collectPredicates(storeBuilder); |
189 | collectRules(storeBuilder); | ||
177 | } catch (TranslationException e) { | 190 | } catch (TranslationException e) { |
178 | throw problemTrace.wrapException(e); | 191 | throw problemTrace.wrapException(e); |
179 | } | 192 | } |
@@ -379,14 +392,16 @@ public class ModelInitializer { | |||
379 | 392 | ||
380 | private static CardinalityInterval getCardinalityInterval( | 393 | private static CardinalityInterval getCardinalityInterval( |
381 | tools.refinery.language.model.problem.Multiplicity problemMultiplicity) { | 394 | tools.refinery.language.model.problem.Multiplicity problemMultiplicity) { |
382 | if (problemMultiplicity instanceof ExactMultiplicity exactMultiplicity) { | 395 | switch (problemMultiplicity) { |
396 | case ExactMultiplicity exactMultiplicity -> { | ||
383 | return CardinalityIntervals.exactly(exactMultiplicity.getExactValue()); | 397 | return CardinalityIntervals.exactly(exactMultiplicity.getExactValue()); |
384 | } else if (problemMultiplicity instanceof RangeMultiplicity rangeMultiplicity) { | 398 | } |
399 | case RangeMultiplicity rangeMultiplicity -> { | ||
385 | var upperBound = rangeMultiplicity.getUpperBound(); | 400 | var upperBound = rangeMultiplicity.getUpperBound(); |
386 | return CardinalityIntervals.between(rangeMultiplicity.getLowerBound(), | 401 | return CardinalityIntervals.between(rangeMultiplicity.getLowerBound(), |
387 | upperBound < 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(upperBound)); | 402 | upperBound < 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.atMost(upperBound)); |
388 | } else { | 403 | } |
389 | throw new TracedException(problemMultiplicity, "Unknown multiplicity"); | 404 | default -> throw new TracedException(problemMultiplicity, "Unknown multiplicity"); |
390 | } | 405 | } |
391 | } | 406 | } |
392 | 407 | ||
@@ -612,23 +627,29 @@ public class ModelInitializer { | |||
612 | } | 627 | } |
613 | var builder = Query.builder(name).parameters(parameters); | 628 | var builder = Query.builder(name).parameters(parameters); |
614 | for (var body : predicateDefinition.getBodies()) { | 629 | for (var body : predicateDefinition.getBodies()) { |
615 | try { | 630 | buildConjunction(body, parameterMap, commonLiterals, builder); |
616 | var localScope = extendScope(parameterMap, body.getImplicitVariables()); | ||
617 | var problemLiterals = body.getLiterals(); | ||
618 | var literals = new ArrayList<>(commonLiterals); | ||
619 | for (var problemLiteral : problemLiterals) { | ||
620 | toLiteralsTraced(problemLiteral, localScope, literals); | ||
621 | } | ||
622 | builder.clause(literals); | ||
623 | } catch (RuntimeException e) { | ||
624 | throw TracedException.addTrace(body, e); | ||
625 | } | ||
626 | } | 631 | } |
627 | return builder.build(); | 632 | return builder.build(); |
628 | } | 633 | } |
629 | 634 | ||
630 | private Map<tools.refinery.language.model.problem.Variable, Variable> extendScope( | 635 | private void buildConjunction( |
631 | Map<tools.refinery.language.model.problem.Variable, Variable> existing, | 636 | Conjunction body, HashMap<tools.refinery.language.model.problem.Variable, ? extends Variable> parameterMap, |
637 | List<Literal> commonLiterals, AbstractQueryBuilder<?> builder) { | ||
638 | try { | ||
639 | var localScope = extendScope(parameterMap, body.getImplicitVariables()); | ||
640 | var problemLiterals = body.getLiterals(); | ||
641 | var literals = new ArrayList<>(commonLiterals); | ||
642 | for (var problemLiteral : problemLiterals) { | ||
643 | toLiteralsTraced(problemLiteral, localScope, literals); | ||
644 | } | ||
645 | builder.clause(literals); | ||
646 | } catch (RuntimeException e) { | ||
647 | throw TracedException.addTrace(body, e); | ||
648 | } | ||
649 | } | ||
650 | |||
651 | private Map<tools.refinery.language.model.problem.Variable, ? extends Variable> extendScope( | ||
652 | Map<tools.refinery.language.model.problem.Variable, ? extends Variable> existing, | ||
632 | Collection<? extends tools.refinery.language.model.problem.Variable> newVariables) { | 653 | Collection<? extends tools.refinery.language.model.problem.Variable> newVariables) { |
633 | if (newVariables.isEmpty()) { | 654 | if (newVariables.isEmpty()) { |
634 | return existing; | 655 | return existing; |
@@ -642,8 +663,9 @@ public class ModelInitializer { | |||
642 | return localScope; | 663 | return localScope; |
643 | } | 664 | } |
644 | 665 | ||
645 | private void toLiteralsTraced(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope, | 666 | private void toLiteralsTraced( |
646 | List<Literal> literals) { | 667 | Expr expr, Map<tools.refinery.language.model.problem.Variable, ? extends Variable> localScope, |
668 | List<Literal> literals) { | ||
647 | try { | 669 | try { |
648 | toLiterals(expr, localScope, literals); | 670 | toLiterals(expr, localScope, literals); |
649 | } catch (RuntimeException e) { | 671 | } catch (RuntimeException e) { |
@@ -651,9 +673,12 @@ public class ModelInitializer { | |||
651 | } | 673 | } |
652 | } | 674 | } |
653 | 675 | ||
654 | private void toLiterals(Expr expr, Map<tools.refinery.language.model.problem.Variable, Variable> localScope, | 676 | private void toLiterals( |
655 | List<Literal> literals) { | 677 | Expr expr, Map<tools.refinery.language.model.problem.Variable, ? extends Variable> localScope, |
656 | switch (expr) { | 678 | List<Literal> literals) { |
679 | var extractedOuter = extractModalExpr(expr); | ||
680 | var outerModality = extractedOuter.modality(); | ||
681 | switch (extractedOuter.body()) { | ||
657 | case LogicConstant logicConstant -> { | 682 | case LogicConstant logicConstant -> { |
658 | switch (logicConstant.getLogicValue()) { | 683 | switch (logicConstant.getLogicValue()) { |
659 | case TRUE -> literals.add(BooleanLiteral.TRUE); | 684 | case TRUE -> literals.add(BooleanLiteral.TRUE); |
@@ -665,12 +690,13 @@ public class ModelInitializer { | |||
665 | var target = getPartialRelation(atom.getRelation()); | 690 | var target = getPartialRelation(atom.getRelation()); |
666 | var polarity = atom.isTransitiveClosure() ? CallPolarity.TRANSITIVE : CallPolarity.POSITIVE; | 691 | var polarity = atom.isTransitiveClosure() ? CallPolarity.TRANSITIVE : CallPolarity.POSITIVE; |
667 | var argumentList = toArgumentList(atom.getArguments(), localScope, literals); | 692 | var argumentList = toArgumentList(atom.getArguments(), localScope, literals); |
668 | literals.add(target.call(polarity, argumentList)); | 693 | literals.add(extractedOuter.modality.wrapConstraint(target).call(polarity, argumentList)); |
669 | } | 694 | } |
670 | case NegationExpr negationExpr -> { | 695 | case NegationExpr negationExpr -> { |
671 | var body = negationExpr.getBody(); | 696 | var body = negationExpr.getBody(); |
672 | if (!(body instanceof Atom atom)) { | 697 | var extractedInner = extractModalExpr(body); |
673 | throw new TracedException(body, "Cannot negate literal"); | 698 | if (!(extractedInner.body() instanceof Atom atom)) { |
699 | throw new TracedException(extractedInner.body(), "Cannot negate literal"); | ||
674 | } | 700 | } |
675 | var target = getPartialRelation(atom.getRelation()); | 701 | var target = getPartialRelation(atom.getRelation()); |
676 | Constraint constraint; | 702 | Constraint constraint; |
@@ -683,7 +709,8 @@ public class ModelInitializer { | |||
683 | } | 709 | } |
684 | var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables()); | 710 | var negatedScope = extendScope(localScope, negationExpr.getImplicitVariables()); |
685 | var argumentList = toArgumentList(atom.getArguments(), negatedScope, literals); | 711 | var argumentList = toArgumentList(atom.getArguments(), negatedScope, literals); |
686 | literals.add(constraint.call(CallPolarity.NEGATIVE, argumentList)); | 712 | var innerModality = extractedInner.modality().merge(outerModality.negate()); |
713 | literals.add(innerModality.wrapConstraint(constraint).call(CallPolarity.NEGATIVE, argumentList)); | ||
687 | } | 714 | } |
688 | case ComparisonExpr comparisonExpr -> { | 715 | case ComparisonExpr comparisonExpr -> { |
689 | var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()), | 716 | var argumentList = toArgumentList(List.of(comparisonExpr.getLeft(), comparisonExpr.getRight()), |
@@ -694,14 +721,70 @@ public class ModelInitializer { | |||
694 | default -> throw new TracedException( | 721 | default -> throw new TracedException( |
695 | comparisonExpr, "Unsupported operator"); | 722 | comparisonExpr, "Unsupported operator"); |
696 | }; | 723 | }; |
697 | literals.add(new EquivalenceLiteral(positive, argumentList.get(0), argumentList.get(1))); | 724 | literals.add(outerModality.createEquivalence(positive, argumentList.get(0), argumentList.get(1))); |
725 | } | ||
726 | default -> throw new TracedException(extractedOuter.body(), "Unsupported literal"); | ||
727 | } | ||
728 | } | ||
729 | |||
730 | private record ConcreteModality(@Nullable Concreteness concreteness, @Nullable Modality modality) { | ||
731 | public static final ConcreteModality NULL = new ConcreteModality((Concreteness) null, null); | ||
732 | |||
733 | public ConcreteModality(tools.refinery.language.model.problem.Concreteness concreteness, | ||
734 | tools.refinery.language.model.problem.Modality modality) { | ||
735 | this( | ||
736 | switch (concreteness) { | ||
737 | case PARTIAL -> Concreteness.PARTIAL; | ||
738 | case CANDIDATE -> Concreteness.CANDIDATE; | ||
739 | }, | ||
740 | switch (modality) { | ||
741 | case MUST -> Modality.MUST; | ||
742 | case MAY -> Modality.MAY; | ||
743 | case NONE -> throw new IllegalArgumentException("Invalid modality"); | ||
744 | } | ||
745 | ); | ||
746 | } | ||
747 | |||
748 | public ConcreteModality negate() { | ||
749 | var negatedModality = modality == null ? null : modality.negate(); | ||
750 | return new ConcreteModality(concreteness, negatedModality); | ||
751 | } | ||
752 | |||
753 | public ConcreteModality merge(ConcreteModality outer) { | ||
754 | var mergedConcreteness = concreteness == null ? outer.concreteness() : concreteness; | ||
755 | var mergedModality = modality == null ? outer.modality() : modality; | ||
756 | return new ConcreteModality(mergedConcreteness, mergedModality); | ||
698 | } | 757 | } |
699 | default -> throw new TracedException(expr, "Unsupported literal"); | 758 | |
759 | public Constraint wrapConstraint(Constraint inner) { | ||
760 | if (concreteness != null && modality != null) { | ||
761 | return new ModalConstraint(modality, concreteness, inner); | ||
762 | } | ||
763 | return inner; | ||
764 | } | ||
765 | |||
766 | public Literal createEquivalence(boolean positive, Variable left, Variable right) { | ||
767 | if (concreteness != null && modality != null) { | ||
768 | var polarity = positive ? CallPolarity.POSITIVE : CallPolarity.NEGATIVE; | ||
769 | return wrapConstraint(ReasoningAdapter.EQUALS_SYMBOL).call(polarity, left, right); | ||
770 | } | ||
771 | return new EquivalenceLiteral(positive, left, right); | ||
700 | } | 772 | } |
701 | } | 773 | } |
702 | 774 | ||
775 | private record ExtractedModalExpr(ConcreteModality modality, Expr body) { | ||
776 | } | ||
777 | |||
778 | private ExtractedModalExpr extractModalExpr(Expr expr) { | ||
779 | if (expr instanceof ModalExpr modalExpr) { | ||
780 | return new ExtractedModalExpr(new ConcreteModality(modalExpr.getConcreteness(), modalExpr.getModality()), | ||
781 | modalExpr.getBody()); | ||
782 | } | ||
783 | return new ExtractedModalExpr(ConcreteModality.NULL, expr); | ||
784 | } | ||
785 | |||
703 | private List<Variable> toArgumentList( | 786 | private List<Variable> toArgumentList( |
704 | List<Expr> expressions, Map<tools.refinery.language.model.problem.Variable, Variable> localScope, | 787 | List<Expr> expressions, Map<tools.refinery.language.model.problem.Variable, ? extends Variable> localScope, |
705 | List<Literal> literals) { | 788 | List<Literal> literals) { |
706 | var argumentList = new ArrayList<Variable>(expressions.size()); | 789 | var argumentList = new ArrayList<Variable>(expressions.size()); |
707 | for (var expr : expressions) { | 790 | for (var expr : expressions) { |
@@ -709,12 +792,14 @@ public class ModelInitializer { | |||
709 | throw new TracedException(expr, "Unsupported argument"); | 792 | throw new TracedException(expr, "Unsupported argument"); |
710 | } | 793 | } |
711 | var variableOrNode = variableOrNodeExpr.getVariableOrNode(); | 794 | var variableOrNode = variableOrNodeExpr.getVariableOrNode(); |
712 | if (variableOrNode instanceof Node node) { | 795 | switch (variableOrNode) { |
796 | case Node node -> { | ||
713 | int nodeId = getNodeId(node); | 797 | int nodeId = getNodeId(node); |
714 | var tempVariable = Variable.of(semanticsUtils.getNameWithoutRootPrefix(node).orElse("_" + nodeId)); | 798 | var tempVariable = Variable.of(semanticsUtils.getNameWithoutRootPrefix(node).orElse("_" + nodeId)); |
715 | literals.add(new ConstantLiteral(tempVariable, nodeId)); | 799 | literals.add(new ConstantLiteral(tempVariable, nodeId)); |
716 | argumentList.add(tempVariable); | 800 | argumentList.add(tempVariable); |
717 | } else if (variableOrNode instanceof tools.refinery.language.model.problem.Variable problemVariable) { | 801 | } |
802 | case tools.refinery.language.model.problem.Variable problemVariable -> { | ||
718 | if (variableOrNodeExpr.getSingletonVariable() == problemVariable) { | 803 | if (variableOrNodeExpr.getSingletonVariable() == problemVariable) { |
719 | argumentList.add(Variable.of(problemVariable.getName())); | 804 | argumentList.add(Variable.of(problemVariable.getName())); |
720 | } else { | 805 | } else { |
@@ -724,8 +809,8 @@ public class ModelInitializer { | |||
724 | } | 809 | } |
725 | argumentList.add(variable); | 810 | argumentList.add(variable); |
726 | } | 811 | } |
727 | } else { | 812 | } |
728 | throw new TracedException(variableOrNode, "Unknown argument"); | 813 | default -> throw new TracedException(variableOrNode, "Unknown argument"); |
729 | } | 814 | } |
730 | } | 815 | } |
731 | return argumentList; | 816 | return argumentList; |
@@ -801,4 +886,116 @@ public class ModelInitializer { | |||
801 | return defaultAssertions; | 886 | return defaultAssertions; |
802 | } | 887 | } |
803 | } | 888 | } |
889 | |||
890 | private void collectRules(ModelStoreBuilder storeBuilder) { | ||
891 | for (var importedProblem : importedProblems) { | ||
892 | for (var statement : importedProblem.getStatements()) { | ||
893 | if (statement instanceof RuleDefinition ruleDefinition) { | ||
894 | collectRule(ruleDefinition, storeBuilder); | ||
895 | } | ||
896 | } | ||
897 | } | ||
898 | } | ||
899 | |||
900 | private void collectRule(RuleDefinition ruleDefinition, ModelStoreBuilder storeBuilder) { | ||
901 | var name = semanticsUtils.getNameWithoutRootPrefix(ruleDefinition) | ||
902 | .orElseGet(() -> "::rule" + ruleCount); | ||
903 | ruleCount++; | ||
904 | var rule = toRule(name, ruleDefinition); | ||
905 | switch (ruleDefinition.getKind()) { | ||
906 | case DECISION -> storeBuilder.tryGetAdapter(DesignSpaceExplorationBuilder.class) | ||
907 | .ifPresent(dseBuilder -> dseBuilder.transformation(rule)); | ||
908 | case PROPAGATION -> storeBuilder.tryGetAdapter(PropagationBuilder.class) | ||
909 | .ifPresent(propagationBuilder -> propagationBuilder.rule(rule)); | ||
910 | case REFINEMENT -> { | ||
911 | // Rules not marked for decision or propagation are not invoked automatically. | ||
912 | } | ||
913 | } | ||
914 | } | ||
915 | |||
916 | private Rule toRule(String name, RuleDefinition ruleDefinition) { | ||
917 | var problemParameters = ruleDefinition.getParameters(); | ||
918 | int arity = problemParameters.size(); | ||
919 | var parameters = new NodeVariable[arity]; | ||
920 | var parameterMap = HashMap.<tools.refinery.language.model.problem.Variable, NodeVariable>newHashMap(arity); | ||
921 | var commonLiterals = new ArrayList<Literal>(); | ||
922 | var parametersToFocus = new ArrayList<tools.refinery.language.model.problem.Variable>(); | ||
923 | for (int i = 0; i < arity; i++) { | ||
924 | var problemParameter = problemParameters.get(i); | ||
925 | var parameter = Variable.of(problemParameter.getName()); | ||
926 | parameters[i] = parameter; | ||
927 | parameterMap.put(problemParameter, parameter); | ||
928 | var parameterType = problemParameter.getParameterType(); | ||
929 | if (parameterType != null) { | ||
930 | var partialType = getPartialRelation(parameterType); | ||
931 | var modality = new ConcreteModality(problemParameter.getConcreteness(), | ||
932 | problemParameter.getModality()); | ||
933 | commonLiterals.add(modality.wrapConstraint(partialType).call(parameter)); | ||
934 | } | ||
935 | if (ruleDefinition.getKind() == RuleKind.DECISION && | ||
936 | problemParameter.getBinding() == ParameterBinding.SINGLE) { | ||
937 | commonLiterals.add(MultiObjectTranslator.MULTI_VIEW.call(CallPolarity.NEGATIVE, parameter)); | ||
938 | } | ||
939 | if (problemParameter.getBinding() == ParameterBinding.FOCUS) { | ||
940 | parametersToFocus.add(problemParameter); | ||
941 | } | ||
942 | } | ||
943 | var builder = Rule.builder(name).parameters(parameters); | ||
944 | for (var precondition : ruleDefinition.getPreconditions()) { | ||
945 | buildConjunction(precondition, parameterMap, commonLiterals, builder); | ||
946 | } | ||
947 | for (var consequent : ruleDefinition.getConsequents()) { | ||
948 | buildConsequent(consequent, parameterMap, parametersToFocus, builder); | ||
949 | } | ||
950 | return builder.build(); | ||
951 | } | ||
952 | |||
953 | private void buildConsequent( | ||
954 | Consequent body, HashMap<tools.refinery.language.model.problem.Variable, NodeVariable> parameterMap, | ||
955 | Collection<tools.refinery.language.model.problem.Variable> parametersToFocus, RuleBuilder builder) { | ||
956 | try { | ||
957 | var actionLiterals = new ArrayList<ActionLiteral>(); | ||
958 | HashMap<tools.refinery.language.model.problem.Variable, NodeVariable> localScope; | ||
959 | if (parametersToFocus.isEmpty()) { | ||
960 | localScope = parameterMap; | ||
961 | } else { | ||
962 | localScope = new LinkedHashMap<>(parameterMap); | ||
963 | for (var parameterToFocus : parametersToFocus) { | ||
964 | var originalParameter = parameterMap.get(parameterToFocus); | ||
965 | var focusedParameter = Variable.of(originalParameter.getName() + "#focused"); | ||
966 | localScope.put(parameterToFocus, focusedParameter); | ||
967 | actionLiterals.add(PartialActionLiterals.focus(originalParameter, focusedParameter)); | ||
968 | } | ||
969 | } | ||
970 | for (var action : body.getActions()) { | ||
971 | actionLiterals.add(toActionLiteral(action, localScope)); | ||
972 | } | ||
973 | builder.action(actionLiterals); | ||
974 | } catch (RuntimeException e) { | ||
975 | throw TracedException.addTrace(body, e); | ||
976 | } | ||
977 | } | ||
978 | |||
979 | private ActionLiteral toActionLiteral( | ||
980 | Action action, HashMap<tools.refinery.language.model.problem.Variable, NodeVariable> localScope) { | ||
981 | if (!(action instanceof AssertionAction assertionAction)) { | ||
982 | throw new TracedException(action, "Unknown action"); | ||
983 | } | ||
984 | var partialRelation = getPartialRelation(assertionAction.getRelation()); | ||
985 | var truthValue = getTruthValue(assertionAction.getValue()); | ||
986 | var problemArguments = assertionAction.getArguments(); | ||
987 | var arguments = new NodeVariable[problemArguments.size()]; | ||
988 | for (int i = 0; i < arguments.length; i++) { | ||
989 | var problemArgument = problemArguments.get(i); | ||
990 | if (!(problemArgument instanceof NodeAssertionArgument nodeAssertionArgument)) { | ||
991 | throw new TracedException(problemArgument, "Invalid argument"); | ||
992 | } | ||
993 | var variableOrNode = nodeAssertionArgument.getNode(); | ||
994 | if (!(variableOrNode instanceof tools.refinery.language.model.problem.Variable problemVariable)) { | ||
995 | throw new TracedException(problemArgument, "Invalid argument"); | ||
996 | } | ||
997 | arguments[i] = localScope.get(problemVariable); | ||
998 | } | ||
999 | return PartialActionLiterals.merge(partialRelation, truthValue, arguments); | ||
1000 | } | ||
804 | } | 1001 | } |