key: cord-0046598-4lfqrt29
authors: Graham-Lengrand, Stéphane; Jovanović, Dejan; Dutertre, Bruno
title: Solving Bitvectors with MCSAT: Explanations from Bits and Pieces
date: 2020-05-30
journal: Automated Reasoning
DOI: 10.1007/978-3-030-51074-9_7
sha: 4e602931251bed4bcca93a45df5b488849c3cdbb
doc_id: 46598
cord_uid: 4lfqrt29

We present a decision procedure for the theory of fixed-sized bitvectors in the MCSAT framework. MCSAT is an alternative to CDCL(T) for SMT solving and can be seen as an extension of CDCL to domains other than the Booleans. Our procedure uses BDDs to record and update the sets of feasible values of bitvector variables. For explaining conflicts and propagations, we develop specialized word-level interpolation for two common fragments of the theory. For full generality, explaining conflicts outside of the covered fragments resorts to local bitblasting. The approach is implemented in the Yices 2 SMT solver and we present experimental results.

Model-constructing satisfiability (MCSAT) [19, 20, 24] is an alternative to the CDCL(T ) scheme [28] for Satisfiability Modulo Theories (SMT). While CDCL(T ) interfaces a CDCL SAT solver [23] with black-box decision procedures, MCSAT integrates first-order reasoning into CDCL directly. Like CDCL, MCSAT alternates between search and conflict analysis. In the search phase, MCSAT assigns values to first-order variables and propagates unit consequences of these assignments. If a conflict occurs during search, e.g., when the domain of a first-order variable is empty, MCSAT enters conflict analysis and learns an explanation, which is a symbolic representation of what was wrong with the assignments causing the conflict. As in CDCL, the learned clause triggers backtracking from which search can resume. Decision procedures based on MCSAT have demonstrated strong performance in theories such as non-linear real [24] and integer arithmetic [19] . These theories are relatively well-behaved and provide features such as quantifier elimination and interpolation-the building blocks of conflict resolution in MCSAT.

We describe an MCSAT decision procedure for the theory of bitvectors (BV). In contrast to arithmetic, the complexity of BV in terms of syntax and semantics, combined with the lack of word-level interpolation and quantifier elimination, makes the development of BV decision procedures (MCSAT or not) very difficult. The state-of-the art BV decision procedures are all based on a "preprocess and bitblast" pipeline [12, 22, 25] : they reduce the BV problems to a pure SAT problem by reducing the word-level semantics to bit-level semantics. Exceptions to the bitblasting approach do exist, such as [4, 16] , which generally do not perform as well as bitblasting except on small classes of crafted examples, and the MCSAT approach of [30] , which we discuss below and in the conclusion.

An MCSAT decision procedure must provide two theory-specific reasoning mechanisms.

First, the procedure must maintain a set of values that are feasible for each variable. This set is updated during the search. It is used to propagate variable values and to detect a conflict when the set becomes empty. Finding a suitable representation for domains is a key step in integrating a theory into MCSAT. We represent variable domains with Binary Decision Diagrams (BDDs) [5] . BDDs can represent any set of bitvector values. By being canonical, they offer a simple mechanism to detect when a domain becomes a singleton-in which case MCSAT can perform a theory propagation-and when a domain becomes empty-in which case MCSAT enters conflict analysis. In short, BDDs offer a generic mechanism for proposing and propagating values, and for detecting conflicts. In contrast, previous work by Zeljić et al. [30] represents bitvector domains using intervals and patterns, which cannot represent every set of bitvector values precisely; they over-approximate the domains.

