Documentation

This class provides an API for starting and shutting down connections to various different solvers that support online interaction modes.

Simple data-type encapsulating some implementation of an online solver.

A live connection to a running solver process.

This data structure should be used in a single-threaded manner or with external synchronization to ensure that only a single thread has access at a time. Unsynchronized multithreaded use will lead to race conditions and very strange results.

Standard input stream for the solver process.

The solver's stdout, for easier parsing of responses.

The amount of time that a solver is allowed to attempt to satisfy any particular goal.

The timeout value may be retrieved with getGoalTimeoutInMilliSeconds or getGoalTimeoutInSeconds.

Get the SolverGoalTimeout raw numeric value in units of seconds.

If the solver cannot voluntarily limit itself to the requested timeout period, this runs a local async process with a slightly longer time period that will forcibly terminate the solver process if it expires while the solver process is still running.

Note that this will require re-establishment of the solver process and any associated context for any subsequent solver goal evaluation.

This datatype describes how a solver will behave following an error.

An impolite way to shut down a solver. Prefer to use shutdownSolverProcess, unless the solver is unresponsive or in some unrecoverable error state.

Push a new solver assumption frame.

Pop a previous solver assumption frame.

Pop a previous solver assumption frame, but allow this to fail if the solver has exited.

Pop all assumption frames and remove all top-level asserts from the global scope. Forget all declarations except those in scope at the top level.

Perform an action in the scope of a solver assumption frame.

Perform an action in the scope of a solver assumption frame, where the given bound variables are considered free within that frame.

Open a second solver assumption frame. For abduction, we want the final assertion to be a in a new frame, so that it can be closed before asking for abducts. The following two commands allow frame 2 to be pushed and popped independently of other commands

Close a second solver assumption frame.

Send a check command to the solver, and get the SatResult without asking a model.

Send a check command to the solver and get the model in the case of a SAT result.

Following a successful check-sat command, build a ground evaluation function that will evaluate terms in the context of the current model.

After an unsatisfiable check-sat command, compute a set of the named assertions that (together with all the unnamed assertions) form an unsatisfiable core. Note: the returned unsatisfiable core might not be minimal.

get-abuct nm t queries the solver for the first abduct, which is returned as an SMT function definition named nm. The remaining abducts are obtained from the solver by successive invocations of the get-abduct-next command, which return SMT functions bound to the same nm as the first. The name nm is bound within the current assertion frame. Note that this is an unstable API; we expect that the return type will change to a parsed expression in the future

After an unsatisfiable check-with-assumptions command, compute a set of the supplied assumptions that (together with previous assertions) form an unsatisfiable core. Note: the returned unsatisfiable set might not be minimal. The boolean value returned along with the name indicates if the assumption was negated or not: True indidcates a positive atom, and False represents a negated atom.

Get the sat result from a previous SAT command.

Check if the given formula is satisfiable in the current solver state, without requesting a model. This is done in a fresh frame, which is exited after the check call.

Check if the formula is satisifiable in the current solver state. This is done in a fresh frame, which is exited after the continuation complets. The evaluation function can be used to query the model. The model is valid only in the given continuation.