Introduction

A key mathematical concept in the modeling of both software and hardware systems is the concept of (persistent) arrays. For example, arrays are used to model (mutable) array data structure or the memory heap (e.g., Frama-C tool for C) for program analysis [1,2,3,4,5], as well as memories [6,7,8] for hardware design verification. Efficient methods for reasoning about arrays are essential for analyzing and understanding software and hardware.

Dedicated methods for array reasoning are typically found in Satisfiability Modulo Theories (SMT) solvers, which provide the automated reasoning capabilities of numerous formal methods toolchains. These solvers check the satisfiability of a first-order formula in some background theory 𝒯 (or combination of theories). If the formula is true in some model of the theory(ies), it is said to be satisfiable (SAT). If not, it is said to be unsatisfiable (UNSAT). While most SMT solvers traditionally follow the CDCL(𝒯) [9] scheme for solving (i.e., deciding) such satisfiability problems, the Model-Constructing Satisfiability (MCSat) [10] scheme offers a deeper integration of Boolean and theory reasoning that has proved particularly successful for nonlinear arithmetic. MCSat also offers a new explanation functionality generalizing unsat cores to theory reasoning, which provides new algorithms for interpolation [11] and quantifier-supporting reasoning [12].

Yices2 is a state-of-the-art SMT-solver that implements both the CDCL(𝒯) and MCSat schemes, in two distinct (sub-)solvers. Nonlinear arithmetic is only supported in the MCSat-based solver, which does offer the aforementioned explanation and interpolation functionalities for all of the theories it supports. Until recently, these theories did not include the theory of arrays, which was only supported in the CDCL(𝒯)-based solver. More generally and to the best of our knowledge, no SMT-solver has been supporting arrays in the MCSat approach. Hence, even if a solver uses an MCSat-like procedure to reason about nonlinear arithmetic (e.g., cvc5 [13], Z3 [14]), the nonlinear arithmetic reasoner interacts with the rest of the solver via a traditional theory combination scheme (typically a variant of the Nelson-Oppen scheme [15]) when trying to solve benchmarks involving both arrays and nonlinear constraints (e.g., benchmarks for the SMT logics QF_ANIA and QF_AUFNIA). Yices2 itself did not support this theory combination, as its CDCL(𝒯) and MCSat components do not interact. In this work, we address this limitation by extending the MCSat component of Yices2 with array reasoning.

The contributions of this paper are: 1) we describe how to integrate array reasoning in an MCSatbased SMT solver using the concept of weak equivalence graph [16]; 2) we describe the implementation of that integration in Yices2 -the source is publicly available on GitHub 1 ; 3) we experimentally evaluate our implementation on the array benchmarks from SMT-LIB and compare it against other SMT solvers.

Notation. We assume the standard many-sorted first-order logical setting with the usual notions of signature, term, formula, and interpretation. A theory is a pair 𝒯 = (Σ, I), where Σ is a signature and I is a class of Σ-interpretations that are the models of 𝒯. A Σ-formula 𝜑 is satisfiable (resp., unsatisfiable) in 𝒯 if it is satisfied by some (resp., no) interpretation in I.

Theory of Arrays.

Let 𝒯 𝐴 be the standard theory of arrays [17] with extensionality. We assume sorts for arrays, indices, and elements, and function symbols read and write. Here and rest of the paper, we use 𝑎 and 𝑏 to refer to arrays, 𝑖 and 𝑗 to refer to array indices, and 𝑒 to refer to array elements. The theory contains the class of all interpretations satisfying the following axioms: ∀𝑎, 𝑖, 𝑗, 𝑒. 𝑖 = 𝑗 ⟹ read(write(a, j, e), i) = 𝑒 (idx)

∀𝑎, 𝑖, 𝑗, 𝑒. 𝑖 ≠ 𝑗 ⟹ read(write(a, j, e), i) = read(a, i) (read-over-write)

∀𝑎, 𝑏. (∀𝑖. read(a, i) = read(b, i)) ⟹ 𝑎 = 𝑏 (ext)

