diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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 ``. 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 diff --git a/src/Algorithm/EqSat/Storage/Extract.hs b/src/Algorithm/EqSat/Storage/Extract.hs --- a/src/Algorithm/EqSat/Storage/Extract.hs +++ b/src/Algorithm/EqSat/Storage/Extract.hs @@ -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))) diff --git a/src/Algorithm/EqSat/Storage/Import.hs b/src/Algorithm/EqSat/Storage/Import.hs --- a/src/Algorithm/EqSat/Storage/Import.hs +++ b/src/Algorithm/EqSat/Storage/Import.hs @@ -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) ] 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 @@ -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) ] 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.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 diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -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)