Second, once a conflict has been detected, the procedure must construct a symbolic explanation of the conflict. This explanation must rule out the partial assignment that caused the conflict, but it is desirable for explanations to generalize and rule out larger parts of the search space. For this purpose, previous work [30] relied on incomplete abstraction techniques (replace a value by an interval; extend a value into a larger set by leaving some bits unassigned), and left open the idea of using interpolation to produce explanations. Instead of aiming for a uniform, generic explanation mechanism, we take a modular approach. We develop efficient word-level explanation procedures for two useful fragments of BV, based on interpolation. Our first fragment includes bitvector equalities, extractions, and concatenations where word-level explanations can be constructed through model-based variants of classic equality reasoning techniques (e.g., [4, 9, 10] ). Our second fragment is a subset of linear arithmetic where explanations are constructed by interval reasoning in modular arithmetic. When conflicts do not fit into either fragment, we build an explanation by bitblasting and extracting an unsat core. Although this fallback produces theory lemmas expressed at the bit-level, it is used only as a last resort. In addition, this bitblasting-based procedure is local and limited to constraints that are relevant to the current conflict; we do not apply bitblasting to the full problem. Section 2, is an overview of MCSAT. It also presents the BDD approach and general considerations for conflict explanation. Section 3 describes our interpolation algorithm for equality with concatenation and extraction. Section 4 presents our interpolation method for a fragment of linear bitvector arithmetic. Section 5 presents the normalization technique we apply to conflicts in the hope of express-ing them in that bitvector arithmetic fragment. Section 6 presents an evaluation of the approach, which we implemented in the Yices 2 solver [11] . 1

By BV, we denote the theory of quantifier-free fixed-sized bitvectors, a.k.a. QF BV in SMT-LIB [1] . A first-order term u of BV is sorted as either a Boolean or a bitvector of a fixed length (a.k.a. bitwidth), denoted |u|. Its set of variables (a.k.a. uninterpreted constants) is denoted var(u). This paper only uses a few BV operators. The concatenation of bitvector terms t and u is denoted t • u; the binary predicates < u , ≤ u denote unsigned comparisons, and < s , ≤ s denote signed comparisons. In such comparisons, both operands must have the same bitwidth. If n is the bitwidth of u, and l and h are two integer indices such that 0 ≤ l < h ≤ n, then u[h:l], extracts h−l bits of u, namely the bits at indices between l and h−1 (included Our convention is to have bitvector indices start from the right-hand side, so that bit 0 is the right-most bit and 0011[2:] is 11. We use standard notations for bitvector arithmetic, which coincides with arithmetic modulo 2 w where w is the bitwidth. We sometimes use integer constants e.g., 0, 1, −1 for bitvectors when the bitwidth is clear. We use the standard (quantifier-free) notions of literal, clause, cube, and formula [29] .

A model of a BV formula Φ is an assignment that gives a bitvector (resp. Boolean) value to all bitvector (resp. Boolean) variables of Φ, in such a way that Φ evaluates to true, under the standard interpretation of Boolean and bitvector symbols. To simplify the presentation, we assume in this paper that there are no Boolean variables, although they are supported in our implementation.

MCSAT searches for a model of an input quantifier-free formula by building a partial assignment-maintained in a trail -and extends the concepts of unit propagation and consistency to first-order terms and literals [19, 20, 24] . Reasoning is implemented by theory-specific plugins, each of which has a partial view of the trail. In the case of BV, the bitvector plugin sees in the trail an assignment M of the form x 1 → v 1 , . . . , x n → v n that gives values to bitvector variables, and a set of bitvector literals L 1 , . . . , L t , called constraints, that must be true in the current trail. MCSAT and its bitvector plugin maintain the invariant that none of the literals L i evaluates to false under M; either L i is true or some variable of L i has no value in M. To maintain this invariant, they detect unit inconsistencies: We say that literal L i is unit in y if y is the only unassigned variable of L i , and that a trail is unit inconsistent if there is a variable y and a subset {C 1 , . . . , C m } of {L 1 , . . . , L t }, called a conflict, such that every C j is unit in y and the formula ∃y m i = 1 C i evaluates to false under M. In such a case, y is called the conflict variable and C 1 , . . . , C m are called the conflict literals.

When such a conflict is detected, the current assignment, or partial model, M cannot be extended to a full model; some values assigned to x 1 , . . . , x n must be revised. As in CDCL, MCSAT backtracks and updates the current assignment by learning a new clause that explains the conflict. This new clause must not contain other variables than x 1 , . . . , x n and it must rule out the current assignment. For some theories, this conflict explanation can be built by quantifier elimination. More generally, we can build an explanation from an interpolant. 

To detect conflicts, we must keep track of the set of feasible values for every unassigned variable y. These sets are frequently updated during search so an efficient representation is critical. The following operations are needed: -updating the set when a new constraint becomes unit in y, -detecting when the set becomes empty, -selecting a value from the set.

For BV, Zeljić et al. [30] represent sets of feasible values using both intervals and bit patterns. For example, the set defined by the interval [0000, 0011] and the pattern ???1 is the pair {0001, 0011} (i.e., all bitvectors in the interval whose low-order bit is 1). This representation is lightweight and efficient but it is not precise. Some sets are not representable exactly. We use Binary Decision Diagrams (BDD) [5] over the bits of y. The major advantage is that BDDs provide an exact implementation of any set of values for y. Updating sets of values amounts to computing the conjunction of BDDs (i.e., set intersection). Checking whether a set is empty and selecting a value in the set (if it is not), can be done efficiently by, respectively, checking whether the BDD is false, and performing a top-down traversal of the BDD data structure. There is a risk that the BDD representation explodes but this risk is reduced in our context since each BDD we build is for a single variable (and most variables do not have too many bits). We use the CUDD package [8] to implement BDDs.

Given a conflict as described previously, the clause (x 1 v 1 ) ∨ · · · ∨ (x n v n ), which is falsified by model M only, is an interpolant for m i = 1 C i at M according to Definition 1. This gives the following trivial conflict explanation:

We seek to generalize model M with a formula that rules out bigger parts of the search space than just M. A first improvement is replacing the constraints by a core C, that is, a minimal subset of {C 1 , . . . , C n } that evaluates to false in M. 3 To produce the interpolant I, we can bitblast the constraints C 1 , . . . , C m and solve the resulting SAT problem under the assumptions that each bit of x 1 , . . . , x n is true or false as indicated by the values v 1 , . . . , v n . Since the SAT problem encodes a conflict, the SAT solver will return an unsat core, from which we can extract bits of v 1 , . . . , v n that contribute to unsatisfiability. This generalizes M by leaving some bits unassigned, as in [30] .

This method is general. It works whatever the constraints C 1 , . . . , C m , so we use it as a default procedure. The bitblasting step focuses on constraints that are unit in y, which typically leads to a much smaller SAT problem than bitblasting the whole problem from the start. However, the bitblasting approach can still be costly and it may produce weak explanations.

). After backtracking, we might similarly learn that (x 2 [3] ⇒ x 1 [3] ). In this way, it will take eight iterations to learn enough information to represent the high-level explanation:

