Remote¶

Using an intrepid-server from python; see Running as a service.

remote ¶

This module runs intrepyd on an intrepid-server, the REST service of intrepyd (https://github.com/formalmethods/intrepid-server): after use_remote(), every Context is a RemoteContext, which has the same methods as a Context, and turns each of them into the equivalent REST call. A script written for intrepyd runs unchanged against the service:

import intrepyd as ip

ip.use_remote('http://127.0.0.1:8000')
ctx = ip.Context()                      # a context on the service
a = ctx.mk_input('a', ctx.mk_boolean_type())
...

use_local() goes back to local contexts. A RemoteContext can also be made explicitly, with RemoteContext(url), whatever the mode.

The nets of a remote context are Net objects, named after the name the service gives them, which is also the one in ctx.net2name; its types are the names of the types of the REST API ('bool', 'int8', ...). Engines, traces and simulators are objects with the methods of the local ones, and trace values are the same strings.

RemoteContext ¶

RemoteContext(url=None, transport=None)

A context on an intrepid-server, with the methods of Context

Args: url (str): the service, e.g. 'http://127.0.0.1:8000'; by default the one of use_remote() transport (callable): sends the REST calls instead of HTTP, as transport(method, path, params, body) -> (status, answer)

undef `property` ¶

undef

The undef net, as Context.undef

true `property` ¶

true

The net true, as Context.true

false `property` ¶

false

The net false, as Context.false

push_namespace ¶

push_namespace(name)

Pushes a namespace

pop_namespace ¶

pop_namespace()

Pops a namespace

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_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_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=ENGINES, max_depth=None)

Creates a portfolio (see intrepyd.portfolio), which the service runs

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

RemoteError ¶

RemoteError(method, path, status, message)

Bases: Exception

An error answered by the service

use_remote ¶

use_remote(address)

Makes every Context created from now on a RemoteContext on the service at address, e.g. 'http://127.0.0.1:8000' or '127.0.0.1:8000'

use_local ¶

use_local()

Makes every Context created from now on a local one again