Context¶

Context ¶

Context()

An intrepyd context

After intrepyd.use_remote(url), Context() makes a RemoteContext on the service at url instead (see intrepyd.remote)

push_namespace ¶

push_namespace(name)

Pushes a namespace

pop_namespace ¶

pop_namespace()

Pops a namespace

mk_boolean_type ¶

mk_boolean_type()

Creates boolean type

mk_int8_type ¶

mk_int8_type()

Creates int8 type

mk_int16_type ¶

mk_int16_type()

Creates int16 type

mk_int32_type ¶

mk_int32_type()

Creates int32 type

mk_int64_type ¶

mk_int64_type()

Creates int64 type

mk_uint8_type ¶

mk_uint8_type()

Creates uint8 type

mk_uint16_type ¶

mk_uint16_type()

Creates uint16 type

mk_uint32_type ¶

mk_uint32_type()

Creates uint32 type

mk_uint64_type ¶

mk_uint64_type()

Creates uint64 type

mk_real_type ¶

mk_real_type()

Creates real type

mk_float16_type ¶

mk_float16_type()

Creates float16 type

mk_float32_type ¶

mk_float32_type()

Creates float32 type

mk_float64_type ¶

mk_float64_type()

Creates float64 type

mk_int_type ¶

mk_int_type()

Creates infinite precision int type

mk_undef ¶

mk_undef()

Creates undef net

mk_true ¶

mk_true(name=None)

Creates net true

mk_false ¶

mk_false(name=None)

Creates net false

mk_number ¶

mk_number(value, type_, name=None)

Creates a number from a value and a type

mk_not ¶

mk_not(x, name=None)

Creates the net !x

mk_and ¶

mk_and(x, y, name=None)

Creates the net x && y

mk_or ¶

mk_or(x, y, name=None)

Creates the net x || y

mk_xor ¶

mk_xor(x, y, name=None)

Creates the net x ^ y

mk_implies ¶

mk_implies(x, y, name=None)

Creates the net x -> y

mk_iff ¶

mk_iff(x, y, name=None)

Creates the net x <-> y

mk_eq ¶

mk_eq(x, y, name=None)

Creates the predicate x = y

mk_leq ¶

mk_leq(x, y, name=None)

Creates the predicate x <= y

mk_lt ¶

mk_lt(x, y, name=None)

Creates the predicate x < y

mk_geq ¶

mk_geq(x, y, name=None)

Creates the predicate x >= y

mk_gt ¶

mk_gt(x, y, name=None)

Creates the predicate x > y

mk_neq ¶

mk_neq(x, y, name=None)

Creates the predicate x != y

mk_add ¶

mk_add(x, y, name=None)

Creates the term x + y

mk_mul ¶

mk_mul(x, y, name=None)

Creates the term x * y

mk_div ¶

mk_div(x, y, name=None)

Creates the term x / y

mk_mod ¶

mk_mod(x, y, name=None)

Creates the term x % y

mk_sub ¶

mk_sub(x, y, name=None)

Creates the term x - y

mk_minus ¶

mk_minus(x, name=None)

Creates the term -x

mk_ite ¶

mk_ite(i, t, e, name=None)

Creates the term ite(i, t, e)

mk_input ¶

mk_input(name, type_)

Creates a primary input

mk_output ¶

mk_output(x, name=None)

Tag a net as output

mk_latch ¶

mk_latch(name, type_)

Creates a latch

set_latch_init_next ¶

set_latch_init_next(latch, init, nex)

Sets the initial and next value of a latch

mk_substitute ¶

mk_substitute(term, new_term, old_term)

Replaces the occurrences of oldTerm, that are found in term, with newTerm

mk_assumption ¶

mk_assumption(net)

Creates an assumption @deprecated

push_assumption ¶

push_assumption(net)

Pushes an assumption

pop_assumption ¶

pop_assumption()

Pops an assumption

mk_cast_to_int8 ¶

mk_cast_to_int8(net, name=None)

Casts a net to an int8

mk_cast_to_int16 ¶

mk_cast_to_int16(net, name=None)

Casts a net to an int16

mk_cast_to_int32 ¶

mk_cast_to_int32(net, name=None)

Casts a net to an int32

mk_cast_to_int64 ¶

mk_cast_to_int64(net, name=None)

Casts a net to an int64

mk_cast_to_uint8 ¶

mk_cast_to_uint8(net, name=None)

Casts a net to an uint8

mk_cast_to_uint16 ¶

mk_cast_to_uint16(net, name=None)

Casts a net to an uint16

mk_cast_to_uint32 ¶

mk_cast_to_uint32(net, name=None)

Casts a net to an uint32

mk_cast_to_uint64 ¶

mk_cast_to_uint64(net, name=None)

Casts a net to an uint64

mk_bmc ¶

mk_bmc()

Creates a BMC engine

mk_optimizing_bmc ¶

mk_optimizing_bmc()

Creates an optimizing BMC engine

mk_backward_reach ¶

mk_backward_reach()

Creates a backward reachability engine

mk_pdr ¶

mk_pdr()

Creates an IC3/PDR engine

mk_portfolio ¶

mk_portfolio(engines=None, max_depth=None, certificates=False)

Creates a portfolio: an engine that runs several engines in parallel, each in a process of its own, and stops them all at the first conclusive answer (see intrepyd.portfolio). engines defaults to all of portfolio.ENGINES; with certificates, an UNREACHABLE answer comes with a proof certificate.

mk_simulator ¶

mk_simulator()

Creates a simulator

mk_trace ¶

mk_trace()

Creates an empty trace

to_string ¶

to_string(net)

Returns the given net as a string, as given from the underlying smt-solver.

get_default_value ¶

get_default_value(type_)

Returns a default value for the given type