srtree-db 0.1.3.2 → 0.1.3.3
raw patch · 6 files changed
+90/−14 lines, 6 filesdep ~srtreePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: srtree
API changes (from Hackage documentation)
Files
- ChangeLog.md +15/−0
- src/Algorithm/EqSat/Storage/Extract.hs +39/−3
- src/Algorithm/EqSat/Storage/Import.hs +3/−3
- src/Algorithm/EqSat/Storage/SQLite.hs +8/−3
- srtree-db.cabal +5/−5
- test/Main.hs +20/−0
ChangeLog.md view
@@ -1,5 +1,20 @@ # Changelog for srtree-db +## 0.1.3.3++- **Extraction of merged e-classes** (`Storage.Extract`): resolve an e-class id+ through `eclass.canonical` when its page is missing, so stale ids from+ `dataset_fit` (classes later merged away) still extract correctly.+- **Cyclic `_best` chains** (`Storage.Extract`): `extractBestFromDB` now+ backtracks over the class's other e-nodes when the `_best` chain hits a+ cycle, instead of returning `<extraction failed>`. Added the+ `extract-cyclic-best` regression test.+- **NaN e-node keys** (`Storage.SQLite`, `Storage.Import`): use+ `INSERT OR IGNORE` for `enode`/`eclass_node`/`enode_child`. Every NaN+ serializes to `"Const NaN"` while `Eq Double` treats NaNs as distinct, so+ colliding keys used to abort the whole `saveGraph` transaction.+- Require `srtree >= 3.0.0.6`.+ ## 0.1.3.2 - **fitdata: NLopt restart-scale escalation** (`fitOneNLopt`): parameterized
src/Algorithm/EqSat/Storage/Extract.hs view
@@ -27,6 +27,21 @@ ( SqlBackend(..), SqlValue(..), sqlToInt, sqlToBlob ) import Algorithm.EqSat.Storage.ClassStore (classStoreTable) +-- | Resolve an e-class id to its canonical root via the @eclass@ table.+-- Merged-away (non-canonical) ids have no page blob, so extraction must map+-- them to the root first. Canonical chains are short; the walk is bounded.+canonicalEid :: SqlBackend db => db -> EClassId -> IO EClassId+canonicalEid db = step (0 :: Int)+ where+ step k eid+ | k >= 16 = pure eid+ | otherwise = do+ rows <- queryDb db "SELECT canonical FROM eclass WHERE eid = ?"+ [SqlInteger (fromIntegral eid)]+ case rows of+ [[c]] | sqlToInt c /= eid -> step (k + 1) (sqlToInt c)+ _ -> pure eid+ -- | Reconstruct a 'Fix SRTree' for the given e-class by walking the page -- store and relational tables directly. No 'EGraph' state is needed. --@@ -45,7 +60,10 @@ | otherwise = do mPage <- readPage db eid case mPage of- Nothing -> pure Nothing+ Nothing -> do+ -- A merged-away id has no page; retry at its canonical root.+ eid' <- canonicalEid db eid+ if eid' == eid then pure Nothing else go seen n eid' Just page -> do let ec = decode page :: EClass nodes = Set.toList (_eNodes ec)@@ -139,11 +157,29 @@ | otherwise = do mPage <- readPage db eid case mPage of- Nothing -> pure Nothing+ Nothing -> do+ -- A merged-away id (e.g. a stale dataset_fit eid) has no page;+ -- retry at its canonical root.+ eid' <- canonicalEid db eid+ if eid' == eid then pure Nothing else go seen n eid' Just page -> do let ec = decode page :: EClass best = _best (_info ec)- expandNode (IntSet.insert eid seen) n best+ -- On well-formed graphs the best is extractable. If it (or+ -- a descendant) lies on a cyclic/supersaturated @_best@+ -- chain, backtrack over the class's other e-nodes instead+ -- of failing the whole extraction.+ others = [ en | en <- Set.toList (_eNodes ec), en /= best ]+ tryNodes (IntSet.insert eid seen) n (best : others)++ -- Try candidate e-nodes in order, returning the first extractable tree.+ tryNodes :: IntSet -> Int -> [ENode] -> IO (Maybe (Fix SRTree))+ tryNodes _ _ [] = pure Nothing+ tryNodes seen n (en : ens) = do+ r <- expandNode seen n en+ case r of+ Just t -> pure (Just t)+ Nothing -> tryNodes seen n ens expandNode :: IntSet -> Int -> ENode -> IO (Maybe (Fix SRTree)) expandNode _ _ (EVar ix) = pure (Just (Fix (Var ix)))
src/Algorithm/EqSat/Storage/Import.hs view
@@ -191,7 +191,7 @@ -- eliminating the O(n) post-pass that 'writeMissingPages' used to do. writeNode :: SqlBackend db => db -> EClassId -> ENode -> String -> [(EClassId, Int, Int)] -> Int -> Maybe Double -> Maybe Int -> IO () writeNode db eid en key children h fit mdsid = do- runDb db "INSERT INTO enode (key, op, op_detail) VALUES (?, ?, ?)"+ runDb db "INSERT OR IGNORE INTO enode (key, op, op_detail) VALUES (?, ?, ?)" [ SqlText (T.pack key) , SqlText (T.pack (enodeOpTag en)) , SqlText (T.pack (enodeOpDetail en)) ]@@ -199,12 +199,12 @@ [ SqlInteger (fromIntegral eid) , SqlInteger (fromIntegral eid) , SqlInteger (fromIntegral h) ]- runDb db "INSERT INTO eclass_node (eid, enode_key) VALUES (?, ?)"+ runDb db "INSERT OR IGNORE INTO eclass_node (eid, enode_key) VALUES (?, ?)" [ SqlInteger (fromIntegral eid), SqlText (T.pack key) ] -- enode_child rows exist only for ENAry nodes (EBin/Uni children live in the -- content key); the multiset is unique. forM_ (naryChildrenOf en) $ \(c, n) ->- runDb db "INSERT INTO enode_child (enode_key, child_eid, cnt) VALUES (?, ?, ?)"+ runDb db "INSERT OR IGNORE INTO enode_child (enode_key, child_eid, cnt) VALUES (?, ?, ?)" [ SqlText (T.pack key) , SqlInteger (fromIntegral c) , SqlInteger (fromIntegral n) ]
src/Algorithm/EqSat/Storage/SQLite.hs view
@@ -258,14 +258,19 @@ writeNodes db rows = forM_ (HashMap.toList (_grENodeToEClass rows)) $ \(en, eid) -> do let key = enodeKey en- run db "INSERT INTO enode (key, op, op_detail) VALUES (?, ?, ?)"+ -- Content-addressed inserts: distinct e-nodes can share a key (every NaN+ -- constant serializes to "Const NaN" while Eq Double treats NaNs as+ -- distinct, so the node map may hold several of them). The key is the+ -- identity, so colliding rows are canonicalized with OR IGNORE instead of+ -- aborting the whole save with a UNIQUE-constraint failure.+ run db "INSERT OR IGNORE INTO enode (key, op, op_detail) VALUES (?, ?, ?)" [ SqlText (T.pack key) , SqlText (T.pack (enodeOpTag en)) , SqlText (T.pack (enodeOpDetail en)) ]- run db "INSERT INTO eclass_node (eid, enode_key) VALUES (?, ?)"+ run db "INSERT OR IGNORE INTO eclass_node (eid, enode_key) VALUES (?, ?)" [ SqlInteger (fromIntegral eid), SqlText (T.pack key) ] forM_ (naryChildren en) $ \(c, n) ->- run db "INSERT INTO enode_child (enode_key, child_eid, cnt) VALUES (?, ?, ?)"+ run db "INSERT OR IGNORE INTO enode_child (enode_key, child_eid, cnt) VALUES (?, ?, ?)" [ SqlText (T.pack key) , SqlInteger (fromIntegral c) , SqlInteger (fromIntegral n) ]
srtree-db.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: srtree-db-version: 0.1.3.2+version: 0.1.3.3 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@@ -43,7 +43,7 @@ , text >=1.2 && <2.2 , direct-sqlite >=2.3 && <2.4 , postgresql-libpq >=0.10 && <0.12- , srtree >=3.0.0.4 && <3.1+ , srtree >=3.0.0.6 && <3.1 , vector >=0.12 && <0.14 , mtl >=2.2 && <2.4 default-language: Haskell2010@@ -62,7 +62,7 @@ , directory >=1.3 && <1.4 , direct-sqlite >=2.3 && <2.4 , postgresql-libpq >=0.10 && <0.12- , srtree >=3.0.0.4 && <3.1+ , srtree >=3.0.0.6 && <3.1 , srtree-db >=0.1 && <0.2 default-language: Haskell2010 @@ -75,7 +75,7 @@ base >=4.14 && <5 , optparse-applicative >=0.17 && <0.19 , srtree-db >=0.1 && <0.2- , srtree >=3.0.0.4 && <3.1+ , srtree >=3.0.0.6 && <3.1 , bytestring >=0.10 && <0.13 , binary >=0.8 && <0.9 , containers >=0.6 && <0.9@@ -105,7 +105,7 @@ , text >=1.2 && <2.2 , direct-sqlite >=2.3 && <2.4 , postgresql-libpq >=0.10 && <0.12- , srtree >=3.0.0.4 && <3.1+ , srtree >=3.0.0.6 && <3.1 , srtree-db >=0.1 && <0.2 , vector >=0.12 && <0.14 , mtl >=2.2 && <2.4
test/Main.hs view
@@ -36,6 +36,7 @@ import Algorithm.EqSat.Storage.ClassStore import Algorithm.EqSat.Storage.SQLite import Algorithm.EqSat.Storage.Query (getOrCreateDataset)+import Algorithm.EqSat.Storage.Extract (extractBestFromDB) import Algorithm.EqSat.Storage.Backend (SqlBackend, queryDb, execDb, runDb) import Algorithm.EqSat.Storage.Postgres () import qualified Algorithm.EqSat.Storage.Query as Q@@ -529,9 +530,28 @@ assertBool "DB: pairs distinct" (dA /= dC) closeDb db +-- | A cyclic @_best@ chain must not make extraction fail: 'extractBestFromDB'+-- backtracks over the class's other e-nodes and still returns a finite tree.+testExtractCyclicBest :: SqlBackend db => IO db -> (db -> IO ()) -> Test+testExtractCyclicBest openDb closeDb = TestCase $ do+ db <- openDb+ (eg, eidAdd, eidP2, _) <- buildGraph+ -- Force a cycle: add.best -> (p2 * x2), p2.best -> (add + x1). Both+ -- classes keep their original (extractable) e-nodes as fallbacks.+ let (_, eg') = runIn eg $ do+ ecA <- getEClass eidAdd+ ecP <- getEClass eidP2+ insertClass ecA { _info = (_info ecA) { _best = EBin Mul eidP2 eidP2 } }+ insertClass ecP { _info = (_info ecP) { _best = EBin Add eidAdd eidAdd } }+ _ <- saveGraphTest db eg'+ m <- extractBestFromDB db eidAdd+ assertBool "cyclic _best chain falls back to another e-node" (isJust m)+ closeDb db+ runPagedSuite :: SqlBackend db => String -> (IO db, db -> IO ()) -> [Test] runPagedSuite tag (openDb, closeDb) = [ TestLabel (tag <> " paged-roundtrip") (testPagedRoundtrip openDb closeDb)+ , TestLabel (tag <> " extract-cyclic-best") (testExtractCyclicBest openDb closeDb) , TestLabel (tag <> " paged-mutate-persist") (testPagedMutatePersist openDb closeDb) , TestLabel (tag <> " paged-fallback") (testPagedFallback openDb closeDb) , TestLabel (tag <> " lazy-load") (testLazyLoad openDb closeDb)