Related Work. The theory of arrays has been a significant focus in the development of SMT solvers since their early days. Two main approaches have been utilized to decide the theory of arrays: rewritingbased and instantiation-based techniques.

Rewriting-based techniques address the problem using rewrite rules with a specific ordering to ensure completeness. Some notable work in this category can be found in [18,19].

On the other hand, instantiation-based techniques involve adding instantiations of array axioms, typically done lazily under certain conditions to minimize the number of instantiations. Most CDCL(𝒯)based SMT solvers, such as proposed in [20,21,22,23], utilize instantiation-based approaches.

One specific instantiation-based approach is the weakly equivalent arrays method, as implemented in the CDCL(𝒯)-based SMT solver SMTInterpol [16,24], as well as in the CDCL(𝒯) solver in Yices2. 2 Our work leverages weakly equivalent arrays reasoning, integrating it into an MCSat-based SMT solver.

Weakly Equivalent Arrays

Our approach uses the weakly equivalent arrays decision procedure proposed by [16], which we briefly describe here. The procedure exploits the use of chains of write function applications by introducing the notion of weak equivalence: two arrays connected via a chain of write function application can differ only at finitely many indices. This essentially generalizes the read-over-write axiom to reason about a chain of write applications. The lemmas produced from that reasoning have the advantage of using small number of new terms. In fact, we can compute the set of terms that would appear in those lemmas by scanning the input formula. Note that the finiteness of that set of terms used for generating all lemmas is a key requirement for termination, making MCSat a decision procedure.

Let 𝜙 be the input formula whose satisfiability is under question and 𝒜 be the set of array terms in 𝜙.

𝑎 ≅ 𝑖 𝑏 ∶= 𝑎 ≈ 𝑖 𝑏 ∨ (∃𝑎 ′ 𝑏 ′ 𝑗𝑘.𝑎 ≈ 𝑖 𝑎 ′ ∧ 𝑖 ∼ 𝑉 𝑗 ∧ read(a ′ , j) ∼ 𝑉 read(b ′ , k) ∧ 𝑘 ∼ 𝑉 𝑖 ∧ 𝑏 ′ ≈ 𝑖 𝑏)

Lemma 2. Weakeq-ext: Given an equivalence relation ∼ 𝑉 , if array terms 𝑎 and 𝑏 connected via a path 𝑃 in 𝐺 𝑊 and for all indices 𝑖 ∈ 𝐼 𝑛𝑑𝑖𝑐𝑒𝑠(𝑃) we have 𝑎 ≅ 𝑖 𝑏, then 𝑎 ∼ 𝑉 𝑏 holds.

To produce the full explanation, we need to add equality constraints of the path involved in readover-weakeq and weakeq-ext. Definition 6. Let 𝐶𝑜𝑛𝑑(⋅) (resp. 𝐶𝑜𝑛𝑑 𝑖 (⋅)) be the function that takes as input a path 𝑃 in the weak equivalence graph and computes a condition under which a weak equivalent or weak congruence holds (resp. weak equivalence modulo 𝑖 holds), defined by induction on 𝑃 as follows:

𝐶𝑜𝑛𝑑(∅) ∶= 𝑡𝑟𝑢𝑒 𝐶𝑜𝑛𝑑 𝑖 (∅) ∶= 𝑡𝑟𝑢𝑒 𝐶𝑜𝑛𝑑((𝑎 ↔ 𝑏) ⋅ 𝑃) ∶= (𝑎 = 𝑏) ∧ 𝐶𝑜𝑛𝑑(𝑃) 𝐶𝑜𝑛𝑑 𝑖 ((𝑎 ↔ 𝑏) ⋅ 𝑃) ∶= (𝑎 = 𝑏) ∧ 𝐶𝑜𝑛𝑑 𝑖 (𝑃) 𝐶𝑜𝑛𝑑((𝑎 𝑗 ↔ 𝑏) ⋅ 𝑃) ∶= 𝐶𝑜𝑛𝑑(𝑃) 𝐶𝑜𝑛𝑑 𝑖 ((𝑎 𝑗 ↔ 𝑏) ⋅ 𝑃) ∶= (𝑖 ≠ 𝑗) ∧ 𝐶𝑜𝑛𝑑 𝑖 (𝑃) 𝐶𝑜𝑛𝑑(𝑎 ≈ 𝑖 𝑏) ∶= 𝐶𝑜𝑛𝑑 𝑖 (𝑃)

