@@ -1546,6 +1546,67 @@ public MaxUsedBddNodesStats getMaxUsedBddNodesStats() {
1546
1546
return maxusedbddnodesstats ;
1547
1547
}
1548
1548
1549
+ /**
1550
+ * Stores statistics about the maximum memory usage. The data is obtained through best effort, and may not be
1551
+ * entirely accurate.
1552
+ */
1553
+ public static class MaxMemoryStats {
1554
+ protected boolean enabled = false ;
1555
+
1556
+ protected long maxMemoryBytes ;
1557
+
1558
+ protected MaxMemoryStats () {
1559
+ }
1560
+
1561
+ void copyFrom (MaxMemoryStats that ) {
1562
+ this .maxMemoryBytes = that .maxMemoryBytes ;
1563
+ }
1564
+
1565
+ public void enableMeasurements () {
1566
+ enabled = true ;
1567
+ }
1568
+
1569
+ public void disableMeasurements () {
1570
+ enabled = false ;
1571
+ }
1572
+
1573
+ public void resetMeasurements () {
1574
+ maxMemoryBytes = 0 ;
1575
+ }
1576
+
1577
+ public void newMeasurement () {
1578
+ long newMemoryBytes = Runtime .getRuntime ().totalMemory () - Runtime .getRuntime ().freeMemory ();
1579
+ maxMemoryBytes = Math .max (newMemoryBytes , maxMemoryBytes );
1580
+ }
1581
+
1582
+ public long getMaxMemoryBytes () {
1583
+ return maxMemoryBytes ;
1584
+ }
1585
+
1586
+ @ Override
1587
+ public String toString () {
1588
+ StringBuilder sb = new StringBuilder ();
1589
+ sb .append ("Max memory: " );
1590
+ sb .append (maxMemoryBytes );
1591
+ sb .append (" bytes" );
1592
+ return sb .toString ();
1593
+ }
1594
+ }
1595
+
1596
+ /**
1597
+ * Singleton object for maximum memory usage statistics.
1598
+ */
1599
+ protected MaxMemoryStats maxmemorystats = new MaxMemoryStats ();
1600
+
1601
+ /**
1602
+ * Return the current maximum memory usage statistics for this BDD factory.
1603
+ *
1604
+ * @return maximum memory usage statistics
1605
+ */
1606
+ public MaxMemoryStats getMaxMemoryStats () {
1607
+ return maxmemorystats ;
1608
+ }
1609
+
1549
1610
// TODO: bdd_sizeprobe_hook
1550
1611
// TODO: bdd_reorder_probe
1551
1612
@@ -2098,6 +2159,17 @@ public static interface MaxUsedBddNodesStatsCallback {
2098
2159
public void maxUsedBddNodes (MaxUsedBddNodesStats stats );
2099
2160
}
2100
2161
2162
+ /** Maximum memory usage statistics callback. */
2163
+ @ FunctionalInterface
2164
+ public static interface MaxMemoryStatsCallback {
2165
+ /**
2166
+ * Maximum memory usage statistics callback.
2167
+ *
2168
+ * @param stats The statistics.
2169
+ */
2170
+ public void maxMemory (MaxMemoryStats stats );
2171
+ }
2172
+
2101
2173
/** Continuously BDD nodes usage and BDD operations statistics callback. */
2102
2174
@ FunctionalInterface
2103
2175
public static interface ContinuousStatsCallback {
@@ -2124,12 +2196,12 @@ public static interface ContinuousStatsCallback {
2124
2196
/** The registered operator cache statistics callbacks, or {@code null} if none registered. */
2125
2197
protected List <CacheStatsCallback > cacheCallbacks = null ;
2126
2198
2127
- /**
2128
- * The registered maximum BDD nodes usage statistics callback statistics callbacks, or {@code null} if none
2129
- * registered.
2130
- */
2199
+ /** The registered maximum BDD nodes usage statistics callbacks, or {@code null} if none registered. */
2131
2200
protected List <MaxUsedBddNodesStatsCallback > maxUsedBddNodesCallbacks = null ;
2132
2201
2202
+ /** The registered maximum memory usage statistics callbacks, or {@code null} if none registered. */
2203
+ protected List <MaxMemoryStatsCallback > maxMemoryCallbacks = null ;
2204
+
2133
2205
/**
2134
2206
* The registered continuously BDD nodes usage and BDD operations statistics callbacks, or {@code null} if none
2135
2207
* registered.
@@ -2196,6 +2268,18 @@ public void registerMaxUsedBddNodesStatsCallback(MaxUsedBddNodesStatsCallback ca
2196
2268
maxUsedBddNodesCallbacks .add (callback );
2197
2269
}
2198
2270
2271
+ /**
2272
+ * Register a maximum memory usage statistics callback.
2273
+ *
2274
+ * @param callback The callback to register.
2275
+ */
2276
+ public void registerMaxMemoryStatsCallback (MaxMemoryStatsCallback callback ) {
2277
+ if (maxMemoryCallbacks == null ) {
2278
+ maxMemoryCallbacks = new LinkedList <>();
2279
+ }
2280
+ maxMemoryCallbacks .add (callback );
2281
+ }
2282
+
2199
2283
/**
2200
2284
* Register a continuously BDD nodes usage and BDD operations statistics callback.
2201
2285
*
@@ -2313,6 +2397,27 @@ public void unregisterMaxUsedBddNodesStatsCallback(MaxUsedBddNodesStatsCallback
2313
2397
throw new IllegalArgumentException ();
2314
2398
}
2315
2399
2400
+ /**
2401
+ * Unregister a maximum memory usage statistics callback.
2402
+ *
2403
+ * @param callback The callback to unregister.
2404
+ * @throws IllegalArgumentException If callback is not registered.
2405
+ */
2406
+ public void unregisterMaxMemoryStatsCallback (MaxMemoryStatsCallback callback ) {
2407
+ if (maxMemoryCallbacks != null ) {
2408
+ for (Iterator <MaxMemoryStatsCallback > iter = maxMemoryCallbacks .iterator (); iter .hasNext ();) {
2409
+ if (iter .next () == callback ) {
2410
+ iter .remove ();
2411
+ if (maxMemoryCallbacks .isEmpty ()) {
2412
+ maxMemoryCallbacks = null ;
2413
+ }
2414
+ return ;
2415
+ }
2416
+ }
2417
+ }
2418
+ throw new IllegalArgumentException ();
2419
+ }
2420
+
2316
2421
/**
2317
2422
* Unregister a continuously BDD nodes usage and BDD operations statistics callback.
2318
2423
*
@@ -2379,6 +2484,15 @@ public boolean hasMaxUsedBddNodesStatsCallback() {
2379
2484
return maxUsedBddNodesCallbacks != null ;
2380
2485
}
2381
2486
2487
+ /**
2488
+ * Returns whether this BDD factory has a registered maximum memory usage statistics callback.
2489
+ *
2490
+ * @return {@code true} if such a callback is registered, {@code false} otherwise.
2491
+ */
2492
+ public boolean hasMaxMemoryStatsCallback () {
2493
+ return maxMemoryCallbacks != null ;
2494
+ }
2495
+
2382
2496
/**
2383
2497
* Returns whether this BDD factory has a registered continuously BDD nodes usage and BDD operations statistics
2384
2498
* callback.
@@ -2447,6 +2561,15 @@ public void invokeMaxUsedBddNodesStatsCallbacks() {
2447
2561
}
2448
2562
}
2449
2563
2564
+ /** Invoke all registered maximum memory usage statistics callbacks. */
2565
+ public void invokeMaxMemoryStatsCallbacks () {
2566
+ if (maxMemoryCallbacks != null ) {
2567
+ for (MaxMemoryStatsCallback callback : maxMemoryCallbacks ) {
2568
+ callback .maxMemory (maxmemorystats );
2569
+ }
2570
+ }
2571
+ }
2572
+
2450
2573
/**
2451
2574
* Invoke all registered continuously BDD nodes usage and BDD operations statistics callbacks.
2452
2575
*
@@ -2529,6 +2652,15 @@ public static void defaultMaxUsedBddNodesStatsCallback(MaxUsedBddNodesStats stat
2529
2652
System .out .println (stats .toString ());
2530
2653
}
2531
2654
2655
+ /**
2656
+ * Default maximum memory usage statistics callback.
2657
+ *
2658
+ * @param stats The statistics.
2659
+ */
2660
+ public static void defaultMaxMemoryStatsCallback (MaxMemoryStats stats ) {
2661
+ System .out .println (stats .toString ());
2662
+ }
2663
+
2532
2664
/**
2533
2665
* Default continuously BDD nodes usage and BDD operations statistics callback.
2534
2666
*
0 commit comments