cvc5-rs 0.3.1

High-level Rust bindings for the cvc5 SMT solver
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
144
145
146
147
148
149
150
151
152
153
154
155

use cvc5_sys::*;
use std::ffi::CString;
use std::fmt;

/// Solver statistics collected during solving.
pub struct Statistics {
    pub(crate) inner: Cvc5Statistics,
}

impl Statistics {
    pub(crate) fn from_raw(raw: Cvc5Statistics) -> Self {
        Self { inner: raw }
    }

    /// Look up a statistic by name.
    pub fn get(&self, name: &str) -> Stat {
        let c = CString::new(name).unwrap();
        Stat {
            inner: unsafe { cvc5_stats_get(self.inner, c.as_ptr()) },
        }
    }

    /// Initialize the statistics iterator.
    ///
    /// - `internal` — include internal (non-public) statistics.
    /// - `dflt` — include statistics that still have their default value.
    pub fn iter_init(&self, internal: bool, dflt: bool) {
        unsafe { cvc5_stats_iter_init(self.inner, internal, dflt) }
    }

    /// Return `true` if the iterator has more elements.
    pub fn iter_has_next(&self) -> bool {
        unsafe { cvc5_stats_iter_has_next(self.inner) }
    }

    /// Advance the iterator and return the next `(name, stat)` pair.
    pub fn iter_next(&self) -> (String, Stat) {
        let mut name: *const std::os::raw::c_char = std::ptr::null();
        let s = unsafe { cvc5_stats_iter_next(self.inner, &mut name) };
        let n = unsafe {
            std::ffi::CStr::from_ptr(name)
                .to_string_lossy()
                .into_owned()
        };
        (n, Stat { inner: s })
    }

    /// Advance the iterator and return only the next [`Stat`], ignoring the name.
    pub fn iter_next_stat(&self) -> Stat {
        self.iter_next().1
    }
}

impl fmt::Debug for Statistics {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "Statistics({self})")
    }
}

impl fmt::Display for Statistics {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        let s = unsafe { cvc5_stats_to_string(self.inner) };
        write!(f, "{}", unsafe {
            std::ffi::CStr::from_ptr(s).to_string_lossy()
        })
    }
}

/// A single statistic value.
pub struct Stat {
    pub(crate) inner: Cvc5Stat,
}

impl Stat {
    /// Return `true` if this is an internal (non-public) statistic.
    pub fn is_internal(&self) -> bool {
        unsafe { cvc5_stat_is_internal(self.inner) }
    }

    /// Return `true` if this statistic still has its default value.
    pub fn is_default(&self) -> bool {
        unsafe { cvc5_stat_is_default(self.inner) }
    }

    /// Return `true` if this statistic holds an integer value.
    pub fn is_int(&self) -> bool {
        unsafe { cvc5_stat_is_int(self.inner) }
    }

    /// Return `true` if this statistic holds a double value.
    pub fn is_double(&self) -> bool {
        unsafe { cvc5_stat_is_double(self.inner) }
    }

    /// Return `true` if this statistic holds a string value.
    pub fn is_string(&self) -> bool {
        unsafe { cvc5_stat_is_string(self.inner) }
    }

    /// Return `true` if this statistic holds a histogram.
    pub fn is_histogram(&self) -> bool {
        unsafe { cvc5_stat_is_histogram(self.inner) }
    }

    /// Get the integer value of this statistic.
    pub fn get_int(&self) -> i64 {
        unsafe { cvc5_stat_get_int(self.inner) }
    }

    /// Get the double value of this statistic.
    pub fn get_double(&self) -> f64 {
        unsafe { cvc5_stat_get_double(self.inner) }
    }

    /// Get the string value of this statistic.
    pub fn get_string(&self) -> String {
        unsafe {
            std::ffi::CStr::from_ptr(cvc5_stat_get_string(self.inner))
                .to_string_lossy()
                .into_owned()
        }
    }

    /// Get the histogram value as a list of `(key, count)` pairs.
    pub fn get_histogram(&self) -> Vec<(String, u64)> {
        let mut keys: *mut *const std::os::raw::c_char = std::ptr::null_mut();
        let mut values: *mut u64 = std::ptr::null_mut();
        let mut size = 0usize;
        unsafe { cvc5_stat_get_histogram(self.inner, &mut keys, &mut values, &mut size) };
        (0..size)
            .map(|i| unsafe {
                let k = std::ffi::CStr::from_ptr(*keys.add(i))
                    .to_string_lossy()
                    .into_owned();
                let v = *values.add(i);
                (k, v)
            })
            .collect()
    }
}

impl fmt::Debug for Stat {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "Stat({self})")
    }
}

impl fmt::Display for Stat {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        let s = unsafe { cvc5_stat_to_string(self.inner) };
        write!(f, "{}", unsafe {
            std::ffi::CStr::from_ptr(s).to_string_lossy()
        })
    }
}