, where 𝑃 is a path between 𝑎 and 𝑏, and

∀𝑗 ∈ 𝐼 𝑛𝑑𝑖𝑐𝑒𝑠(𝑃).𝑖 ≁ 𝑉 𝑗 𝐶𝑜𝑛𝑑(𝑎 ≅ 𝑖 𝑏) ∶= ⎧ ⎪ ⎨ ⎪ ⎩ 𝐶𝑜𝑛𝑑(𝑎 ≈ 𝑖 𝑏) if 𝑎 ≈ 𝑖 𝑏 𝐶𝑜𝑛𝑑(𝑎 ≈ 𝑖 𝑎 ′ ) ∧ 𝑖 = 𝑗 ∧read(a ′ , j) = read(b ′ , k) ∧𝑘 = 𝑖 ∧ 𝐶𝑜𝑛𝑑(𝑏 ′ ≈ 𝑖 𝑏) if 𝑎 ≈ 𝑖 𝑎 ′ ∧ 𝑖 ∼ 𝑉 𝑗 ∧read(a ′ , j) ∼ 𝑉 read(b ′ , k) ∧𝑘 ∼ 𝑉 𝑖 ∧ 𝑏 ′ ≈ 𝑖 𝑏 Algorithm 1: check-read-over-write-conflict(𝐺 𝑊 , 𝑉, ∼ 𝑉 ) for 𝑎, 𝑏, 𝑖, 𝑗 ∈ 𝑉 such that read(a, i), read(b, j) ∈ 𝑉 do if 𝑎 ≈ 𝑖 𝑏 ∧ 𝑖 ∼ 𝑉 𝑗 ∧ read(a, i) ≁ 𝑉 read(b, j) then return 𝑖 = 𝑗 ∧ 𝐶𝑜𝑛𝑑(𝑎 ≈ 𝑖 𝑏) ∧ read(a, i) ≠ read(b, j); end return NULL;

The algorithm 3 presents a decision procedure based on weakly equivalent arrays reasoning for the extensional theory of arrays. The procedure is sound and complete [16] for the theory.

MCSat Overview

MCSat applies CDCL-like mechanisms to perform theory reasoning. (Figure 1 illustrates the high level flow of the MCSat framework.) The MCSat architecture consists of a core solver, an assingment trail, and reasoning plugins. The core solver explicitly and incrementally constructs models with firstorder variable assignments-maintained in the assignment trail-while maintaining the invariant that none of the constraints evaluate to false. It is also responsible for dispatching notifications (e.g. new term notification) and handling requests from the reasoning plugins. The core solver decides upon assignments (values provided by reasoning plugins) when there is choice, it can propagate them when there is not, and it backtracks upon conflict. One of its key roles is to perform conflict analysis when a reasoning plugin detects a conflicting state. The lemmas learned via conflict analysis are based on theory-specific explanations, provided by reasoning plugins, of conflicts and propagations.

When formulas are asserted in MCSat, the core solver notifies all plugins of the asserted formulas. The reasoning plugins analyze the formulas and report all relevant terms back to the core. Relevant terms include theory variables and Boolean terms (excluding negations). When computing the value of a compound Boolean term or its negation, relevant terms are the term itself and its closest sub-terms needed for value computation.