A procedure that can produce (x 1 x 2 ) directly is much more efficient.

Our first specialized interpolation mechanism applies when constraints C = {C 1 , . . . , C m } belong to the following grammar:

where e ranges over any bitvector terms such that y ∈ var(e). Without loss of generality, we can assume that C is a core. We split C into a set of equalities

1: function e graph(Es, M) 2: Initialize(G) each evaluable term or slice is its own component 3:

for t1 t2 ∈ Es do 4:

if y ∈ var(t 1 ) and y ∈ var(t 2 ) and

select representative for merged component 9:

G ← merge(t1, t2, t3, G) merge the components with representative t3 10:

return G Slicing. Our first step rewrites C into an equivalent sliced form. This computes the coarsest-base slicing [4, 9] of equalities and disequalities in C. The goal of this rewriting step is to split the variables into slices that can be treated as independent terms. Explanations. After slicing, we obtain a set E s of equalities and a set D s that contains disjunctions of disequalities. We can treat each slice as a separate variable, so the problem lies within the theory of equality on a finite domain. We first analyze the conflict with equality reasoning against the model, as shown in Algorithm 1. We construct the E-graph G from E s [10] , while also taking into account the partial model M that triggered the conflict. The model can evaluate terms e such that y ∈ var(e) to values [[e]] M , and those can be the source of the conflict. To use the model for evaluating terms, we maintain two invariants during E-graph construction: 1. If a component contains an evaluable term c, then the representative of that component is evaluable. 2. Two evaluable terms c 1 and c 2 in the same component must evaluate to the same value, otherwise this is the source of the conflict. The E-graph construction can detect and explain basic conflicts between the equalities in E and the current assignment. S ← ∅ where we collect interface terms 3:

