The default, synchronous, callback-style solver — and the main public entry point of yopl. This is the page to read first if you want to understand what all the solvers do; the other three pages describe how their driver wrapper differs from this one.

A solver is the engine that takes a rule database, a goal to prove, and an environment of logic variables, and runs SLD-resolution with backtracking until either:

• it finds a binding of the variables that satisfies the goal — a solution, or
• it exhausts the search space — failure.

Internally, all four solvers in yopl share the same proof loop (prove): an explicit stack of choice points and goal frames, env.push() / env.pop() to checkpoint and undo unifications on backtrack, and a small instruction set (POP, rule expansion). What differs between the four files is not the proof algorithm — it is only how each one delivers solutions back to the caller and how it invokes JavaScript-implemented goal predicates.

JavaScript gives us two independent axes for that delivery:

Two questions decide which one you want:

1. Do any of your goal predicates or your result handler need to await? If yes, you need an async solver — its prove loop is async and awaits any inline-function goal you supply, and the async callback variant also awaits the result callback before backtracking. Sync solvers will silently treat a returned Promise as truthy and break.
2. Do you want to pull solutions lazily, stop after the first one, or interleave them with other work? If yes, you want a generator-based solver. With a callback solver the engine drives you; with a generator you drive the engine and can simply break out of the for loop.

solve is the synchronous, push-based combination: the solver runs to completion in one synchronous call, invoking your callback once per solution.

import solve from 'yopl';
// or, equivalently:
import solve from 'yopl/solve.js';

solve(rules, name, args, callback): void

The callback receives the live environment — the same one the solver is about to backtrack. Read what you need from it (typically with assemble(variable, env) from deep6/traverse/assemble.js) before you return; do not stash env for later use.

The callback's return value is ignored. The solver always continues searching for the next solution after it returns. To stop early, throw — there is no built-in cancellation in the sync callback driver. If you need clean early termination, use solvers-gen and break out of the for loop instead.

• Your rules and predicates are pure JS, no await needed.
• You want all solutions (or you are happy to enumerate them all even if you only use the first few), and you are fine processing them inside the callback.
• You want the simplest, lowest-overhead driver — no generator suspension, no microtask scheduling.

If any of these don't hold, see the other three solver pages.

import {variable} from 'deep6/env.js';
import assemble from 'deep6/traverse/assemble.js';
import solve from 'yopl';
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');
solve(rules, 'member', [list, X], env => {
 console.log('X =', assemble(X, env));
});
// X = 1
// X = 2
// X = 3

A rule is a function — or an array of functions for a disjunction — that receives a fresh batch of logical variables and returns an array of terms. The first term is the rule head ({args: [...]}); the rest are body goals.

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

A body goal can be:

• a structured term: {name: 'member', args: [X, V]}
• a bare string (rule name with no args): 'true'
• an inline JS function (env, goals, stack) => boolean | GoalFrame for predicates implemented directly in JavaScript. In the async solvers this function may be async, and the proof loop will await it.

See rules-system for helpers (head, term, list, cut, call, ...) that build these shapes ergonomically.