The trail is a key data structure in MCSat, holding relevant term assignments for easy retrieval of the satisfying assignment upon termination of the MCSat search. The trail functions as a partial model constructed by MCSat during the search process, allowing for term evaluation based on the model values of their relevant subterms. A term 𝑡 can be evaluated (or is evaluable) in the trail 𝑀 if 𝑡 has an assignment in 𝑀, or if all closest relevant sub-terms of 𝑡 have been assigned in 𝑀. Evaluation-consistency is maintained in the trail, ensuring that no term evaluates to different values within it.

The role of reasoning plugins is to provide assignments for decisions, perform propagations, detect conflicts, and produce explanations. So, to implement a new theory in the MCSat framework, we need a reasoning plugin for that theory that must support in decision-making, propagation (including conflict detection), and explanation generation for propagated terms. Moreover, to ensure termination, there is the finite-basis requirement on plugins, i.e. any literals introduced by plugins come from a finite set of literals.

MCSat Equality and Uninterpreted Functions Plugin

The Equality and Uninterpreted Function (EUF) MCSat-Plugin provides equality reasoning over the uninterpreted sorts and uninterpreted function. The equality reasoning is done by tracking terms of uninterpreted sorts and uninterpreted functions and their trail values in an E-graph [25,26,27] EUF plugin updates the E-graph when new assignments are made in the trail to the tracked terms. This extended E-graph ensures: 1) If an equivalence class contains an evaluable term 𝑐, then the representative of that class is evaluable; 2) Two evaluable terms 𝑐 1 and 𝑐 2 in the same equivalence class must evaluate to the same value, otherwise this is a source of conflict. The conflict is reported to the core MCSat solver as a set of equalities and disequalities that contributed to the conflict. Propagation and Explanation. The EUF plugin propagates model values of uninterpreted sort terms when two class nodes get merged and one of them is not evaluable. In our implementation we also track equalities between Boolean terms in the E-graph. This allows the EUF plugin to propagate Boolean terms based on equivalence classes. The explanations of these propagations are tracked (or lazily produced), and are provided to the core solver when the propagated terms appear in a conflict when doing conflict analysis and lemma learning. We satisfy the finite-basis requirement because the EUF plugin only "introduces" equalities (disequalities) between terms that already exist in the trail.

Decision Assignment. The EUF plugin is also responsible for providing assignment values for variables and function applications of uninterpreted sorts. A value to uninterpreted sort term is essentially an integer identifier that the MCSat partial model keeps track of. The EUF plugin maintains a set of infeasible values for each term to be decided (terms that EUF is responsible to provide assignment for).

Extending MCSat-EUF Plugin with Arrays Reasoning

To be able to do model-based arrays reasoning in MCSat, we extend the EUF plugin with: i) tracking of relevant array terms, ii) array propagation and explanation, iii) array conflict detection, and iv) array decision assignment.

Relevant Array Terms. The extended EUF plugin tracks array terms, in addition to uninterpreted function terms, as relevant terms when the core solver notifies it about new terms. Array terms include array variables, array write terms, and array read terms. 3 The set of relevant terms returned to the core solver may also include terms not present in the term notified by the core solver. These additional terms are array read terms and indices, as defined by the set 𝑉 (1) in Section 2.

Example 1. Let read(a, i), write(b, j, e) be the new terms notified by the core solver to the extended EUF 3 Array reads in Yices2 are uninterpreted function applications, so there was no need to extend the EUF plugin for those terms.

plugin. The relevant array terms set, in this case, is {write(b, j, e), 𝑎, 𝑏} ∪ {read(write(b, j, e), j), read(b, j), 𝑗, 𝑒} ∪ {read(a, i), 𝑖}.

The main purpose of adding these additional terms is to prompt the MCSat core solver to make decisions on these terms, resulting in assignments to these terms in the trail. This allows us to detect array theory conflicts, for such a trail with assignments, using weakly equivalent arrays reasoning. It is important to note that we are able to satisfy the finite-basis requirement of the extended plugin as weakly equivalent arrays reasoning only uses the tracked terms in the generated arrays lemmas.

Propagation and Explanation.

