Skip to content

Commit 0cca70e

Browse files
atzedijkstraatzedijkstra
committed
dramatic performance improvement by moving workstore to backtracking state (thus not globally growing)
1 parent 2f1dd8b commit 0cca70e

File tree

2 files changed

+27
-43
lines changed

2 files changed

+27
-43
lines changed

‎chr-core/src/CHR/Solve/MonoBacktrackPrio.hs‎

Lines changed: 19 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -155,25 +155,16 @@ type WorkInx = WorkTime
155155

156156
type WorkInxSet = IntSet.IntSet
157157

158-
data WorkOrFreeList cnstr
159-
= WorkWork
160-
{ _worfWork :: !(Work cnstr)
161-
}
162-
| WorkFreeList
163-
{ _worfNext :: {-# UNPACK #-} !WorkTime
164-
}
165-
166158
data WorkStore cnstr
167159
= WorkStore
168160
{ _wkstoreTrie :: !(TT.TreeTrie (TT.TrTrKey cnstr) [WorkInx]) -- ^ map from the search key of a constraint to index in table
169-
, _wkstoreTable :: !(IntMap.IntMap (WorkOrFreeList cnstr)) -- ^ all the work ever entered. FIXME: do GC. Infra in place but need to ensure it can be safely done because trace/etc gathers work via inx instead of directly
161+
, _wkstoreTable :: !(IntMap.IntMap (Work cnstr)) -- ^ all the work ever entered. FIXME: do GC
170162
, _wkstoreNextFreeWorkInx :: {-# UNPACK #-} !WorkTime -- ^ Next free work/constraint identification, used by solving to identify whether a rule has been used for a constraint.
171-
, _wkstoreNextFreeListInx :: {-# UNPACK #-} !WorkTime -- ^ Next free work/constraint identification, used by solving to identify whether a rule has been used for a constraint.
172163
}
173164
deriving (Typeable)
174165

175166
emptyWorkStore :: TT.TTCtxt (TT.TrTrKey cnstr) => WorkStore cnstr
176-
emptyWorkStore = WorkStore TT.empty IntMap.empty initWorkTime (-1)
167+
emptyWorkStore = WorkStore TT.empty IntMap.empty initWorkTime
177168

178169
data WorkQueue
179170
= WorkQueue
@@ -257,7 +248,7 @@ data CHRGlobState cnstr guard bprio prio subst env m
257248
{ _chrgstStore :: !(CHRStore cnstr guard bprio prio) -- ^ Actual database of rules, to be searched
258249
, _chrgstNextFreeRuleInx :: {-# UNPACK #-} !CHRInx -- ^ Next free rule identification, used by solving to identify whether a rule has been used for a constraint.
259250
-- The numbering is applied to constraints inside a rule which can be matched.
260-
, _chrgstWorkStore :: !(WorkStore cnstr) -- ^ Actual database of solvable constraints
251+
-- , _chrgstWorkStore :: !(WorkStore cnstr) -- ^ Actual database of solvable constraints
261252
-- , _chrgstNextFreeWorkInx :: {-# UNPACK #-} !WorkTime -- ^ Next free work/constraint identification, used by solving to identify whether a rule has been used for a constraint.
262253
, _chrgstScheduleQueue :: !(Que.MinPQueue (CHRPrioEvaluatableVal bprio) (CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m (SolverResult subst)))
263254
, _chrgstTrace :: !(SolveTrace' cnstr (StoredCHR cnstr guard bprio prio) subst)
@@ -267,7 +258,7 @@ data CHRGlobState cnstr guard bprio prio subst env m
267258
deriving (Typeable)
268259

269260
emptyCHRGlobState :: TT.TTCtxt (TT.TrTrKey c) => CHRGlobState c g b p s e m
270-
emptyCHRGlobState = CHRGlobState emptyCHRStore 0 emptyWorkStore Que.empty emptySolveTrace 0 emptyVarToNmMp
261+
emptyCHRGlobState = CHRGlobState emptyCHRStore 0 Que.empty emptySolveTrace 0 emptyVarToNmMp
271262

272263
-- | Backtrackable state
273264
data CHRBackState cnstr bprio subst env
@@ -277,6 +268,7 @@ data CHRBackState cnstr bprio subst env
277268
, _chrbstRuleWorkQueue :: !WorkQueue -- ^ work queue for rule matching
278269
, _chrbstSolveQueue :: !WorkQueue -- ^ solve queue, constraints which are not solved by rule matching but with some domain specific solver, yielding variable subst constributing to backtrackable bindings
279270
, _chrbstResidualQueue :: [WorkInx] -- ^ residual queue, constraints which are residual, no need to solve, etc
271+
, _chrbstWorkStore :: !(WorkStore cnstr) -- ^ Actual database of solvable constraints
280272

281273
, _chrbstMatchedCombis :: !(Set.Set MatchedCombi) -- ^ all combis of chr + work which were reduced, to prevent this from happening a second time (when propagating)
282274

@@ -288,8 +280,8 @@ data CHRBackState cnstr bprio subst env
288280
}
289281
deriving (Typeable)
290282

291-
emptyCHRBackState :: (CHREmptySubstitution s, Bounded (CHRPrioEvaluatableVal bp)) => CHRBackState c bp s e
292-
emptyCHRBackState = CHRBackState minBound emptyWorkQueue emptyWorkQueue [] Set.empty 0 chrEmptySubst Map.empty []
283+
emptyCHRBackState :: (TT.TTCtxt (TT.TrTrKey c), CHREmptySubstitution s, Bounded (CHRPrioEvaluatableVal bp)) => CHRBackState c bp s e
284+
emptyCHRBackState = CHRBackState minBound emptyWorkQueue emptyWorkQueue [] emptyWorkStore Set.empty 0 chrEmptySubst Map.empty []
293285

294286
-- | Monad for CHR, taking from 'LogicStateT' the state and backtracking behavior
295287
type CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m
@@ -349,7 +341,6 @@ class ( IsCHRConstraint env c s
349341
mkLabel ''WaitForVar
350342
mkLabel ''StoredCHR
351343
mkLabel ''CHRStore
352-
mkLabel ''WorkOrFreeList
353344
mkLabel ''WorkStore
354345
mkLabel ''WorkQueue
355346
mkLabel ''CHRGlobState
@@ -496,13 +487,13 @@ addConstraintAsWork
496487
addConstraintAsWork c = do
497488
let via = cnstrSolvesVia c
498489
addw i w = do
499-
fstl ^* chrgstWorkStore ^* wkstoreTable =$: IntMap.insert i (WorkWork w)
490+
sndl ^* chrbstWorkStore ^* wkstoreTable =$: IntMap.insert i w
500491
return (via,i)
501492
i <- fresh
502493
w <- case via of
503494
-- a plain rule is added to the work store
504495
ConstraintSolvesVia_Rule -> do
505-
fstl ^* chrgstWorkStore ^* wkstoreTrie =$: TT.insertByKeyWith (++) k [i]
496+
sndl ^* chrbstWorkStore ^* wkstoreTrie =$: TT.insertByKeyWith (++) k [i]
506497
addToWorkQueue i
507498
return $ Work k c i
508499
where k = TT.toTreeTrieKey c -- chrToKey c -- chrToWorkKey c
@@ -526,7 +517,7 @@ addConstraintAsWork c = do
526517
slvSucces
527518
-}
528519
where
529-
fresh = modifyAndGet (fstl ^* chrgstWorkStore ^* wkstoreNextFreeWorkInx) $ \i -> (i, i + 1)
520+
fresh = modifyAndGet (sndl ^* chrbstWorkStore ^* wkstoreNextFreeWorkInx) $ \i -> (i, i + 1)
530521

531522
-------------------------------------------------------------------------------------------
532523
--- Solver combinators
@@ -589,16 +580,9 @@ slvScheduleRun = slvSplitFromSchedule >>= maybe mzero snd
589580
-------------------------------------------------------------------------------------------
590581

591582
lkupWork :: MonoBacktrackPrio c g bp p s e m => WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
592-
lkupWork i = fmap (_worfWork . IntMap.findWithDefault (panic "MBP.wkstoreTable.lookup") i) $ getl $ fstl ^* chrgstWorkStore ^* wkstoreTable
583+
lkupWork i = fmap (IntMap.findWithDefault (panic "MBP.wkstoreTable.lookup") i) $ getl $ sndl ^* chrbstWorkStore ^* wkstoreTable
593584
{-# INLINE lkupWork #-}
594585

595-
addWorkToFreeList :: MonoBacktrackPrio c g bp p s e m => WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m ()
596-
addWorkToFreeList i = (fstl ^* chrgstWorkStore) =$: \st ->
597-
st { _wkstoreTable = IntMap.insert i (WorkFreeList $ _wkstoreNextFreeListInx st) $ _wkstoreTable st
598-
, _wkstoreNextFreeListInx = i
599-
}
600-
{-# INLINE addWorkToFreeList #-}
601-
602586
lkupChr :: MonoBacktrackPrio c g bp p s e m => CHRInx -> CHRMonoBacktrackPrioT c g bp p s e m (StoredCHR c g bp p)
603587
lkupChr i = fmap (IntMap.findWithDefault (panic "MBP.chrSolve.chrstoreTable.lookup") i) $ getl $ fstl ^* chrgstStore ^* chrstoreTable
604588
{-# INLINE lkupChr #-}
@@ -874,7 +858,7 @@ chrSolve opts env = slv
874858
-- work2 <- lkupWork workInx
875859

876860
-- find all matching chrs for the work
877-
foundChrInxs <- slvLookup (workKey work ) (chrgstStore ^* chrstoreTrie )
861+
foundChrInxs <- slvLookup (workKey work ) (fstl ^* chrgstStore ^* chrstoreTrie )
878862
-- foundChrInxs2 <- slvLookup2 (workKey work2) (chrgstStore ^* chrstoreTrie2)
879863
-- remove duplicates, regroup
880864
let foundChrGroupedInxs = Map.unionsWith Set.union $ map (\(CHRConstraintInx i j) -> Map.singleton i (Set.singleton j)) foundChrInxs
@@ -1035,10 +1019,10 @@ slvLookup
10351019
:: ( MonoBacktrackPrio c g bp p s e m
10361020
, Ord (TT.TrTrKey c)
10371021
) => CHRKey c -- ^ work key
1038-
-> Lens (CHRGlobState c g bp p s e m) (TT.TreeTrie (TT.TrTrKey c) [x])
1022+
-> Lens (CHRGlobState c g bp p s e m, CHRBackState c bp s e) (TT.TreeTrie (TT.TrTrKey c) [x])
10391023
-> CHRMonoBacktrackPrioT c g bp p s e m [x]
10401024
slvLookup key t =
1041-
(getl $ fstl ^* t) >>= \t -> do
1025+
(getl t) >>= \t -> do
10421026
{-
10431027
let lkup how = concat $ TreeTrie.lookupResultToList $ TreeTrie.lookupPartialByKey how key t
10441028
return $ Set.toList $ Set.fromList $ lkup TTL_WildInTrie ++ lkup TTL_WildInKey
@@ -1078,8 +1062,10 @@ slvCandidate waitingWk alreadyMatchedCombis wi (StoredCHR {_storedHeadKeys = ks,
10781062
-- each match expressed as the list of constraints (in the form of Work + Key) found in the workList wlTrie, thus giving all combis with constraints as part of a CHR,
10791063
-- partititioned on before or after last query time (to avoid work duplication later)
10801064
slvCandidate
1081-
:: ( MonoBacktrackPrio c g bp p s e m
1065+
:: forall c g bp p s e m
1066+
. ( MonoBacktrackPrio c g bp p s e m
10821067
-- , Ord (TTKey c), PP (TTKey c)
1068+
-- , ExtrValVarKey (VarLookupVal s) ~ VarLookupKey s
10831069
) => WorkInxSet -- ^ active in queue
10841070
-> Set.Set MatchedCombi -- ^ already matched combis
10851071
-> WorkInx -- ^ work inx
@@ -1096,7 +1082,8 @@ slvCandidate waitingWk alreadyMatchedCombis wi (StoredCHR {_storedHeadKeys = ks,
10961082
&& Set.notMember (MatchedCombi ci wi) alreadyMatchedCombis)
10971083
$ combineToDistinguishedEltsBy (==) $ ws1 ++ [[wi]] ++ ws2
10981084
where
1099-
lkup k = slvLookup k (chrgstWorkStore ^* wkstoreTrie)
1085+
-- lkup :: CHRKey c -> CHRMonoBacktrackPrioT c g bp p s e m [WorkInx]
1086+
lkup k = slvLookup k (sndl ^* chrbstWorkStore ^* wkstoreTrie)
11001087
{-# INLINE slvCandidate #-}
11011088

11021089
-- | Match the stored CHR with a set of possible constraints, giving a substitution on success

‎chr-lang/term/queens.chr‎

Lines changed: 8 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -2,17 +2,14 @@
22
-- Higher queen problems are very slow, can be used for optimizing the solver
33

44
{- Performance (MacBook (12", Early 2016), 1,2 GHz Intel Core m5, 8 GB 1867 MHz LPDDR3):
5-
Queens 4 (2 solutions)
6-
--------
7-
real 0m0.589s
8-
user 0m0.533s
9-
sys 0m0.038s
105

11-
Queens 5 (10 solutions)
6+
Queens 6 (4 solutions)
127
--------
13-
real 0m32.401s
14-
user 0m31.368s
15-
sys 0m0.604s
8+
---------------- DONE (28.498958s / 788842 = 0.000036127587s) term/queens.chr ----------------
9+
10+
real 0m28.520s
11+
user 0m28.118s
12+
sys 0m0.273s
1613
-}
1714

1815
{-
@@ -22,16 +19,16 @@ row @ Row r <=> Queen r 1 \/ Queen r 2 \/ Queen r 3 \/ Queen r 4.
2219
-}
2320

2421
{-
25-
-}
2622
-- 5 Queens problem
2723
queens @ Queens <=> Row 1, Row 2, Row 3, Row 4, Row 5.
2824
row @ Row r <=> Queen r 1 \/ Queen r 2 \/ Queen r 3 \/ Queen r 4 \/ Queen r 5.
25+
-}
2926

3027
{-
28+
-}
3129
-- 6 Queens problem
3230
queens @ Queens <=> Row 1, Row 2, Row 3, Row 4, Row 5, Row 6.
3331
row @ Row r <=> Queen r 1 \/ Queen r 2 \/ Queen r 3 \/ Queen r 4 \/ Queen r 5 \/ Queen r 6.
34-
-}
3532

3633
{-
3734
-- 8 Queens problem

0 commit comments

Comments
 (0)