Struct QueryHeap 

pub struct QueryHeap<'a> { /* private fields */ }

Working heap for proof search.

Wraps a shared read-only program heap (&[Cell]) and an owned mutable cell buffer for query-time allocations. Supports branching via an optional parent pointer for backtracking.

Implementations

impl<'a> QueryHeap<'a>

pub fn new( prog_cells: &'a [Cell], root: Option<*const QueryHeap<'a>>, ) -> QueryHeap<'a>

pub fn branch(&self, count: usize) -> Vec<QueryHeap<'a>>

Trait Implementations

impl Heap for QueryHeap<'_>

fn term_string(&self, addr: usize) -> String

Create String to represent cell, can be recursively used to format complex structures or list

fn deref_addr(&self, addr: usize) -> usize

fn heap_push(&mut self, cell: Cell) -> usize

fn heap_len(&self) -> usize

fn get_id(&self) -> usize

fn truncate(&mut self, len: usize)

fn _set_arg(&mut self, value: usize) -> usize

fn set_const(&mut self, id: usize) -> usize

fn set_ref(&mut self, ref_addr: Option<usize>) -> usize

fn bind(&mut self, binding: &[(usize, usize)])

Update address value of ref cells affected by binding @binding: List of (usize, usize) tuples representing heap indexes, left -> right

fn unbind(&mut self, binding: &[(usize, usize)])

Reset Ref cells affected by binding to self references @binding: List of (usize, usize) tuples representing heap indexes, left -> right

fn str_symbol_arity(&self, addr: usize) -> (usize, usize)

Get the symbol id and arity of functor structure

fn term_vars(&self, addr: usize, args: bool) -> Vec<usize>

Collect all REF, cells in structure or referenced by structure If cell at addr is a reference return that cell

fn str_iterator(&self, addr: usize) -> RangeInclusive<usize>

Given address to a str cell create an operator over the sub terms addresses, including functor/predicate

fn normalise_args(&mut self, addr: usize, args: &mut Vec<usize>)

fn _copy_complex( &mut self, other: &impl Heap, addr: usize, update_addr: &mut usize, )

fn _copy_simple(&mut self, other: &impl Heap, addr: usize, update_addr: &usize)

fn _copy_term(&mut self, other: &impl Heap, addr: usize) -> usize

fn copy_term_with_ref_map( &mut self, other: &impl Heap, addr: usize, ref_map: &mut HashMap<usize, usize>, ) -> usize

Copy a term from other heap into self, tracking variable identity via ref_map. Unbound Ref cells in other are mapped to fresh Ref cells in self; the same source Ref always maps to the same target Ref. Call with a shared ref_map across multiple terms to preserve variable sharing (e.g. across literals in a clause).

fn _copy_ref_map_complex( &mut self, other: &impl Heap, addr: usize, ref_map: &mut HashMap<usize, usize>, ) -> Option<Cell>

Pre-pass helper for copy_term_with_ref_map: recursively copy complex sub-terms and return the Cell to later insert, or None for simple cells.

fn _copy_ref_map_simple( &mut self, other: &impl Heap, addr: usize, ref_map: &mut HashMap<usize, usize>, )

Post-pass helper for copy_term_with_ref_map: push a simple cell, handling Ref identity via ref_map.

fn _term_equal(&self, addr1: usize, addr2: usize) -> bool

fn contains_args(&self, addr: usize) -> bool

fn _print_heap(&self)

Debug function for printing formatted string of current heap state

fn list_string(&self, addr: usize) -> String

Create a string from a list

fn func_string(&self, addr: usize) -> String

Create a string for a functor structure

fn tuple_string(&self, addr: usize) -> String

Create a string for a tuple

fn set_string(&self, addr: usize) -> String

Create a string for a set

impl Index<Range<usize>> for QueryHeap<'_>

type Output = [(Tag, usize)]

The returned type after indexing.

fn index(&self, index: Range<usize>) -> &Self::Output

Performs the indexing (container[index]) operation.

impl Index<usize> for QueryHeap<'_>

type Output = (Tag, usize)

The returned type after indexing.

fn index(&self, index: usize) -> &Self::Output

Performs the indexing (container[index]) operation.

impl IndexMut<usize> for QueryHeap<'_>

fn index_mut(&mut self, index: usize) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.