Skip to main content
Fig. 9 | Formal Methods in System Design

Fig. 9

From: Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic

Fig. 9

Rules for handling extraction operations in bit-vector formulas. In extr-split and extr-arith, \(D \in \{L, R\}\). In extr-split, \(l < i \le u\). In \({\textsc {extr-cc}}_{LR}\), \(\exists _{Ls_1r_1}\) denotes existential quantification over all constants occurring in \(s_1\) or \(t_1\) but not in \({\varGamma }_R \cup {\varDelta }_R \cup \{s_2, r_2\}\). In \({\textsc {extr-cc}}_{RL}\), \(\forall _{Rs_1r_1}\) denotes universal quantification over all constants occurring in \(s_1\) or \(t_1\) but not in \({\varGamma }_L \cup {\varDelta }_L \cup \{s_2, r_2\}\). The rules cut\(_{LR}\) and cut\(_{RL}\) are only allowed for formulas \(\phi \) in which all constants are common to both \({\varGamma }_L \cup {\varDelta }_L\) and \({\varGamma }_R \cup {\varDelta }_R\)

Back to article page