Skip to content

LeastFreeVarsSips counts bound variables instead of unbound variables #2586

@jjjxia

Description

@jjjxia

LeastFreeVarsSips is documented as selecting the atom with the fewest unbound variables. However, its current implementation adds a variable to freeVars when the variable is already bound:

std::set<std::string> freeVars;
visit(*atom, [&](const Variable& var) {
    if (bindingStore.isBound(var.getName())) {
        freeVars.insert(var.getName());
    }
});
cost.push_back((double)freeVars.size());

Should the condition be negated?

- if (bindingStore.isBound(var.getName())) {
+ if (!bindingStore.isBound(var.getName())) {

Minimal reproducer

.decl Seed(x:number)
.decl Low(z:number, w:number)
.decl High(x:number, y:number)
.decl Result(y:number, z:number, w:number)

Seed(1).
Low(2, 3).
High(1, 4).

Result(y, z, w) :- Seed(x), Low(z, w), High(x, y).

.output Result

Run:

build/src/souffle \
  -P RamSIPS:least-free-vars \
  --show=transformed-ram \
  repro.dl

The generated RAM evaluates Low before High:

FOR t0 IN Seed
 FOR t1 IN Low
  FOR t2 IN High ON INDEX t2.0 = t0.0

After Seed(x) has been evaluated:

Atom Unbound variables
Low(z, w) z, w
High(x, y) y

Based on the documented behavior, High(x, y) should be selected first because it has fewer unbound variables.

Expected ordering:

FOR t0 IN Seed
 FOR t1 IN High ON INDEX t1.0 = t0.0
  FOR t2 IN Low

For comparison, the expected ordering is currently produced by:

build/src/souffle \
  -P RamSIPS:least-free \
  --show=transformed-ram \
  repro.dl

Scope

This does not affect the default configuration, which uses RamSIPS:all-bound. It is triggered when RamSIPS:least-free-vars is selected explicitly.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions