Engines¶

EngineResult ¶

Bases: Enum

Results from engine's reachability calls

Engine ¶

Engine(ctx)

Abstract intreface for an Engine

add_target ¶

add_target(net)

Adds a target to be solved

reach_targets ¶

reach_targets()

Tries to reach any of the previously added targets

get_last_reached_targets ¶

get_last_reached_targets()

Returns the list of targets that has been reached last

get_last_trace ¶

get_last_trace()

Returns the last produced trace

remove_last_reached_targets ¶

remove_last_reached_targets()

Removes all the reached targets from the last call from the engine

add_watch ¶

add_watch(net)

Track the value of net in future traces

set_produce_certificates ¶

set_produce_certificates()

Makes an UNREACHABLE answer come with a proof certificate, which get_last_certificate() returns: an SMT-LIB 2 script, each of whose check-sat must answer unsat, that any SMT solver can run to check the proof (z3 FILE, cvc5 FILE, ...). The library checks it first, with a solver of its own: a certificate that does not hold turns the answer into UNKNOWN. Needs intrepid 1.4 or newer.

get_last_certificate ¶

get_last_certificate()

Returns the proof certificate of the last answer, if it was UNREACHABLE and certificates were asked for (set_produce_certificates), as SMT-LIB 2 text; None otherwise

can_reach ¶

can_reach()

Tells if the engine can reach targets

can_prove ¶

can_prove()

Tells if the engine can prove targets to be unreachable

can_optimize ¶

can_optimize()

Tells if the engine can prove targets to be unreachable

Bmc ¶

Bmc(ctx)

Bases: Engine

A Bounded Model Checking engine

set_current_depth ¶

set_current_depth(depth)

Sets the current depth to use for BMC

set_use_induction ¶

set_use_induction()

Turn on induction

set_use_attack_path_axioms ¶

set_use_attack_path_axioms(source, target)

Tells bmc to apply internally axioms for source and target of an attack

set_allow_targets_at_any_depth ¶

set_allow_targets_at_any_depth()

Looks for counterexamples at any depth, not just the current

OptimizingBmc ¶

OptimizingBmc(ctx)

Bases: Bmc

An Optimizing Bounded Model Checking engine

BackwardReach ¶

BackwardReach(ctx)

Bases: Engine

A Backward Reachability Model Checking algorithm

Pdr ¶

Pdr(ctx)

Bases: Engine

An IC3/PDR engine, on top of z3's Spacer: it can prove targets unreachable by finding an inductive invariant, also when k-induction and backward reachability cannot; it works best on unbounded integers