srtree-db-0.1.0.0: src/Algorithm/EqSat/Storage/Stream.hs
{-# LANGUAGE OverloadedStrings #-}
-- | Proof-of-concept for an O(1)-memory matcher: instead of building the
-- in-RAM pattern trie (@_patDB@, O(nodes)), stream the @enode@/@eclass_node@
-- tables through a SQLite cursor and match each node as it is read. Peak memory
-- is O(budget) (the bounded result set), independent of graph size.
--
-- This validates the mechanism behind P2.3 (the SQL/streaming matcher rewrite)
-- before committing to replacing the trie. It is SQLite-specific (uses
-- 'Database.SQLite3' directly, since 'SqlBackend' returns whole grids).
module Algorithm.EqSat.Storage.Stream
( streamByOpCount
, streamMatchNAry
, streamRootsByOp
) where
import Database.SQLite3
( Database, SQLData(..), StepResult(..)
, bind, columns, step, withStatement )
import qualified Data.Text as T
import qualified Data.IntSet as IntSet
import Algorithm.EqSat.Egraph (EClassId, ENode(..))
import Algorithm.EqSat.Storage.Types (parseEnodeKey)
import Data.Int (Int64)
-- | Stream the @enode@ table by @op_detail@ and count rows without accumulating
-- them (the O(1)-memory baseline for a streaming matcher).
streamByOpCount :: Database -> T.Text -> IO Int
streamByOpCount db op = withStatement db
"SELECT e.key FROM enode e WHERE e.op_detail = ?" $ \stmt -> do
bind stmt [SQLText op]
go stmt 0
where
go stmt n = do
r <- step stmt
case r of
Done -> pure n
Row -> go stmt (n + 1)
-- | Stream the @eclass_node JOIN enode@ for a given operator, reconstruct each node
-- from its content key, and collect at most @budget@ e-class ids that actually
-- contain a node of that operator. Memory is O(@budget@), not O(nodes).
streamMatchNAry :: Database -> T.Text -> Int -> IO [EClassId]
streamMatchNAry db opBudget budget = withStatement db
"SELECT n.eid, n.enode_key FROM eclass_node n \
\JOIN enode e ON e.key = n.enode_key WHERE e.op_detail = ?" $ \stmt -> do
bind stmt [SQLText opBudget]
go stmt budget []
where
go stmt budgetLeft acc
| budgetLeft <= 0 = pure (reverse acc)
| otherwise = do
r <- step stmt
case r of
Done -> pure (reverse acc)
Row -> do
cols <- columns stmt
let eid = case cols of (SQLInteger i : _) -> fromIntegral i; _ -> 0
key = case cols of (_ : SQLText k : _) -> T.unpack k; _ -> ""
ok = case parseEnodeKey key of
Just (ENAry _ _) -> True
Just _ -> True
Nothing -> False
if ok
then go stmt (budgetLeft - 1) (eid : acc)
else go stmt budgetLeft acc
-- | Stream the distinct e-class ids that contain a node of a given @op_detail@
-- through a SQLite cursor, stopping after @budget@ non-excluded rows. This is
-- the O(1)-memory candidate-root source for the streaming n-ary matcher: it
-- never materializes the whole (operator -> root set) index in RAM. Memory is
-- O(@budget@ + size of @exclude@).
streamRootsByOp :: Database -> T.Text -> Int -> [EClassId] -> IO [EClassId]
streamRootsByOp db opDetail budget exclude = withStatement db
"SELECT DISTINCT n.eid FROM eclass_node n \
\JOIN enode e ON e.key = n.enode_key WHERE e.op_detail = ?" $ \stmt -> do
bind stmt [SQLText opDetail]
let ex = IntSet.fromList exclude
go stmt ex budget []
where
go stmt ex n acc
| n <= 0 = pure (reverse acc)
| otherwise = do
r <- step stmt
case r of
Done -> pure (reverse acc)
Row -> do
cols <- columns stmt
let eid = case cols of (SQLInteger i : _) -> fromIntegral i; _ -> 0
if IntSet.member eid ex
then go stmt ex n acc
else go stmt ex (n - 1) (eid : acc)