Asynchronous, callback-style solver. Same proof engine as solve, with two await points added so it can cooperate with Promise-returning code.

The synchronous solvers cannot host any goal that needs to wait — there is nowhere for them to suspend. If a JS-implemented predicate has to read a file, query a database, call an HTTP API, or even just yield to the event loop, the proof loop has to be async and await it. That is exactly what solvers/async does:

1. Inline-function goal predicates may be async. When the proof loop encounters an inline (env, goals, stack) => … goal, it awaits the result before deciding whether to continue, push a sub-frame, or backtrack. Sync solvers would treat the returned Promise as truthy and produce wrong proofs.
2. The result callback may be async. The solver awaits the callback before backtracking, so a callback that, say, writes each solution to a database will not race ahead of the proof loop or cause solutions to be processed out of order.

The cost is that the entire proof loop runs as an async function: every step goes through a microtask, which is meaningfully slower than the sync driver. Use the sync solvers when you can; use this one when you must.

• One or more goal predicates need to await (I/O, timers, async APIs, dynamic import(), …).
• The per-solution callback needs to await (e.g. it persists or forwards each solution).
• You want a callback-style API and don't need lazy enumeration. If you do, use solvers-asyncGen.

If neither of those applies, prefer solve — it is significantly cheaper.

import asyncSolve from 'yopl/solvers/async.js';

asyncSolve(rules, name, args, callback): Promise<void>

Same parameters as solve. The returned promise resolves when the search space is exhausted (and after the last callback invocation has settled).

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

const rules = {
  // an async predicate: pretend this is a database lookup
  fetchUser: [
    (Id, Name) => [
      {args: [Id, Name]},
      async (env, goals, stack) => {
        const row = await db.users.find(assemble(Id, env));
        return env.bindVal(Name.name, row.name) ? goals : null;
      }
    ]
  ]
};

const Name = variable('Name');

await asyncSolve(rules, 'fetchUser', [42, Name], async env => {
  await log(`found ${assemble(Name, env)}`);
});