/egg.dl

Primary LanguageShell

Rebuild souffle with the following change: in src/include/souffle/datastructure/EquivalenceRelation.h, add a method:

    /**
     * Returns unionfind parent of Node
     * @param x
     */
    value_type findNode(value_type x) const {
        if (!sds.nodeExists(x)) return x;
        return sds.findNode(x);
    }

to the EquivalenceRelation class.

Change SOUFFLE_PATH in compile.dl to point to the directory containing the souffle and souffle-compile binaries.

Compile with ./compile.dl program.dl, then run with ./out.

There are two versions implementing eqsat for math: correct.dl and fast.dl. As the name suggests, correct.dl is correct but slow. fast.dl is incorrect because it misses some tuples, but is very fast. The difference between them is that correct.dl properly canonizes e-nodes, whereas fast.dl only drops e-nodes subsumed by more canonical ones.