smtlib/theories/
arrays_ex.rs

1#![doc = concat!("```ignore\n", include_str!("./ArraysEx.smt2"), "```")]
2
3use std::marker::PhantomData;
4
5use smtlib_lowlevel::ast;
6
7use crate::terms::{app, Const, IntoWithStorage, STerm, Sorted, StaticSorted};
8
9/// Representation of a functional array with extensionality. A possibly
10/// unbounded container of values of sort Y, indexed by values of sort X.
11#[derive(Debug)]
12pub struct Array<'st, X: Sorted<'st>, Y: Sorted<'st>>(STerm<'st>, PhantomData<X>, PhantomData<Y>);
13
14impl<'st, X: Sorted<'st>, Y: Sorted<'st>> Clone for Array<'st, X, Y> {
15    fn clone(&self) -> Self {
16        *self
17    }
18}
19
20impl<'st, X: Sorted<'st>, Y: Sorted<'st>> Copy for Array<'st, X, Y> {}
21
22impl<'st, X: Sorted<'st>, Y: Sorted<'st>> IntoWithStorage<'st, Array<'st, X, Y>>
23    for Const<'st, Array<'st, X, Y>>
24{
25    fn into_with_storage(self, _st: &'st smtlib_lowlevel::Storage) -> Array<'st, X, Y> {
26        self.1
27    }
28}
29
30impl<'st, X: StaticSorted<'st>, Y: StaticSorted<'st>> From<STerm<'st>> for Array<'st, X, Y> {
31    fn from(t: STerm<'st>) -> Self {
32        Array(t, PhantomData, PhantomData)
33    }
34}
35impl<'st, X: StaticSorted<'st>, Y: StaticSorted<'st>> From<Array<'st, X, Y>> for STerm<'st> {
36    fn from(value: Array<'st, X, Y>) -> Self {
37        value.0
38    }
39}
40
41impl<'st, X: StaticSorted<'st>, Y: StaticSorted<'st>> StaticSorted<'st> for Array<'st, X, Y> {
42    type Inner = Self;
43
44    const AST_SORT: ast::Sort<'static> =
45        ast::Sort::new_simple_parametric("Array", &[X::AST_SORT, Y::AST_SORT]);
46
47    fn static_st(&self) -> &'st smtlib_lowlevel::Storage {
48        self.0.st()
49    }
50}
51
52#[allow(unused)]
53impl<'st, X: StaticSorted<'st>, Y: StaticSorted<'st>> Array<'st, X, Y> {
54    /// The value stored at `index` --- `(select self index)`
55    fn select(self, index: X) -> Y {
56        app(self.st(), "select", (self.0.term(), index.term())).into()
57    }
58    /// Copy of this array with `value` stored at `index` --- `(store self index
59    /// value)`
60    fn store(self, index: X, value: Y) -> Array<'st, X, Y> {
61        app(
62            self.st(),
63            "store",
64            (self.0.term(), index.term(), value.term()),
65        )
66        .into()
67    }
68}
69
70#[cfg(test)]
71mod tests {
72    use smtlib_lowlevel::backend::z3_binary::Z3Binary;
73
74    use super::Array;
75    use crate::{
76        terms::{Sorted, StaticSorted},
77        Int, Solver, Storage,
78    };
79
80    /// Check that an array can be defined using the high-level API
81    #[test]
82    fn define_array() -> Result<(), Box<dyn std::error::Error>> {
83        let st = Storage::new();
84        let mut solver = Solver::new(&st, Z3Binary::new("z3")?)?;
85        let a = Array::<Int, Int>::new_const(&st, "a");
86
87        solver.assert(a._eq(a))?;
88
89        let _model = solver.check_sat_with_model()?.expect_sat()?;
90
91        Ok(())
92    }
93
94    /// Check that a value stored at an index can be correctly retrieved
95    #[test]
96    fn read_stored() -> Result<(), Box<dyn std::error::Error>> {
97        let st = Storage::new();
98        let mut solver = Solver::new(&st, Z3Binary::new("z3")?)?;
99        let a = Array::<Int, Int>::new_const(&st, "a");
100        let x = Int::new_const(&st, "x");
101        let y = Int::new_const(&st, "y");
102
103        let updated = a.store(x.into(), y.into());
104        let read = updated.select(x.into());
105
106        solver.assert(read._eq(y))?;
107
108        let _model = solver.check_sat_with_model()?.expect_sat()?;
109
110        Ok(())
111    }
112
113    /// Check that a value stored at an index is guaranteed to be retrieved
114    #[test]
115    fn read_stored_incorrect() -> Result<(), Box<dyn std::error::Error>> {
116        let st = Storage::new();
117        let mut solver = Solver::new(&st, Z3Binary::new("z3")?)?;
118        let a = Array::<Int, Int>::new_const(&st, "a");
119        let x = Int::new_const(&st, "x");
120        let y = Int::new_const(&st, "y");
121
122        let updated = a.store(x.into(), y.into());
123        let read = updated.select(x.into());
124
125        solver.assert(read._neq(y))?;
126
127        let res = solver.check_sat()?;
128
129        match res {
130            crate::SatResult::Unsat => Ok(()),
131            s => Err(Box::new(crate::Error::UnexpectedSatResult {
132                expected: crate::SatResult::Unsat,
133                actual: s,
134            })),
135        }
136    }
137
138    /// Check that a store does not affect values other than the target index
139    #[test]
140    fn read_untouched() -> Result<(), Box<dyn std::error::Error>> {
141        let st = Storage::new();
142        let mut solver = Solver::new(&st, Z3Binary::new("z3")?)?;
143        let a = Array::<Int, Int>::new_const(&st, "a");
144        let x = Int::new_const(&st, "x");
145        let y = Int::new_const(&st, "y");
146        let z = Int::new_const(&st, "z");
147
148        let updated = a.store(x.into(), y.into());
149        let read = updated.select(z.into());
150
151        solver.assert(x._neq(z))?;
152        solver.assert(read._neq(y))?;
153
154        let _model = solver.check_sat_with_model()?.expect_sat()?;
155
156        Ok(())
157    }
158}
smtlib/theories/arrays_ex.rs

smtlib/theories/
arrays_ex.rs
