diff options
author | Kristóf Marussy <kristof@marussy.com> | 2023-06-15 20:41:09 +0200 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2023-06-15 20:49:33 +0200 |
commit | 2599ceeccbcfb531b3a95427b1b8904caf102242 (patch) | |
tree | 9af7b51d7cafc4d966dc4915cc899fc116998c51 /subprojects/store-query/src/main | |
parent | refactor: simplified Dnf parameter directions (diff) | |
download | refinery-2599ceeccbcfb531b3a95427b1b8904caf102242.tar.gz refinery-2599ceeccbcfb531b3a95427b1b8904caf102242.tar.zst refinery-2599ceeccbcfb531b3a95427b1b8904caf102242.zip |
refactor(query): structural equality matcher
Add the ability to create assertions without pre-processing Dnf clauses (raw
matchin mode). Also fix tests broken by Dnf pre-processing.
Diffstat (limited to 'subprojects/store-query/src/main')
2 files changed, 47 insertions, 0 deletions
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java index 64790f42..c5b51b81 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java | |||
@@ -119,6 +119,11 @@ public final class Dnf implements Constraint { | |||
119 | if (arity() != other.arity()) { | 119 | if (arity() != other.arity()) { |
120 | return false; | 120 | return false; |
121 | } | 121 | } |
122 | for (int i = 0; i < arity(); i++) { | ||
123 | if (!symbolicParameters.get(i).getDirection().equals(other.getSymbolicParameters().get(i).getDirection())) { | ||
124 | return false; | ||
125 | } | ||
126 | } | ||
122 | int numClauses = clauses.size(); | 127 | int numClauses = clauses.size(); |
123 | if (numClauses != other.clauses.size()) { | 128 | if (numClauses != other.clauses.size()) { |
124 | return false; | 129 | return false; |
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java index bb60ccc9..1eeb5723 100644 --- a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java +++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java | |||
@@ -6,6 +6,9 @@ | |||
6 | package tools.refinery.store.query.equality; | 6 | package tools.refinery.store.query.equality; |
7 | 7 | ||
8 | import tools.refinery.store.query.dnf.Dnf; | 8 | import tools.refinery.store.query.dnf.Dnf; |
9 | import tools.refinery.store.query.dnf.DnfClause; | ||
10 | import tools.refinery.store.query.dnf.SymbolicParameter; | ||
11 | import tools.refinery.store.query.literal.Literal; | ||
9 | import tools.refinery.store.util.CycleDetectingMapper; | 12 | import tools.refinery.store.util.CycleDetectingMapper; |
10 | 13 | ||
11 | import java.util.List; | 14 | import java.util.List; |
@@ -19,6 +22,45 @@ public class DeepDnfEqualityChecker implements DnfEqualityChecker { | |||
19 | return mapper.map(new Pair(left, right)); | 22 | return mapper.map(new Pair(left, right)); |
20 | } | 23 | } |
21 | 24 | ||
25 | public boolean dnfEqualRaw(List<SymbolicParameter> symbolicParameters, | ||
26 | List<? extends List<? extends Literal>> clauses, Dnf other) { | ||
27 | int arity = symbolicParameters.size(); | ||
28 | if (arity != other.arity()) { | ||
29 | return false; | ||
30 | } | ||
31 | for (int i = 0; i < arity; i++) { | ||
32 | if (!symbolicParameters.get(i).getDirection().equals(other.getSymbolicParameters().get(i).getDirection())) { | ||
33 | return false; | ||
34 | } | ||
35 | } | ||
36 | int numClauses = clauses.size(); | ||
37 | if (numClauses != other.getClauses().size()) { | ||
38 | return false; | ||
39 | } | ||
40 | for (int i = 0; i < numClauses; i++) { | ||
41 | var literalEqualityHelper = new LiteralEqualityHelper(this, symbolicParameters, | ||
42 | other.getSymbolicParameters()); | ||
43 | if (!equalsWithSubstitutionRaw(literalEqualityHelper, clauses.get(i), other.getClauses().get(i))) { | ||
44 | return false; | ||
45 | } | ||
46 | } | ||
47 | return true; | ||
48 | } | ||
49 | |||
50 | private boolean equalsWithSubstitutionRaw(LiteralEqualityHelper helper, List<? extends Literal> literals, | ||
51 | DnfClause other) { | ||
52 | int size = literals.size(); | ||
53 | if (size != other.literals().size()) { | ||
54 | return false; | ||
55 | } | ||
56 | for (int i = 0; i < size; i++) { | ||
57 | if (!literals.get(i).equalsWithSubstitution(helper, other.literals().get(i))) { | ||
58 | return false; | ||
59 | } | ||
60 | } | ||
61 | return true; | ||
62 | } | ||
63 | |||
22 | protected boolean doCheckEqual(Pair pair) { | 64 | protected boolean doCheckEqual(Pair pair) { |
23 | return pair.left.equalsWithSubstitution(this, pair.right); | 65 | return pair.left.equalsWithSubstitution(this, pair.right); |
24 | } | 66 | } |