Content-addressed store of claims already proved unsatisfiable. More...

#include <proof_cache.h>

Public Member Functions
	proof_cachet (const std::string &dir, const optionst &options, const std::string &build_identity)
bool	proved (const std::string &cone_key) const
	True iff a proof is stored for `cone_key`.
void	record (const std::string &cone_key) const
	Record `cone_key` as proved. Idempotent.
size_t	hits () const
size_t	misses () const

Detailed Description

Content-addressed store of claims already proved unsatisfiable.

A claim's key is the 128-bit digest of its sliced SSA cone (see fingerprint.h) combined with a fingerprint of everything else the verdict was contingent on: the ESBMC build, every option in effect, and the data model. An entry is the file named by that key; its presence is the proof.

Only UNSAT is stored. A cached SAT could not reproduce its counterexample, and a report must never show a trace that was not just produced.

Constructor & Destructor Documentation

◆ proof_cachet()

proof_cachet::proof_cachet	(	const std::string &	dir,
		const optionst &	options,
		const std::string &	build_identity )

Parameters

dir	cache directory, created if absent
options	every option in effect, folded into each key
build_identity	the ESBMC that is running, from proof_cache_build_identity

Member Function Documentation

◆ hits()

size_t proof_cachet::hits ( ) const

inline

◆ misses()

size_t proof_cachet::misses ( ) const

inline

◆ proved()

bool proof_cachet::proved ( const std::string & cone_key ) const

True iff a proof is stored for cone_key.

◆ record()

void proof_cachet::record ( const std::string & cone_key ) const

Record cone_key as proved. Idempotent.

The documentation for this class was generated from the following files:

src/util/ssa/proof_cache.h
src/util/ssa/proof_cache.cpp

Public Member Functions