solvers gen - uhop/yopl GitHub Wiki

solvers-gen

Synchronous, pull-based solver. Same proof engine as solve, but exposed as a generator function so the caller drives enumeration instead of being called back.

Why a generator driver?

A callback-style solver hands you every solution it finds, whether you want them or not. A generator-style solver lets the caller decide when (and whether) to ask for the next one. That changes what is easy:

  • Lazy enumeration. The proof loop suspends after each yield env and only resumes on the next it.next() (or the next iteration of for...of). If you only need the first solution, the solver only does the work for the first solution.
  • Clean early termination. break out of a for...of loop and the generator's return() cleans up — no exceptions, no flag variables. With solve the only way to stop early is to throw.
  • Composition. You can wrap, filter, map, take, or zip solution streams with any generator utility.
  • Inversion of control. Your code stays on the outside of the loop. This is often easier to integrate into existing iteration code than a callback that fires N times in the middle of a function.

The trade-off is that the proof loop is now a JavaScript generator, which has some overhead per yield, and goal predicates are still called synchronously — if you need await inside a predicate or between solutions, use solvers-asyncGen instead.

When to choose solvers-gen

  • You want only the first N solutions, or you want to stop as soon as some condition is met.
  • You want to interleave solutions with other synchronous work without nesting it inside a callback.
  • You want to pipe solutions through generator utilities.
  • Your goal predicates are pure synchronous JS (no await).

Import

import gen from 'yopl/solvers/gen.js';

Signature

gen(rules, name, args): Generator<Env>

rules, name, and args mean exactly what they do in solve. The returned generator yields the live unification environment once per solution. Read what you need from each env before resuming the generator — the next next() call will backtrack and rewrite it.

Example — first solution only

import {variable} from 'deep6/env.js';
import assemble from 'deep6/traverse/assemble.js';
import gen from 'yopl/solvers/gen.js';

const rules = {
  member: [(V, X) => [{args: [{value: V, next: X}, V]}], (V, X) => [{args: [{next: X}, V]}, {name: 'member', args: [X, V]}]]
};

const list = {value: 1, next: {value: 2, next: {value: 3, next: null}}};
const X = variable('X');

const it = gen(rules, 'member', [list, X]);
const {value: env} = it.next();
console.log(assemble(X, env)); // 1
// no further work is done — the generator is discarded

Example — bounded enumeration

let count = 0;
for (const env of gen(rules, 'member', [list, X])) {
  console.log(assemble(X, env));
  if (++count === 2) break; // stops the proof loop cleanly
}
// 1
// 2
⚠️ **GitHub.com Fallback** ⚠️