For propagation, we rely on the existing EUF propagation mechanism that propagates model values of terms that are unassigned in the MCSat trail. This covers the read terms and array terms that are evaluable in the E-graph but are not assigned in the MCSat trail. Therefore, the explanation procedure of the existing EUF plugin can be used to explain array term propagations.

Example 2. Let 𝑀 ∶= {read(a, i) ↦ 𝛼 1 , 𝑎 ↦ 𝛼 2 } be an assignment in the solver trail. Suppose the extended EUF plugin deduces, using the E-graph, that the array term 𝑏 is equal to 𝑎 and read(b, j) is equal to read(a, i) -note that 𝑏 and read(b, j) do not have assignments in the trail. The plugin returns the assignment values {𝑏 ↦ 𝛼 2 , read(b, j) ↦ 𝛼 1 } as propagations to the core solver, which adds these assignments to the solver trail.

Array Conflict detection via Weak-Equivalence Graph.

To check that the equivalence relation (assignment in the trail and E-graph) satisfies the array theory axioms, we can build the weak equivalence graph for every term in 𝑉 that has an assignment in the trail. First, we check the (idx) lemma. If violated, we report its negation as a conflict. Otherwise, we check for generalized read-over-write axiom violation using Algorithm 1. We report the conflict detected by the algorithm. Otherwise, we check for generalized extensionality axiom violation using Algorithm 2. Similarly, we report the conflict detected by the algorithm. If no conflicts are detected, then the current MCSat trail satisfies the arrays axioms.

Array Decision Assignment.

We use a simple mechanism to make decisions for array variables and array writes. We choose different values for different array terms when making decisions. If two array terms get merged they get equal values via propagation.

Implementation Details

We have implemented our approach in the MCSat solver of Yices2 [28]. The MCSat implementation in Yices2 already supports real/integer arithmetic [29], bitvectors [30,27], and uninterpreted functions [27].

Here we provide some important details of our implementation.

Eager Lemma Instantiation. When the core solver notifies the EUF plugin about new write terms, we eagerly instantiate the (idx) axiom for each write and assert the resulting lemma to the solver by adding it to the clause database.

Relevant Array Terms Set. As described in [16], we also optimize our implementation by using a smaller relevant array terms set 𝑉. If the element theory is stably infinite, we do not need to add read(a, i) for every write (a, i, e). This optimization has the potential to reduce the number of read terms in 𝑉, resulting in less work for both Algorithm 1 and Algorithm 2. Weak Equivalence Graph Data Structure and Conflict Detection. We utilize the data structure proposed in [16] to store the weak equivalence graph. Every vertex in the graph corresponds to an array term, and an edge represents a write operation between the two vertices -the direction can inverted during the construction of the graph. This data structure offers an efficient way to detect if two arrays are weakly equivalent (as well as modulo i equivalent). For further details, we recommend referring to Section 7 in [16]. The reasoning for weakly equivalent arrays, as presented earlier, assumes that we have a model that satisfies the EUF axioms. It is important to note that the MCSat model is built incrementally as the search progresses, unlike in CDCL(𝒯) where the model is built after the reasoning is complete. Therefore, we do not wait till we have a full model that is consistent with the EUF axioms. Instead, we construct the weak equivalence graph as soon as we have a model value for each term in the set 𝑉 (see (1)). This allows to detect array conflicts earlier than the approach where we wait until the EUF model is complete.

Experimental Evaluation

Solvers and Benchmarks. We refer to the implementation of our proposed approach in Yices2 as Yices2-MCSat-we have used the git commit #17369e6. To evaluate its performance, we have done experiments on various quantifier-free logic benchmarks containing arrays from the SMT-LIB [31] release 2023 [32], including QF_AX, QF_ABV, QF_AUFBV, QF_ALIA, QF_AUFLIA, QF_ANIA, and QF_AUFNIA. We have evaluated the different optimizations of our implementation on the QF_AX benchmarks. Moreover, we have compared the optimized version against cvc5 [13] (version 2024-03-25-a40d28f), MathSAT5 [33] (version 5.6.10), and Z3 [14] (version 4.13.0). Yices2 (git commit #17369e6) and Bitwuzla [34] (version 0.4.0) have been also included in the experiments for the supported logics.

