aboutsummaryrefslogtreecommitdiffstats
path: root/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java
blob: d6a9e02c0c04f92eb46b3e0b4319985af9aa78ec (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
/*
 * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
 *
 * SPDX-License-Identifier: EPL-2.0
 */
package tools.refinery.store.reasoning.translator;

import tools.refinery.store.query.substitution.Substitution;
import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
import tools.refinery.store.reasoning.representation.PartialRelation;
import tools.refinery.store.query.term.Variable;
import tools.refinery.store.query.literal.Literal;

import java.util.*;

public final class Advice {
	private final AnyPartialSymbol source;
	private final PartialRelation target;
	private final AdviceSlot slot;
	private final boolean mandatory;
	private final List<Variable> parameters;
	private final List<Literal> literals;
	private boolean processed;

	public Advice(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot, boolean mandatory, List<Variable> parameters, List<Literal> literals) {
		if (mandatory && !slot.isMonotonic()) {
			throw new IllegalArgumentException("Only monotonic advice can be mandatory");
		}
		this.source = source;
		this.target = target;
		this.slot = slot;
		this.mandatory = mandatory;
		checkArity(parameters);
		this.parameters = parameters;
		this.literals = literals;
	}

	public AnyPartialSymbol source() {
		return source;
	}

	public PartialRelation target() {
		return target;
	}

	public AdviceSlot slot() {
		return slot;
	}

	public boolean mandatory() {
		return mandatory;
	}

	public List<Variable> parameters() {
		return parameters;
	}

	public List<Literal> literals() {
		return literals;
	}

	public boolean processed() {
		return processed;
	}

	public List<Literal> substitute(List<Variable> substituteParameters) {
		checkArity(substituteParameters);
		markProcessed();
		// Use a renewing substitution to remove any non-parameter variables and avoid clashed between variables
		// coming from different advice in the same clause.
		var substitution = Substitution.builder().putManyChecked(parameters, substituteParameters).renewing().build();
		return literals.stream().map(literal -> literal.substitute(substitution)).toList();
	}

	private void markProcessed() {
		processed = true;
	}

	public void checkProcessed() {
		if (mandatory && !processed) {
			throw new IllegalStateException("Mandatory advice %s was not processed".formatted(this));
		}
	}

	private void checkArity(List<Variable> toCheck) {
		if (toCheck.size() != target.arity()) {
			throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(),
					target.arity(), parameters.size()));
		}
	}

	public static Builder builderFor(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) {
		return new Builder(source, target, slot);
	}


	@Override
	public String toString() {
		return "Advice[source=%s, target=%s, slot=%s, mandatory=%s, parameters=%s, literals=%s]".formatted(source,
				target, slot, mandatory, parameters, literals);
	}

	public static class Builder {
		private final AnyPartialSymbol source;
		private final PartialRelation target;
		private final AdviceSlot slot;
		private boolean mandatory;
		private final List<Variable> parameters = new ArrayList<>();
		private final List<Literal> literals = new ArrayList<>();

		private Builder(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) {
			this.source = source;
			this.target = target;
			this.slot = slot;
		}

		public Builder mandatory(boolean mandatory) {
			this.mandatory = mandatory;
			return this;
		}

		public Builder mandatory() {
			return mandatory(false);
		}

		public Builder parameters(List<Variable> variables) {
			parameters.addAll(variables);
			return this;
		}

		public Builder parameters(Variable... variables) {
			return parameters(List.of(variables));
		}

		public Builder parameter(Variable variable) {
			parameters.add(variable);
			return this;
		}

		public Builder literals(Collection<Literal> literals) {
			this.literals.addAll(literals);
			return this;
		}

		public Builder literals(Literal... literals) {
			return literals(List.of(literals));
		}

		public Builder literal(Literal literal) {
			literals.add(literal);
			return this;
		}

		public Advice build() {
			return new Advice(source, target, slot, mandatory, Collections.unmodifiableList(parameters),
					Collections.unmodifiableList(literals));
		}
	}
}