C0 ← ∅ where we collect the disequalities that evaluate to false 4:

for C ∈ Ds do 5:

if is empty(C interface ) and is empty(C free ) then 7:

we collect the disequalities made false in the model 10:

for t1 t2 ∈ C interface with y ∈ var(rep(t1, G)) do 11:

S ← S ∪ {rep(t1, G)} we collect the interface term 12:

If the E-graph construction does not raise a conflict, then M is compatible with the equalities in E s . Since C conflicts with M, the conflict explanation must involve D s . To obtain an explanation, we decompose each disjunct C ∈ D s into (C Es ∨ C M ∨ C interface ∨ C free ) as follows.

-C Es contains disequalities t 1 t 2 such that t 1 and t 2 have the same E-graph representatives; such disequalities are false because of the equalities in E s . -C interface contains disequalities t 1 t 2 such that t 1 and t 2 have distinct representatives t 1 and t 2 , t 1 is evaluable and t 2 is a slice; we can still satisfy t 1 t 2 by picking a good value for y; we say t 1 is an interface term. -C free contains disequalities t 1 t 2 such that t 1 and t 2 have distinct slices as representatives; we can still satisfy t 1 t 2 by picking a good value for y. The disjuncts in D s take part in the conflict either when (i) one of the clauses in D s is false because C interface and C free are both empty; or (ii) the finite domains are too small to satisfy the disequalities in C interface and C free , given the values assigned in M. In either case, we can produce a conflict explanation with Algorithm 2.

In a type (i) conflict, the algorithm produces an interpolant C rep M that is derived from a single element of D s . Because we assume that C is a core, a type (i) conflict can happen only if D s is a singleton. Here is how the algorithm behaves on such a conflict: Example 4. Let r 1 and r 2 be bit ranges of the same length, let r 3 , r 4 , r 5 

For a conflict of type (ii), the equalities and disequalities that hold in M between the interface terms make the slices of y require more values than there exist. So the produced conflict clause includes (the negation of) all such equalities and disequalities. An example can be given as follows: [1] is added to S. Since all clauses of D s have been processed, the conflict is of type (ii). Indeed, y[0] must be different from 0 because of the second clause, y [1] must also be different from 0 because of the third clause, but y[0] and y [1] must be different from each other because of the first clause. Since both y[0] and y [1] have only one bit, there are only two possible values for these two slices, so the three constrains are in conflict. Algorithm 2 produces the conflict clause [1] is necessary because, if it were true in M, we would not have to satisfy y[0] y [1] and therefore y ← 11 would work. Disequality [1] is also necessary because, if it were true in M, say with x 1 ← 01 (resp. x 1 ← 10), then y ← 11 (resp. y ← 00) would work.

Correctness of the method relies on the following lemma, whose proof can be found in [15] . 

Our second specialized explanation mechanism applies when constraints C = {C 1 , . . . , C m } belong to the following grammar: 

