z3 0.20.0

High-level rust bindings for the Z3 SMT solver from Microsoft Research
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143

use crate::Context;
use crate::ast::{Ast, Real};
use std::convert::TryFrom;
use z3_sys::*;

/// [`Ast`] node representing a real algebraic number value.
///
/// `Algebraic` is a sub-sort of [`Real`]: every algebraic number is a real number,
/// but not every real is algebraic. Use [`From<Algebraic>`] to widen to `Real`,
/// or [`TryFrom<Real>`] to narrow (fails if the `Real` is not a concrete algebraic value).
pub struct Algebraic {
    pub(crate) ctx: Context,
    pub(crate) z3_ast: Z3_ast,
}

impl Algebraic {
    /// Check if the given AST is a value in the Z3 real algebraic number package.
    pub fn is_value(ast: &impl Ast) -> bool {
        unsafe { Z3_algebraic_is_value(ast.get_ctx().z3_ctx.0, ast.get_z3_ast()) }
    }

    /// Check if the algebraic number is positive.
    pub fn is_positive(&self) -> bool {
        unsafe { Z3_algebraic_is_pos(self.ctx.z3_ctx.0, self.z3_ast) }
    }

    /// Check if the algebraic number is negative.
    pub fn is_negative(&self) -> bool {
        unsafe { Z3_algebraic_is_neg(self.ctx.z3_ctx.0, self.z3_ast) }
    }

    /// Check if the algebraic number is zero.
    pub fn is_zero(&self) -> bool {
        unsafe { Z3_algebraic_is_zero(self.ctx.z3_ctx.0, self.z3_ast) }
    }

    /// Return the sign of the algebraic number: -1 if negative, 0 if zero, 1 if positive.
    pub fn sign(&self) -> i32 {
        unsafe { Z3_algebraic_sign(self.ctx.z3_ctx.0, self.z3_ast) }
    }

    /// Add two algebraic numbers.
    pub fn add(a: &Algebraic, b: &Algebraic) -> Algebraic {
        assert_eq!(a.ctx.z3_ctx, b.ctx.z3_ctx);
        unsafe {
            Algebraic::wrap(
                &a.ctx,
                Z3_algebraic_add(a.ctx.z3_ctx.0, a.z3_ast, b.z3_ast).unwrap(),
            )
        }
    }

    /// Subtract two algebraic numbers.
    pub fn sub(a: &Algebraic, b: &Algebraic) -> Algebraic {
        assert_eq!(a.ctx.z3_ctx, b.ctx.z3_ctx);
        unsafe {
            Algebraic::wrap(
                &a.ctx,
                Z3_algebraic_sub(a.ctx.z3_ctx.0, a.z3_ast, b.z3_ast).unwrap(),
            )
        }
    }

    /// Multiply two algebraic numbers.
    pub fn mul(a: &Algebraic, b: &Algebraic) -> Algebraic {
        assert_eq!(a.ctx.z3_ctx, b.ctx.z3_ctx);
        unsafe {
            Algebraic::wrap(
                &a.ctx,
                Z3_algebraic_mul(a.ctx.z3_ctx.0, a.z3_ast, b.z3_ast).unwrap(),
            )
        }
    }

    /// Divide two algebraic numbers.
    pub fn div(a: &Algebraic, b: &Algebraic) -> Algebraic {
        assert_eq!(a.ctx.z3_ctx, b.ctx.z3_ctx);
        unsafe {
            Algebraic::wrap(
                &a.ctx,
                Z3_algebraic_div(a.ctx.z3_ctx.0, a.z3_ast, b.z3_ast).unwrap(),
            )
        }
    }

    /// Return the k-th root of the algebraic number. Requires k > 0.
    pub fn root(&self, k: u32) -> Algebraic {
        unsafe {
            Algebraic::wrap(
                &self.ctx,
                Z3_algebraic_root(self.ctx.z3_ctx.0, self.z3_ast, k).unwrap(),
            )
        }
    }

    /// Return this algebraic number raised to the k-th power.
    pub fn power(&self, k: u32) -> Algebraic {
        unsafe {
            Algebraic::wrap(
                &self.ctx,
                Z3_algebraic_power(self.ctx.z3_ctx.0, self.z3_ast, k).unwrap(),
            )
        }
    }

    /// Return true if `a < b`.
    pub fn lt(a: &Algebraic, b: &Algebraic) -> bool {
        assert_eq!(a.ctx.z3_ctx, b.ctx.z3_ctx);
        unsafe { Z3_algebraic_lt(a.ctx.z3_ctx.0, a.z3_ast, b.z3_ast) }
    }

    /// Return true if `a > b`.
    pub fn gt(a: &Algebraic, b: &Algebraic) -> bool {
        assert_eq!(a.ctx.z3_ctx, b.ctx.z3_ctx);
        unsafe { Z3_algebraic_gt(a.ctx.z3_ctx.0, a.z3_ast, b.z3_ast) }
    }

    /// Return true if `a == b` (algebraic equality).
    pub fn eq_algebraic(a: &Algebraic, b: &Algebraic) -> bool {
        assert_eq!(a.ctx.z3_ctx, b.ctx.z3_ctx);
        unsafe { Z3_algebraic_eq(a.ctx.z3_ctx.0, a.z3_ast, b.z3_ast) }
    }
}

impl From<Algebraic> for Real {
    fn from(a: Algebraic) -> Real {
        unsafe { Real::wrap(&a.ctx, a.z3_ast) }
    }
}

impl TryFrom<Real> for Algebraic {
    type Error = ();

    /// Returns `Ok(Algebraic)` if the `Real` is a concrete algebraic value,
    /// or `Err(())` if it is a symbolic expression.
    fn try_from(real: Real) -> Result<Self, ()> {
        if Algebraic::is_value(&real) {
            Ok(unsafe { Algebraic::wrap(&real.ctx, real.z3_ast) })
        } else {
            Err(())
        }
    }
}