srtree-db 0.1.3.3 → 0.1.4.0

raw patch · 9 files changed

+313/−87 lines, 9 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• ChangeLog.md +21/−0
• app/FitData.hs +3/−3
• src/Algorithm/EqSat/Storage/Backend.hs +5/−1
• src/Algorithm/EqSat/Storage/Postgres.hs +13/−5
• src/Algorithm/EqSat/Storage/Query.hs +16/−3
• src/Algorithm/EqSat/Storage/SQLite.hs +187/−66
• src/Algorithm/EqSat/Storage/Schema.hs +28/−8
• srtree-db.cabal +1/−1
• test/Main.hs +39/−0

@@ -1,5 +1,26 @@ # Changelog for srtree-db +## 0.1.4.0++- **Split-DB correctness**: the egraph DB is now genuinely structure-only when a+  separate fit DB is used.+  - New `createSchemaStructure` / `structureSchemaSQL` (no dataset tables).+  - New `saveGraphStructure`: writes structure only and strips+    fitness/DL/theta from serialized class pages.+  - New `loadGraphResidentNoFit`, `loadGraphResidentFor`, `loadGraphLazyNoFit`:+    structure-only / dataset-scoped loads that do not read the egraph DB's+    dataset tables. Dataset fields in page blobs are cleared before+    `dataset_fit` is applied, so stale fitness cannot leak.+  - New `pushFitFit` and `pushFitSplit`: write complete per-dataset fit+    snapshots to a fit DB (including correct `size`/`dl`), with pages streamed+    from the egraph DB when the graph is paged.+  - New `getOrCreateDatasetFit` (fit schema only).+  - `readDatasetFit` now creates the fit schema rather than the legacy combined+    schema.+- **`fitdata`/`refit`**: use `getOrCreateDatasetFit`, so fit DBs no longer gain+  egraph structure tables.+- Require no `srtree` bump (still `>= 3.0.0.6`).+ ## 0.1.3.3  - **Extraction of merged e-classes** (`Storage.Extract`): resolve an e-class id

@@ -39,7 +39,7 @@ import Algorithm.EqSat.Storage.Backend (SqlBackend(..), SqlValue(..), sqlToInt) import Algorithm.EqSat.Storage.Extract (reconstructFromCache, expandTreeIds) import Algorithm.EqSat.Storage.SQLite (loadPagesBulk)-import Algorithm.EqSat.Storage.Query (getOrCreateDataset, writeDatasetFit)+import Algorithm.EqSat.Storage.Query (getOrCreateDatasetFit, writeDatasetFit) import Algorithm.EqSat.Storage.Schema (createSchemaFit) import Algorithm.EqSat.Storage.Types (serializeTheta) import Database.SQLite3 (Database, open, close, exec)@@ -132,7 +132,7 @@   withSQLite fitdataFitdb $ \fitDb -> do     createSchemaFit fitDb     withSQLite fitdataEgraph $ \egDb -> do-      dsid <- getOrCreateDataset fitDb fitdataDataset+      dsid <- getOrCreateDatasetFit fitDb fitdataDataset        total <- countUnfitted egDb fitDb dsid       putStrLn $ "Found " ++ show total ++ " unfitted e-classes"@@ -509,7 +509,7 @@   hFlush stdout   withSQLite fitdataFitdb $ \fitDb -> do     createSchemaFit fitDb-    dsid <- getOrCreateDataset fitDb fitdataDataset+    dsid <- getOrCreateDatasetFit fitDb fitdataDataset     runDb fitDb "DELETE FROM dataset_fit WHERE dataset_id = ?" [SqlInteger (fromIntegral dsid)]     putStrLn $ "Cleared fit data for dataset " ++ show dsid ++ "."     hFlush stdout

@@ -75,8 +75,12 @@   -- implement this; others fall back to a grid 'queryDb' (unbounded, documented).   -- The blob is delivered hex-decoded (raw) to the callback.   streamPages :: db -> Text -> (Int64 -> BS.ByteString -> IO ()) -> IO ()-  -- | Create the egraph schema (tables, indexes) for this driver.+  -- | Create the legacy combined egraph schema (structure + dataset tables)+  -- for this driver.   createSchemaDb :: db -> IO ()+  -- | Create the structure-only egraph schema (no dataset/fit tables) for+  -- this driver.+  createSchemaDbStructure :: db -> IO ()   -- | Create the fit dataset schema (tables, indexes) for this driver.   createSchemaDbFit :: db -> IO () 

