#include <util/ssa/proof_cache.h>
#include <ac_config.h>
#include <fmt/format.h>
#include <util/config/config.h>
#include <util/message/message.h>
#include <util/ssa/fingerprint.h>
#include <boost/dll/runtime_symbol_info.hpp>
#include <cstring>
#include <filesystem>
#include <fstream>
#include <optional>
#include <set>
#include <sstream>
#include <thread>
#include <vector>
#include <unistd.h>

Include dependency graph for proof_cache.cpp:

Functions
std::string	proof_cache_inactive_reason (const optionst &options)
	Why a proof cache would not be consulted under `options`, or empty when it would be.
void	report_proof_cache_inactive (const std::string &why)
	Say, once per run, that a named cache directory will not be consulted.
bool	proof_cache_contradicted (bool was_hit, bool counterexample_found)
	True when the solver has just contradicted a proof the cache stood in for.
std::string	proof_cache_build_identity (const std::string &build_id)
	The ESBMC that is running, as far as it can be established: `build_id` alone when that names one build, otherwise it plus a digest of the executable.
std::string	proof_cache_context (const optionst &options, const std::string &build_identity)
	Digest of everything outside the cone that the verdict depends on.

Function Documentation

◆ proof_cache_build_identity()

std::string proof_cache_build_identity ( const std::string & build_id )

The ESBMC that is running, as far as it can be established: build_id alone when that names one build, otherwise it plus a digest of the executable.

Empty when neither is available – a key that cannot name the verifier must not be used to skip it.

◆ proof_cache_context()

std::string proof_cache_context	(	const optionst &	options,
		const std::string &	build_identity )

Digest of everything outside the cone that the verdict depends on.

Every option is folded in unabridged bar a short allowlist of ones that reach nothing but the report: a curated list of "options that matter" is the classic way a cache like this goes unsound.

◆ proof_cache_contradicted()

bool proof_cache_contradicted	(	bool	was_hit,
		bool	counterexample_found )

True when the solver has just contradicted a proof the cache stood in for.

Only a counterexample does: a vacuous discharge, a solver error and an SMT-LIB-only emission all mean the claim was not re-checked, not that the stored proof was wrong.

◆ proof_cache_inactive_reason()

std::string proof_cache_inactive_reason ( const optionst & options )

Why a proof cache would not be consulted under options, or empty when it would be.

Covers what the option set alone decides; a run adds the thread-interleaving exclusion on top.

◆ report_proof_cache_inactive()

void report_proof_cache_inactive ( const std::string & why )

Say, once per run, that a named cache directory will not be consulted.

A run that reuses nothing is otherwise indistinguishable from one whose cache is working.