solve

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.

What a solver actually does

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.

Why four solvers?

JavaScript gives us two independent axes for that delivery:

	Push (callback)	Pull (generator)
Sync	solve	solvers/gen
Async	solvers/async	solvers/asyncGen

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

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

Signature

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

Parameter	Type	Description
rules	Rules	Rule database — a {name: rule} object.
name	string	Name of the initial goal to prove.
args	unknown[]	Argument vector that will be unified against the matching rule heads.
callback	(env: Env) => void	Invoked once per solution with the live unification environment.

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.

When to choose solve

• 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.

Example

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

Rule shape (shared by all four solvers)

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.