ts_enginet Class Reference

BMC over a transition system, unrolled step by step in a single solver. More...

#include <ts_engines.h>

Public Member Functions
	ts_enginet (const transition_systemt &ts, const namespacet &ns, optionst &options, bool incremental=true)
	Without incremental, the solver is never asked to track assumptions; only solve_prefix and solve_bound may be used.
int	bmc (uint64_t max_k, bool push_pop)
	Exit codes follow do_bmc_strategy: 0 SUCCESSFUL or UNKNOWN, 1 FAILED, 6 solver error.
smt_resultt	solve_bound (unsigned k)
	One monolithic BMC query on a fresh engine: steps 0..k unrolled, the violation at step k asserted, a single check-sat.
smt_resultt	solve_prefix ()

Protected Member Functions
expr2tc	bad_literal (unsigned step) const
bool	check_prefix ()
	Returns false if the prefix itself violates a property.
void	assume_prefix ()
void	add_step (unsigned step)
void	close_step (unsigned step)
smt_resultt	solve_bad (unsigned step, bool push_pop)
void	report_counterexample (unsigned step)

Protected Attributes
const transition_systemt &	ts
const namespacet &	ns
std::unique_ptr< smt_convt >	solver

Detailed Description

BMC over a transition system, unrolled step by step in a single solver.

Each step's violation is queried through its own activation literal.

Constructor & Destructor Documentation

ts_enginet()

ts_enginet::ts_enginet	(	const transition_systemt &	ts,
		const namespacet &	ns,
		optionst &	options,
		bool	incremental = true )

Without incremental, the solver is never asked to track assumptions; only solve_prefix and solve_bound may be used.

Member Function Documentation

add_step()

void ts_enginet::add_step ( unsigned step )

protected

assume_prefix()

void ts_enginet::assume_prefix ( )

protected

bad_literal()

expr2tc ts_enginet::bad_literal ( unsigned step ) const

protected

bmc()

int ts_enginet::bmc	(	uint64_t	max_k,
		bool	push_pop )

Exit codes follow do_bmc_strategy: 0 SUCCESSFUL or UNKNOWN, 1 FAILED, 6 solver error.

check_prefix()

bool ts_enginet::check_prefix ( )

protected

Returns false if the prefix itself violates a property.

Assumptions before the loop only hold from here on: each prefix property already carries the ones that precede it.

close_step()

void ts_enginet::close_step ( unsigned step )

protected

report_counterexample()

void ts_enginet::report_counterexample ( unsigned step )

protected

solve_bad()

smt_resultt ts_enginet::solve_bad ( unsigned step, bool push_pop )

protected

solve_bound()

smt_resultt ts_enginet::solve_bound

(

unsigned

k

)

One monolithic BMC query on a fresh engine: steps 0..k unrolled, the violation at step k asserted, a single check-sat.

solve_prefix()

smt_resultt ts_enginet::solve_prefix

(

)

Member Data Documentation

ns

const namespacet& ts_enginet::ns

protected

solver

std::unique_ptr<smt_convt> ts_enginet::solver

protected

ts

const transition_systemt& ts_enginet::ts

protected

---

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

• src/transition-system/ts_engines.h
• src/transition-system/ts_engines.cpp