@@ -14,6 +14,7 @@ -- @postgresql://@ DSN. module Algorithm.EqSat.Storage.Postgres   ( schemaEgraphPostgres+  , schemaStructurePostgres   , schemaFitPostgres   , connectPostgres   , closePostgres@@ -33,14 +34,14 @@  import Algorithm.EqSat.Storage.Backend (SqlValue(..), SqlBackend(..), sqlToInt, sqlToText) --- | PostgreSQL DDL for the egraph section.+-- | PostgreSQL DDL for the structure-only egraph section. -- -- Differences from SQLite: @BIGINT@ identity keys, @DOUBLE PRECISION@ -- metrics, and foreign keys declared @DEFERRABLE INITIALLY DEFERRED@ so the--- writer can insert @eclass_node@/@fit@ rows before their referenced--- @eclass@ rows within the @BEGIN@..@COMMIT@ transaction of 'saveGraph'.-schemaEgraphPostgres :: [Text]-schemaEgraphPostgres =+-- writer can insert @eclass_node@ rows before their referenced @eclass@ rows+-- within the @BEGIN@..@COMMIT@ transaction of 'saveGraph'.+schemaStructurePostgres :: [Text]+schemaStructurePostgres =   [ "CREATE TABLE IF NOT EXISTS meta ("     <> " key TEXT PRIMARY KEY,"     <> " value TEXT NOT NULL)"@@ -72,6 +73,12 @@     <> " updated_at TEXT)"   ] +-- | PostgreSQL DDL for the legacy combined egraph section. The Postgres+-- egraph schema never contained dataset tables, so it is identical to the+-- structure-only schema.+schemaEgraphPostgres :: [Text]+schemaEgraphPostgres = schemaStructurePostgres+ -- | PostgreSQL DDL for a per-dataset fit DB (no FK to eclass). schemaFitPostgres :: [Text] schemaFitPostgres =@@ -164,6 +171,7 @@         pure seed0    createSchemaDb conn = mapM_ (execDb conn) schemaEgraphPostgres+  createSchemaDbStructure conn = mapM_ (execDb conn) schemaStructurePostgres   createSchemaDbFit conn = mapM_ (execDb conn) schemaFitPostgres    -- Grid fallback (Postgres is not the out-of-core target): the cursor-based

