diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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 diff --git a/app/FitData.hs b/app/FitData.hs --- a/app/FitData.hs +++ b/app/FitData.hs @@ -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 diff --git a/src/Algorithm/EqSat/Storage/Backend.hs b/src/Algorithm/EqSat/Storage/Backend.hs --- a/src/Algorithm/EqSat/Storage/Backend.hs +++ b/src/Algorithm/EqSat/Storage/Backend.hs @@ -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 () diff --git a/src/Algorithm/EqSat/Storage/Postgres.hs b/src/Algorithm/EqSat/Storage/Postgres.hs --- a/src/Algorithm/EqSat/Storage/Postgres.hs +++ b/src/Algorithm/EqSat/Storage/Postgres.hs @@ -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 diff --git a/src/Algorithm/EqSat/Storage/Query.hs b/src/Algorithm/EqSat/Storage/Query.hs --- a/src/Algorithm/EqSat/Storage/Query.hs +++ b/src/Algorithm/EqSat/Storage/Query.hs @@ -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)] diff --git a/src/Algorithm/EqSat/Storage/SQLite.hs b/src/Algorithm/EqSat/Storage/SQLite.hs --- a/src/Algorithm/EqSat/Storage/SQLite.hs +++ b/src/Algorithm/EqSat/Storage/SQLite.hs @@ -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 diff --git a/src/Algorithm/EqSat/Storage/Schema.hs b/src/Algorithm/EqSat/Storage/Schema.hs --- a/src/Algorithm/EqSat/Storage/Schema.hs +++ b/src/Algorithm/EqSat/Storage/Schema.hs @@ -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 () diff --git a/srtree-db.cabal b/srtree-db.cabal --- a/srtree-db.cabal +++ b/srtree-db.cabal @@ -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 diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -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))