Crate z3 

Z3

Z3 is a theorem prover from Microsoft Research.

This library aims to provide an idiomatic Rust wrapper around Z3.

Basic Usage

The simplest way to use Z3 is to build a formula (also known as an Ast) and use Z3’s Solver to find solutions to it.

This example walks through the process of expressing a simple math problem in the language of SMT, asserting it into a Solver, and extracting answers from it. Z3 can encode much more varied and complex problems than this example shows (and some of these features are supported by the Rust bindings), but this covers the absolute basics.

Consider the following problem:

Three friends, named Alice, Bob, and Charlie, wish to divide 30 apples amongst themselves, subject to the following constraints:

• Everyone must get at least one apple.
• All apples must be accounted for.
• Alice must receive at least 5 apples.
• Bob must receive an even number of apples.
• Charlie must get at least as many apples as Bob.
• The number of apples Alice receives must be exactly 3 more than the number Charlie receives.

What are the possible distributions of apples they could make?

To express this in Z3, we define symbolic Int Asts representing the number of apples each friend has, and assert the constraints of the problem into a Solver. We can then query the Solver for a solution:

 // define Int values representing the number of apples each friend has
 let alice = Int::fresh_const("alice");
 let bob = Int::fresh_const("bob");
 let charlie = Int::fresh_const("charlie");
 // instantiate a Solver
 let solver = Solver::new();
 // encode the constraints of the problem as Bool-valued Asts
 // and assert them in the solver
 solver.assert((&alice + &bob + &charlie).eq(30));
 solver.assert(alice.ge(0));
 solver.assert(bob.ge(0));
 solver.assert(charlie.ge(0));
 solver.assert(alice.ge(5));
 solver.assert((&bob % 2).eq(0));
 solver.assert(charlie.ge(&bob));
 solver.assert(alice.eq(&charlie * 3));
 // iterate over the solutions to our variables
 for solution in solver
     .solutions([alice, bob, charlie], false)
     // we use take to ensure that this loop terminates in case there are very many solutions
     .take(100) {
     // extract concrete values for each modeled Int Ast
     let solution: Vec<u64> = solution.iter().map(Int::as_u64).map(Option::unwrap).collect();
     let alice = solution[0];
     let bob = solution[1];
     let charlie = solution[2];
     println!("alice: {alice}, bob: {bob}, charlie: {charlie}");
     // check that the concrete values match the constraints we gave the solver
     assert_eq!(alice + bob + charlie, 30);
     assert!(alice >= 5);
     assert_eq!(bob % 2, 0);
     assert!(charlie >= bob);
     assert_eq!(alice, charlie * 3);
 }

In this case, there are 2 solutions, and the above snippet gives the following output:

alice: 21, bob: 2, charlie: 7

alice: 18, bob: 6, charlie: 6

Re-exports

pub use datatype_builder::DatatypeAccessor;

Modules

ast

Abstract syntax tree (AST).

datatype_builder

Helpers for building custom datatype sorts. The main entry point is create_datatypes which returns a list of sorts(more than one for the case that you are defining a set of mutually recursive data types)

Structs

ApplyResult

Collection of subgoals resulting from applying of a tactic to a goal.

Config

Configuration used to initialize logical contexts.

Context

Manager of all other Z3 objects, global configuration options, etc.

ContextHandle

Handle that can be used to interrupt a computation from another thread.

DatatypeBuilder

Build a custom datatype sort.

DatatypeSort

A custom datatype sort.

DatatypeVariant

Inner variant for a custom datatype sort.

FuncDecl

Function declaration. Every constant and function have an associated declaration.

FuncEntry

Store the value of the interpretation of a function in a particular point. https://z3prover.github.io/api/html/classz3py_1_1_func_entry.html

FuncInterp

Stores the interpretation of a function in a Z3 model. https://z3prover.github.io/api/html/classz3py_1_1_func_interp.html

Goal

Set of formulas that can be solved and/or transformed using tactics and solvers.

IsNotApp

A struct to represent when an ast is not a function application.

Model

Model for the constraints inserted into the logical context.

Optimize

Context for solving optimization queries.

Params

Parameter set used to configure many components (simplifiers, tactics, solvers, etc).

Pattern

A pattern for quantifier instantiation, used to guide quantifier instantiation.

Probe

Function/predicate used to inspect a goal and collect information that may be used to decide which solver and/or preprocessing step will be used.

RecFuncDecl

Recursive function declaration. Every function has an associated declaration.

Solver

(Incremental) solver, possibly specialized by a particular tactic or logic.

Sort

Sorts represent the various ‘types’ of Asts.

SortDiffers

A struct to represent when two sorts are of different types.

Statistics

Statistical data about a solver.

StatisticsEntry

A key, value entry within Statistics.

Synchronized

A Send and Sync wrapper for Z3 structures associated with a Context.

Tactic

Basic building block for creating custom solvers for specific problem domains.

Version

Enums

AstKind

The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.

DeclKind

The different kinds of interpreted function kinds.

GoalPrec

Precision of a given goal. Some goals can be transformed using over/under approximations.

SatResult

Result of a satisfiability query.

SortKind

The different kinds of Z3 types.

StatisticsValue

The value for a key in Statistics.

Symbol

Symbols are used to name several term and type constructors.

Traits

PrepareSynchronized

This trait allows a type to opt-in to multithreading through Synchronized.

Solvable

Indicates that a type can be evaluated from a Model and produce a Bool counterexample, allowing usage in the Solver::solutions iterator pattern.

Translate

Represents types that depend on a Context and can be translated to another Context.

Functions

full_version

get_global_param

Get a global (or module) parameter.

reset_all_global_params

Restore the value of all global (and module) parameters. This command will not affect already created objects (such as tactics and solvers).

set_global_param

Set a global (or module) parameter. This setting is shared by all Z3 contexts.

version

with_z3_config

Runs the provided callback with all inner Z3 calls using a Context derived from the provided Config.

with_z3_contextDeprecated

Runs the provided callback with all inner Z3 calls using the provided Context.