@@ -9,6 +9,7 @@ -- SQLite and PostgreSQL backends. module Algorithm.EqSat.Storage.Query   ( getOrCreateDataset+  , getOrCreateDatasetFit   , datasetId   , firstDatasetId   , writeDatasetFit@@ -35,12 +36,24 @@  import Algorithm.EqSat.Storage.Backend   ( SqlBackend, SqlValue(..), runDb, queryDb, sqlToInt, sqlToMaybeDouble, sqlToText )-import Algorithm.EqSat.Storage.Schema (createSchema)+import Algorithm.EqSat.Storage.Schema (createSchema, createSchemaFit) --- | Resolve a dataset name to its @dataset@ row id, creating it if needed.+-- | Resolve a dataset name to its @dataset@ row id, creating the legacy+-- combined schema if needed. getOrCreateDataset :: SqlBackend db => db -> String -> IO Int getOrCreateDataset db name = do   createSchema db+  getOrCreateDatasetId db name++-- | Resolve a dataset name in a per-dataset fit DB, creating the fit schema if+-- needed (no egraph structure tables are added).+getOrCreateDatasetFit :: SqlBackend db => db -> String -> IO Int+getOrCreateDatasetFit db name = do+  createSchemaFit db+  getOrCreateDatasetId db name++getOrCreateDatasetId :: SqlBackend db => db -> String -> IO Int+getOrCreateDatasetId db name = do   m <- datasetId db name   case m of     Just i  -> pure i@@ -100,7 +113,7 @@   :: SqlBackend db => db -> Int   -> IO [(EClassId, (Maybe Double, Maybe Double, Int, Text))] readDatasetFit db ds = do-  createSchema db+  createSchemaFit db   rows <- queryDb db     "SELECT eid, fitness, dl, size, theta FROM dataset_fit WHERE dataset_id = ?"     [SqlInteger (fromIntegral ds)]

@@ -20,23 +20,30 @@ -- ('Algorithm.EqSat.Storage.Postgres'). module Algorithm.EqSat.Storage.SQLite   ( saveGraph+  , saveGraphStructure   , loadGraph   , loadGraphResident+  , loadGraphResidentNoFit+  , loadGraphResidentFor   , loadGraphLazy+  , loadGraphLazyNoFit   , pushFit+  , pushFitFit+  , pushFitSplit   , refreshFitness   , query   , flushStore   , loadPagesBulk   , emptyPagedGraph   , createSchema+  , createSchemaStructure   , createSchemaFit   ) where  import Control.Monad (forM, forM_, when, foldM) import Control.Exception (SomeException, catch, displayException) import Control.Monad.Identity (runIdentity)-import Control.Monad.State.Strict (execStateT)+import Control.Monad.State.Strict (execStateT, runStateT) import Data.Int (Int64) import Data.Maybe (catMaybes, fromMaybe, listToMaybe) import Data.Text (Text)@@ -59,7 +66,7 @@  import Data.SRTree.Eval (Target) import Algorithm.EqSat.Egraph-  ( EGraph(..), EClassId, ENode(..), Consts(..)+  ( EGraph(..), EGraphST, ClassStore, EClassId, ENode(..), Consts(..)   , EClassPageStore(..), EClass(..), EClassData(..)   , EGraphDB(..), emptyDB, canonical, insertRange, eChildren, eOpKey ) import Algorithm.EqSat.Build (populate)@@ -73,7 +80,7 @@ import Algorithm.EqSat.Storage.Query (readDatasetFit, writeDatasetFit, firstDatasetId) import Algorithm.EqSat.Storage.Stream (streamRootsByOp) import Algorithm.EqSat.Storage.Types-import Algorithm.EqSat.Storage.Schema (egraphSchemaSQL, fitSchemaSQL, createSchema, createSchemaFit)+import Algorithm.EqSat.Storage.Schema (egraphSchemaSQL, structureSchemaSQL, fitSchemaSQL, createSchema, createSchemaStructure, createSchemaFit)  -- | Default cache capacity (pages) for the lazily paged e-class store. -- Kept small: the cache is an LRU of deserialized EClass objects (each with@@ -142,6 +149,7 @@             k eid blob             go stmt   createSchemaDb db = mapM_ (exec db) egraphSchemaSQL+  createSchemaDbStructure db = mapM_ (exec db) structureSchemaSQL   createSchemaDbFit db = mapM_ (exec db) fitSchemaSQL  toSqlData :: SqlValue -> SQLData@@ -184,21 +192,41 @@ -- out-of-core persistence -- and never rebuilds the canonical/node tables from -- the (bounded, partial) resident caches. saveGraph :: SqlBackend db => db -> Int -> EGraph -> IO (Either String ())-saveGraph db dsid eg = do-  createSchema db+saveGraph db dsid eg = saveGraphWith True (createSchema db) db (Just dsid) eg++-- | Save only the e-graph structure. No @dataset@/@dataset_fit@ rows are+-- written, and the serialized class pages have their dataset-specific fields+-- (fitness/DL/theta) cleared, so a structure-only database contains no+-- per-dataset data at rest.+saveGraphStructure :: SqlBackend db => db -> EGraph -> IO (Either String ())+saveGraphStructure db eg = saveGraphWith False (createSchemaStructure db) db Nothing eg++saveGraphWith+  :: SqlBackend db+  => Bool                    -- ^ write dataset_fit rows too (legacy combined mode)+  -> IO ()                   -- ^ schema creation action+  -> db -> Maybe Int -> EGraph+  -> IO (Either String ())+saveGraphWith writeFit mkSchema db mdsid eg = do+  mkSchema   let rows0 = exportEGraph eg   case _classStore eg of     Just _  -> commitWith $ do       writeMeta db rows0     Nothing -> do       gr <- graphClassRows eg-      let rows = rows0 { _grEClasses = gr }+      let rowsBase = rows0 { _grEClasses = gr }+          rows = if writeFit+                   then rowsBase+                   else rowsBase { _grEClasses = IntMap.map stripRowDatasetInfo gr }       commitWith $ do         clearTables db         writeMeta db rows         writeNodes db rows         writeClasses db rows-        writeDatasetFitRows db dsid rows+        case (writeFit, mdsid) of+          (True, Just dsid) -> writeDatasetFitRows db dsid rows+          _                 -> pure ()         writeClassPages db rows   where     commitWith writes = do@@ -210,6 +238,14 @@           pure (Left ("saveGraph failed: " <> displayException e))       pure result +-- | Clear per-dataset fields from class metadata. @_size@ is structural and is+-- deliberately kept.+stripDatasetInfo :: EClassData -> EClassData+stripDatasetInfo info = info { _fitness = Nothing, _dl = Nothing, _theta = [] }++stripRowDatasetInfo :: EClassRow -> EClassRow+stripRowDatasetInfo r = r { _rcInfo = stripDatasetInfo (_rcInfo r) }+ -- | Enumerate every canonical e-class row of a graph. For a paged graph the -- resident @_eClass@ is a bounded cache that may hold classes created or mutated -- after the last flush, so it is the authoritative source for any class it@@ -299,6 +335,53 @@ -- --------------------------------------------------------------------------- -- reading +-- | Read a dataset's fit rows into an eid-keyed map. 'Nothing' means "no+-- dataset" (structure-only load): no dataset tables are queried, so this works+-- on a pure structure database.+readFitFor+  :: SqlBackend db+  => Maybe Int -> db+  -> IO (IntMap.IntMap (Maybe Double, Maybe Double, Int, [Target]))+readFitFor Nothing _ = pure IntMap.empty+readFitFor (Just ds) db = do+  rows <- readDatasetFit db ds+  pure $ IntMap.fromList+    [ (eid, (f, d, sz, parseTheta (T.unpack th)))+    | (eid, (f, d, sz, th)) <- rows ]++-- | Apply a dataset's fit rows to decoded e-classes.+--+-- @clearMissing@ controls classes that have no row in the selected dataset:+--   * 'True'  - clear fitness/DL/theta (split mode: fitness is dataset state+--               and a class that was not fitted for this dataset is+--               unevaluated).+--   * 'False' - keep the values embedded in the page blob (legacy combined+--               databases, where paged writes historically stored fitness in+--               the page and not every class had a @dataset_fit@ row).+--+-- @_size@ is structural; a positive size from the fit row is accepted for+-- compatibility with older fit writers, otherwise the structural size is kept.+applyFitMap+  :: Bool+  -> IntMap.IntMap (Maybe Double, Maybe Double, Int, [Target])+  -> IntMap.IntMap EClass+  -> IntMap.IntMap EClass+applyFitMap clearMissing fitMap = IntMap.mapWithKey apply+  where+    apply eid ec =+      let info0 = _info ec+          info1 = if clearMissing then stripDatasetInfo info0 else info0+          ec0   = ec { _info = info1 }+      in case IntMap.lookup eid fitMap of+           Nothing -> ec0+           Just (f, d, s, th) ->+             ec0 { _info = info1+                     { _fitness = f+                     , _dl      = d+                     , _size    = if s > 0 then s else _size info1+                     , _theta   = th+                     } }+ -- | Reconstruct the e-graph stored by a previous 'saveGraph'. -- -- When the database carries e-class pages (@cstore_page@), the graph is@@ -318,12 +401,7 @@       -- risk metrics come from @dataset_fit@ (the legacy @fit@ table is gone);       -- the legacy non-dataset loader uses the first dataset's values.       mdsid <- firstDatasetId db-      fit    <- case mdsid of-                  Nothing -> pure []-                  Just ds -> do-                    rows <- readDatasetFit db ds-                    pure [ (eid, (f, d, sz, parseTheta (T.unpack th)))-                         | (eid, (f, d, sz, th)) <- rows ]+      fitMap <- readFitFor mdsid db       let canon     = IntMap.fromList [ (eid, c) | (eid, c, _) <- ecLst ]           nodeToEClass = HashMap.fromList enodes       ps <- openClassStore db defaultClassCap 1000@@ -333,19 +411,13 @@           -- fully relational path (databases written before the page store)           -- Parent pointers are recomputed from nodeToEClass (the parent table           -- has been removed; buildClasses handles the fallback).-          let classes = buildClasses canon nodeToEClass IntMap.empty (IntMap.fromList fit) (IntMap.fromList [ (eid, h) | (eid, _, h) <- ecLst ])+          let classes = buildClasses canon nodeToEClass IntMap.empty fitMap (IntMap.fromList [ (eid, h) | (eid, _, h) <- ecLst ])               rows    = GraphRows canon nodeToEClass classes nextId trackDBs           pure (importEGraph rows)         else do           -- paged path: classes come from the serialized pages; the @fit@           -- table overrides their risk metrics (it is the current DB truth).-          let fitMap = IntMap.fromList fit-              applyFit eid ec =-                case IntMap.lookup eid fitMap of-                  Nothing -> ec-                  Just (f, d, s, th) ->-                    ec { _info = (_info ec){ _fitness = f, _dl = d, _size = s, _theta = th } }-              classes  = IntMap.mapWithKey applyFit+          let classes  = applyFitMap False fitMap                            (IntMap.fromList [ (eid, decode (BL.fromStrict page)) | (eid, page) <- pages ])               toRow eid ec = EClassRow (_eNodes ec) (_parents ec) (_height ec) (_info ec)               rows = GraphRows canon nodeToEClass (IntMap.mapWithKey toRow classes) nextId trackDBs@@ -359,37 +431,38 @@ -- Note: if some eclasses are referenced by nodes but don't have pages -- (e.g. created during eqsat but not flushed), this will skip them. loadGraphResident :: SqlBackend db => db -> IO (Either String EGraph)-loadGraphResident db = do-  m <- readMeta db+loadGraphResident db = firstDatasetId db >>= \mdsid -> loadGraphResidentWithFit False mdsid db++-- | Load a structure-only resident graph. No dataset tables are queried, so+-- every class starts unevaluated. Safe on a pure structure database.+loadGraphResidentNoFit :: SqlBackend db => db -> IO (Either String EGraph)+loadGraphResidentNoFit db = loadGraphResidentWithFit True Nothing db++-- | Load a resident graph applying fit rows for a specific dataset in the same+-- database.+loadGraphResidentFor :: SqlBackend db => db -> Int -> IO (Either String EGraph)+loadGraphResidentFor db dsid = loadGraphResidentWithFit True (Just dsid) db++loadGraphResidentWithFit :: SqlBackend db => Bool -> Maybe Int -> db -> IO (Either String EGraph)+loadGraphResidentWithFit clearMissing mdsid db = do+  m <- readMeta db `catch` \(_ :: SomeException) -> pure Nothing   case m of     Nothing -> pure (Left "srtree-db: no e-graph stored in this database")     Just (nextId, trackDBs) -> do       enodes <- readNodes db       ecLst  <- readClasses db-      mdsid <- firstDatasetId db-      fit    <- case mdsid of-                  Nothing -> pure []-                  Just ds -> do-                    rows <- readDatasetFit db ds-                    pure [ (eid, (f, d, sz, parseTheta (T.unpack th)))-                         | (eid, (f, d, sz, th)) <- rows ]+      fitMap <- readFitFor mdsid db       let canon     = IntMap.fromList [ (eid, c) | (eid, c, _) <- ecLst ]           nodeToEClass = HashMap.fromList enodes       ps <- openClassStore db defaultClassCap 1000       pages <- allPages ps       if null pages         then do-          let classes = buildClasses canon nodeToEClass IntMap.empty (IntMap.fromList fit) (IntMap.fromList [ (eid, h) | (eid, _, h) <- ecLst ])+          let classes = buildClasses canon nodeToEClass IntMap.empty fitMap (IntMap.fromList [ (eid, h) | (eid, _, h) <- ecLst ])               rows    = GraphRows canon nodeToEClass classes nextId trackDBs           pure (importEGraph rows)         else do-          let fitMap = IntMap.fromList fit-              applyFit eid ec =-                case IntMap.lookup eid fitMap of-                  Nothing -> ec-                  Just (f, d, s, th) ->-                    ec { _info = (_info ec){ _fitness = f, _dl = d, _size = s, _theta = th } }-              classes  = IntMap.mapWithKey applyFit+          let classes  = applyFitMap clearMissing fitMap                            (IntMap.fromList [ (eid, decode (BL.fromStrict page)) | (eid, page) <- pages ])               -- Filter nodeToEClass to only reference eclasses that have pages               validEids = IntMap.keysSet classes@@ -484,7 +557,17 @@ -- current, so nothing O(nodes) is materialized at load. loadGraphLazy :: SqlBackend db => db -> Int -> Int -> Int -> Int -> IO (Either String EGraph) --                              db   dsid  residentCap nodeCap canonicalCap-loadGraphLazy db dsid residentCap nodeCap canonicalCap = do+loadGraphLazy db dsid = loadGraphLazyWithFit False (Just dsid) db++-- | Structure-only lazy load: no dataset tables are queried, so every class+-- starts unevaluated. Safe on a pure structure database.+loadGraphLazyNoFit :: SqlBackend db => db -> Int -> Int -> Int -> IO (Either String EGraph)+loadGraphLazyNoFit db = loadGraphLazyWithFit True Nothing db++loadGraphLazyWithFit+  :: SqlBackend db+  => Bool -> Maybe Int -> db -> Int -> Int -> Int -> IO (Either String EGraph)+loadGraphLazyWithFit clearMissing mdsid db residentCap nodeCap canonicalCap = do   m <- readMeta db `catch` \(_ :: SomeException) -> do          -- The egraph tables may not exist yet on a fresh database (e.g. first          -- insert); treat that as "no e-graph stored" rather than crashing.@@ -492,10 +575,8 @@   case m of     Nothing -> pure (Left "srtree-db: no e-graph stored in this database")     Just (nextId, trackDBs) -> do-      dsFit  <- readDatasetFit db dsid-      let fitMap = IntMap.fromList [ (eid, (f, d, sz, parseTheta (T.unpack th)))-                                   | (eid, (f, d, sz, th)) <- dsFit ]-          -- slim (no theta) map for the out-of-core path: the eqsat matcher's+      fitMap <- readFitFor mdsid db+      let -- slim (no theta) map for the out-of-core path: the eqsat matcher's           -- conditions read only class _consts, never theta, so attaching it on           -- every page read would retain O(#classes) target vectors in RAM.           fitSlim = IntMap.map (\(f, d, sz, _) -> (f, d, sz)) fitMap@@ -521,7 +602,7 @@           -- metadata, applied on page reads (not baked into the pages).           let base = classStoreHandle ps               h    = base { cpsLookup = \eid ->-                              fmap (fmap (applyDsFit fitSlim eid)) (cpsLookup base eid) }+                              fmap (fmap (applyDsFit clearMissing fitSlim eid)) (cpsLookup base eid) }               eDB  = seedEDBPaged nextId trackDBs HashMap.empty residentCap nodeCap canonicalCap               eg   = EGraph IntMap.empty HashMap.empty IntMap.empty eDB (Just h)           pure (Right eg)@@ -543,11 +624,21 @@ -- keeping the per-class @[Target]@ vectors out of the resident read path avoids -- O(#classes) memory; theta stays in @dataset_fit@ for the query path. applyDsFit-  :: IntMap.IntMap (Maybe Double, Maybe Double, Int)+  :: Bool+  -> IntMap.IntMap (Maybe Double, Maybe Double, Int)   -> EClassId -> EClass -> EClass-applyDsFit m eid ec = case IntMap.lookup eid m of-  Nothing -> ec-  Just (f, dl, sz) -> ec { _info = (_info ec) { _fitness = f, _dl = dl, _size = sz } }+applyDsFit clearMissing m eid ec =+  let info0 = _info ec+      info1 = if clearMissing then stripDatasetInfo info0 else info0+      ec0   = ec { _info = info1 }+  in case IntMap.lookup eid m of+       Nothing -> ec0+       Just (f, dl, sz) ->+         ec0 { _info = info1+                 { _fitness = f+                 , _dl      = dl+                 , _size    = if sz > 0 then sz else _size info1+                 } }  -- | Cheap emptiness test for the page store (avoids materializing every page -- blob just to pick the relational vs paged load path).@@ -622,40 +713,70 @@     headOrDefault _   (x:_) = x  -- | Push the graph's risk metrics into the @dataset_fit@ table for a dataset--- (leaves structure intact). On a paged graph the classes are streamed page by--- page (O(1) memory) rather than materialized via 'cpsAll'.+-- in a legacy combined DB (leaves structure intact). On a paged graph the+-- classes are streamed page by page (O(1) memory) rather than materialized via+-- 'cpsAll'. pushFit :: SqlBackend db => db -> Int -> EGraph -> IO ()-pushFit db dsid eg = do-  createSchema db-  run db "DELETE FROM dataset_fit WHERE dataset_id = ?" [SqlInteger (fromIntegral dsid)]+pushFit = pushFitWith createSchema++-- | Like 'pushFit', but creates the per-dataset fit schema. Use this when the+-- fit table lives in a separate fit DB and the graph is resident (or the page+-- store lives in the same DB).+pushFitFit :: SqlBackend db => db -> Int -> EGraph -> IO ()+pushFitFit = pushFitWith createSchemaFit++-- | Write fit rows to a separate fit DB, reading paged classes from the egraph+-- DB. Required when the graph is paged and the fit DB is a different file: the+-- paged page store lives in the egraph DB, not in the fit DB.+pushFitSplit :: (SqlBackend egDb, SqlBackend fitDb) => egDb -> fitDb -> Int -> EGraph -> IO ()+pushFitSplit = pushFitWithSource createSchemaFit++pushFitWith :: SqlBackend db => (db -> IO ()) -> db -> Int -> EGraph -> IO ()+pushFitWith mkSchema db = pushFitWithSource mkSchema db db++pushFitWithSource+  :: (SqlBackend egDb, SqlBackend fitDb)+  => (fitDb -> IO ())+  -> egDb -> fitDb -> Int -> EGraph -> IO ()+pushFitWithSource mkSchema egDb fitDb dsid eg = do+  mkSchema fitDb+  run fitDb "DELETE FROM dataset_fit WHERE dataset_id = ?" [SqlInteger (fromIntegral dsid)]   case _classStore eg of     Nothing -> do       let rows0 = exportEGraph eg-      writeDatasetFitRows db dsid rows0+      writeDatasetFitRows fitDb dsid rows0     Just _ -> do       -- flush so every dirty page is in @cstore_page@, then stream each class-      -- and write its row, discarding it (O(1) memory).+      -- from the egraph DB and write its row to the fit DB (O(1) memory).       flushStore eg-      execDb db "BEGIN"-      streamPages db classStoreTable $ \_eid blob -> do+      execDb fitDb "BEGIN"+      streamPages egDb classStoreTable $ \_eid blob -> do         let ec = decode (BL.fromStrict blob)             info = _info ec-        writeDatasetFit db dsid (_eClassId ec) (_fitness info) (_dl info)+        writeDatasetFit fitDb dsid (_eClassId ec) (_fitness info) (_dl info)           (T.pack (serializeTheta (_theta info))) (_size info)-      execDb db "COMMIT"+      execDb fitDb "COMMIT"  -- | Overwrite in-memory fitness/DL with the values currently stored in the -- database for a dataset (per e-class, by canonical id). refreshFitness :: SqlBackend db => db -> Int -> EGraph -> IO (Either String EGraph) refreshFitness db dsid eg = do   dsFit <- readDatasetFit db dsid-  let m = forM_ dsFit $ \(eid, (fitM, _, _, theta)) ->-            case fitM of-              Nothing -> pure ()-              Just f  -> do-                c <- canonical eid-                insertFitness c f (parseTheta (T.unpack theta))-  pure (Right (runIdentity $ execStateT m eg))+  let applyFit :: ClassStore m => EGraphST m ()+      applyFit = forM_ dsFit $ \(eid, (fitM, _, _, theta)) ->+        case fitM of+          Nothing -> pure ()+          Just f  -> do+            c <- canonical eid+            insertFitness c f (parseTheta (T.unpack theta))+  case _classStore eg of+    -- Resident graph: the pure ClassStore instance is sufficient.+    Nothing -> pure (Right (runIdentity $ execStateT applyFit eg))+    -- Paged graph: run through the IO ClassStore so page reads/writes use the+    -- live store (the pure instance would see an empty resident map).+    Just _  -> do+      (_, eg') <- runStateT applyFit eg+      pure (Right eg')  -- | Bulk-load page blobs for a list of e-class IDs in one query, returning -- an IntMap of deserialized EClass values. For lists exceeding SQLite's

@@ -9,12 +9,15 @@ --   * Dataset-fit section (per-dataset, write-heavy during fitting): --     @dataset@, @dataset_fit@, @expression_index@ ----- 'egraphSchemaSQL' is the DDL for the egraph DB.+-- 'structureSchemaSQL' is the DDL for a structure-only egraph DB.+-- 'egraphSchemaSQL' is the legacy combined DDL (structure + dataset tables). -- 'fitSchemaSQL' is the DDL for a per-dataset fit DB (no FK to eclass). module Algorithm.EqSat.Storage.Schema-  ( egraphSchemaSQL+  ( structureSchemaSQL+  , egraphSchemaSQL   , fitSchemaSQL   , createSchema+  , createSchemaStructure   , createSchemaFit   ) where @@ -22,10 +25,12 @@  import Algorithm.EqSat.Storage.Backend (SqlBackend(..)) --- | DDL for the egraph database.--- Full schema including dataset tables for backward compatibility with importEqs.-egraphSchemaSQL :: [Text]-egraphSchemaSQL =+-- | DDL for a structure-only egraph database.+--+-- This is the split-DB egraph section: no dataset/fit tables, so an egraph DB+-- written in split mode contains no per-dataset data at rest.+structureSchemaSQL :: [Text]+structureSchemaSQL =   [ "CREATE TABLE IF NOT EXISTS meta ("     <> " key TEXT PRIMARY KEY,"     <> " value TEXT NOT NULL)"@@ -60,7 +65,13 @@   , "CREATE TABLE IF NOT EXISTS frontier ("     <> " eid INTEGER PRIMARY KEY REFERENCES eclass(eid) ON DELETE CASCADE,"     <> " updated_at TEXT)"-  , "CREATE TABLE IF NOT EXISTS dataset ("+  ]++-- | Dataset/fit tables used by the legacy combined egraph DB (with FKs to+-- @eclass@) and by 'importEqs'.+datasetSchemaSQL :: [Text]+datasetSchemaSQL =+  [ "CREATE TABLE IF NOT EXISTS dataset ("     <> " id INTEGER PRIMARY KEY,"     <> " name TEXT NOT NULL UNIQUE,"     <> " created TEXT)"@@ -83,6 +94,11 @@     <> " first_seen TEXT)"   ] +-- | DDL for the legacy combined egraph database (structure + dataset tables).+-- Kept for backward compatibility with importEqs and old DB files.+egraphSchemaSQL :: [Text]+egraphSchemaSQL = structureSchemaSQL <> datasetSchemaSQL+ -- | DDL for a per-dataset fit database. -- No FK to eclass (e-graph lives in a separate DB). fitSchemaSQL :: [Text]@@ -110,9 +126,13 @@     <> " first_seen TEXT)"   ] --- | Create (or ensure) the egraph schema on the given backend.+-- | Create (or ensure) the legacy combined egraph schema on the given backend. createSchema :: SqlBackend db => db -> IO () createSchema = createSchemaDb++-- | Create (or ensure) the structure-only egraph schema on the given backend.+createSchemaStructure :: SqlBackend db => db -> IO ()+createSchemaStructure = createSchemaDbStructure  -- | Create (or ensure) the fit schema on the given backend. createSchemaFit :: SqlBackend db => db -> IO ()

@@ -1,6 +1,6 @@ cabal-version: 2.4 name:          srtree-db-version:       0.1.3.3+version:       0.1.4.0 synopsis:      SQL persistence and querying for srtree e-graphs description:   Reusable storage layer for srtree multiset e-graphs:                a driver-neutral serialization of the Algorithm.EqSat.Store

@@ -606,9 +606,48 @@   assertBool "ancestors should include Mul" (eidMul `elem` ancestors)   closeDb db +-- | Split-mode round-trip: structure-only save writes no fit rows; a no-fit+-- load leaves every class unevaluated; fit rows from a separate dataset apply+-- cleanly.+testSplitSaveLoad :: SqlBackend db => IO db -> (db -> IO ()) -> Test+testSplitSaveLoad openDb closeDb = TestCase $ do+  db <- openDb+  (eg, eidAdd, _eidP2, eidP3) <- buildGraph+  createSchemaFit db+  r <- saveGraphStructure db eg+  case r of+    Left err -> assertFailure ("saveGraphStructure failed: " <> err)+    Right () -> pure ()+  dsid <- Q.getOrCreateDatasetFit db "split-test"+  cntRows <- queryDb db+    "SELECT COUNT(*) FROM dataset_fit WHERE dataset_id = ?"+    [SqlInteger (fromIntegral dsid)]+  let cnt = case cntRows of { [[n]] -> sqlToInt n; _ -> -1 }+  assertEqual "structure-only save must not write fit rows" 0 cnt++  me0 <- loadGraphResidentNoFit db+  case me0 of+    Left err -> assertFailure ("loadGraphResidentNoFit failed: " <> err)+    Right eg0 -> do+      let fits = [ _fitness (_info ec) | ec <- IntMap.elems (_eClass eg0) ]+      assertBool "no-fit load must leave all classes unevaluated"+        (all isNothing fits)+      -- Write this dataset's fit rows, then load them back.+      pushFitFit db dsid eg+      me1 <- loadGraphResidentFor db dsid+      case me1 of+        Left err -> assertFailure ("loadGraphResidentFor failed: " <> err)+        Right eg1 -> do+          assertEqual "fitness applied from fit rows"+            (Just 0.9) (evalIn eg1 (getFitness eidAdd))+          let th = evalIn eg1 (getTheta eidP3)+          assertEqual "theta applied from fit rows" 1 (length th)+  closeDb db+ runSuite :: SqlBackend db => String -> (IO db, db -> IO ()) -> [Test] runSuite tag (openDb, closeDb) =   [ TestLabel (tag <> " save-load-roundtrip") (testSaveLoadRT openDb closeDb)+  , TestLabel (tag <> " split-save-load")     (testSplitSaveLoad openDb closeDb)   , TestLabel (tag <> " queries")             (testQueries openDb closeDb)   , TestLabel (tag <> " sync")                (testSync openDb closeDb)   , TestLabel (tag <> " enode-parent")        (testEnodeParent (openDb, closeDb))