TestTagsPreservationDuringResolutionImpl

Constructors

Link copied to clipboard
constructor(solverFactory: SolverFactory)

Properties

Link copied to clipboard

A long test max duration, four times mediumDuration; used for queries involving deeper search or recursion.

Link copied to clipboard

A medium test max duration, twice shortDuration; used for queries involving a handful of resolution steps.

Link copied to clipboard

A short test max duration, used for queries expected to resolve almost immediately.

Link copied to clipboard

Functions

Link copied to clipboard

Case 3: the query is tagged differently from the theory clause, at the same depth (F, G or X) — once with a different tag value for the same key, once with a different key altogether.

Link copied to clipboard
open override fun testQueryTaggedLikeTheory()

Case 2: the query is tagged exactly like the theory clause, at the same depth (F, G or X; CLAUSE has no query counterpart, since a query is a plain goal, not a wrapping clause).

Link copied to clipboard
open override fun testTagOriginDuringComputation()

Case 4: exercises a small recursive theory (a hand-rolled count/2, walking a hand-rolled list of nodes l/2 terminated by e, and building up a Peano-style succ/1-wrapped zero result) whose resolution goes through several goal-selection/rule-selection/rule-execution/backtracking cycles, so that a tag can flow through multiple unification steps.

Link copied to clipboard

Case 1: the theory clause is tagged (at each of the four depths), and the query is not.