Skip to main content
The System module provides platform-specific utilities for measuring CPU time and memory usage, setting resource limits, and handling system signals. These functions are essential for monitoring solver performance and implementing timeouts.

​
Time measurement

​
cpuTime

static inline double cpuTime(void)
Returns the CPU time consumed by the current process in seconds.
​
return
double
CPU time in seconds
Implementation varies by platform:
  • Windows/MinGW: Uses clock() with CLOCKS_PER_SEC
  • Unix/Linux/macOS: Uses getrusage(RUSAGE_SELF) for precise user time

​
Usage

#include "minisat/utils/System.h"

using namespace Minisat;

double start = cpuTime();
// ... perform computation
double elapsed = cpuTime() - start;
printf("Elapsed CPU time: %.2f seconds\n", elapsed);

​
Memory measurement

​
memUsed

double memUsed()
Returns the current memory usage of the process in megabytes.
​
return
double
Current memory usage in MB, or 0 if unsupported on this architecture
This function returns 0 on architectures where memory measurement is not implemented.

​
memUsedPeak

double memUsedPeak(bool strictlyPeak = false)
Returns the peak memory usage of the process in megabytes.
​
strictlyPeak
bool
default:"false"
If true, returns only the historical peak. If false, returns the maximum of current and peak usage.
​
return
double
Peak memory usage in MB, or 0 if unsupported on this architecture

​
Usage

double mem_current = memUsed();
double mem_peak = memUsedPeak();
printf("Memory: current=%.1f MB, peak=%.1f MB\n", mem_current, mem_peak);

​
Resource limits

​
limitMemory

void limitMemory(uint64_t max_mem_mb)
Sets a limit on the total memory usage of the process. When the limit is exceeded, the program will be terminated by the operating system.
​
max_mem_mb
uint64_t
required
Maximum memory limit in megabytes
The exact semantics of memory limiting vary by architecture and operating system. On some systems, this may set a soft limit that can be exceeded temporarily.

​
Usage

// Limit process to 2 GB of memory
limitMemory(2048);

​
limitTime

void limitTime(uint32_t max_cpu_time)
Sets a limit on the maximum CPU time the process can consume. When the limit is exceeded, the program receives a signal (typically SIGXCPU).
​
max_cpu_time
uint32_t
required
Maximum CPU time in seconds
The exact semantics vary by architecture. On Unix systems, this typically uses setrlimit(RLIMIT_CPU, ...) which sends SIGXCPU when exceeded.

​
Usage

// Limit CPU time to 5 minutes
limitTime(300);

​
Signal handling

​
sigTerm

void sigTerm(void handler(int))
Sets up handling for available termination signals (SIGINT, SIGTERM, etc.). Allows graceful shutdown when the process receives interrupt signals.
​
handler
void (*)(int)
required
Signal handler function that takes the signal number as parameter

​
Usage

#include "minisat/utils/System.h"
#include <signal.h>

using namespace Minisat;

volatile bool interrupted = false;

void SIGINT_handler(int signum) {
    interrupted = true;
    printf("\n*** INTERRUPTED ***\n");
}

int main() {
    sigTerm(SIGINT_handler);
    
    while (!interrupted) {
        // Main computation loop
        // Check interrupted flag periodically
    }
    
    return 0;
}
The signals handled may vary by platform. Typically includes:
  • SIGINT (Ctrl+C)
  • SIGTERM (termination request)
  • SIGXCPU (CPU time limit exceeded)

​
FPU precision control

​
setX86FPUPrecision

void setX86FPUPrecision()
Ensures that double-precision floating-point values are represented with the same precision in memory and CPU registers. This is important for consistent behavior across different compilations and platforms.
This function is primarily relevant for x86 architectures where the FPU may use extended precision (80-bit) internally. It sets the FPU control word to use 64-bit (double) precision.

​
Usage

int main() {
    setX86FPUPrecision();
    // ... rest of program
}
On Linux, this function uses _FPU_SETCW() from <fpu_control.h>. On other platforms, it may be a no-op if FPU control is not available or necessary.

​
Complete example

#include "minisat/utils/System.h"
#include <stdio.h>
#include <signal.h>

using namespace Minisat;

volatile bool interrupted = false;

void interrupt_handler(int) {
    interrupted = true;
}

int main() {
    // Set up FPU precision
    setX86FPUPrecision();
    
    // Set resource limits
    limitMemory(4096);  // 4 GB memory limit
    limitTime(3600);    // 1 hour CPU time limit
    
    // Set up signal handler
    sigTerm(interrupt_handler);
    
    // Start timing
    double start_time = cpuTime();
    double start_mem = memUsed();
    
    // Main computation
    while (!interrupted) {
        // ... solver loop
        
        // Monitor resources
        if (cpuTime() - start_time > 600.0) {
            printf("Timeout reached\n");
            break;
        }
    }
    
    // Report statistics
    printf("CPU time: %.2f s\n", cpuTime() - start_time);
    printf("Memory used: %.1f MB\n", memUsed());
    printf("Peak memory: %.1f MB\n", memUsedPeak());
    
    return 0;
}

​
Platform compatibility

​
cpuTime
cross-platform
Fully supported on Windows (MSVC, MinGW) and Unix-like systems (Linux, macOS, BSD)
​
memUsed / memUsedPeak
limited support
Returns 0 on unsupported architectures. Check implementation for your specific platform.
​
limitMemory / limitTime
platform-specific
Uses setrlimit() on Unix systems. Semantics vary by OS.
​
sigTerm
platform-specific
Available signals depend on the operating system
​
setX86FPUPrecision
x86 only
Only active on x86 Linux with fpu_control.h. No-op on other platforms.

Build docs developers (and LLMs) love

Get started for freeTalk to us