ResF4MonomialLookupTableT<Key> — tree-structured leading-term index for the F4 resolution. More...

#include "newdelete.hpp"
#include "schreyer-resolution/res-moninfo.hpp"
#include "schreyer-resolution/res-monomial-types.hpp"

Classes
class	ResF4MonomialLookupTableT< Key >
struct	ResF4MonomialLookupTableT< Key >::mi_node

Functions
void	minimalize_res_varpower_monomials (const VECTOR(res_varpower_monomial) &elems, VECTOR(int) &result_minimals, stash *mi_stash=nullptr)

Detailed Description

ResF4MonomialLookupTableT<Key> — tree-structured leading-term index for the F4 resolution.

Note: AI-generated documentation. Verify against the source before relying on it.

Declares the resolution counterpart of f4-monlookup.hpp: a templated Janet-style binary tree over res_*_monomial encodings, parameterised on the Key payload returned by lookups so the same code base can index basis-element indices, (level, index) pairs, or any other identifier the caller needs. Each mi_node stores a (var, exp) test, left and right children inside a doubly-linked sibling list under a header, and either descends to a child node or terminates at a leaf carrying the Key. insert_vp and insert_minimal_vp walk the tree splitting on the encoded variable exponents, while find_one_divisor_vp and find_one_divisor_packed report any payload whose stored monomial divides the query — the standard divisor lookup the F4 reducer-selection step depends on.

The class duplicates the older f4-monlookup.hpp pattern by design: the resolution side standardises on the res_* monomial typedefs from res-monomial-types.hpp and carries a richer Key than F4's plain int. A future cleanup may collapse them, but keeping the trees separate today lets each evolve at its own pace without coupling the F4 and resolution code paths.

See also: res-moninfo.hpp; res-monomial-types.hpp; res-schreyer-frame.hpp; f4/f4-monlookup.hpp

Definition in file res-f4-monlookup.hpp.

Classes

Functions

Detailed Description