Portfolio¶
Portfolio ¶
Bases: Engine
Runs several engines in parallel, and answers with the first conclusive answer of any of them
The _*_impl methods of Engine wrap the C API of one engine: a portfolio has none, and implements the public methods instead.
Args: context (Context): the context of the circuit engines (iterable): which of ENGINES to run, all by default max_depth (int=None): the deepest depth that bmc and kind try; None for no limit certificates (bool=False): whether an UNREACHABLE answer comes with a proof certificate (get_last_certificate)
reach_targets ¶
Runs the engines until one of them answers REACHABLE or UNREACHABLE, and returns that answer; returns UNKNOWN if none of them does, or none does within timeout seconds
get_last_engine ¶
Returns the name of the engine that gave the last answer, or None if the last answer was UNKNOWN
get_last_errors ¶
Returns the errors of the engines that failed in the last reach_targets(), as a dictionary engine -> message