Zee3.Solver (zee3 v0.6.0)

Copy Markdown

API to send commands to the solver.

The Zee3.program/2 macro can do anything the funcions in this module can do, but sometimes, when we're using the solver interactively and performing complex algorithms outside the solver, using this lower level functions is clearer.

Summary

Functions

assert(pid, constraint)
check_sat(pid, opts \\ [])

Check the Z3 program for satisfiability.

check_sat!(pid, opts \\ [])

Check the Z3 program for satisfiability. Raises on error.

check_sat_and_get_model(pid, opts \\ [])

Check the Z3 program for satisfiability and returns the model.

check_sat_and_get_model!(pid, opts \\ [])

Check the Z3 program for satisfiability and returns the model. Raises on error.

check_sat_assuming(pid, assumptions, opts \\ [])

Check the Z3 program for satisfiability assuming a number of assumptions.

check_sat_assuming!(pid, assumptions, opts \\ [])

Check the Z3 program for satisfiability assuming a number of assumptions.

child_spec(init_arg)

Returns a specification to start this module under a supervisor.

datalog_get_tuples(state, solutions)
declare_const(pid, name, type)

Declare an uninterpreted constant.

declare_datatypes(pid, smt_declaration, constructor_atoms)

Declares a datatype in Z3 and registers its constructors with the Elixir atom registry.

declare_fun(pid, name, param_types, return_type)

Declare an uninterpreted function.

declare_rel(pid, name, param_types)

Declare a datalog relation.

declare_sort(pid, name)

Declare an uninterpreted sort.

declare_var(pid, name, type)

Declare a variable for use in datalog rules.

entity_id(pid, value)
eval_smt2_code(pid, input)

Send raw SMT-LIB2 text (given as iodata/0) to the solver. Constants and functions defined inside this text aren't available in the model.

parse_solution_into_rel_args(solution)
pop(pid)

Pops the current scope from the solver stack, discarding all assertions and variables declared since the last push.

push(pid)

Pushes a new scope onto the solver stack.

query(pid, name, opts \\ [])
query!(pid, name, opts \\ [])
raw_bit_vec32_from_integer(integer)
rule(pid, body)

Define a new datalog rule.

start_link(opts \\ [])

Start a Zee3 solver process.

stop(pid)

Functions

assert(pid, constraint)

check_sat(pid, opts \\ [])

Check the Z3 program for satisfiability.

check_sat!(pid, opts \\ [])

Check the Z3 program for satisfiability. Raises on error.

check_sat_and_get_model(pid, opts \\ [])

Check the Z3 program for satisfiability and returns the model.

check_sat_and_get_model!(pid, opts \\ [])

Check the Z3 program for satisfiability and returns the model. Raises on error.

check_sat_assuming(pid, assumptions, opts \\ [])

Check the Z3 program for satisfiability assuming a number of assumptions.

check_sat_assuming!(pid, assumptions, opts \\ [])

Check the Z3 program for satisfiability assuming a number of assumptions.

child_spec(init_arg)

Returns a specification to start this module under a supervisor.

See Supervisor.

datalog_get_tuples(state, solutions)

declare_const(pid, name, type)

Declare an uninterpreted constant.

declare_datatypes(pid, smt_declaration, constructor_atoms)

Declares a datatype in Z3 and registers its constructors with the Elixir atom registry.

declare_fun(pid, name, param_types, return_type)

Declare an uninterpreted function.

declare_rel(pid, name, param_types)

Declare a datalog relation.

declare_sort(pid, name)

Declare an uninterpreted sort.

declare_var(pid, name, type)

Declare a variable for use in datalog rules.

entity_id(pid, value)

eval_smt2_code(pid, input)

Send raw SMT-LIB2 text (given as iodata/0) to the solver. Constants and functions defined inside this text aren't available in the model.

If you need these values to be available, use the declare-const/2 and declare-fun/3 functions explicitly.

parse_solution_into_rel_args(solution)

pop(pid)

Pops the current scope from the solver stack, discarding all assertions and variables declared since the last push.

push(pid)

Pushes a new scope onto the solver stack.

query(pid, name, opts \\ [])

query!(pid, name, opts \\ [])

raw_bit_vec32_from_integer(integer)

rule(pid, body)

Define a new datalog rule.

start_link(opts \\ [])

Start a Zee3 solver process.

stop(pid)