Problem 674: Solving $\mathcal{I}$-equations
View on Project EulerProject Euler Problem 674 Solution
EulerSolve provides an optimized solution for Project Euler Problem 674, Solving $\mathcal{I}$-equations, with C++, Python, Java, and a step-by-step mathematical explanation.
Problem Summary We are given a list of symbolic expressions built from variables and a binary constructor. For each unordered pair of positions containing different expressions, we ask whether a substitution can make the two expression trees identical. If no such substitution exists, that pair contributes \(0\). If a substitution does exist, the resulting common tree is evaluated numerically, and the overall total is taken modulo $$M=10^9.$$ A brute-force search over all substitutions is hopeless, so the solution works directly with tree structure, recursive unification, and a cache of repeated pair computations. Mathematical Approach The key observation is that each pair of expressions can be handled in two stages: first solve the symbolic equation by unification, then evaluate the unified term by a fixed arithmetic rule. Step 1: Model the expressions as rooted binary trees In abstract form, the expressions follow the grammar $$E ::= v \mid I(E,E),$$ where \(v\) denotes a variable. Thus every expression is either a leaf carrying a variable name or an internal node with exactly two children. Structural equality means same tree shape and same variable labels in the corresponding positions. This viewpoint turns the problem into a question about tree equations rather than about string manipulation....
Detailed mathematical approach
Problem Summary
We are given a list of symbolic expressions built from variables and a binary constructor. For each unordered pair of positions containing different expressions, we ask whether a substitution can make the two expression trees identical. If no such substitution exists, that pair contributes \(0\). If a substitution does exist, the resulting common tree is evaluated numerically, and the overall total is taken modulo
$$M=10^9.$$
A brute-force search over all substitutions is hopeless, so the solution works directly with tree structure, recursive unification, and a cache of repeated pair computations.
Mathematical Approach
The key observation is that each pair of expressions can be handled in two stages: first solve the symbolic equation by unification, then evaluate the unified term by a fixed arithmetic rule.
Step 1: Model the expressions as rooted binary trees
In abstract form, the expressions follow the grammar
$$E ::= v \mid I(E,E),$$
where \(v\) denotes a variable. Thus every expression is either a leaf carrying a variable name or an internal node with exactly two children. Structural equality means same tree shape and same variable labels in the corresponding positions.
This viewpoint turns the problem into a question about tree equations rather than about string manipulation.
Step 2: Solve one pair by recursive unification
For two expressions \(E_1\) and \(E_2\), we seek a substitution \(\sigma\) such that
$$\sigma(E_1)=\sigma(E_2).$$
A substitution maps variables to expressions and extends recursively:
$$\sigma\bigl(I(A,B)\bigr)=I\bigl(\sigma(A),\sigma(B)\bigr).$$
The recursive cases are straightforward. If both current nodes are binary constructor nodes, then their left children must unify and their right children must unify. If one side is a variable, we may bind that variable to the other side, provided the binding is legal. If neither rule applies, the pair cannot be unified.
Before each comparison, already known bindings are followed until the current node is fully resolved. This is why chains such as \(a \mapsto b\) and \(b \mapsto I(c,d)\) behave exactly as the direct binding \(a \mapsto I(c,d)\).
Step 3: Prevent cyclic substitutions with the occurs-check
The only dangerous kind of binding is a self-referential one. If a variable \(v\) is to be replaced by a term \(T\), we must require
$$v\notin \operatorname{Vars}(T).$$
This is the classical occurs-check. Without it, an equation such as
$$v=I(v,w)$$
would force an infinite cyclic object instead of an ordinary finite term. The implementations explicitly reject such cases, so any successful unification always produces an acyclic expression tree.
Step 4: Evaluate the unified tree modulo \(10^9\)
Once unification succeeds, the common term is interpreted numerically. Unbound variables contribute \(0\). For the binary constructor, the recursive valuation rule is
$$J(x,y)=\bigl(1+x+y\bigr)^2+(y-x)\pmod{M}.$$
Equivalently, if \(V_\sigma(E)\) denotes the value of expression \(E\) under the successful substitution \(\sigma\), then
$$V_\sigma(v)=0\quad\text{for an unresolved variable},$$
$$V_\sigma\bigl(I(A,B)\bigr)=J\bigl(V_\sigma(A),V_\sigma(B)\bigr).$$
Therefore the pair contribution is
$$P(E_1,E_2)= \begin{cases} V_\sigma(E_1), & \text{if }E_1\text{ and }E_2\text{ unify},\\ 0, & \text{otherwise}. \end{cases}$$
Because the two expressions become identical after applying \(\sigma\), evaluating either side gives the same value.
Step 5: Compress duplicates and reconstruct the final sum
The full input may contain many repeated expressions. After converting every parsed tree to one canonical textual form, equal expressions can be merged into unique representatives \(U_0,U_1,\dots,U_{U-1}\).
For those representatives, define the symmetric pair table
$$C_{i,j}=P(U_i,U_j),\qquad C_{i,j}=C_{j,i}.$$
If the original list has \(N\) positions and the expression at position \(p\) corresponds to representative index \(a_p\), then the required total is
$$S=\sum_{\substack{1\le p\lt q\le N \\ a_p\ne a_q}} C_{a_p,a_q}\pmod{M}.$$
The condition \(a_p\ne a_q\) matters: even if the same structural expression appears at different positions, that positional pair is excluded by the problem statement.
Worked Example
Take
$$E_1=I(a,b),\qquad E_2=I(c,I(c,d)).$$
The roots have the same binary shape, so we unify their children. From the left children we get
$$a\mapsto c.$$
From the right children we get
$$b\mapsto I(c,d).$$
This second binding is legal because \(b\) does not occur inside \(I(c,d)\). Hence the pair unifies, and the common resolved tree is
$$I(c,I(c,d)).$$
Now evaluate it. Since \(c\) and \(d\) remain unbound, both contribute \(0\). The inner node gives
$$J(0,0)=(1+0+0)^2+(0-0)=1.$$
The outer node then gives
$$J(0,1)=(1+0+1)^2+(1-0)=4+1=5.$$
So this pair contributes \(5\) modulo \(10^9\). By contrast, the pair \(a\) and \(I(a,b)\) fails immediately, because binding \(a\) to a term that already contains \(a\) violates the occurs-check.
How the Code Works
The C++, Python, and Java implementations first parse the entire input into expression trees while preserving the original order and all duplicates. They then serialize each tree into a canonical form so that structurally identical expressions receive the same unique index.
Next, the implementation computes the pair value for every unique-expression pair. Each pair is processed by recursive unification with an occurs-check; if unification succeeds, the resolved tree is evaluated recursively modulo \(10^9\). During evaluation, already resolved subtrees are memoized inside the current pair computation so that repeated branches are not recomputed. The C++ implementation additionally distributes the unique-pair precomputation across several worker tasks, while the Python and Java implementations perform the same logic in direct nested loops.
Finally, the implementations scan all original input positions \((p,q)\) with \(p<q\), skip the pairs whose two positions refer to the same canonical expression, and add the cached value \(C_{a_p,a_q}\) for the remaining pairs.
Complexity Analysis
Let \(N\) be the total number of input expressions, \(U\) the number of distinct structural expressions after deduplication, and \(L\) the total size of all parsed trees. Parsing plus canonicalization is linear in the input size, so it costs \(O(L)\) time.
The dominant symbolic phase is the unique-pair table. Its cost is
$$O\bigl(U^2\cdot T_{\text{pair}}\bigr),$$
where \(T_{\text{pair}}\) is the cost of one unification and, when successful, one recursive evaluation. On ordinary acyclic inputs this is close to linear in the number of visited nodes, although the occurs-check can revisit large subtrees in harder cases. The final positional summation costs \(O(N^2)\) time. Memory usage is \(O(L+U^2)\) for the stored trees and the pair cache. Parallelism in the C++ implementation improves wall-clock time but not the asymptotic bound.
Footnotes and References
- Problem page: https://projecteuler.net/problem=674
- Unification in computer science: Wikipedia - Unification (computer science)
- Occurs check: Wikipedia - Occurs check
- Substitution in logic: Wikipedia - Substitution (logic)
- Abstract syntax tree: Wikipedia - Abstract syntax tree
Problem 674 source code
C++
#include <algorithm>
#include <atomic>
#include <cstdint>
#include <fstream>
#include <future>
#include <iomanip>
#include <iostream>
#include <map>
#include <memory>
#include <mutex>
#include <set>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <vector>
// --- Configuration ---
const long long MOD = 1000000000;
const std::string FILENAME = "solutionsCpp/I-expressions.txt";
// --- Data Structures ---
enum NodeType { VARIABLE, I_OP };
struct Node {
NodeType type;
virtual ~Node() = default;
};
using NodePtr = std::shared_ptr<Node>;
struct VarNode : Node {
std::string name;
VarNode(std::string n) : name(n) { type = VARIABLE; }
};
struct INode : Node {
NodePtr left;
NodePtr right;
INode(NodePtr l, NodePtr r) : left(l), right(r) { type = I_OP; }
};
// --- Serialization Helper ---
std::string serialize(NodePtr n) {
if (n->type == VARIABLE) {
return std::static_pointer_cast<VarNode>(n)->name;
}
auto i = std::static_pointer_cast<INode>(n);
return "I(" + serialize(i->left) + "," + serialize(i->right) + ")";
}
// --- Robust Parser ---
class Parser {
std::string input;
size_t pos;
void skipWhitespace() {
while (pos < input.size() && isspace(input[pos]))
pos++;
}
bool consume(char c) {
skipWhitespace();
if (pos < input.size() && input[pos] == c) {
pos++;
return true;
}
return false;
}
bool matchString(const std::string &s) {
skipWhitespace();
if (input.compare(pos, s.size(), s) == 0) {
pos += s.size();
return true;
}
return false;
}
NodePtr parseTerm() {
if (matchString("I(") || matchString("J(")) {
auto left = parseTerm();
if (!consume(','))
throw std::runtime_error("Expected ','");
auto right = parseTerm();
if (!consume(')'))
throw std::runtime_error("Expected ')'");
return std::make_shared<INode>(left, right);
} else {
skipWhitespace();
std::string name;
while (pos < input.size() && (isalnum(input[pos]) || input[pos] == '_')) {
name += input[pos++];
}
if (name.empty())
throw std::runtime_error("Unexpected char");
return std::make_shared<VarNode>(name);
}
}
public:
Parser(const std::string &content) : input(content), pos(0) {}
NodePtr parseNext() { return parseTerm(); }
bool hasMore() {
skipWhitespace();
return pos < input.size();
}
};
// --- Unification Engine ---
using Bindings = std::map<std::string, NodePtr>;
struct NodePtrHash {
size_t operator()(const NodePtr &p) const noexcept {
std::uintptr_t x = reinterpret_cast<std::uintptr_t>(p.get());
x ^= (x >> 33);
x *= 0xff51afd7ed558ccdULL;
x ^= (x >> 33);
x *= 0xc4ceb9fe1a85ec53ULL;
x ^= (x >> 33);
return static_cast<size_t>(x);
}
};
NodePtr resolve(NodePtr node, const Bindings &bindings) {
if (node->type == VARIABLE) {
auto v = std::static_pointer_cast<VarNode>(node);
auto it = bindings.find(v->name);
if (it != bindings.end()) {
return resolve(it->second, bindings);
}
}
return node;
}
// Occurs check with visited set optimization
bool occurs(const std::string &varName, NodePtr term, const Bindings &bindings,
std::unordered_set<NodePtr, NodePtrHash> &visited) {
NodePtr r = resolve(term, bindings);
if (visited.count(r))
return false;
visited.insert(r);
if (r->type == VARIABLE) {
return std::static_pointer_cast<VarNode>(r)->name == varName;
} else {
auto iNode = std::static_pointer_cast<INode>(r);
return occurs(varName, iNode->left, bindings, visited) ||
occurs(varName, iNode->right, bindings, visited);
}
}
bool unify(NodePtr t1, NodePtr t2, Bindings &bindings) {
NodePtr r1 = resolve(t1, bindings);
NodePtr r2 = resolve(t2, bindings);
if (r1 == r2)
return true;
if (r1->type == VARIABLE) {
auto v1 = std::static_pointer_cast<VarNode>(r1);
if (r2->type == VARIABLE &&
std::static_pointer_cast<VarNode>(r2)->name == v1->name)
return true;
std::unordered_set<NodePtr, NodePtrHash> visited;
if (occurs(v1->name, r2, bindings, visited))
return false;
bindings[v1->name] = r2;
return true;
}
if (r2->type == VARIABLE) {
auto v2 = std::static_pointer_cast<VarNode>(r2);
std::unordered_set<NodePtr, NodePtrHash> visited;
if (occurs(v2->name, r1, bindings, visited))
return false;
bindings[v2->name] = r1;
return true;
}
if (r1->type == I_OP && r2->type == I_OP) {
auto i1 = std::static_pointer_cast<INode>(r1);
auto i2 = std::static_pointer_cast<INode>(r2);
return unify(i1->left, i2->left, bindings) &&
unify(i1->right, i2->right, bindings);
}
return false;
}
// --- Evaluation ---
long long evalJ(long long x, long long y) {
long long sum = (1 + x + y) % MOD;
long long term1 = (sum * sum) % MOD;
long long diff = (y - x) % MOD;
long long res = (term1 + diff) % MOD;
if (res < 0)
res += MOD;
return res;
}
using EvalCache = std::map<NodePtr, long long>;
long long evaluate(NodePtr node, const Bindings &bindings, EvalCache &cache) {
NodePtr r = resolve(node, bindings);
auto it = cache.find(r);
if (it != cache.end())
return it->second;
long long result;
if (r->type == VARIABLE) {
result = 0;
} else {
auto iNode = std::static_pointer_cast<INode>(r);
long long lv = evaluate(iNode->left, bindings, cache);
long long rv = evaluate(iNode->right, bindings, cache);
result = evalJ(lv, rv);
}
cache[r] = result;
return result;
}
long long solvePair(NodePtr e1, NodePtr e2) {
Bindings bindings;
if (unify(e1, e2, bindings)) {
EvalCache cache;
return evaluate(e1, bindings, cache);
}
return 0;
}
// --- Main ---
int main() {
try {
std::cout << "--- Project Euler 674 Solver (Final Corrected) ---\n";
std::ifstream file(FILENAME, std::ios::binary | std::ios::ate);
if (!file.is_open())
return 1;
std::streamsize size = file.tellg();
file.seekg(0, std::ios::beg);
std::string content((std::istreambuf_iterator<char>(file)),
std::istreambuf_iterator<char>());
std::cout << "Parsing file (" << size << " bytes)..." << std::endl;
Parser fileParser(content);
// 1. Parse ALL expressions, preserving order and duplicates
std::vector<NodePtr> fileExprs;
while (fileParser.hasMore()) {
fileExprs.push_back(fileParser.parseNext());
}
size_t totalExprs = fileExprs.size();
std::cout << "Parsed " << totalExprs << " total expressions from file."
<< std::endl;
// 2. Map to unique IDs to handle duplicates efficiently
std::map<std::string, int> strToId;
std::vector<NodePtr> uniqueExprs;
std::vector<int> fileIds; // The file as a list of IDs
for (auto &e : fileExprs) {
std::string s = serialize(e);
if (strToId.find(s) == strToId.end()) {
strToId[s] = uniqueExprs.size();
uniqueExprs.push_back(e);
}
fileIds.push_back(strToId[s]);
}
std::cout << "Found " << uniqueExprs.size() << " unique expressions."
<< std::endl;
// 3. Pre-compute LSV for all unique pairs (i, j) where i <= j
// We use a linear map index for pairs
int nUnique = uniqueExprs.size();
std::cout << "Pre-computing LSVs for unique pairs..." << std::endl;
// Use a flat vector for the cache: cache[i * n + j]
std::vector<long long> pairCache(nUnique * nUnique, -1);
// Parallelize pre-computation
unsigned int numThreads = std::thread::hardware_concurrency();
if (numThreads == 0)
numThreads = 4;
std::atomic<int> progress(0);
std::vector<std::future<void>> futures;
size_t chunkSize = (nUnique + numThreads - 1) / numThreads;
for (unsigned int t = 0; t < numThreads; ++t) {
size_t start = t * chunkSize;
size_t end = std::min(start + chunkSize, (size_t)nUnique);
if (start >= end)
break;
futures.push_back(std::async(std::launch::async, [&, start, end]() {
for (size_t i = start; i < end; ++i) {
for (size_t j = i; j < nUnique; ++j) { // Compute for j >= i
// If i == j, result implies unification of identical trees -> eval
// at 0.
long long val = solvePair(uniqueExprs[i], uniqueExprs[j]);
pairCache[i * nUnique + j] = val;
pairCache[j * nUnique + i] = val; // Symmetric
}
if (i % 5 == 0)
progress.fetch_add(5);
}
}));
}
for (auto &f : futures)
f.get();
std::cout << "\nPre-computation done." << std::endl;
// 4. Sum over file positions
std::cout << "Summing over file pairs..." << std::endl;
long long totalSum = 0;
// Loop over file positions (i, j)
for (size_t i = 0; i < totalExprs; ++i) {
for (size_t j = i + 1; j < totalExprs; ++j) {
int id1 = fileIds[i];
int id2 = fileIds[j];
// "pairs made of distinct expressions" -> Skip if same unique
// expression
if (id1 == id2)
continue;
totalSum = (totalSum + pairCache[id1 * nUnique + id2]) % MOD;
}
}
std::cout << "\nFinal Result (Last 9 digits): " << std::setfill('0')
<< std::setw(9) << totalSum << std::endl;
} catch (const std::exception &e) {
std::cerr << "\nException: " << e.what() << std::endl;
return 1;
}
return 0;
}
Python
import sys
import os
sys.setrecursionlimit(20000)
MOD = 1000000000
class VarNode:
def __init__(self, name):
self.type = 'VAR'
self.name = name
class INode:
def __init__(self, left, right):
self.type = 'I'
self.left = left
self.right = right
def serialize(n):
if n.type == 'VAR':
return n.name
return 'I(' + serialize(n.left) + ',' + serialize(n.right) + ')'
class Parser:
def __init__(self, input_str):
self.s = input_str
self.pos = 0
self.n = len(self.s)
def skip(self):
while self.pos < self.n and self.s[self.pos].isspace():
self.pos += 1
def consume(self, c):
self.skip()
if self.pos < self.n and self.s[self.pos] == c:
self.pos += 1
return True
return False
def matchString(self, string):
self.skip()
if self.s.startswith(string, self.pos):
self.pos += len(string)
return True
return False
def parse_term(self):
if self.matchString('I(') or self.matchString('J('):
left = self.parse_term()
self.consume(',')
right = self.parse_term()
self.consume(')')
return INode(left, right)
else:
self.skip()
start = self.pos
while self.pos < self.n and (self.s[self.pos].isalnum() or self.s[self.pos] == '_'):
self.pos += 1
name = self.s[start:self.pos]
return VarNode(name)
def has_more(self):
self.skip()
return self.pos < self.n
def resolve(node, bindings):
if node.type == 'VAR' and node.name in bindings:
return resolve(bindings[node.name], bindings)
return node
def occurs(var_name, term, bindings, visited):
r = resolve(term, bindings)
if id(r) in visited:
return False
visited.add(id(r))
if r.type == 'VAR':
return r.name == var_name
return occurs(var_name, r.left, bindings, visited) or occurs(var_name, r.right, bindings, visited)
def unify(t1, t2, bindings):
r1 = resolve(t1, bindings)
r2 = resolve(t2, bindings)
if r1 is r2: return True
if r1.type == 'VAR':
if r2.type == 'VAR' and r2.name == r1.name: return True
visited = set()
if occurs(r1.name, r2, bindings, visited): return False
bindings[r1.name] = r2
return True
if r2.type == 'VAR':
visited = set()
if occurs(r2.name, r1, bindings, visited): return False
bindings[r2.name] = r1
return True
if r1.type == 'I' and r2.type == 'I':
return unify(r1.left, r2.left, bindings) and unify(r1.right, r2.right, bindings)
return False
def evalJ(x, y):
s = (1 + x + y) % MOD
term1 = (s * s) % MOD
diff = (y - x) % MOD
res = (term1 + diff) % MOD
return res
def evaluate(node, bindings, cache):
r = resolve(node, bindings)
if id(r) in cache:
return cache[id(r)]
if r.type == 'VAR':
res = 0
else:
lv = evaluate(r.left, bindings, cache)
rv = evaluate(r.right, bindings, cache)
res = evalJ(lv, rv)
cache[id(r)] = res
return res
def solve_pair(e1, e2):
bindings = {}
if unify(e1, e2, bindings):
return evaluate(e1, bindings, {})
return 0
def solve():
content = ""
paths = ['I-expressions.txt', 'solutionsCpp/I-expressions.txt', '../I-expressions.txt']
for path in paths:
if os.path.exists(path):
with open(path, 'r') as f:
content = f.read()
break
if not content:
return "File not found"
parser = Parser(content)
file_exprs = []
while parser.has_more():
file_exprs.append(parser.parse_term())
str_to_id = {}
unique_exprs = []
file_ids = []
for e in file_exprs:
s = serialize(e)
if s not in str_to_id:
str_to_id[s] = len(unique_exprs)
unique_exprs.append(e)
file_ids.append(str_to_id[s])
n_unique = len(unique_exprs)
pair_cache = {}
for i in range(n_unique):
for j in range(i, n_unique):
val = solve_pair(unique_exprs[i], unique_exprs[j])
pair_cache[(i, j)] = val
pair_cache[(j, i)] = val
total_sum = 0
total_exprs = len(file_exprs)
for i in range(total_exprs):
for j in range(i + 1, total_exprs):
id1 = file_ids[i]
id2 = file_ids[j]
if id1 == id2:
continue
total_sum = (total_sum + pair_cache[(id1, id2)]) % MOD
return str(total_sum)
if __name__ == '__main__':
print(solve())
Java
import java.io.IOException;
import java.nio.file.Files;
import java.nio.file.Paths;
import java.util.*;
public class Euler674 {
static final long MOD = 1000000000L;
enum NodeType {
VARIABLE, I_OP
}
static abstract class Node {
NodeType type;
}
static class VarNode extends Node {
String name;
VarNode(String name) {
this.type = NodeType.VARIABLE;
this.name = name;
}
}
static class INode extends Node {
Node left, right;
INode(Node left, Node right) {
this.type = NodeType.I_OP;
this.left = left;
this.right = right;
}
}
static String serialize(Node n) {
if (n.type == NodeType.VARIABLE) {
return ((VarNode) n).name;
}
INode i = (INode) n;
return "I(" + serialize(i.left) + "," + serialize(i.right) + ")";
}
static class Parser {
String s;
int pos;
Parser(String s) {
this.s = s;
this.pos = 0;
}
void skip() {
while (pos < s.length() && Character.isWhitespace(s.charAt(pos))) {
pos++;
}
}
boolean consume(char c) {
skip();
if (pos < s.length() && s.charAt(pos) == c) {
pos++;
return true;
}
return false;
}
boolean matchString(String str) {
skip();
if (s.startsWith(str, pos)) {
pos += str.length();
return true;
}
return false;
}
Node parseTerm() {
if (matchString("I(") || matchString("J(")) {
Node left = parseTerm();
consume(',');
Node right = parseTerm();
consume(')');
return new INode(left, right);
} else {
skip();
int start = pos;
while (pos < s.length() && (Character.isLetterOrDigit(s.charAt(pos)) || s.charAt(pos) == '_')) {
pos++;
}
return new VarNode(s.substring(start, pos));
}
}
boolean hasMore() {
skip();
return pos < s.length();
}
}
static Node resolve(Node node, Map<String, Node> bindings) {
if (node.type == NodeType.VARIABLE) {
VarNode v = (VarNode) node;
if (bindings.containsKey(v.name)) {
return resolve(bindings.get(v.name), bindings);
}
}
return node;
}
static boolean occurs(String varName, Node term, Map<String, Node> bindings, Set<Node> visited) {
Node r = resolve(term, bindings);
if (!visited.add(r))
return false;
if (r.type == NodeType.VARIABLE) {
return ((VarNode) r).name.equals(varName);
} else {
INode i = (INode) r;
return occurs(varName, i.left, bindings, visited) || occurs(varName, i.right, bindings, visited);
}
}
static boolean unify(Node t1, Node t2, Map<String, Node> bindings) {
Node r1 = resolve(t1, bindings);
Node r2 = resolve(t2, bindings);
if (r1 == r2)
return true;
if (r1.type == NodeType.VARIABLE) {
VarNode v1 = (VarNode) r1;
if (r2.type == NodeType.VARIABLE && ((VarNode) r2).name.equals(v1.name))
return true;
Set<Node> visited = new HashSet<>();
if (occurs(v1.name, r2, bindings, visited))
return false;
bindings.put(v1.name, r2);
return true;
}
if (r2.type == NodeType.VARIABLE) {
VarNode v2 = (VarNode) r2;
Set<Node> visited = new HashSet<>();
if (occurs(v2.name, r1, bindings, visited))
return false;
bindings.put(v2.name, r1);
return true;
}
if (r1.type == NodeType.I_OP && r2.type == NodeType.I_OP) {
INode i1 = (INode) r1;
INode i2 = (INode) r2;
return unify(i1.left, i2.left, bindings) && unify(i1.right, i2.right, bindings);
}
return false;
}
static long evalJ(long x, long y) {
long sum = (1 + x + y) % MOD;
long term1 = (sum * sum) % MOD;
long diff = (y - x) % MOD;
long res = (term1 + diff) % MOD;
if (res < 0)
res += MOD;
return res;
}
static long evaluate(Node node, Map<String, Node> bindings, Map<Node, Long> cache) {
Node r = resolve(node, bindings);
if (cache.containsKey(r))
return cache.get(r);
long res;
if (r.type == NodeType.VARIABLE) {
res = 0;
} else {
INode i = (INode) r;
long lv = evaluate(i.left, bindings, cache);
long rv = evaluate(i.right, bindings, cache);
res = evalJ(lv, rv);
}
cache.put(r, res);
return res;
}
static long solvePair(Node e1, Node e2) {
Map<String, Node> bindings = new HashMap<>();
if (unify(e1, e2, bindings)) {
return evaluate(e1, bindings, new IdentityHashMap<>());
}
return 0;
}
public static String solve() {
String content = "";
String[] paths = { "I-expressions.txt", "solutionsCpp/I-expressions.txt", "../I-expressions.txt" };
for (String path : paths) {
try {
content = new String(Files.readAllBytes(Paths.get(path)));
break;
} catch (IOException ignored) {
}
}
if (content.isEmpty())
return "File not found";
Parser parser = new Parser(content);
List<Node> fileExprs = new ArrayList<>();
while (parser.hasMore()) {
fileExprs.add(parser.parseTerm());
}
Map<String, Integer> strToId = new HashMap<>();
List<Node> uniqueExprs = new ArrayList<>();
List<Integer> fileIds = new ArrayList<>();
for (Node e : fileExprs) {
String s = serialize(e);
if (!strToId.containsKey(s)) {
strToId.put(s, uniqueExprs.size());
uniqueExprs.add(e);
}
fileIds.add(strToId.get(s));
}
int nUnique = uniqueExprs.size();
long[] pairCache = new long[nUnique * nUnique];
for (int i = 0; i < nUnique; ++i) {
for (int j = i; j < nUnique; ++j) {
long val = solvePair(uniqueExprs.get(i), uniqueExprs.get(j));
pairCache[i * nUnique + j] = val;
pairCache[j * nUnique + i] = val;
}
}
long totalSum = 0;
int totalExprs = fileExprs.size();
for (int i = 0; i < totalExprs; ++i) {
for (int j = i + 1; j < totalExprs; ++j) {
int id1 = fileIds.get(i);
int id2 = fileIds.get(j);
if (id1 == id2)
continue;
totalSum = (totalSum + pairCache[id1 * nUnique + id2]) % MOD;
}
}
return Long.toString(totalSum);
}
public static void main(String[] args) {
System.out.println(solve());
}
}