An interval takes the form [l ; u[, where the lower bound l and upper bound u are evaluable terms of some bitwidth w, with l included and u excluded. The notion of interval used here is considered modulo 2 w . We do not require l ≤ u u so an interval may "wrap around" in Z/2 w Z. Given a constraint C with unevaluable term t, we produce an interval I C of forbidden values for t according to the rules of Table 1 Table 1 applies, and I C1 is interval full with condition x 1 0. Given the supported grammar, term t contains a unique subterm of the form y[w:]. We transform I C into an interval of forbidden values for y[w:] by applying procedure forbid( t , I C , c C ) shown in Fig. 1 , which proceeds by recursion on t. Its specification is given below, and correctness is proved by induction on t. Running forbid( t Ci , I Ci , c Ci ) for all constraints C i , 1 ≤ i ≤m, produces a family of triples (w i ,

First, assume that one of the triples obtained above is of the form (w, full, c), coming from constraint C. As the interval forbids the full domain of values for y[w:], we produce conflict clause C ∧ c ⇒ ⊥. This formula is an interpolant for A at M. This is illustrated in Example 7.1. Assume now that no interval is full (as in Example 7.2). We group the triples (w, I, c) into different layers characterized by their bitwidths w: I will henceforth be called a w-interval, restricting the feasible values for y[w:], and c I denotes its associated condition in the triple. Ordering the groups of intervals by decreasing bitwidths w 1 > w 2 > · · · > w j , as shown in Fig. 2 , S j denotes the set of produced w j -intervals. The properties satisfied by the triples entail that

To produce an interpolant, we replace B by a quantifier-free clause.

The simplest case is when there is only one bitwidth w = w 1 : the fact that B is falsified by M means that I∈S1 [[I]] M is the full domain Z/2 w Z. Property " I∈S1 I is the full domain" is then expressed symbolically as a conjunction of constraints in the bitvector language. To compute them, we first extract a sequence I 1 , . . . , I q of intervals from the set S 1 , originating from a subset C of When several bitwidths are involved, the intervals must "complement each other" at different bitwidths so that no value for y is feasible. For a bitwidth w i , the union of the w i -intervals in model M may not necessarily cover the full domain (i.e., I∈Si [[I]] M may be different from Z/2 wi Z). The coverage can leave "holes", and values in that hole are ruled out by constraints of other bitwidths. To produce the interpolant, we adapt the coverage-extraction algorithm into Algorithm 3, which takes as input the sequence of sets (S 1 , . . . , S j ) as described in Fig. 2, and produces the interpolant's constraints d 1 , . . . , d p , collected in set output. The algorithm proceeds in decreasing bitwidth order, starting with w 1 , and calling itself recursively on smaller bitwidths to cover the holes that the current layer leaves uncovered (termination of that recursion is thus trivial). For every hole that I∈S1 [[I]] M leaves uncovered, it must determine how intervals of smaller bitwidths can cover it. [ that needs to be covered by the intervals of bitwidth w 2 and smaller. This is performed by a recursive call on bitwidth w 2 (l. 14); the fact that only hole I needs to be covered by the recursive call, rather than the full domain Z/2 w2 Z, is implemented by adding to S 2 in the recursive call the complement [next[w 2 :] ; baseline[w 2 :][ of I. The result of the recursive call is added to the output variable, as well as the fact that the hole must be small. The final interpolant is ( d ∈ output d) ⇒ ⊥. An example of run on a variant of Example 6.2 is given in [15] .

As implemented in Yices 2, MCSAT processes a conflict by first computing the conflict core with BDDs, and then normalizing the constraints using the rules of Fig. 3 . In the figure, u, u 1 and u 2 stand for any bitvector terms, ±-ext k (u) is the sign-extension of u with k bits, and bvnot(u) is the bitwise negation of u. The bottom left rule is applied with lower priority than the others (as upper-bits extraction distributes over • but not over +) and only if exactly one of {u 1 , u 2 } is evaluable (and not 0). In the implementation, u[|u|:0] is identified with u, • is associative, and +, × are subject to ring normalization. This is helped by the internal (flattened) representation of concatenations and bitvector polynomials in Yices 2. Normalization allows the specialized interpolation procedure to apply at least to the following grammar: 5

Atoms a :: = e 1 + t e 2 + t e 1 e 2 + t e 1 + t e 2 e 1 e 2 Terms t :

where ∈ {≤ u , < u , ≤ s , < s , }. Rewriting can often help further, by eliminating occurrences of the conflict variable (thus making more subterms evaluable) and increasing the chances that two unevaluable terms t 1 and t 2 become syntactically equal in an atom e 1 +t 1 e 2 +t 2 . 6 Finally, we cache evaluable terms to avoid recomputing conditions of the form y / ∈ var(e). These conditions are needed to determine whether the specialized procedures apply to a given conflict core.

We implemented our approach in the MCSAT solver within Yices 2 [11] . To evaluate its effectiveness, and the impact of the different modules, we ran the MCSAT solver with different settings on the 41,547 QF BV benchmarks available in the SMT-LIB library [1] . We used a three-minute timeout per instance. Each curve in Fig. 4 shows the number of solved instances for each solver variant; all: the procedures of Sects. 3 and 4, with the bitblasting baseline when these do not apply; bb: only the bitblasting baseline; bb+eq: procedure of Sect. 3 plus the baseline; bb+arith: procedure of Sect. 4 plus the baseline; all-prop is the same as all but with no propagation of bitvector assignments during search. For reference, we also included the version of the Yices 2 MCSAT solver that entered the 2019 SMT competition 7 , marked as smtcomp2019.

The solver combining all explainer modules solved 33,236 benchmarks before timeout, 14,174 of which are solved by pure simplification, and 19,062 of which actually rely on MCSAT explanations. 14,313 of those are solved without ever calling the default bitblasting baseline (only the dedicated explainers of Sects. 3 and 4 are used), while the other 4,749 instances are solved by a combination of the three explainers.

The results show that both equality and arithmetic explainers contribute to the effectiveness of the overall solver, individually and combined. A bit more than half of the problem instances involving MCSAT explanations are fully within the scope of the two dedicated explainers. Of course these explainers are still useful beyond that half, in combination with the bitblasting explainer. The results also show that the eager MCSAT value propagation mechanism introduced in [19] is important for effective solving in practice.

For comparison, we also ran two solvers CDCL(T ) solvers based on bitblasting on the same benchmarks and with the same timeout. We picked Yices 2 [11] (version 2.6.1) and Boolector [27] (version 3.2.0) and we used the same backend SAT solver for both, namely CaDiCaL [6] . Yices 2 solved 40,962 instances and Boolector solved 40,763 instances. We found 794 instances in the SMTLib benchmarks where our MCSAT solver was faster than Boolector by more than 2 sec. The pspace/ndist* and pspace/shift1add* instances are trivial for MCSAT (solved in less than 0.25 sec. each), while Boolector hit our 3-minute timeout on all ndist.a.* instances and all but 3 shift1add* ones. The brummayerbiere4 instances are trivial for MCSAT (solved in less than 0.03 sec.) while Boolector ran out of memory in our experimentation (except for one instance). Instances with a significant runtime difference in favour of MCSAT are among spear/openldap_v2.3.35/* and brummayerbiere/bitrev* (MCSAT is systematically better), float/mult* (MCSAT is almost systematically better), float/div*, asp/SchurNumbers/*, 20190311-bv-term-small-rw-Noetzli/*, and Sage2/*. MCSAT is almost systematically faster on uclid/catchconv/* and faster on more than half of spear/samba_v3.0.24/*.

Using an alternative MCSAT approach to bitvector solving, Zeljić et al. reported that their solver could solve 23704 benchmarks from a larger set of 49971 instances with a larger timeout of 1200 s [30] . 8 We have not managed to reproduce the results of Zeljić's solver on our Linux server for direct comparison.

To debug the implementation of our explainers, every conflict explanation that is produced when solving in debug mode is sent on-the-fly to (non-MCSAT) Yices 2, which checks the validity of the clause by bitblasting. In debug mode, every normalization we perform with the rules of Sect. 5 is also sent to Yices 2 to prove the equality between the original term and the normalized term. Performance benchmarking was only done after completing, without any red flag, a full run of MCSAT in debug mode on the 41,547 QF BV benchmarks instances.

The paper presents ongoing work on building an MCSAT solver for the theory of bitvectors. We have presented two main ideas for the treatment of BV in MCSAT, that go beyond the approach proposed by Zeljić et al. [30] .

First, by relying on BDDs for representing feasible sets, our design keeps the main search mechanism of MCSAT generic and leaves fragment-specific mechanisms to conflict explanation. The explanation mechanism is selected based on the constraints involved in the conflict. BDDs are also used to minimize the conflicts, which increases the chances that a dedicated explanation mechanism can be applied. BDDs offer a propagation mechanism that differs from those in [30] in that the justification for a propagated assignment is computed lazily, only when it is needed in conflict analysis. Computing the conflict core at that point effectively recovers justification of the propagations.

Second, we propose explanation mechanisms for two fragments of the theory: the core fragment of BV that includes equality, concatenation and extraction; and a fragment of linear arithmetic. Compared to previous work on coarsest-base slicing, such as [4] , our work applies the slicing on the conflict constraints only, rather than the whole problem. This should in general make the slices coarser, which we expect to positively impact efficiency. Our work on explaining arithmetic constraints is novel, notwithstanding the mechanisms studied by Janota and Wintersteiger [17] that partly inspired our Table 1 but addressed a smaller fragment of arithmetic outside of the context of MCSAT.

We have implemented the overall approach in the Yices 2 SMT solver. Experiments show that the overall approach is effective on practical benchmarks, with all the proposed modules adding to the solver performance. MCSAT is not yet competitive with bitblasting, but we are making progress. The main challenge is devising efficient word-level explanation mechanisms that can handle all or a least a large fragment of BV. Finding high-level interpolants in BV is still an open problem and our work on MCSAT shows progress for some fragments of the bitvector theory. For MCSAT to truly compete with bitblasting, we will need interpolation methods that cover larger classes of constraints.

A key step in that direction is to extend the bitvector arithmetic explainer so that it handles multiplications by constants, then multiplication by evaluable terms, and, finally, arbitrary multiplications. Deeper integration of fragmentspecific explainers could potentially help explaining hybrid conflicts that involve constraints from different fragments. To complement the explainers that we are developing, we plan to further explore the connection between interpolant generation and the closely related domain of quantifier elimination, particularly those techniques by John and Chakraborty [18] for the bitvector theory. The techniques by Niemetz et al. [26] for solving quantified bitvector problems using invertibility conditions could also be useful for interpolant generation in MCSAT.

Future work also includes relating our approach to the report by Chihani, Bobot, and Bardin [7] , which aims at lifting the CDCL mechanisms to the word level of bitvector reasoning, and therefore seems very close to MCSAT. Finally, we plan to explore integrating our MCSAT treatment of bitvectors with other components of SMT-solvers, whether in the context of MCSAT or in different architectures. An approach for this is the recent framework of Conflict-Driven Satisfiability (CDSAT) [2, 3] , which precisely aims at organizing collaboration between generic theory modules.

The Satisfiability Modulo Theories Library (SMT-LIB)

Conflict-driven satisfiability for theory combination: transition system and completeness

Satisfiability modulo theories and assignments

A scalable decision procedure for fixed-width bitvectors

Graph-based algorithms for boolean function manipulation

CDCL-inspired Word-level Learning for Bit-vector Constraint Solving

CUDD: the CU Decision Diagram package

An efficient decision procedure for the theory of fixed-sized bit-vectors

Simplify: a theorem prover for program checking

Yices 2.2

CAV 2007

An MCSAT treatment of bit-vectors

Interpolating bit-vector arithmetic constraints in MCSAT

Solving bitvectors with MCSAT: explanations from bits and pieces (long version)

CAV 2014

On intervals and bounds in bit-vector arithmetic

A layered algorithm for quantifier elimination from linear modular constraints

Solving nonlinear integer arithmetic with MCSAT

The design and implementation of the model constructing satisfiability calculus

Quickxplain: conflict detection for arbitrary constraint propagation algorithms

Decision Procedures -An Algorithmic Point of View, Second Edition

Conflict-driven clause learning SAT solvers

A model-constructing satisfiability calculus

Boolector 2.0

Solving quantified bit-vectors using invertibility conditions

Btor2, BtorMC and Boolector 3.0

Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL (T)

Handbook of Automated Reasoning

Deciding bit-vector formulas with mcSAT