Experimental Setup. The experiments were conducted on a 96-core AMD-CPU server running Ubuntu 20.04.6 LTS. We used a time limit of 3 minutes and a memory limit of 8 GB for each benchmark solved by the solvers.

The results are presented in tables 1 to 5. Each table provides information on the logic category, total number of benchmarks in the top row. The solved column shows the number of solved instances, the sat/unsat column shows the number of solved satisfiable/unsatisfiable instances, the time column shows the total solving time for each solver. The aggregated results are also presented in Figure 2, showing cactus plots of different logics. 1 displays the results of evaluating various options of our implementation on the arrays (QF_AX) benchmarks.

Evaluation of Optimizations. Table

The default option, Yices2-MCSat, incorporates all optimizations outlined in Section 4.1. These optimizations include: a) utilizing a smaller relevant array term set, b) eagerly adding the (idx) lemma when the core solver detects a write to the EUF plugin, and c) checking for array conflicts when all relevant array terms have been assigned a value in the trail. Yices-MCSat-no-opt-a and Yices-MCSat-noopt-b refer to versions without optimization a and optimization b, respectively. Yices-MCSat-no-c-1 and Yices-MCSat-no-c-2 are versions without optimization c, with the former checking for array conflicts (early check) whenever the E-graph does not identify a conflict, and the latter checking for array conflicts (late check) when each term in the E-graph has an assignment in the trail. The results clearly indicate the significance of all optimizations, with optimization a standing out as the most critical. Additionally, we were able to replicate the impact of optimization a, as proposed in [16].

Comparison Againts Other SMT solvers. In Table 2, results for the arrays (QF_AX) benchmarks are shown. Yices2-MCSat solves all the benchmarks and performs competitively with other solvers, even solving more benchmarks than cvc5. Table 3 displays results for the arrays with nonlinear arithmetic (QF_ANIA and QF_AUFNIA) benchmarks. In this category, Yices2-MCSat demonstrates its strength by solving the highest number of benchmarks compared to other solvers, with a couple of benchmarks lead over MathSAT5. 4 We can notice the complementarity of the various approaches in Figure 2b.

For the arrays with linear arithmetic (QF_ALIA and QF_AUFLIA) benchmarks in Table 4, Yices2-MCSat competes closely with cvc5 and Z3, although it falls behind MathSAT5 and Yices2 in terms of the number of benchmarks solved. The longer solving time for Yices2-MCSat in this category may be due to its use of CAD-based [35] nonlinear reasoning engine even for linear problems.

Table 5 presents the results for the arrays with bitvectors (QF_ABV and QF_AUFBV) benchmarks. Yices2-MCAST's performance is better than cvc5 but not on par with other solvers. Yices2-MCSat uses word-level model-based reasoning for bitvector constraints, which is less efficient than the bit-blasting approach used by the other solvers on SMT-LIB bitvector benchmarks containing bitwise operations. This difference in approach may explain Yices2-MCSat's performance on these benchmarks.

Conclusion and Future Work

We have presented a new MCSat-based solver for the extensional theory of arrays. The array decision procedure at its core incorporates EUF and weakly equivalent arrays reasoning. By using the weakly equivalent arrays reasoning, we meet the finite-basis requirement of the MCSat framework. Our approach has been implemented in the Yices2 SMT solver, enabling it to tackle array problems involving nonlinear arithmetic. The performance of this new solver is competitive with the current state of the art and excels in handling array problems with nonlinear arithmetic constraints. Our future plans include expanding the implementation to include constant arrays and the diff function [19,36], which will allow us to experiment with generating quantifier-free array interpolants using the model-based interpolation procedure [11] in Yices2-MCSat. Ultimately, we aim to use this to model-check array-based transition systems [37,38] in the Sally [39,40] model-checker.