From 2599ceeccbcfb531b3a95427b1b8904caf102242 Mon Sep 17 00:00:00 2001
From: Kristóf Marussy <kristof@marussy.com>
Date: Thu, 15 Jun 2023 20:41:09 +0200
Subject: 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.
---
 .../java/tools/refinery/store/query/dnf/Dnf.java   |  5 +++
 .../query/equality/DeepDnfEqualityChecker.java     | 42 ++++++++++++++++++++++
 2 files changed, 47 insertions(+)

(limited to 'subprojects/store-query/src/main/java')

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 {
 		if (arity() != other.arity()) {
 			return false;
 		}
+		for (int i = 0; i < arity(); i++) {
+			if (!symbolicParameters.get(i).getDirection().equals(other.getSymbolicParameters().get(i).getDirection())) {
+				return false;
+			}
+		}
 		int numClauses = clauses.size();
 		if (numClauses != other.clauses.size()) {
 			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 @@
 package tools.refinery.store.query.equality;
 
 import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.dnf.DnfClause;
+import tools.refinery.store.query.dnf.SymbolicParameter;
+import tools.refinery.store.query.literal.Literal;
 import tools.refinery.store.util.CycleDetectingMapper;
 
 import java.util.List;
@@ -19,6 +22,45 @@ public class DeepDnfEqualityChecker implements DnfEqualityChecker {
 		return mapper.map(new Pair(left, right));
 	}
 
+	public boolean dnfEqualRaw(List<SymbolicParameter> symbolicParameters,
+							   List<? extends List<? extends Literal>> clauses, Dnf other) {
+		int arity = symbolicParameters.size();
+		if (arity != other.arity()) {
+			return false;
+		}
+		for (int i = 0; i < arity; i++) {
+			if (!symbolicParameters.get(i).getDirection().equals(other.getSymbolicParameters().get(i).getDirection())) {
+				return false;
+			}
+		}
+		int numClauses = clauses.size();
+		if (numClauses != other.getClauses().size()) {
+			return false;
+		}
+		for (int i = 0; i < numClauses; i++) {
+			var literalEqualityHelper = new LiteralEqualityHelper(this, symbolicParameters,
+					other.getSymbolicParameters());
+			if (!equalsWithSubstitutionRaw(literalEqualityHelper, clauses.get(i), other.getClauses().get(i))) {
+				return false;
+			}
+		}
+		return true;
+	}
+
+	private boolean equalsWithSubstitutionRaw(LiteralEqualityHelper helper, List<? extends Literal> literals,
+											  DnfClause other) {
+		int size = literals.size();
+		if (size != other.literals().size()) {
+			return false;
+		}
+		for (int i = 0; i < size; i++) {
+			if (!literals.get(i).equalsWithSubstitution(helper, other.literals().get(i))) {
+				return false;
+			}
+		}
+		return true;
+	}
+
 	protected boolean doCheckEqual(Pair pair) {
 		return pair.left.equalsWithSubstitution(this, pair.right);
 	}
-- 
cgit v1.2.3-54-g00ecf