We propose a general scheme for treating the theory of bit-vectors (BV) in the MCSAT framework, complementing the approach by Zelji´c, Wintersteiger, and Ru¨mmer. MCSAT assigns values to first-order variables. In order to keep track of the set of feasible values for a given bit-vector variable, we propose the use of Binary Decision Diagram. This allows an assignment mechanism that is generic for BV. When a conflict arises, involving some of the constraints and some of the assignments made so far, MCSAT must produce an explanation for the conflict. This mechanism can be specialized according to the constraints involved in the conflict. We propose an explanation mechanism that applies when these constraints are in the core fragment of BV, based on slicing and equality reasoning. We plan to add support for more BV fragments in the future.
In this preliminary report of work in progress, we broach the theory of bit-vectors (BV) in the context of model-constructing satisfiability (MCSAT), an approach to SMT-solving proposed in [dMJ13, JBdM13, Jov17]. MCSAT builds on the mechanisms of CDCL [MLM09], adapting them to first-order terms and first-order theories. A treatment of BV in the MCSAT framework was proposed by Zelji´c, Wintersteiger, and Ru¨mmer in [ZWR16]. The present work in progress explores some ideas that can complement their approach.
In MCSAT, the range of values that can be assigned to a first-order variable is restricted by the constraints to be satisfied. This restriction mechanism is theory-specific, and finding a suitable representation to express such a range is a key step in integrating this theory into the MCSAT framework. The approach proposed in [ZWR16] for BV uses intervals and patterns to express restrictions on the range of feasible values for a given bit-vector variable.
The first idea that we are exploring is the use of a more general representation to record the range of feasible values for a given variable, namely Binary Decision Diagrams (BDD) [Bry86] over the bits of the variable. BDDs can express the exact range of feasible values, regardless of the nature of the bit-vector constraints to be satisfied. For instance, BDDs can detect when the range becomes a singleton, in which case MCSAT can propagate the assignment of the last feasible value to the variable. BDDs offer a generic mechanism for proposing and propagating values; the question of specializing the treatment of bit-vectors to specific views of what these bit-vectors represent (e.g. integers), can be limited to the other main mechanism of MCSAT: conflict explanation.
Indeed, MCSAT also features a notion of conflict that generalizes that of CDCL. Typically, a conflict arises when the range of values for a variable becomes empty (a situation easily detected by BDDs): the assignments made so far do not lead to a model. MCSAT must produce a symbolic explanation for a conflict, so that some of the assignments made so far can be undone and replaced by new ones, taking the explanation into account.
The generation of the explanation is theory-specific. For BV, two mechanisms were proposed in [ZWR16] to make a conflict explanation rule out more potential assignments than those that were actually used and that led to the conflict. The first one consists in generalizing a value that was assigned into an interval containing the value. The second one consists in generalizing a value that was assigned by unassigning some of its bits.
These are examples of specialized mechanisms for conflict explanation, which can work better than what we consider as the default explanation mechanism: bit-blasting the constraints that are involved in the conflict. If the said constraints live in a particular fragment of BV, alternative mechanisms can produce high-level explanations that generalize better. We describe such a mechanism for the core fragment of BV made of concatenation, extraction and equality. An MCSAT explanation is produced out of pure equality reasoning: the involved constraints are first transformed according to coarsest-base slicing, as described in e.g. [CMR97, BS09]. We adapt the approach to the generation of conflict explanations for MCSAT.
In Section 2 we review MCSAT, present the BDD approach, and the general considerations for conflict explanation. In Section 3 we present the dedicated conflict explanation method for the core fragment of BV.
MCSAT takes as input a quantifier-free formula and determines whether the formula is satisfiable in a given theory or a combination thereof. In this paper we consider the case where these formulas are built from the symbols of the bit-vectors theory and from bit-vector variables. The problem is satisfiable if we can assign a bit-vector value to every free variable appearing in the problem, in a way that makes the input formula evaluate to true (using the standard model and standard interpretation of symbols). We call such an assignment a model.
To determine satisfiability of the input, MCSAT builds on the ideas of CDCL [MLM09], whose rules are used to handle the Boolean structure of the input. CDCL attempts to construct a Boolean model by building a partial candidate model as sequence of literals, called the trail, elements of which are either decisions on the value of a variable, or an assignment that is a results of a Boolean inference (called propagation).
MCSAT generalizes the notion of trail to allow first-order decisions and propagations (see, e.g., [Jov17]). For example, in the context of bit-vectors, a decision x 7→ 0010 for a bit-vector variable x, is allowed on the trail. As in the case of CDCL, during a run of MCSAT, the trail gets extended with decisions and propagations, and gets pruned when MCSAT backtracks. An example of an MCSAT trail containing bit-vector elements is 2 2.1
J (x <u 0011) 7→ >, x 7→ 0010, (y ◦ y = x) ;C > K .
Above, the element (x <u 0011) 7→ > is a Boolean decision assigning the literal to true, x 7→ 0010 is a bit-vector decision assigning the variable x to a bit-vector value, and the element (y ◦ y = x) ;C > represents a Boolean propagation from clause C, assuming that the input problem contains a clause such as C ≡ (x <u 0011) ⇒ (y ◦ y = x). As in the case of CDCL, we keep the clause C as a decoration of literal y ◦ y = x in the trail.
The assignments in the trail define a partial model that can be used to evaluate literals. For instance, the above trail, as a partial model, evaluates x <u 0011 to true, but does not evaluate y ◦ y = x, because the free variable y is unassigned.
In the CDCL calculus, the search process aims to maintain the invariant that no literal in the problem is implied (either by decision, or unit propagation) to have two different values. Otherwise, a conflict is detected, which triggers conflict analysis, backtracking, and a revision of the search. This also holds in the MCSAT calculus, but in a more general setting that also takes into account the evaluation of theory-specific literals. For instance, in the example above, since the literal (x <u 0011) is assigned to true, the calculus is only allowed to pick values for x that are consistent with this constraint. More generally, in order to ensure consistency, a variable x can only be assigned to a value that is consistent with all literals in the trail where x is the only unassigned variable (unit). In our example, the decision that follows (x 7→ 0010), entails that the literal (x <u 0011) evaluates to true, which is consistent with the previous assignment for (x <u 0011). On the other hand, the assignment x 7→ 0011 would not be allowed since this would imply two different interpretations for the literal (x <i 0011) (both true and false). Now, consider the literal (y ◦ y = x) that is propagated to be true. In order to complete the partial model with an assignment for y, we need to make sure that the literal (y ◦ y = x) can not also evaluate to false. Unfortunately, due to the value of x in the trail, any value that we could pick for y would make the literal (y ◦ y = x) evaluate to false. So no assignment for y is possible, and MCSAT is in a conflict state, from where we must backtrack on the decisions that we made.
As in CDCL, backtracking removes at least one of the decisions that were made in the trail, and performs a conflict analysis. We learn from this conflict analysis a conflict clause, symbolically describing the conflict in terms of the previous decisions that were made. Taking this new clause into account avoids making the same faulty decisions in the future model construction attempts. After finitely many attempts, MCSAT will either succeed in proposing a full model without raising a conflict, or find a conflict that involves no decision but only the input problem. 2.2
Detecting the situation where no value for a given variable is feasible with respect to the trail is a key feature of MCSAT. For this, for each unassigned variable y, we collect all the constraints that can be evaluated as soon as y gets a value, i.e., all constraints whose only unassigned free variable is y, a.k.a. the unit constraints in y. Each of those constraints restricts the range of possible values whose assignment to y would be feasible. The conjunction of those unit constraints may restrict the range of feasible values to a singleton set, which leaves us no choice regarding the value to assign to y and we can propagate it; it may also restrict it to an empty set, which would prompt us to backtrack, as in the example above.
A key objective of an MCSAT implementation for a particular theory is to devise a datastructure that can represent the feasible set of a variable y, with efficient operations for 1. updating the set whenever a new constraint becomes unit in y, 2. detecting when the set becomes empty, and 3. proposing a value from the feasible set.
This data-structure depends on the theory being considered.
For instance, if instead of the theory of bit-vectors we were working in the theory of linear arithmetic, a typical constraint would be an inequality between a linear combination of arithmetic variables and a constant, i.e. a1x1 + · · · anxn + ay l c with l ∈ {<, ≤}. When this constraint becomes unit in y, it means that values have been assigned to x1, . . . , xn, and the inequality simply restricts the values for y by imposing an upper or lower bound (depending on the sign of a). Hence, the conjunction of inequality constraints that are unit in y define the set of feasible values as an interval, with at most two of those constraints being useful, namely that imposing the lowest upper bound (if there is one) and that imposing the greatest lower bound (if there is one). Then it is easy to check whether this interval is a singleton or empty.
Coming back to the theory of bit-vectors, Zelji´c, Wintersteiger and Ru¨mmer [ZWR16] repy[3] y[2] y[1] y[0]
F
T y[3] y[2] y[1] y[0] resent restrictions on feasible values with the combination of an interval (e.g. [0000, 0010]), and of a pattern (e.g., ???1), imposing the value of some of the bits. We propose here to use a Binary Decision Diagram (BDD) [Bry86] over the bits of y. BDDs have the advantage that they can encode the exact set of feasible values: these are exactly those values that give rise to a path to True in the BDD. This precision can also be a disadvantage if the complexity of constructing a BDDs is prohibitive. But, since in the MCSAT context, we are only considering unit constraints, with a single free bit-vector variable, we believe that BDDs are quite appropriate.
The BDD for each variable is initialized with the BDD constant True. Assume that we must satisfy the constraint (y <u x), on two bit-vector variables x and y of length 4. If we assign to x the value 0011, for example, the constraint becomes unit and gives rise to the first BDD of Fig. 1. Assume then another unit constraint (y[0] = x[0]) is processed that forces y to follow the pattern ???1, i.e., forcing y to be odd. The corresponding BDD, the second one of Fig. 1, is combined with the first one in a conjunction, producing the third one. Since this BDD encodes the singleton {0001}, the assignment y 7→ 0001 can then be propagated on the trail.
Note that in case a BDD for y becomes a singleton, the unique assignment y 7→ v that can be “propagated” on the trail does not have an explicit justification and technically has to be placed on the trail as a decision. In contrast, the propagation mechanisms of [ZWR16] have explicit justifications, which can directly be used in conflict analysis: If the propagated assignment contributes to a conflict, having its explicit justification allows an immediate resolution step in the conflict analysis. Having this assignment as a decision (suggested by a singleton BDD {v} for y) would stop the conflict analysis there; but what is learned from the conflict immediately entails y 6' v, which would empty the BDD for y and trigger a new conflict.
Indeed, if at some point the BDD representing the feasible set for y becomes empty, then MCSAT will detect a conflict, explain it, and backjump. We describe this in the next section. 2.3
When the set of feasible values for a bit-vector variable y becomes empty, then the trail contains a set of bit-vector constraints
A(~x, y) = {A1, . . . , Am} , with free variables ~x = x1, . . . , xn, and y, as well as a the assignments x1 7→ v1, . . . , xn 7→ vn forming a partial model M. In addition, the conjunction of BDDs over the bits of y formed by the constraints in A under the partial model M, is the empty BDD.
The trivial and the simplest way to explain this conflict is to state it directly, i.e.
A1 ∧ · · · ∧ Am ⇒ (x1 6' v1) ∨ · · · ∨ (xn 6' vn) .
This conflict allows MCSAT to undo the latest decision and resume the search with some other choice.
For many theories other than bit-vectors, ruling out one model, as above, would not lead to a terminating calculus if the domain of values is infinite: infinitely many attempts would be needed to exhaust the possible values. For the theory of bit-vectors, since the underlying domain is finite, ruling out models one at a time does lead to a sound, complete and terminating calculus. But this is of course impractical. So, as with theories with infinite value domains (e.g, arithmetic [JBdM13]), we should try to learn a general explanation of the conflict that allows us to rule out many more values than one. To do so, we need to identify what it is, about the constraints A1, . . . , Am, and the partial model M, that makes the feasible space for y empty. We will express the explanation as a conflict clause of the form Ac ⇒ I, where Ac ⊆ A is the core of the conflict. We call the clause I above an interpolating clause as defined below. Definition 1 (Interpolating clause). Let A(~x, y) be a set of bit-vector constraints, and let M be a model for ~x. We call a clause I an interpolating clause for A at M, if 1. A ⇒ I is a valid in bit-vectors, 2. I only contains variables ~x, and 3. I evaluates to false in M.
In other words, the interpolating clause interpolates between the constraints A, and the current assignment in the trail.
Apart for the trivial explanation, for bit-vectors, there is a procedure that can provide both the core Ac and the interpolating clause I: bit-blasting with a SAT solver. We can bit-blast the constraints in A1, . . . , Am into a SAT problem and solve the resulting SAT problem under assumptions that all constraints Ai are true, and that each bit of x1, . . . , xn is true or false as indicated by the values v1, . . . , vn. Since the original problem is not satisfiable, the SAT solver will return a core, indicating which bits of v1, . . . , vn (and which constraints A1, . . . , Am) contributed to the unsatisfiability. From this core we can then trivially construct an explanation. The smaller the core, the more values we can rule out with the explanation.
Bit-blasting always applies, and can be used as the default procedure to produce a conflict clause. Note that we only need to bit-blast the set of constraints that were unit in y. This can be significantly smaller than the whole set of bit-vectors constraints on the trail.
Although always applicable, by expanding the constraints to individual bits, the bit-blasting approach is not too appealing as a way of producing explanation. In some cases, when the constraints in A live in a suitable fragment of BV, there are better ways to produce explanations. By better we mean that the cost of generating the explanation may be cheaper, and/or the explanation itself may rule out more values.
Consider, for example, the following constraints
A = {x1 6' x2, x1 ' y, x2 ' y} .
From a model with assignments x1 7→ 1001, x2 7→ 0101, the bit-blasting approach might produce the explanation (x1 ' y ∧ x2 ' y) ⇒ (x1[3] ⇒ x2[3]) . After revising the model, on the second attempt we might similarly learn that (x2[3] ⇒ x1[3]). Continuing in this way, we might need 8 iterations in total to learn enough information to represent the high-level explanation for the conflict:
(x1 ' y ∧ x2 ' y) ⇒ x1 ' x2 .
A procedure that can produce (x1 ' x2) directly would be much more desirable.
Following the MCSAT approach, we propose the following path to producing explanations. First, use BDDs to isolate the core Ac ⊆ A of the constraints in conflict (e.g., by relying on the quick-explain mechanism [Jun01]), and then decide which explanation procedure to apply depending on the fragment of BV where the core Ac lives. The smaller the Ac, the higher the chances are that it lives in an isolated fragment of BV.
In the next section, we present such a procedure for the very simple fragment of BV made of equality, extraction and concatenation. In order to proceed with explaining the conflict, we first reduce the conflicting core E, D into a normalized form of equalities and disequalities between normal terms. Normal terms are either of the form z[h:l], called slices (of a variable z), or constants. Moreover, we make sure that the slices of z that appear in the normalized problem are non-overlapping. The transformed problem has the same free variables as the original problem, and is logically equivalent to it. This transformation is done by computing the coarsest-base slicing, following the well known procedures such as [CMR97, BS09].
Consider for instance the following problem on variables y, of length 6, and x1, of length 8.
E = { x1[3:0] ' x1[7:4] , y[5:2] ' y[3:0] }, D = { y[3:0] 6' x1[7:4] } . 3
Conflict explanation for the core fragment of BV In this section we consider the core fragment of BV, consisting of equalities and disequalities between bit-vector terms made of variables, constants, extraction and concatenation: A ::= t ' u | t 6' u t, u ::= x | c | t[h:l] | t ◦ u where x ranges over the bit-vector variables, each of which has an implicit length, c ranges over the bit-vector constants, and h and l range over integers. Terms are assumed to be well-formed with respect to the bit-vector lengths, i.e. in t ' u, t and u are assumed to be of the same length, and in t[h:l], h and l are assumed to be valid bit-vector indices for t, with l ≤ h. We abbreviate t[i:i] as t[i].
In the rest of the section we propose a procedure that produces a conflict clause, also called explanation, when given a conflict, as defined in the previous section. We therefore have • a set of variables X = {x1, . . . , xn, y}; • a partial assignment M mapping the variables xi to bit vectors values vi; • a set of equalities E = {ai ' bi}i∈E with variables in X, and • a set of disequalities D = {ai 6' bi}i∈D with variables in X.
In addition, we know that there is no model of A = {E, D} extending M with a value for y (it is a conflict). Furthermore, we can assume that this conflict is a core, i.e. that no constraint can be removed from A while remaining a conflict. 3.1
Note that the above slices of y are overlapping. By careful isolating the appropriate indexing intervals, this problem can be transformed into
Es = { x1[3:2] ' x1[7:6] , x1[1:0] ' x1[5:4]) , y[5:4] ' y[3:2] , y[3:2] ' y[1:0] } ,
Ds = { (y[3:2] 6' x1[7:6]) ∨ (y[1:0] 6' x1[5:4]) }.
After slicing, the set of equalities E remains a set of equalities (over normal terms), while the set of disequalities D becomes a set of clauses Ds containing disequalities over normal terms. 3.2
After slicing, we have a set of equalities Es, and a set of clauses Ds, all of whose literals are disequalities. All terms involved have their variables among x1, . . . , xn, y. The model M, made of the trail assignments x1 7→ v1, . . . , xn 7→ vn, allows the evaluation of any normal term that is a constant or the slice of a variable xi. Moreover, since the slices are non-overlapping, the transformed problem lies within the theory of equality (seeing slices as independent terms), with a twist being the cardinality constraints on the bit-vector domain – having to satisfy more disequalities than cardinality allows may be the reason of the conflict.
We first proceed to analyze the conflict with equality reasoning. We construct the E-graph G from Es [DNS05], also taking into account the values assigned by model M, as presented in Algorithm 1. The goal is to make sure that in each component of the E-graph, the terms that M can evaluate all evaluate to the same value, otherwise a conflict is found and the explanation can be produced. The predicate denoted isdefM(t) means that term t can be evaluated in M (i.e. it is not a slice of y), in which case evalM(t) denotes its value. We maintain the invariant that if a component contains a term that evaluates to value v in M, then the representative of that component evaluates to value v in M. To maintain this invariant, we ensure that the following property holds whenever we merge two components: if both representatives have values, these values are identical, and if only one of the two representatives has a value, then this representative becomes the representative of the merged component.
Algorithm 1 E-graph with value management 1: function e graph(Es, M) 2: Initialize(G) 3: for t1 ' t2 ∈ Es do 4: t01 ← rep(t1, G) . get representative for t1’s component 5: t02 ← rep(t2, G) . get representative for t2’s component 6: if isdefM(t01) and isdefM(t02) and evalM(t01) 6= evalM(t02) then 7: raise conflict(E ⇒ t01 ' t02) . D must be empty 8: 9: 10: t3 ← select(t01, t02)
G ← merge(t1, t2, t3, G) return G
. select representative for merged component . merge the components with new representative t3
The E-graph construction can detect and explain conflicts between the equalities in E and the current assignment, as in the following example.
Example 1. Let r1, r2, r3 be bit ranges of the same length. Let E be such that Es = {x1[r1] ' y[r3], x2[r2] ' y[r3]}, and let D be empty. Consider the model M that maps x1 7→ 0 . . . 0, x2 7→ 1 . . . 1. Then, e graph(Es, M) raises the conflict E ⇒ x1[r1] ' x2[r2].
If the E-graph construction does not raise a conflict, then M is compatible with the equalities entailed by Es and provides a value to each E-graph component that has at least one constant term or a slice of some xi. Moreover, giving an arbitrary value to every other component (those entirely made of slices of y) yields a value v for y such that M, y 7→ v satisfies Es, and therefore E. But since we assumed that M cannot be extended into a model of E ∧ D, any assignment of values to components made of slices of y will be inconsistent with the clauses in Ds. In other words, the conflict involves the disequalities.
In order to analyze the (disequality) conflict further, we note that any clause C ∈ Ds can be decomposed into the following components
CEs ∨ CM ∨ Cinterface ∨ Cfree , where • CEs contains disequalities t1 6' t2 such that t1 and t2 have the same E-graph representative: in other words, this disequality is necessarily false because of the equalities in Es; • CM is made of disequalities t1 6' t2 such that t1 and t2 have distinct E-graph representatives, but these evaluate in M to the same value: in other words, this disequality is necessarily false because of the values assigned by M; • Cinterface is made of disequalities t1 6' t2 such that t1 and t2 have distinct E-graph representatives, namely t01 and t02, such that t01 evaluates in M to a value, but t02 does not: it is necessarily a slice of y, and we can still satisfy t1 6' t2 by picking a good value for y; we say t01 is interfaced with a slice of y, and call it interface term; • Cfree is made of disequalities t1 6' t2 such that t1 and t2 have distinct E-graph representatives, neither of which evaluates in M: they are both slices of y, and we can still satisfy t1 6' t2 by picking a good value for y.
As already mentioned, Es is satisfied for any value for y, and it is the conjunction of the clauses in Ds that empties the space of possible values. This can happen when (i) one of the clauses in Ds necessarily evaluates to false, in other words when Cinterface and Cfree are both empty. This can also happen if (ii) there is in each clause in Ds a disequality in Cinterface or Cfree that we can still satisfy, but whichever disequality we choose to satisfy in each clause, there are not enough values to satisfy the conjunction of the chosen disequalities (given the values that M is already using). In either case, we produce the conflict clause with Algorithm 2, scanning through Ds. . where we collect interface terms . where we collect the disequalities that evaluate to false Algorithm 2 Disequality conflict 1: function dis conflict(Ds, M, G) 2: S ← ∅ 3: C0 ← ∅ 4: for C ∈ Ds do 5: Crep ← W{rep(t1, G) 6' rep(t2, G) | (t1 6' t2) ∈ CM} 6: ifMis empty(Cinterface) and is empty(Cfree) then 78:: elseraise conflict(E ∧ D ⇒ CMrep) 9: 10: 11:
C6= ← W{t1 ' t2 | evalM(t1) 6= evalM(t2), t1, t2 ∈ S} C= ← W{t1 6' t2 | evalM(t1) = evalM(t2), t1 6= t2, t1, t2 ∈ S} return E ∧ D ⇒ C0 ∨ C6= ∨ C=
C0 ← C0 ∨ Crep . we collect the disequalities made false in the model
M for t1 6' t2 ∈ Cinterface with isdefM(rep(t1, G)) do
S ← S ∪ {rep(t1, G)} . we collect the interface term 12: 13: 14:
Let us describe how the algorithm behaves on a specific example of conflict of type (i): Example 2. Let r1 and r2 be bit ranges of the same length, let r3, r4, r5 be bit ranges of the same length. Let E be such that Es contains { x1[r1] ' y[r1] , x2[r2] ' y[r2] , y[r3] ' y[r5] , y[r4] ' y[r5] }.
Let D be such that Ds is the singleton
{ (y[r1] 6' y[r2] ∨ y[r3] 6' y[r4]) }.
And let M map x1 and x2 to 0 . . . 0.
Assume the E-graph has selected y[r5] as the representative for the component { y[r3], y[r4], y[r5] }.
Then dis conflict(Ds, M, G) treats the unique clause C of Ds and: • For the first disequality, the representatives of y[r1] and y[r2], namely x1[r1] and x2[r2], both evaluate to 0 . . . 0, so the disequality belongs to CM; • And for the second disequality, the representatives of y[r3] and y[r4] are the same, namely y[r5], so this second disequality (which does not evaluate in M) belongs to CEs . As Cinterface and Cfree are empty, Algorithm 2 raises the conflict E ∧ D ⇒ x1[r1] 6' x2[r2].
More generally in a conflict of type (i), it will always be the case that Ds is a singleton: the clause of Ds that evaluates to false, together with Es and M, empties the range of possible values for y, so having assumed that E, D is a core, it means that Ds is a singleton that only contains that clause.
When analyzing 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 we have. So our conflict clause includes (the negation of) all such equalities and disequalities. An example can be given as follows: Example 3. Let E be empty, and let D be such that Ds is
{ ( x2[0] 6' x2[1] ∨ y[0] 6' y[1] ) , x1[0] 6' y[0] , x1[1] 6' y[1] }.
And let M map x1 and x2 to 00.
As E is empty, the E-graph components are simply the same as the terms of the problem. We detail below the behavior of dis conflict(Ds, M, G): • When treating the first clause, call it C, the first disequality is in CM, as the two sides belong to different components but evaluate to the same value; therefore C0 becomes { x2[0] 6' x2[1] }; the second disequality features two slices of y and therefore is in Cfree, so the clause is potentially satisfiable and we move on to the next clause. • The second clause is a unit one, and its only disequality cannot be evaluated, as its lefthand side can but its right-hand side cannot; so S becomes { x1[0] }; the clause is potentially satisfiable so we move on to the next clause. • Again, the third clause is a unit clause whose only disequality cannot be evaluated, as its left-hand side can but its right-hand side cannot; so S becomes { x1[0] , x1[1] }; the clause is potentially satisfiable and, since this was the last clause of Ds, we conclude that the unsatisfiability of the original problem is a cardinality issue.
Indeed, y[0] should be different from 0 because of the second clause, y[1] should also be different from 0 because of the third clause, but y[0] and y[1] should still be different from each other because of the first clause, and we hit the fact that we only have two values for bits.
Algorithm 2 produces the conflict clause
D ⇒ ( x2[0] 6' x2[1] ∨ x1[0] 6' x1[1] ).
Indeed, x2[0] 6' x2[1] is necessary because, if it were true in M, we would not have to satisfy y[0] 6' y[1] and therefore y ← 11 would work. And x1[0] 6' x1[1] is necessary because, if it were true in M, say with x1 ← 01 (resp. x1 ← 10), then y ← 11 (resp. y ← 00) would work.
Correctness of the method relies on the following lemma: Lemma 1 (The produced clauses are interpolating clauses).
• If Algorithm 1 reaches line 7, t01 ' t02 is an interpolating clause for E ∧ D at M. • If Algorithm 2 reaches line 7, Crep is an interpolating clause for E ∧ D at M.
M • If Algorithm 2 reaches line 14, C0 ∨ C6= ∨ C= is an interpolating clause for E ∧ D at M. 4
In this report on our work in progress, we have presented two main ideas for the treatment of BV in MCSAT, complementing the approach proposed in [ZWR16].
By using BDDs, the search mechanism of MCSAT can be generic, while specific mechanisms for conflict explanation can be chosen depending on the constraints involved in the conflict. Identifying the core of the constraints that contribute to the conflict can be done with BDDs, and increases the chances that a dedicated mechanism can be used for explanations (the default mechanism being bit-blasting). BDDs also offer a propagation mechanism that differs from those in [ZWR16], in that the justification of a propagated assignment is not computed before the assignment is ruled out by a conflict. Computing the core of the conflict at that point can be seen as recovering the justification of the propagation. The propagation mechanisms of [ZWR16] could actually cohabit with our BDD-based mechanisms, whenever the benefits that they give for conflict resolution outweigh the cost of detecting their applicability. Experimentation is needed to compare this cost to the cost of identifying conflict cores through BDDs.
In case the conflicting constraints live in the core fragment of BV, we proposed an explanation mechanism based on coarsest-base slicing and equality reasoning, which we tuned for the production of explanations. Compared to previous work on coarsest-base slicing, such as [BS09], we only apply the transformation on the core constraints of a particular conflict, rather than the whole problem. This should in general make the slices coarser, which we expect to positively impact efficiency.
We are currently working on dedicated explanation mechanisms for bigger or different fragments of BV; for instance the mechanisms studied in [JW16] (outside of the context of MCSAT) should lead to an explanation mechanism for bit-vector arithmetic without multiplication. In general we intend to rely, if possible, on equality reasoning, as equality is one of the aspects of bit-vectors that is lost by bit-blasting but that can be useful in learned lemmas.
Our work in progress of course involves the implementation of the ideas presented in this report. These are mostly based on the MCSAT principle that handling constraints that are unit in a bit-vector variable is in practice easier than handling multivariate constraints. This principle probably applies less to benchmarks whose constraints feature complex re-uses of a single variable, and we anticipate that our approach will apply to software verification problem better than to hardware verification problems.
Future work includes relating our approach to the very recent report by Chihani, Bobot, and Bardin [CBB17], which aims at lifting the CDCL mechanisms to the word level of bit-vector reasoning, and therefore seems very close to MCSAT.
Future work also includes exploring the integration of the proposed 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) [BGLS17], which precisely aims at organizing, along the MCSAT mechanisms, the collaboration between generic theory modules.
Acknowledgments The authors thank Aleksandar Zelji´c for fruitful discussions. The research presented in this paper has been supported in part by NSF grant 1528153. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of NSF or the U.S. Government.