Solving quantified linear arithmetic by counterexample-guided instantiation

Abstract

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedures for linear real arithmetic and linear integer arithmetic formulas with one quantifier alternation. We discuss extensions of these techniques for handling mixed real and integer arithmetic, and to formulas with arbitrary quantifier alternations. For the latter, we use a novel strategy that handles quantified formulas that are not in prenex normal form, which has advantages with respect to existing approaches. All of these techniques can be integrated within the solving architecture used by typical SMT solvers. Experimental results on standardized benchmarks from model checking, static analysis, and synthesis show that our implementation in the SMT solver cvc4 outperforms existing tools for quantified linear arithmetic.

1 Introduction

Among the biggest challenges in automated reasoning is efficient support for quantifiers in the presence of background theories. Quantifiers enable direct encoding of a number of problems of interest, including synthesis of software fragments from specifications [34, 50, 56], construction of transfer functions for program analysis [40], invariant inference [14, 27], as well as analysis of properties that go beyond safety [10, 11].

The most commonly used complete method for deciding constraints over quantified theories is quantifier elimination [29, Section 2.7]. Quantifier elimination algorithms typically solve a more general problem, of transforming arbitrary quantified formula with free variables into a theory-equivalent formula with no quantifiers.

However, depending on the particular variant of the language of constraints, performing actual quantifier elimination can have worse complexity than the decision problem [9], in part because it is required to give an answer on any formula, and the smallest formula resulting from quantifier elimination can be very large [64]. When the goal is to decide the satisfiability of quantified constraints, quantifier elimination may be doing unnecessary work. More importantly, procedures based on quantifier elimination often do not handle the underlying ground constraints in the most efficient way. Thus, quantifier elimination tends to be prohibitively expensive in practice. Recent work involving quantifier elimination [12, 41] has been motivated by avoiding worst-case performance by effectively computing an equisatisfiable set of ground formulas in a lazy fashion.

In the broader scope of automated theorem proving, it is often important to reason about formulas involving multiple theories, each of which may or may not support quantifier elimination. In practice, the goal is to obtain a framework for handling quantified formulas that is both complete for formulas belonging to decidable logics, and empirically effective when completeness guarantees are not known. To this end, modern SMT solvers most commonly use heuristic instantiation-based approaches [18], which are incomplete but work well in practice for undecidable fragments of first-order logic. A long term goal of this work is to capitalize both on recent advances in specialized techniques for quantified linear arithmetic [12, 13, 32, 44], and recent advances in instantiation-based theorem proving for first-order logic [17, 24, 51].

In this paper, we introduce an approach for establishing the satisfiability of formulas in quantified linear arithmetic based on a new quantifier instantiation framework. The use of quantifier instantiation for this task is motivated by the following.

• Procedures based on lazy quantifier instantiation typically establish satisfiability much faster than their theoretical complexity.

• Using quantifier instantiation for decidable fragments enables a uniform integration and composition with existing instantiation-based techniques [17, 18, 51], which are widely used by modern SMT solvers.

• An important class of synthesis problems can be expressed as quantified formulas with one quantifier alternation. As shown in [50], solutions for these problems can be extracted from an unsatisfiable core of quantifier instantiations.

Related work Quantifier elimination has been used to, e.g., show decidability and classification of Boolean algebras [55, 61], Presburger arithmetic [46], decidability of products [22, 42], [39, Chapter 12], and algebraically closed fields [60]. The original result on decidability of Presburger arithmetic is by Presburger [46]. The space bound for Presburger arithmetic was shown in [23]. The matching lower and upper bounds for Presburger arithmetic were shown in [9], see also [33, Lecture 24]. An analysis parameterized by the number of quantifier alternations is presented in [48]. A mechanically verified quantifier elimination algorithm was developed by Nipkow [43].

An approach for lazy quantifier elimination for linear real arithmetic was developed by Monniaux [41]. Integration of linear quantifier elimination into the solving algorithm used by SMT solvers was developed in [12], though the presented integration is not model driven. A lazy approach for quantifier elimination, which relies on an operation called model-based projection, has been developed in the context of SMT-based model checking [32], and can be used for extracting Skolem functions for simulation synthesis [21]. An efficient approach for quantified linear real arithmetic that is based on finding player strategies for establishing satisfiability is given in [20]. A recent approach involving quantified formulas with arbitrary alternations has been developed by Bjørner and Janota [13] for several background theories, which is closely related to the approach in this paper. By comparison, their approach is described in terms of a model-based projection operation whereas ours is based on instantiation. Additionally, their strategy for handling quantified formulas with multiple alternations assumes quantified formulas are in prenex form, whereas ours handles a more general grammar of quantified formulas that includes those not in prenex normal form. We will comment more on the technical differences between these two approaches in the later sections.

The most widely used techniques for quantifier instantiation in SMT were developed in [18], and later in [17, 25], which primarily focused on quantified formulas with uninterpreted functions. Our approach for quantified linear arithmetic instantiates quantified formulas based on a lazy stream of candidate models, terminating when either it finds a finite set of instances are unsatisfiable, or discovers that the original formula is satisfiable. Other approaches in this spirit have been used for quantified Boolean formulas [31], quantified bit-vectors [66], the essentially uninterpreted fragment [26], and, more generally, theories having a locality property [5, 30]; these works do not directly apply to quantified linear arithmetic. A recent approach for quantified formulas with one quantifier alternation has been developed in the SMT solver Yices [19]. The present paper builds upon our previous work for solving synthesis conjectures using quantifier instantiation in SMT [50], where an approach for quantified linear arithmetic was described without a specific method for selecting instances and without completeness guarantees. While the present paper focuses on linear arithmetic, where it outperforms existing approaches, we expect the presented framework to be relevant for other quantified theories. Among the examples of further decidable quantified constraints are quantified theories of term algebras [39, Chapter23], [38, 57] and their extensions [15, 35, 52], feature trees [4, 62], and monadic second-order theories [63].

Contributions This paper makes the following contributions. First, we define a general class of instantiation-based procedures for establishing the satisfiability of quantified formulas in Sect. 2. We demonstrate instances of the procedure are sound and complete for formulas over linear real arithmetic ($\mathrm {LRA}$) and linear integer arithmetic ($\mathrm {LIA}$) with one quantifier alternation in Sects. 3 and 4, two quantified fragments for which many current SMT solvers do not have efficient support for. We describe how these two procedures can be combined for mixed real and integer arithmetic ($\mathrm {LIRA}$) in Sect. 5, although completeness for this fragment is left for future work. We show how our procedure can be integrated into the solving architecture used by SMT solvers and how the procedure can be used for solving formulas with arbitrary quantifier alternation in Sect. 6. A key feature of our strategy for handling quantifier alternations is that we do not impose the restriction that quantified formulas must be in prenex normal form. We show how instantiation procedures can be used in part for solving synthesis problems in Sect. 7. Our approach is sound and complete for quantified linear arithmetic and is based purely on quantifier instantiation, which has the advantage of being composable with existing techniques and whose soundness is straightforward to verify. Section 8 gives experimental results for an implementation of the procedures for $\mathrm {LIA}$ and $\mathrm {LRA}$ in the SMT solver cvc4, which in addition to having the aforementioned advantages, outperforms state-of-the-art SMT solvers and theorem provers for quantified linear arithmetic benchmarks.

1.1 Preliminaries

We consider formulas in multi-sorted first-order logic. A signature ${\varSigma }$ consists of a countable set of sort symbols and a set of function symbols. Given a signature ${\varSigma }$, well-sorted terms, atoms, literals, and formulas are defined as usual, and referred to respectively as ${\varSigma }$-terms. We denote by $FV( t )$ the set of free variables occurring in the term t, and extend this notion to formulas. A ${\varSigma }$-term or formula is ground if it has no free variables. We will consider term tuples $(t_1, \ldots , t_n)$, and denote them by letters in bold font, e.g. $\mathbf {t}$. A term written $t[ \mathbf {k} ]$ denotes a term whose free variables are in the tuple $\mathbf {k}$. A formula is closed if it has no free variables.

A ${\varSigma }$-interpretation $\mathcal {I}$ maps

• each set sort symbol $\tau \in {\varSigma }$ to a non-empty set $\tau ^\mathcal {I}$, the domain of $\tau$ in $\mathcal {I}$,

• each function $f \in {\varSigma }$ of sort $\tau _1 \times \cdots \times \tau _n \rightarrow \tau$ to a total function $f^\mathcal {I}$ of sort $\tau ^\mathcal {I}_1 \times \cdots \times \tau ^\mathcal {I}_n \rightarrow \tau ^\mathcal {I}$ where $n > 0$, and to an element of $\tau ^\mathcal {I}$ when $n = 0$, and

• each variable x of sort $\tau$ to an element of $\tau ^\mathcal {I}$.

We write $t^\mathcal {I}$ to denote the interpretation of t in $\mathcal {I}$, defined inductively as usual. A satisfiability relation between ${\varSigma }$-interpretations and ${\varSigma }$-formulas, written $\mathcal {I}\models \varphi$, is also defined inductively as usual. In particular, we assume that $\mathcal {I}\models \lnot \varphi$ if and only if it is not the case that $\mathcal {I}\models \varphi$. We say that $\mathcal {I}$ is a model of $\varphi$ if $\mathcal {I}$ satisfies $\varphi$. Formulas $\varphi _1$ and $\varphi _2$ are equivalent (up to $\mathbf {k}$) if they are satisfied by the same set of models (when restricted to the interpretation of variables $\mathbf {k}$).

A theory is a pair $T = ({\varSigma }, \mathfrak {I})$ where ${\varSigma }$ is a signature and $\mathfrak {I}$ is a non-empty set of ${\varSigma }$-interpretations, the models of T. We assume ${\varSigma }$ contains the equality predicate, which we denote by $\approx$. Let ${\llbracket {\varphi } \rrbracket }_{T}$ denote the set of T-models of $\varphi$. Observe that ${\llbracket {\lnot \varphi } \rrbracket }_{T} = \mathfrak {I}\setminus {\llbracket {\varphi } \rrbracket }_{T}$. A ${\varSigma }$-formula $\varphi [\mathbf {x}]$ is T-satisfiable if it is satisfied by some interpretation in $\mathfrak {I}$ (i.e. ${\llbracket {\varphi } \rrbracket }_{T} \ne \emptyset$). Dually, a ${\varSigma }$-formula $\varphi [\mathbf {x}]$ is T-unsatisfiable if it is satisfied by no interpretation in $\mathfrak {I}$ (i.e. ${\llbracket {\varphi } \rrbracket }_{T} = \emptyset$). A formula $\varphi$ is T-valid if every model of T is a model of $\varphi$ (i.e., ${\llbracket {\varphi } \rrbracket }_{T} = \mathfrak {I}$).

A set ${\varGamma }$ of formulas T-entails a ${\varSigma }$-formula $\varphi$, written ${\varGamma }\models _T \varphi$, if every model of T that satisfies all formulas in ${\varGamma }$ satisfies $\varphi$ as well. A set of literals M propositionally entails a formula $\varphi$, written $M \models _p \varphi$, if M entails $\varphi$ when considering all atomic formulas in $M \cup \varphi$ as propositional variables; such entailment is that of propositional logic and is independent of the theory.

We write $\mathrm {RA}$ (resp. $\mathrm {IA}$) to denote the theory of real (resp. integer) arithmetic. Its signature consists of the sort $\mathsf {Real}$ (resp. $\mathsf {Int}$), the binary predicate symbols > and <, functions $+$ and $\cdot$ denoting addition and multiplication, and the constants of its sort interpreted as usual. We write $t \le s$ as shorthand for $\lnot ( t > s )$, and $t \ge s$ as shorthand for $\lnot ( t < s )$. We write $\mathrm {LRA}$ (resp. $\mathrm {LIA}$) to denote the language of linear real (resp. integer) arithmetic formulas, that is, whose literals are of the form $(\lnot )( c_1 \cdot x_1 + \cdots + c_n \cdot x_n \bowtie c )$ where $c_1, \ldots , c_n, c$ and $x_1, \ldots , x_n$ are non-zero constants and distinct variables of sort $\mathsf {Real}$ (resp. $\mathsf {Int}$) respectively, and $\bowtie$ is one of >, <, or $\approx$. For each literal of this form, there exists an equivalent literal that is in solved form with respect to $x_i$ for each $i= 1, \ldots , n$. That is, an $\mathrm {LRA}$-literal is in solved form with respect to x if it is of the form $(\lnot )( x \bowtie t )$, where $x \not \in FV( t )$. Similarly, an $\mathrm {LIA}$-literal is in solved form with respect to x if it is of the form $(\lnot )( c \cdot x \bowtie t )$, where $x \not \in FV( t )$ and c is an integer constant greater than zero. For integer constants $c_1$ and $c_2$ and non-zero constant c, we write $c_1 \equiv _c c_2$ to denote that $c_1$ and $c_2$ are congruent modulo c, that is $(c_1 \ \mathsf {mod} \ c) = (c_2 \ \mathsf {mod} \ c)$, and we write $c \mid c_1$ if c divides $c_1$.

We write $\mathrm {LIRA}$ to denote the language of mixed linear real and integer arithmetic formulas, that is, linear arithmetic formulas where variables and constants may be of either real or integer sort.

2 Counterexample-guided quantifier instantiation

In this section, we assume a fixed theory T and a language $\mathfrak {L}$ that is closed under negation and such that the satisfiability of finite sets of $\mathfrak {L}$ formulas modulo T is decidable. We present a procedure for checking satisfiability of formulas in the language $\mathcal {Q}( \mathfrak {L} ) = \{ \exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}] \mid \varphi [\mathbf {k}, \mathbf {x}] \in \mathfrak {L}\}$.

Fig. 1

An instantiation-based procedure $\mathcal {P}_{\mathcal {S}}$ for determining the T-satisfiability of $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$, parameterized by selection function $\mathcal {S}$

2.1 An instantiation procedure and its soundness

Figure 1 presents an instantiation-based procedure for determining the satisfiability of a T-formulas $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$, where $\varphi [\mathbf {k}, \mathbf {x}]$ belongs to $\mathfrak {L}$. The procedure introduces a tuple of distinct fresh variables $\mathbf { e }$ of the same sort as $\mathbf {x}$. It maintains a set of formulas ${\varGamma }$, initially empty, and terminates when either ${\varGamma }$ or ${\varGamma }\cup \{ \lnot \varphi [\mathbf {k}, \mathbf {e}] \}$ is T-unsatisfiable. On each iteration, the procedure invokes the subprocedure $\mathcal {S}$ (over which the procedure is parameterized), which returns a tuple of terms $\mathbf {t}[\mathbf {k}]$ whose free variables are a subset of $\mathbf { k }$. We then add to ${\varGamma }$ the formula ${\varphi [\mathbf {k}, \mathbf {t}[\mathbf {k}]]}$. We call $\mathcal {S}$ the selection function of $\mathcal {P}_{\mathcal {S}}$.

Definition 1

A selection function (for $\mathfrak {L}$) takes as arguments an interpretation $\mathcal {I}$, a set of formulas ${\varGamma }$, and a formula $\lnot \varphi [\mathbf { k }, \mathbf {e}]$ in $\mathfrak {L}$, and a tuple of variables $\mathbf {e}$, where $\mathcal {I}\models {\varGamma }\cup \lnot \varphi [\mathbf { k }, \mathbf {e}]$. It returns a tuple of terms $\mathbf {t}[\mathbf {k}]$ such that ${\varphi [\mathbf { k }, \mathbf {t}[\mathbf {k}]]}$ is also in $\mathfrak {L}$.

The intuition of the algorithm in Fig. 1 is to find a subset of the instances of $\forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$ that are either (a) unsatisfiable, and are thus sufficient for showing that $\forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$ is unsatisfiable, or (b) satisfiable and entail $\forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$. The algorithm recognizes the latter case by checking the satisfiability of ${\varGamma }\cup \lnot \varphi [ \mathbf {k}, \mathbf {e}]$ on each iteration of its main loop. In either case, the algorithm may terminate before enumerating all instances of $\forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$.

The procedure above is agnostic to the theory T. We remark that similar instantiation-based procedures have been developed in recent SMT solvers [19, 50]. In this paper, we will focus on instantiation-based procedures for linear arithmetic, giving technical comparisons to existing approaches when applicable.

We first show that the procedure always returns correct results, regardless of the behavior of the selection function, leaving the termination question for the next subsection. We first prove that when the procedure terminates, the input to the procedure is equivalent to ${\varGamma }$. This means that the procedure $\mathcal {P}_{\mathcal {S}}$ can perform quantifier elimination by means of tracking the contents of ${\varGamma }$.

Lemma 1

If $\mathcal {P}_{\mathcal {S}}$ terminates when ${\varGamma }= \{ \varphi [\mathbf {k}, \mathbf {t}_1], \ldots , \varphi [\mathbf {k}, \mathbf {t}_{n}] \}$, then $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$ is equivalent to $\exists \mathbf {k}\, \varphi [\mathbf {k}, \mathbf {t}_1] \wedge \cdots \wedge \varphi [\mathbf {k}, \mathbf {t}_{n}]$.

Proof

First, clearly all models of $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$ also satisfy $\exists \mathbf {k}\, \varphi [\mathbf {k}, \mathbf {t}_1] \wedge \cdots \wedge \varphi [\mathbf {k}, \mathbf {t}_{n}]$, since each $\varphi [\mathbf {k}, \mathbf {t}_i]$ is a consequence of $\forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$.

To show the opposite direction of the equivalence, in the case that $\mathcal {P}_{\mathcal {S}}$ terminates with “unsat”, we have that ${\varGamma }$ is T-unsatisfiable, and thus $\exists \mathbf {k}\, \varphi [\mathbf {k}, \mathbf {t}_1] \wedge \cdots \wedge \varphi [\mathbf {k}, \mathbf {t}_{n}]$ is T-unsatisfiable. Thus, it is vacuously the case that all of its models satisfy $\forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$. In the case that $\mathcal {P}_{\mathcal {S}}$ terminates with “sat”, we have that ${\varGamma }$ is T-satisfiable and ${\varGamma }' = {\varGamma }\cup \{ \lnot \varphi [\mathbf {k}, \mathbf {e}] \}$ is T-unsatisfiable. Since the only formulas added to ${\varGamma }$ are of the form ${\varphi [\mathbf {k}, \mathbf {t}[\mathbf {k}]]}$, the variables $\mathbf { e }$ do not occur in ${\varGamma }$, and thus ${\varGamma }\cup \{ \exists \mathbf {x}\, \lnot \varphi [\mathbf {k}, \mathbf {x}] \}$ is T-unsatisfiable as well. Let $\mathcal {I}$ be a model of ${\varGamma }$. Since $\mathcal {I}$ is not a model of ${\varGamma }\cup \{ \exists \mathbf {x}\, \lnot \varphi [\mathbf {k}, \mathbf {x}] \}$, it must be the case that $\mathcal {I}\not \models \exists \mathbf {x}\, \lnot \varphi [\mathbf {k}, \mathbf {x}]$, and hence $\mathcal {I}$ is a model for $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$. Thus, in this case all models of $\exists \mathbf {k}\, \varphi [\mathbf {k}, \mathbf {t}_1] \wedge \cdots \wedge \varphi [\mathbf {k}, \mathbf {t}_{n}]$ also satisfy $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$. Thus, the lemma holds. $\square$

Corollary 1

If $\mathcal {P}_{\mathcal {S}}$ terminates with “unsat”, then $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$ is T-unsatisfiable.

Proof

$\mathcal {P}_{\mathcal {S}}$ terminates with “unsat” only if ${\varGamma }$ is T-unsatisfiable. Thus by Lemma 1, we have that $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$ is T-unsatisfiable as well. $\square$

Corollary 2

If $\mathcal {P}_{\mathcal {S}}$ terminates with “sat”, then $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$ is T-satisfiable.

Proof

$\mathcal {P}_{\mathcal {S}}$ terminates with “sat” only if ${\varGamma }$ is T-satisfiable. Thus by Lemma 1, we have that $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$ is T-satisfiable as well. $\square$

2.2 Termination of the instantiation procedure

The following properties of selection functions are of interest for showing the procedure $\mathcal {P}_{\mathcal {S}}$ terminates.

Definition 2

(Finite) A selection function $\mathcal {S}$ is finite for $\varphi [\mathbf { k }, \mathbf {e}]$ if there exists a finite set $\mathcal {S}^*( \varphi [\mathbf { k }, \mathbf {e}], \mathbf {e} )$ such that $\mathcal {S}( \mathcal {I}, {\varGamma }, \lnot \varphi [\mathbf { k }, \mathbf {e}], \mathbf {e} ) \in \mathcal {S}^*( \varphi [\mathbf { k }, \mathbf {e}], \mathbf {e} )$ for all $\mathcal {I}$, ${\varGamma }$.

Definition 3

(Monotonic) A selection function $\mathcal {S}$ is monotonic for $\varphi [\mathbf { k }, \mathbf {e}]$ if whenever ${\varGamma }\models \varphi [\mathbf {k}, \mathbf {t}]$, we have that $\mathcal {S}( \mathcal {I}, {\varGamma }, \lnot \varphi [\mathbf { k }, \mathbf {e}], \mathbf {e} ) \ne \mathbf {t}$.

Observe that, if $\mathcal {S}$ is a monotonic selection function, then for any finite list of terms $\mathbf {t}_1, \ldots \mathbf {t}_n$ we have $\mathcal {S}( \mathcal {I}, \{ {\varphi [\mathbf {k}, \mathbf {t_1}]}, \ldots , {\varphi [\mathbf {k}, \mathbf {t_n}]} \}, \lnot \varphi [\mathbf { k }, \mathbf {e}], \mathbf {e} ) \notin \{ \mathbf {t}_1, \ldots , \mathbf {t}_n\}$.

Definition 4

(Model-Preserving) A selection function $\mathcal {S}$ is model-preserving for $\varphi [\mathbf { k }, \mathbf {e}]$ if whenever $\mathcal {S}( \mathcal {I}, {\varGamma }, \lnot \varphi [\mathbf { k }, \mathbf {e}], \mathbf {e} ) = \mathbf {t}$, we have that $\mathcal {I}\models \lnot \varphi [\mathbf { k }, \mathbf {t}]$.

Lemma 2

A selection function that is model-preserving for $\varphi [\mathbf { k }, \mathbf {e}]$ is also monotonic for $\varphi [\mathbf { k }, \mathbf {e}]$.

Proof

Assume that $\mathcal {S}$ is model-preserving for $\varphi [\mathbf { k }, \mathbf {e}]$ and that $\mathcal {S}( \mathcal {I}, {\varGamma }, \lnot \varphi [\mathbf { k }, \mathbf {e}], \mathbf {e} ) = \mathbf {s}$. By definition of model-preserving, we have that $\mathcal {I}\models \lnot \varphi [\mathbf { k }, \mathbf {s}]$. Thus, for each $\mathbf {t}$ such that $\mathcal {I}\models \varphi [\mathbf { k }, \mathbf {t}]$, we have that $\mathbf {s} \ne \mathbf {t}$. Thus, $\mathcal {S}$ is monotonic for $\varphi [\mathbf { k }, \mathbf {e}]$. $\square$

Theorem 1

If $\mathcal {S}$ is finite and monotonic for $\varphi [\mathbf { k }, \mathbf {e}]$ in $\mathfrak {L}$, then $\mathcal {P}_{\mathcal {S}}$ is a (terminating) decision procedure for the T-satisfiability of $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$.

Proof

Given a monotonic and finite $\mathcal {S}$, the procedure $\mathcal {P}_{\mathcal {S}}$ can only execute a finite number of iterations. Assuming a decision procedure for determining the T-satisfiability of T-formulas in $\mathfrak {L}$, $\mathcal {P}_{\mathcal {S}}( \exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}] )$ must terminate. By Corollaries 1 and 2, $\mathcal {P}_{\mathcal {S}}$ is a decision procedure for the T-satisfiability of $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$. $\square$

By this result, we obtain a sound and complete instantiation strategy from Fig. 1 by virtue of constructing a selection function that is finite and monotonic for formulas residing in a language $\mathfrak {L}$ of interest. It is important to note that the property of being both finite and monotonic is a sufficient condition of a selection function for proving the termination of an instantiation-based procedure according to the algorithm in Fig. 1, although it is not the only sufficient condition for doing so.

Fig. 2

A selection function $\mathcal {S}_{\mathrm {LRA}}$ for linear real arithmetic $\mathrm {LRA}$. Each $\prec$ is either < or $\le$; $\delta ^\ell _i$ is $\delta$ if the $i\mathrm{th}$ lower bound for $\mathsf {e}$ is strict, and 0 otherwise. Similarly, each $\succ$ is either > or $\ge$; $\delta ^u_j$ is $\delta$ if the $j\mathrm{th}$ upper bound for $\mathsf {e}$ is strict, and 0 otherwise

In this paper we will construct selection functions $\mathcal {S}$ that are finite and monotonic for all $\varphi [\mathbf {k}, \mathbf {x}]$ in quantifier-free linear real and integer arithmetic.

3 Instantiation for $\mathrm {LRA}$-formulas

Consider the case where $\mathbf {k}$ and $\mathbf {x}$ are vectors of $\mathsf {Real}$ variables and $\mathfrak {L}$ is the class of quantifier-free $\mathrm {LRA}$-formulas $\varphi [ \mathbf {k}, \mathbf {x} ]$. For simplicity of the presentation, we assume that equalities are eliminated from $\varphi$ by the transformation:

$$\begin{aligned} t \approx 0 {{\mathrm{\ \leadsto \ }}}0 \le t \wedge 0 \ge t \end{aligned}$$

As a result of Theorem 1, to devise a sound and complete instantiation-based procedure for deciding the satisfiability of $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [ \mathbf {k}, \mathbf {x} ]$, it suffices to devise a finite and monotonic selection function for $\mathrm {LRA}$, which we describe in the following.

Figure 2 gives a selection function $\mathcal {S}_{\mathrm {LRA}}$ for $\mathrm {LRA}$, which takes an interpretation $\mathcal {I}$, a set of formulas ${\varGamma }$, the formula $\lnot \varphi [\mathbf { k }, \mathbf { e}]$, and the tuple of variables $\mathbf {e}$. It invokes the recursive procedure $S_R$ which constructs a term corresponding to each variable in $\mathbf { e }$. Analogous to existing approaches for linear quantifier elimination [36, 43], we assume that the signature of linear real arithmetic contains non-standard terms for symbolically representing substitutions (often referred to as virtual terms). In particular, we consider a signature that contains a free distinguished constant $\delta$ of sort $\mathsf {Real}$, representing an infinitesimal positive value. Any quantifier-free constraint containing $\delta$ is equivalent to one that does not by the transformations:

$$\begin{aligned} \begin{array}{r@{}c@{}l@{}c@{}r@{}c@{}l@{}l} \delta< t&{{\mathrm{\ \leadsto \ }}}&0 < t&\quad \text { and }&\quad \delta > t&{{\mathrm{\ \leadsto \ }}}&0 \ge t&\quad \text { where } \delta \not \in FV( t ). \end{array} \end{aligned}$$

Thus we may assume without loss of generality that $\lnot \varphi [\mathbf { k }, \mathbf { e}]$ contains no occurrence of $\delta$.

For each variable $\mathsf {e}_i$ from $\mathbf { e }$, the procedure $S_R$ invokes the (non-deterministic) subprocedure $S_{R0}$, which chooses a term corresponding to $\mathsf {e}_i$ based on a set of literals M over the atoms of $\psi$ which propositionally entail $\psi$ and are satisfied by $\mathcal {I}$, which we call a propositionally satisfying assignment for $\psi$. We partition M into three sets $M_\ell$, $M_u$ and $M_c$, where $M_\ell$ contains literals that correspond to lower bounds for $\mathsf {e}$, $M_u$ contains literals that correspond to upper bounds for $\mathsf {e}$, and $M_c$ contains the remaining literals. The sets $M_\ell$ and $M_u$ are equivalent to sets of literals that are in solved form with respect to $\mathsf {e}$. When $M_\ell$ contains at least one literal, we may return the lower bound whose value is maximal according to $\mathcal {I}$, and similarly for $M_u$. If both $M_\ell$ and $M_u$ are empty, we return the term 0. When $S_{R0}$ returns the term $t_i$, we apply the substitution $\{ \mathsf {e}_i \mapsto t_i \}$ to $\psi$ and $\mathbf {t}$, and append $t_i$ to $\mathbf {t}$. Terms returned by $S_{R0}$ may involve the constant $\delta$. We define a satisfiability relation between models and formulas involving $\delta$, as well as the $\mathsf {max}$ and $\mathsf {min}$ function for terms involving $\delta$ in the obvious way, such that $( t_1 + c_1 \cdot \delta )^\mathcal {I}> ( t_2 + c_2 \cdot \delta )^\mathcal {I}$ if either $t_1^\mathcal {I}> t_2^\mathcal {I}$ or both $t_1^\mathcal {I}= t_2^\mathcal {I}$ and $c_1 > c_2$.

Overall, $\mathcal {S}_{\mathrm {LRA}}$ returns a tuple of terms $\mathbf {t}$, after which we add ${\varphi [ \mathbf { k}, \mathbf {t}]}$ to ${\varGamma }$ in Fig. 1.

Lemma 3

$\mathcal {S}_{\mathrm {LRA}}$ is finite for $\varphi [ \mathbf { k }, \mathbf { e} ]$.

Proof

We first show only a finite number of terms can be returned by $S_{R0}( \mathcal {I}, (\lnot \varphi [\mathbf { k}, \mathbf { e}])\sigma , \mathsf {e} )$ for any $\mathcal {I}, \sigma , \mathsf {e}$. Let A be the set of atoms occurring in $\varphi [ \mathbf { k }, \mathbf { e }] \sigma$. The literals in satisfying assignments of $(\lnot \varphi [\mathbf { k}, \mathbf { e}] )\sigma$ are over these atoms. Let $\{ \mathsf {e}>t_1, \ldots , \mathsf {e}>t_n, \mathsf {e}<s_1, \ldots , \mathsf {e}<s_m \}$ be the set of atoms that are in solved form with respect to $\mathsf {e}$ that are equivalent to the atoms of A containing $\mathsf {e}$, where $\mathsf {e} \not \in FV( t_1, \ldots , t_n, s_1, \ldots , s_m )$. The terms returned by $S_{R0}( \mathcal {I}, ( \lnot \varphi [\mathbf { k}, \mathbf { e}] )\sigma , \mathsf {e} )$ are in the set:

$$\begin{aligned} \begin{array}{c} \{ 0, t_1 (+ \delta ), \ldots , t_n (+ \delta ), s_1 (- \delta ), \ldots , s_m (- \delta ) \} \end{array} \end{aligned}$$

Notice that literals over the atoms in A may occur either with positive or negative polarity in M. Thus for each literal $\mathsf {e} < t_i$ for $i = 1, \ldots , n$, $S_{R0}$ may either return $t_i + \delta$ when considering $(\mathsf {e}>t_i)$ in M as a lower bound for $\mathsf {e}$, or $t_i$ when considering $\lnot ( \mathsf {e} > t_i )$ in M, which is equivalent to $( \mathsf {e} \le t_i )$, as an upper bound for $\mathsf {e}$. Similarly we consider two cases for each literal $\mathsf {e} > s_i$ for $i = 1, \ldots , m$. Since there are only a finite number of recursive calls to $S_R$ within $\mathcal {S}_{\mathrm {LRA}}$, and each call appends only a finite number of possible terms to $\mathbf {t}$, the set of possible return values of $\mathcal {S}_{\mathrm {LRA}}$ is finite, and thus it is finite for $\varphi [ \mathbf { k }, \mathbf { e} ]$. $\square$

Lemma 4

If $\mathcal {I}$ is a model for $\mathrm {LRA}$ and for the quantifier-free formula $\psi$, then $\mathcal {I}$ is also a model for $\psi \{ \mathsf {e} \mapsto S_{R0}( \mathcal {I}, \psi , \mathsf {e} ) \}$.

Proof

Let M be a set of literals of the form described in the definition of $S_{R0}$ for $\mathcal {I}$, $\psi$ and $\mathsf {e}$. Consider the case where $S_{R0}( \mathcal {I}, \psi , \mathsf {e} ) = \ell _i + \delta ^\ell _i$ for some i, where $n>0$. We show that $\mathcal {I}$ satisfies $M \{ \mathsf {e} \mapsto \ell _i + \delta ^\ell _i \}$. First, since $\mathsf {max} \{ (\ell _1 + \delta ^\ell _1)^\mathcal {I}, \ldots , (\ell _n + \delta ^\ell _n)^\mathcal {I}\} = (\ell _i + \delta ^\ell _i)^\mathcal {I}$, we know that $\mathcal {I}$ satisfies $M_\ell \{ \mathsf {e} \mapsto \ell _i + \delta ^\ell _i \}$. In the case that the bound on $\mathsf {e}$ we consider is strict, that is, $\mathsf {e} > \ell _i \in M_\ell$, then $\delta ^\ell _i$ is $\delta$, and $\ell _i^\mathcal {I}< u_j^\mathcal {I}$ for all $j \in \{ 1, \ldots , m \}$. Thus, $\mathcal {I}$ satisfies $(\ell _i + \delta \prec u_j) = (\mathsf {e} \prec u_j) \{ \mathsf {e} \mapsto \ell _i + \delta \}$. In the case that the bound on $\mathsf {e}$ we consider is non-strict, that is, if $\mathsf {e} \ge \ell _i \in M_\ell$, then $\delta ^\ell _i$ is 0, and $\ell _i^\mathcal {I}\le u_j^\mathcal {I}$ for all $j \in \{ 1, \ldots , m \}$. Thus, $\mathcal {I}$ satisfies $(\ell _i \prec u_j) = (\mathsf {e} \prec u_j) \{ \mathsf {e} \mapsto \ell _i \}$. In either case, we have that $\mathcal {I}$ satisfies each literal in $M_u \{ \mathsf {e} \mapsto \ell _i + \delta ^\ell _i \}$. Finally, $\mathcal {I}$ clearly satisfies $M_c \{ \mathsf {e} \mapsto \ell _i + \delta ^\ell _i \} = M_c$. The case when $m>0$ is symmetric to the case when $n>0$. In the case where $n=0$ and $m=0$, we have that $\psi$ does not contain $\mathsf {e}$, and $\mathcal {I}$ satisfies $M \{ \mathsf {e} \mapsto 0 \}$. In each case, $\mathcal {I}$ satisfies $M \{ \mathsf {e} \mapsto S_{R0}( \mathcal {I}, \psi , \mathsf {e} ) \}$, which entails $\psi \{ \mathsf {e} \mapsto S_{R0}( \mathcal {I}, \psi , \mathsf {e} ) \}$, and thus the lemma holds. $\square$

Lemma 5

$\mathcal {S}_{\mathrm {LRA}}$ is model-preserving for $\varphi [ \mathbf { k }, \mathbf { e} ]$.

Proof

Assume $\mathcal {S}_{\mathrm {LRA}}( \mathcal {I}, {\varGamma }, \lnot \varphi [\mathbf { k }, \mathbf { e}], \mathbf {e} )$ returns $\mathbf {t}$. By definition of selection function, $\mathcal {I}$ and $\lnot \varphi [\mathbf { k }, \mathbf { e}]$ are such that $\mathcal {I}\models \lnot \varphi [\mathbf { k }, \mathbf { e}]$. By repeated applications of Lemma 4, we have that $\mathcal {I}$ satisfies all inputs $\psi$ to $S_R$. When $S_R$ terminates, $\psi$ is $\lnot \varphi [\mathbf { k }, \mathbf { t}]$, and thus $\mathcal {I}\models \lnot \varphi [\mathbf { k }, \mathbf { t }]$. $\square$

Theorem 2

$\mathcal {P}_{\mathcal {S}_{\mathrm {LRA}}}$ is a sound and complete procedure for determining the $\mathrm {LRA}$-satisfiability of $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$.

Proof

By Theorem 1 and Lemma 2 of our framework as well as $\mathrm {LRA}$-specific Lemma 3 and Lemma 5. $\square$

We illustrate the procedure through examples. $S_{R0}$ is non-deterministic; we choose instantiations only based on the lower bounds $M_\ell$ found in the procedure $S_{R0}$, though the procedure is free to choose its instantiations based on the upper bounds $M_u$ as well. We underline the literal in $M_\ell$ corresponding to the bound whose value is maximal in $\mathcal {I}$. ${\varGamma }$ is initially empty and on each iteration ${\varGamma }'$ is the union of ${\varGamma }$ and the Skolemized negation $\lnot \varphi [ \mathbf {e}]$ of the input formula $\forall \mathbf {x}\,\varphi [\mathbf {x}]$, where $\mathbf {e}$ are fresh variables of the same sort as $\mathbf {x}$. Each round of $\mathcal {S}_{\mathrm {LRA}}$ computes a tuple $\mathbf {t}[\mathbf { k}]$, which is used to instantiate our quantified formula in Fig. 1. The last column shows the corresponding instance of the quantified formula after simplification, including the elimination of $\delta$.

Example 1

Consider the formula $\forall x\, ( x \le a \vee x \le b )$. Let e be a fresh Skolem variable of the same sort ($\mathsf {Real}$) as x. The Skolemized negation of this formula is $\lnot ( e \le a \vee e \le b )$, which simplifies to $(e> a \wedge e > b)$. The iterations of the loop of $\mathcal {P}_{\mathcal {S}_{\mathrm {LRA}}}$ are summarized in the following table, where ${\varGamma }$ is initially empty, and ${\varGamma }'$ is obtained by adding $(e> a \wedge e > b)$ to ${\varGamma }$ on each iteration.

			$S_{R0}( \mathcal {I}, \psi , \mathsf {e}$)
#	${\varGamma }$	${\varGamma }'$	$\mathsf {e}$	$M_{\ell }$	Return	$\mathbf {t}[\mathbf { k}]$	$\text {Add to } {\varGamma }$
1	sat	sat	e	$\{ \underline{e> a}, e > b \}$	$a + \delta$	$(a+\delta )$	$a < b$
2	sat	sat	e	$\{ e> a, \underline{e>b} \}$	$b + \delta$	$(b+\delta )$	$b < a$
3	unsat

On the first iteration, ${\varGamma }$ and ${\varGamma }' = \{ e> a \wedge e > b \}$ are satisfiable by a model, call it $\mathcal {I}_1$, where assume that $e^{\mathcal {I}_1} =2, a^{\mathcal {I}_1} = 1, b^{\mathcal {I}_1} = 0$. We call $S_{R0}$ with inputs $\mathcal {I}_1$, $(e> a \wedge e > b)$, and e. A propositionally satisfying assignment M for $(e> a \wedge e > b)$ includes both these literals, and the set of lower bounds $M_\ell$ for e on this iteration is $\{ e> a, e > b \}$. Since $a^{\mathcal {I}_1} > b^{\mathcal {I}_1}$, the procedure $S_{R0}$ finds that the literal $e > a$ gives the maximal lower bound for e, and hence it returns the term $a + \delta$. The disjuncts of the instance $a+\delta \le a \vee a+\delta \le b$ added to ${\varGamma }$ on the first iteration simplify to $\bot$ and $a < b$ respectively. On the second iteration, ${\varGamma }$ and ${\varGamma }' = \{ e> a \wedge e > b, a < b \}$ are still satisfiable with a model, call it $\mathcal {I}_2$, where assume that $e^{\mathcal {I}_2} =2, a^{\mathcal {I}_2} = 0, b^{\mathcal {I}_2} = 1$. Since now $b^{\mathcal {I}_2} > a^{\mathcal {I}_2}$, we have that b is now the maximal lower bound for e. Hence, $S_{R0}$ returns $b + \delta$ on the second iteration, and we add the formula $b < a$ to ${\varGamma }$. On the third iteration, ${\varGamma }$ contains both $a<b$ and $b<a$ and hence is $\mathrm {LRA}$-unsatisfiable. Overall, this run shows $\exists ab\, \forall x\, ( a \ge x \vee x \ge b )$ is $\mathrm {LRA}$-unsatisfiable. $\square$

Example 2

To demonstrate how multiple universally quantified variables are handled, consider the formula $\forall xy\, ( x+y< a \vee x-y < b )$ whose Skolemized negation after simplification is $e_1+e_2 \ge a \wedge e_1-e_2 \ge b$. A possible run of $\mathcal {P}_{\mathcal {S}_{\mathrm {LRA}}}$ is as follows.

			$S_{R0}( \mathcal {I}, \psi , \mathsf {e} )$
#	${\varGamma }$	${\varGamma }'$	$\mathsf {e}$	$M_\ell$	Return	$\mathbf {t}[\mathbf { k}]$	$\text {Add to } {\varGamma }$
1	sat	sat	$e_1$	$\{ e_1 \ge a - e_2, \underline{e_1 \ge b + e_2} \}$	$b + e_2$
			$e_2$	$\{ \underline{e_2 \ge \frac{a-b}{2}} \}$	$\frac{a-b}{2}$	$( \frac{a+b}{2},\frac{a-b}{2} )$	$\bot$
2	unsat

On the first iteration, since ${\varGamma }$ and ${\varGamma }'$ are satisfiable say with model $\mathcal {I}_1$, we first call $S_{R0}$ on $\mathcal {I}_1$, $( e_1+e_2 \ge a \wedge e_1-e_2 \ge b )$, and $e_1$. The set $M_\ell$ contains inequalities that are in solved form with respect to $e_1$ that correspond to lower bounds for $e_1$ in $(e_1+e_2 \ge a \wedge e_1-e_2 \ge b)$, which are $\{ e_1 \ge a - e_2 \wedge e_1 \ge b + e_2 \}$. Assuming $b + e_2$ is the maximal lower bound for $e_1$, $S_{R0}$ returns $b + e_2$. In the procedure $S_R$, we then apply the substitution $\{ e_1 \mapsto b + e_2 \}$ to $(e_1+e_2 \ge a \wedge e_1-e_2 \ge b)$, giving us $(b + e_2 + e_2 \ge a \wedge b + e_2 - e_2 \ge b)$, which simplifies to $e_2 \ge \frac{a-b}{2}$. Calling $S_{R0}$ again with input $\mathcal {I}_1$, this formula, and $e_2$, we have that $M_\ell$ now is the set $\{ e_2 \ge \frac{a-b}{2} \}$, and thus $S_{R0}$ returns $\frac{a-b}{2}$ for $e_2$. We apply the substitution $\{ e_2 \mapsto \frac{a-b}{2} \}$ to the term $b + e_2$ we computed for $e_1$, giving us $b + \frac{a-b}{2}$, which simplifies to $\frac{a+b}{2}$. Overall, $\mathcal {S}_{\mathrm {LRA}}$ returns the tuple of terms $( \frac{a+b}{2},\frac{a-b}{2} )$. Applying the substitution $\{ x \mapsto \frac{a+b}{2}, y \mapsto \frac{a-b}{2} \}$ to our input formula results in the formula $( \frac{a+b}{2}+\frac{a-b}{2}< a \vee \frac{a+b}{2}-\frac{a-b}{2} < b )$, which simplifies to $\bot$. This run shows $\exists ab\, \forall xy\, ( x+y< a \vee x-y < b )$ is $\mathrm {LRA}$-unsatisfiable. $\square$

Example 3

To demonstrate how quantified formulas with Boolean structure are handled, consider the formula $\forall x\, ( ( a< x \wedge x< b ) \vee x < a+b )$ whose Skolemized negation is $( a \ge e \vee e \ge b ) \wedge e \ge a+b$. A possible run of $\mathcal {P}_{\mathcal {S}_{\mathrm {LRA}}}$ is as follows.

			$S_{R0}( \mathcal {I}, \psi , \mathsf {e} )$
#	${\varGamma }$	${\varGamma }'$	$\mathsf {e}$	$M_\ell$	$\text {Return}$	$\mathbf {t}[\mathbf { k}]$	$\text {Add to } {\varGamma }$
1	sat	sat	e	$\{ \underline{e \ge a+b} \}$	$a+b$	$(a+b)$	$0< b \wedge a < 0$
2	sat	sat	e	$\{ \underline{ e \ge b}, e \ge a+b \}$	b	(b)	$0 < a$
3	unsat

On the first iteration, we have that ${\varGamma }$ and ${\varGamma }' = \{ ( a \ge e \vee e \ge b ) \wedge e \ge a+b \}$ are satisfiable with a model, call it $\mathcal {I}_1$. In the above run, we assume that $\mathcal {I}_1$ satisfies $a \ge e$ but not $e \ge b$, and hence $e \ge b$ is not included as a lower bound in $M_\ell$. We return the instance for $\{ x \mapsto a+b \}$, which simplifies to $0< b \wedge a < 0$. On the second iteration, the model for ${\varGamma }'$, call it $\mathcal {I}_2$, must now satisfy $0< b \wedge a < 0$, and hence $b^{\mathcal {I}_2}> (a+b)^{\mathcal {I}_2} > a^{\mathcal {I}_2}$. Since $\mathcal {I}_2$ satisfies $e \ge a+b$, it cannot satisfy $a \ge e$, and hence it must satisfy $e \ge b$. Thus, on this iteration, $M_\ell$ contains $e \ge b$ and $e \ge a+b$. Moreover since $b^{\mathcal {I}_2} > (a+b)^{\mathcal {I}_2}$, we know that b must be the maximal lower bound for e, and hence we return an instance based on $\{ x \mapsto b \}$, which simplifies to $0 < a$, after which we find that ${\varGamma }$ is unsatisfiable. This run shows $\exists ab\, \forall x\, ( ( a< x \wedge x< b ) \vee x < a+b )$ is $\mathrm {LRA}$-unsatisfiable. $\square$

Example 4

To demonstrate a case where a variable has no bounds, consider the formula $\forall xy\, (x \le y)$, whose Skolemized negation is $e_1 > e_2$. A possible run of $\mathcal {P}_{\mathcal {S}_{\mathrm {LRA}}}$ on this input is as follows.

			$S_{R0}( \mathcal {I}, \psi , \mathsf {e} )$
#	${\varGamma }$	${\varGamma }'$	$\mathsf {e}$	$M_\ell$	Return	$\mathbf {t}[\mathbf { k}]$	$\text {Add to } {\varGamma }$
1	sat	sat	$e_1$	$\{ \underline{e_1 > e_2} \}$	$e_2$ + $\delta$
			$e_2$	$\emptyset$	0	$( \delta , 0 )$	$\bot$
2	unsat

On the first iteration, after choosing $e_2 + \delta$ for $e_1$, we apply the substitution $\{ e_1 \mapsto e_2 + \delta \}$ to ${\varGamma }'$, giving us the set containing $e_2 + \delta > e_2$, which simplifies to $\top$. Thus when using $S_{R0}$ to choose a term for $e_2$, we have that $M_\ell$ contains neither an upper nor a lower bound for $e_2$, and hence we choose to return the value 0. The instance of our input formula corresponding to the substitution $\{ x \mapsto \delta , y \mapsto 0 \}$ simplifies to $\bot$. This run shows $\forall xy\, (x \le y)$ is $\mathrm {LRA}$-unsatisfiable. $\square$

Example 5

To demonstrate a non-trivial case using the infinitesimal $\delta$, consider the formula $\forall xy\, (x \le 0 \vee y - 2 \cdot x \le 0)$ whose Skolemized negation is $e_1> 0 \wedge e_2 - 2 \cdot e_1 > 0$. A possible run of $\mathcal {P}_{\mathcal {S}_{\mathrm {LRA}}}$ on this input is as follows.

			$S_{R0}( \mathcal {I}, \psi , \mathsf {e} )$
#	${\varGamma }$	${\varGamma }'$	$\mathsf {e}$	$M_\ell$	Return	$\mathbf {t}[\mathbf { k}]$	$\text {Add to } {\varGamma }$
1	sat	sat	$e_1$	$\{ \underline{e_1 > 0} \}$	$\delta$
			$e_2$	$\{ \underline{e_2 > 2 \cdot \delta } \}$	$3 \cdot \delta$	$( \delta , 3 \cdot \delta )$	$\bot$
2	unsat

The instance corresponding to the substition $\{ x \mapsto \delta , y \mapsto 3 \cdot \delta \}$ is $(\delta \le 0 \vee 3 \cdot \delta - 2 \cdot \delta \le 0)$, which simplifies to $( \delta \le 0 \vee \delta \le 0 )$, which after eliminating $\delta$ simplifies to $\bot$. This run shows $\forall xy\, (x \le 0 \vee y - 2 \cdot x \le 0)$ is $\mathrm {LRA}$-unsatisfiable. $\square$

The procedure $\mathcal {P}_{\mathcal {S}_{\mathrm {LRA}}}$, which is an instance of the procedure in Fig. 1, can be understood as lazily enumerating the disjuncts of the Loos–Weispfenning method for quantifier elimination over linear real arithmetic [36], with minor differences which we discuss in the next section. In this way, our approach is similar to the projection-based procedures described in [13, 32]. These approaches compute implicants of quantified formulas, while our approach instead computes a term which is in turn used for instantiation. For our purposes, computing a term instead of an implicant has several advantages. In particular, it allows the instantiation-based procedure to be used as a subprocedure for synthesis, which we describe in Sect. 7, and enables a uniform combination of the approach with existing instantiation-based techniques for first-order logic [18, 24, 51].

3.1 Comparison to existing approaches

Recent approaches (including ours) for solving quantified linear arithmetic share similarities with one another. In particular, given an existentially quantified formula $\exists \mathbf {x}. \varphi$, based on some strategy, they enumerate (possibly lazily) a finite set of ground formulas that are entailed by this formula. We give a brief overview contrasting the technical details of existing approaches in this section.

We have mentioned that the approach in Fig. 2 involves the use of a free distinguished constant $\delta$, representing an infinitesimal positive value. Other approaches also involve use of a free distinguished constant $\infty$, representing an arbitrarily large positive value. Like $\delta$, this term can be eliminated from quantifier-free constraints, noting:

$$\begin{aligned} \begin{array}{r@{}c@{}l@{}c@{}r@{}c@{}l@{}l} \infty < t&{{\mathrm{\ \leadsto \ }}}&\bot&\quad \text { and }&\quad \infty > t&{{\mathrm{\ \leadsto \ }}}&\top&\quad \text { where } \infty \not \in FV( t ). \end{array} \end{aligned}$$

Fig. 3

An alternative return value for $S_{R0}$ that is analogous to Loos and Weispfenning’s method

Fig. 4

An alternative return value for $S_{R0}$ that is analogous to Ferrante and Rackoff’s method

The two most widely known algorithms for quantifier elimination for linear real arithmetic are the method based on virtual term substitution by Loos and Weispfenning [36], and the method based on interior points by Ferrante and Rackoff [23]. In the context of our approach, two alternatives for the return value of $S_{R0}$ (Figs. 3 and 4) closely approximate the effect of these methods.

Recent approaches are inspired by of one (or both) of these methods. The approaches described in [13, 32] are closely based on the Loos–Weispfenning method, and the approach described in [19] is closely based on Ferrante–Rackoff method. The approach described in [43] examines a certified version of both approaches. The approach in Fig. 2 is inspired by the Loos–Weispfenning method, but does not use infinities.

Fig. 5

An alternative return value for $S_{R0}$

Another possible return value is given in Fig. 5 that does not use any virtual terms. The approach in Fig. 5 may be advantageous when considering quantified formulas having nested quantification, where eliminating virtual terms from quantified constraints is not obvious.

4 Instantiation for $\mathrm {LIA}$-formulas

We now turn our attention to the class of $\mathrm {LIA}$-formulas $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [ \mathbf {k}, \mathbf {x} ]$, where $\mathbf {x}$ and $\mathbf {k}$ are vectors of $\mathsf {Int}$ variables, and $\varphi [ \mathbf {k}, \mathbf {x} ]$ is quantifier-free. We again assume all equalities are eliminated from $\varphi$ by replacing them with a conjunction of inequalities. Additionally, we assume the signature of integer arithmetic is extended with symbols $\small \mathsf {div}^{+}$ and $\small \mathsf {div}^{-}$, denoting integer division rounding up and down respectively, and that the language of $\mathrm {LIA}$ includes terms of the form $t\ \small \mathsf {div}^p\ c$, where $p \in \{ +, - \}$ and c is a non-zero integer constant. All occurrences of these symbols can be eliminated from any quantifier-free formula $\varphi$ by repeated applications of the transformation:

$$\begin{aligned} \varphi [ t\ \small \mathsf {div}^p \ c] {{\mathrm{\ \leadsto \ }}}\varphi [ d ] \wedge c \cdot d\approx t\pm ^p m \wedge 0 \le m < c \end{aligned}$$

(1)

where d and m are distinct fresh variables, and $\pm ^p$ is $+$ if p is $+$ and analogously for −.

Fig. 6

A selection function $\mathcal {S}_{\mathrm {LIA}}$ for linear integer arithmetic $\mathrm {LIA}$

Figure 6 gives a selection function $\mathcal {S}_{\mathrm {LIA}}$ for $\mathrm {LIA}$. The procedure invokes the recursive procedure $S_I$, which takes as arguments $\mathcal {I}$, $\lnot \varphi [\mathbf { k },\mathbf { e}]$, variables $\mathbf { e }$ that we have yet to incorporate into the substitutions, an integer $\theta$, terms $\mathbf { t }$ found as substitutions for variables from $\mathbf { e }$ so far, and a tuple of symbols $\mathbf {p}$ from $\{ +, - \}$ which we refer to as polarities. Due to the transformation (1), we may assume without loss of generality that $\lnot \varphi [\mathbf { k },\mathbf { e}]$ contains no instance of integer division. The role of $\theta$ will be to capture divisibility relationships through the procedure, where $\theta$ is initially 1. The procedure invokes a call to $S_{I0}( \mathcal {I}, \psi , \mathsf {e}_i, \theta )$ which based on the propositionally satisfying assignment for $\psi$ returns a tuple of the form $(c, t_i, p_i)$, where c is a constant, $t_i$ is a term, and $p_i$ is a polarity. The procedure for constructing the term $t_i$ in the procedure $S_{I0}$ is similar to the procedure $S_{R0}$ in the previous section, where we find the lower bound of the form $c_i \cdot \mathsf {e} \ge \ell _i$ such that the (rational) value $( \frac{\ell _i}{ c_i } )^\mathcal {I}$ is maximal, and similarly for $M_u$. Additionally, $S_{I0}$ adds a constant $\rho$ to the maximal lower bound (resp. subtracts a constant from the minimal lower bound). This constant ensures that the returned term $t_i$ and $\mathsf {e}$ are congruent modulo $\theta \cdot c$ in $\mathcal {I}$, a fact which in part suffices to show the overall function to be model-preserving. It then constructs a substitution with coefficients $\sigma$ of the form $\{ c \cdot \mathsf {e}_i \mapsto t_i \}$, where $c \ne 0$. A substitution of this form may be applied to integer terms of the form $c \cdot ( d \cdot \mathsf {e}_i + s )$ where $\mathsf {e}_i \not \in FV( s )$ and $( c \cdot ( d \cdot \mathsf {e}_i + s ) ) \sigma$ is defined as $d \cdot t_i + c \cdot s$. Additionally, we define $( s_1 \bowtie s_2 )\sigma$ as $( c \cdot s_1 ) \sigma \bowtie ( c \cdot s_2 ) \sigma$ for $\bowtie \in \{ <, > \}$, and thus we can apply $\sigma$ to arbitrary $\mathrm {LIA}$-formulas. After constructing $\sigma$, the procedure $S_I$ invokes a recursive call where $\sigma$ is applied to $\psi$ and $(c \cdot \mathbf {t})$, $\theta$ is multiplied by c, the term $\theta \cdot t_i$ is appended to $\mathbf {t}$, and $p_i$ is appended to $\mathbf {p}$.

Overall, $\mathcal {S}_{\mathrm {LIA}}$ returns a vector of terms $(\mathbf {t}\ \small \mathsf {div}^{\mathbf {p}} \ \theta )$, that is, integer division applied pairwise to the terms in $\mathbf {t}$ and the constant $\theta$, where $\mathbf {p}$ determines whether this division rounds up or down. When using this selection function in the context of Fig. 1, the instance ${\varphi [ \mathbf { k}, \mathbf {t}\ \small \mathsf {div}^{\mathbf {p}} \ \theta ]}$ is added to ${\varGamma }$. Note that our selection function chooses $\mathbf {p}$ such that integer division rounds up for terms coming from lower bounds, and rounds down for terms coming from upper bounds. This choice is not required for correctness, but can reduce the number of instances needed for showing unsatisfiability.

Lemma 6

$\mathcal {S}_{\mathrm {LIA}}$ is finite for $\varphi [ \mathbf { k }, \mathbf { e } ]$.

Proof

First, we show only a finite number of tuples are returned by $S_{I0}( \mathcal {I}, ( \lnot \varphi [\mathbf { k}, \mathbf { e}] )\sigma , \mathsf {e}, \theta )$ for any $\mathcal {I}, \sigma , \mathsf {e}$ and finite $\theta$. Let A be the set of atoms occurring in $\varphi [ \mathbf { k }, \mathsf {e}_i ] \sigma$. The literals in satisfying assignments of $(\lnot \varphi [\mathbf { k}, \mathbf { e}] )\sigma$ are over these atoms. Let $\{ a_1 \cdot \mathsf {e}> t_1, \ldots , a_n \cdot \mathsf {e} > t_n, b_1 \cdot \mathsf {e}< s_1, \ldots , b_m \cdot \mathsf {e} < s_m \}$ be the set of atoms that are in solved form with respect to $\mathsf {e}$ and are equivalent to the atoms of A that contain $\mathsf {e}$, where we have $\mathsf {e}_i \not \in FV( t_1, \ldots , t_n, s_1, \ldots , s_m )$ and $a_1> 0, \ldots , a_n> 0, b_1> 0, \ldots , b_m > 0$. The tuples returned by the call to $S_{I0}( \mathcal {I}, ( \lnot \varphi [\mathbf { k}, \mathbf { e}] )\sigma , \mathsf {e}, \theta )$ are in the set:

$$\begin{aligned} \left\{ \left( a_i, t_i - \rho , - \right) \mid 1 \le i \le n, 0 \le \rho< \theta \cdot a_i \right\}&\cup&\\ \left\{ \left( a_i, t_i+1+\rho , + \right) \mid 1 \le i \le n, 0 \le \rho< \theta \cdot a_i \right\}&\cup&\\ \left\{ \left( b_i, s_i-1-\rho , - \right) \mid 1 \le i \le m, 0 \le \rho< \theta \cdot b_i \right\}&\cup&\\ \left\{ \left( b_i, s_i+\rho , + \right) \mid 1 \le i \le m, 0 \le \rho< \theta \cdot b_i \right\}&\cup&\left\{ \left( 1, \rho , + \right) \mid 0 \le \rho < \theta \right\} \end{aligned}$$

Notice that since atoms can appear positively or negatively in M, we consider two possible tuples for each literal in the above set. Since $\theta$ is finite, there are a finite number of tuples of this form. Since there are only a finite number of recursive calls to $S_I$ within $\mathcal {S}_{\mathrm {LIA}}$, and each call modifies $\mathbf {t}$ based a finite number of possible tuples coming from the set above, the set of possible return values of $\mathcal {S}_{\mathrm {LIA}}$ is finite, and thus it is finite for $\varphi [ \mathbf { k }, \mathbf { e} ]$. $\square$

Lemma 7

If $\mathcal {I}$ is a model for $\mathrm {LIA}$ and for quantifier-free $\psi$, $\theta \ge 1$, and $S_{I0}( \mathcal {I}, \psi , \mathsf {e}, \theta ) = ( c, t, p )$, then:

• 1. c1.] $( c \cdot \mathsf {e} )^\mathcal {I}\equiv _{\theta \cdot c} t^\mathcal {I}$, and

• 2. $\mathcal {I}\models \psi \{ c \cdot \mathsf {e} \mapsto t \}$.

Proof

We first show part 7. When $n>0$ and $S_{I0}( \mathcal {I}, \psi , \mathsf {e}, \theta ) = ( c_i, \ell _i + \rho , + )$, we have

$$\begin{aligned} \left( \ell _i + \rho \right) ^\mathcal {I}\equiv _{\theta \cdot c_i} \left( \ell _i + \left( c_i \cdot \mathsf {e} - \ell _i \right) ^\mathcal {I}\ \mathsf {mod} \ \left( \theta \cdot c_i \right) \right) ^\mathcal {I}\equiv _{\theta \cdot c_i} \left( c_i \cdot \mathsf {e} \right) ^\mathcal {I}. \end{aligned}$$

When $m>0$ and $S_{I0}( \mathcal {I}, \psi , \mathsf {e}, \theta ) = ( d_j, u_j - \rho , - )$, we have

$$\begin{aligned} \left( u_j - \rho \right) ^\mathcal {I}\equiv _{\theta \cdot d_j} \left( u_j - \left( u_j - d_j \cdot \mathsf {e} \right) ^\mathcal {I}\ \mathsf {mod} \ \left( \theta \cdot d_j \right) \right) ^\mathcal {I}\equiv _{\theta \cdot d_j} \left( d_j \cdot \mathsf {e} \right) ^\mathcal {I}. \end{aligned}$$

When $n=0$, $m=0$, and $S_{I0}( \mathcal {I}, \psi , \mathsf {e}, \theta ) = ( 1, \rho , + )$, we have

$$\begin{aligned} \rho ^\mathcal {I}\equiv _{\theta \cdot 1} \left( \mathsf {e}^\mathcal {I}\ \mathsf {mod} \ \theta \right) ^\mathcal {I}\equiv _{\theta \cdot 1} \left( 1 \cdot \mathsf {e} \right) ^\mathcal {I}\end{aligned}$$

To show part 7, we first focus on the case where $n>0$ and $S_{I0}( \mathcal {I}, \psi , \mathsf {e}, \theta ) = ( c_i, \ell _i + \rho , + )$. We have that $\rho = ( c_i \cdot \mathsf {e} - \ell _i )^\mathcal {I}\ \mathsf {mod} \ ( \theta \cdot c_i )$. Let M be a set of literals of the form described in the body of $S_{I0}( \mathcal {I}, \psi , \mathsf {e} )$. We show that $\mathcal {I}$ satisfies each literal in $M \sigma$, where $\sigma = \{ c_i \cdot \mathsf {e} \mapsto \ell _i + \rho \}$. First, consider an atom in $M_\ell \sigma$ that is equivalent to $( c_j \cdot \mathsf {e} \ge \ell _j ) \sigma$ for some $j \in \{ 1, \ldots , n \}$. This is equivalent to $( c_j \cdot c_i \cdot \mathsf {e} \ge c_i \cdot \ell _j ) \sigma$, which is equivalent to $\frac{c_j \cdot c_i}{c_i} \cdot ( \ell _i + \rho ) \ge \frac{c_j \cdot c_i}{c_j} \cdot \ell _j$, which is satisfied by $\mathcal {I}$ since $( \frac{\ell _i}{ c_i } )^\mathcal {I}\ge ( \frac{\ell _j}{ c_j } )^\mathcal {I}$ by our selection of $( c_i, \ell _i + \rho )$ and since $\rho \ge 0$. Second, consider the atom in $M_u \sigma$ that is equivalent to $( d_j \cdot \mathsf {e} \le u_j ) \sigma$ for some $j \in \{ 1, \ldots , m \}$. Let $\rho ' = ( c_i \cdot \mathsf {e} - \ell _i )^\mathcal {I}$, which is greater than 0 since $\mathcal {I}$ satisfies $(c_i \cdot \mathsf {e} \ge \ell _i)$. Since $( c_i \cdot \mathsf {e} )^\mathcal {I}= ( \ell _i + \rho ' )^\mathcal {I}$, we have that $\mathcal {I}$ satisfies $( d_j \cdot \mathsf {e} \le u_j ) \{ c_i \cdot \mathsf {e} \mapsto \ell _i + \rho ' \}$, which is equivalent to $( d_j \cdot ( \ell _i + \rho ' ) \le c_i \cdot u_j )$. Since $\rho = \rho ' \ \mathsf {mod} \ ( \theta \cdot c_i ) \le \rho '$, we have that $\mathcal {I}$ also satisfies $( d_j \cdot ( \ell _i + \rho ) \le c_i \cdot u_j )$, which is $( d_j \cdot \mathsf {e} \le u_j ) \sigma$. Finally, $\mathcal {I}$ satisfies $M_c \sigma$ as $M_c \sigma = M_c$ and $\mathcal {I}\models M_c$. Thus, $\mathcal {I}$ satisfies $M \sigma$, which entails $\psi \sigma$. The case when $m>0$ and $S_{I0}( \mathcal {I}, \psi , \mathsf {e}, \theta ) = ( d_j, u_j - \rho , - )$ is symmetric. When $n=0$, $m=0$, and $S_{I0}( \mathcal {I}, \psi , \mathsf {e} ) = ( 1, \rho , + )$, the assignment M does not contain $\mathsf {e}$, and thus $\mathcal {I}$ satisfies $M \{ c \cdot \mathsf {e} \mapsto \rho \} = M$ and $\psi \{ c \cdot \mathsf {e} \mapsto \rho \}$. $\square$

Lemma 8

Each recursive call to $S_I( \mathcal {I}, \psi , ( \mathsf {e}_i, \ldots , \mathsf {e}_n ), \theta , ( t_1, \ldots , t_{i-1} ), \mathbf {p} )$ within a call to $\mathcal {S}_{\mathrm {LIA}}( \mathcal {I}, {\varGamma }, \lnot \varphi [\mathbf { k }, \mathbf { e}], ( \mathsf {e}_1, \ldots , \mathsf {e}_n ) )$ is such that:

• 1. $\theta \mid t_j^\mathcal {I}$ for each $1 \le j < i$, and

• 2. $\mathcal {I}\models \psi$ and $\psi$ is equivalent to $\lnot \varphi [\mathbf { k }, \mathbf { e}] \{ \theta \cdot \mathsf {e}_1 \mapsto t_1 \} \cdot \ldots \cdot \{ \theta \cdot \mathsf {e}_{i-1} \mapsto t_{i-1} \}$.

Proof

Both statements clearly hold for the initial call to $S_I$ in the body of $\mathcal {S}_{\mathrm {LIA}}$. Now, assume both statements hold for some call to $S_I( \mathcal {I}, \psi , ( \mathsf {e}_i, \mathbf { e}' ), \theta , ( t_1, \ldots , t_{i-1} ), \mathbf {p} )$, and assume $( c, t_i, p_i) = S_{I0}( \mathcal {I}, \psi , \mathsf {e}_i, \theta )$. We show that both statements hold for the call to $S_I( \mathcal {I}, \psi \sigma , \mathbf { e}', \theta \cdot c, ( ( c \cdot t_1 )\sigma , \ldots , ( c \cdot t_{i-1} )\sigma , \theta \cdot t_i ), (\mathbf {p}, p_i) )$, where $\sigma = \{ c \cdot \mathsf {e}_i \mapsto t_i \}$.

To show part 1, we have from Lemma 7 part 1 that:

$$\begin{aligned} ( c \cdot \mathsf {e}_i )^\mathcal {I}\equiv _{\theta \cdot c} t_i^\mathcal {I}\end{aligned}$$

(2)

Consider a $t_j$ where $1 \le j < i$, which by our assumption is such that $\theta \mid t_j^\mathcal {I}$, and thus $\theta \cdot c \mid ( c \cdot t_j )^\mathcal {I}$. By (2), we have that $\theta \cdot c \mid ( ( c \cdot t_j )\sigma )^\mathcal {I}$. Also by (2), we have that $c \mid t_i^\mathcal {I}$, and thus $\theta \cdot c \mid ( \theta \cdot t_i )^\mathcal {I}$.

To show part 2, by our assumption, $\mathcal {I}\models \psi$ and thus by Lemma 7 part 7 we have that $\mathcal {I}\models \psi \sigma$. By our assumption, $\psi$ is equivalent to $\lnot \varphi [\mathbf { k }, \mathbf { e}] \{ \theta \cdot \mathsf {e}_1 \mapsto t_1 \} \cdot \ldots \cdot \{ \theta \cdot \mathsf {e}_{i-1} \mapsto t_{i-1} \}$. Thus, $\psi \sigma$ is equivalent to $\lnot \varphi [\mathbf { k }, \mathbf { e}] \{ (\theta \cdot c) \cdot \mathsf {e}_1 \mapsto ( c \cdot t_1 ) \sigma \} \cdot \ldots \cdot \{ (\theta \cdot c) \cdot \mathsf {e}_{i-1} \mapsto ( c \cdot t_{i-1} ) \sigma \} \cdot \{ (\theta \cdot c) \cdot \mathsf {e}_i \mapsto \theta \cdot t_i \}$. Thus, the lemma holds. $\square$

Lemma 9

$\mathcal {S}_{\mathrm {LIA}}$ is model-preserving for $\varphi [ \mathbf { k }, \mathbf { e} ]$.

Proof

Assume $\mathcal {S}_{\mathrm {LIA}}( \mathcal {I}, {\varGamma }, \lnot \varphi [\mathbf { k }, \mathbf { e}], \mathbf {e} ) = \mathbf {t}$, where $\mathbf { e} = ( \mathsf {e}_1, \ldots , \mathsf {e}_n )$ and $\mathbf {t} = ( t_1, \ldots , t_n )$. By Lemma 8 and the definition of $\mathcal {S}_{\mathrm {LIA}}$, there is a $\theta$ such that for each $i = 1, \ldots , n$, term $t_i$ is of the form $s_i\ \small \mathsf {div}^p \ \theta$ where $\theta \mid s_i^\mathcal {I}$, and $\mathcal {I}\models ( \lnot \varphi [\mathbf { k }, \mathbf { e}] ) \{ \theta \cdot \mathsf {e}_1 \mapsto s_1 \} \cdot \ldots \cdot \{ \theta \cdot \mathsf {e}_n \mapsto s_n \}$. Thus, $\mathcal {I}$ satisfies $( \lnot \varphi [\mathbf { k }, \mathbf { e}] ) \{ \mathbf { e } \mapsto \mathbf {t} \} =$ $\lnot \varphi [\mathbf { k }, \mathbf {t}]$, and thus $\mathcal {S}_{\mathrm {LIA}}$ is model-preserving for $\varphi [ \mathbf { k }, \mathbf { e} ]$. $\square$

Theorem 3

$\mathcal {P}_{\mathcal {S}_{\mathrm {LIA}}}$ is a sound and complete procedure for determining the $\mathrm {LIA}$-satisfiability of $\exists \mathbf {k}\, \forall \mathbf {x}\, \varphi [\mathbf {k}, \mathbf {x}]$.

Proof

By Theorem 1, Lemma 2, Lemma 6 and Lemma 9. $\square$

Example 6

To demonstrate a case involving a substitution with coefficients, consider the formula $\forall xy\, ( 2 \cdot x< a \vee x + 3 \cdot y < b )$ whose negation is $2 \cdot e_1 \ge a \wedge e_1 + 3 \cdot e_2 \ge b$. A possible run of $\mathcal {P}_{\mathcal {S}_{\mathrm {LIA}}}$ on this input is as follows.

			$S_{I0}( \mathcal {I}, \psi , \mathsf {e}, \theta )$
#	${\varGamma }$	${\varGamma }'$	$\mathsf {e}$	$\theta$	$M_\ell$	Return	$\mathbf {t}[\mathbf { k}]$	$\text {Add to } {\varGamma }$
1	sat	sat	$e_1$	1	$\{ \underline{2 \cdot e_1 \ge a}, \ldots \}$	$(2, a, +)$
			$e_2$	2	$\{ \underline{6 \cdot e_2 \ge 2 \cdot b - a} \}$	$(6, 2 \cdot b - a, +)$	$( 6 \cdot a, 4 \cdot b - 2 \cdot a )\ \small \mathsf {div}^{+} \ 12$	$\psi _1$
2	unsat

We assume $\rho = 0$ for all calls to $S_{I0}$ in this run. Applying the substitution $\{ 2 \cdot e_1 \mapsto a \}$ to $e_1 + 3 \cdot e_2 \ge b$ results in the bound $6 \cdot e_2 \ge 2 \cdot b - a$ for $e_2$. We add to ${\varGamma }$ an instance, call it $\psi _1$, which is equivalent to $2 \cdot ((6 \cdot a)\ \small \mathsf {div}^{+} \ 12 )< a \vee (6 \cdot a)\ \small \mathsf {div}^{+} \ 12 + 3 \cdot ((4 \cdot b - 2 \cdot a)\ \small \mathsf {div}^{+} \ 12) < b$, which after eliminating integer division is:

which is equisatisfiable to:

$$\begin{aligned} ( 6 \cdot a + m_1< 6 \cdot a \vee 12 \cdot b + m_1 + 3 \cdot m_2< 12 \cdot b ) \wedge 0\le & {} m_1< 12 \wedge \\ 0\le & {} m_2 < 12 \end{aligned}$$

which is $\mathrm {LIA}$-unsatisfiable. Thus, $\exists ab\, \forall xy\, ( 2 \cdot x< a \vee x + 3 \cdot y < b )$ is $\mathrm {LIA}$-unsatisfiable. $\square$

Example 7

To demonstrate a case involving a non-zero value of $\rho$, consider the formula $\forall xy\, ( 3 \cdot x + y \not \approx a \vee 0> y \vee y > 2 )$ whose negation is $3 \cdot e_1 + e_2 \approx a \wedge 0 \le e_2 \wedge e_2 \le 2$, where $\approx$ denotes the conjunction of non-strict upper and lower bounds. A possible run of $\mathcal {P}_{\mathcal {S}_{\mathrm {LIA}}}$ on this input is as follows.

			$S_{I0}( \mathcal {I}, \psi , \mathsf {e}, \theta )$
#	${\varGamma }$	${\varGamma }'$	$\mathsf {e}$	$\theta$	$M_\ell$	Return	$\mathbf {t}[\mathbf { k}]$	$\text {Add to } {\varGamma }$
1	sat	sat	$e_1$	1	$\{ \underline{3 \cdot e_1 \ge a-e_2} \}$	$(3, a-e_2, +)$
			$e_2$	3	$\{ \underline{e_2 \ge 0} \}$	$(1, 0, +)$	$( a, 0 )\ \small \mathsf {div}^{+}\ 3$	$\psi _1$
2	sat	sat	$e_1$	1	$\{ \underline{3 \cdot e_1 \ge a-e_2} \}$	$(3, a-e_2, +)$
			$e_2$	3	$\{ \underline{e_2 \ge 0} \}$	$(1, 1, +)$	$( a-1, 1 )\ \small \mathsf {div}^{+}\ 3$	$\psi _2$
3	sat	sat	$e_1$	1	$\{ \underline{3 \cdot e_1 \ge a-e_2} \}$	$(3, a-e_2, +)$
			$e_2$	3	$\{ \underline{e_2 \ge 0} \}$	$(1,2, +)$	$( a-2, 2 )\ \small \mathsf {div}^{+}\ 3$	$\psi _3$
4	unsat

On the first iteration, we assume that ${\varGamma }'$ is satisfied by a model, call it $\mathcal {I}_1$, that interprets all variables as 0, and hence the values chosen for $e_1$ and $e_2$ correspond to their maximal lower bounds in $\mathcal {I}_1$, $a-e_2$ and 0 respectively, where in each call to $S_{I0}$ we have $\rho = 0$. The instance $\psi _1$ added to ${\varGamma }$ on this iteration is equivalent to $3 \cdot (a\ \small \mathsf {div}^{+}\ 3) \not \approx a$ and implies that $a^{\mathcal {I}} \not \equiv _3 0$ in subsequent models $\mathcal {I}$. Thus, models $\mathcal {I}$ satisfying $3 \cdot e_1 + e_2 \approx a$ are such that $e_2^{\mathcal {I}} \not \equiv _3 0$. On the next iteration, ${\varGamma }'$ is satisfied by a model, call it $\mathcal {I}_2$, where the maximal lower bound for $e_2$ is 0. By the above reasoning and since $\mathcal {I}_2$ satisfies $3 \cdot e_1 + e_2 \approx a$, it must be that $\rho = ((e_2-0)^{\mathcal {I}_2} \ \mathsf {mod} \ 3) \ne 0$. Assume $(e_2-0)^{\mathcal {I}_2} \equiv _3 1$. The instance $\psi _2$ is equivalent to $3 \cdot ((a-1)\ \small \mathsf {div}^{+}\ 3) + 1 \not \approx a$, which implies that $a^{\mathcal {I}} \not \equiv _3 1$ in subsequent models $\mathcal {I}$, and hence $e_2^{\mathcal {I}} \not \equiv _3 1$. The instance $\psi _3$ is equivalent to $3 \cdot ((a-2)\ \small \mathsf {div}^{+}\ 3) + 2 \not \approx a$ and implies that $a^{\mathcal {I}} \not \equiv _3 2$, which together with the two previous instances are T-unsatisfiable. This run shows $\exists a\, \forall xy\, ( 3 \cdot x + y \not \approx a \vee 0> y \vee y > 2 )$ is $\mathrm {LIA}$-unsatisfiable. $\square$

The procedure $\mathcal {P}_{\mathcal {S}_{\mathrm {LIA}}}$ can be understood to lazily enumerating disjuncts of Cooper’s algorithm for quantifier elimination over linear integer arithmetic [16], with minor differences. The algorithm is essentially enumerating a single path of [16] by using the model to select a satisfied case split for each variable over an entire block of quantifiers.¹ Like that approach, the worst-case performance is dependent upon the size of coefficients of monomials, which is manifested in our case by the fact that the number of possible return values of $S_{I0}$ is proportional to the size of $\theta$. While not shown here, our implementation takes steps to reduce the size of $\theta$ by factoring out common divisors in $\theta$ and the coefficients returned by $S_{I0}$.

4.1 Comparison to existing approaches

The approach taken in $\mathcal {P}_{\mathcal {S}_{\mathrm {LIA}}}$ is similar to the one taken in Section 2.5 in [13]. The most substantial difference between the two algorithms is that $\mathcal {P}_{\mathcal {S}_{\mathrm {LIA}}}$ implements a variant of Cooper’s algorithm while $resolve$ in [13] uses the model to guide an execution of the Omega test [47]. The most similar aspects of the approaches are the computation of a feasible $\rho$ and the computation of the d values in the grey shadow cases of $resolve$. These differ in that a different d value is selected to ensure separation between each upper bound and the greatest lower bound in a projection whereas $\rho$ is selected using the current value of $c_i \cdot e$ (the selection of d is agnostic to e in our parlance) to ensure all bounds are satisfied by a single instantiation.

5 Instantiation for $\mathrm {LIRA}$-formulas

The methods in the previous two sections can be used in part for the class of $\mathrm {LIRA}$-formulas with one alternation where constraints are over both real and integer variables. For convenience, we assume the signature of $\mathrm {LIRA}$ is extended with conversion functions $\small \mathsf {to\_int}^{+}$ and $\small \mathsf {to\_int}^{-}$ of sort $\mathsf {Real}\rightarrow \mathsf {Int}$, denoting the result of rounding its (real) argument to an integer. All occurrences of these symbols can be eliminated from quantifier-free constraints by the transformation:

$$\begin{aligned} \varphi [ \small \mathsf {to\_int}^p( t ) ] {{\mathrm{\ \leadsto \ }}}\varphi [ i ] \wedge 0 \le \pm ^p( i - t ) < 1 \end{aligned}$$

(3)

where i is a fresh constant of type $\mathsf {Int}$, and $\pm ^p$ is $+$ if p is $+$ and analogously for −.

Figure 7 gives a selection function $\mathcal {S}_{\mathrm {LIRA}}$ for $\mathrm {LIRA}$, where by the above transformation we may assume without loss of generality that $\lnot \varphi [\mathbf { k },\mathbf { e_r }, \mathbf { e_i}]$ contains no conversion functions. Real variables $\mathbf {\mathsf {e_r}}$ are processed before integer ones $\mathbf { e_i}$. The procedure invokes the selection function $S_R$ for $\mathrm {LRA}$ which returns a set of terms $\mathbf {t_r}$. Afterwards, we apply a transformation, denoted ${\small \mathsf {to\_lia}}$, to the formula $\lnot \varphi [\mathbf { k },\mathbf {t_r}, \mathbf { e_i}]$, which returns a pair $( \mathcal {I}', \varphi ' )$ where $\mathcal {I}'$ is an extension of $\mathcal {I}$, and $\varphi '$ is a $\mathrm {LIA}$ formula. We construct $\varphi '$ by replacing each literal L of the form $(\lnot )( \mathbf { c_i \cdot x_i } + \mathbf { c_r \cdot x_r } \bowtie c )$ in $\lnot \varphi [\mathbf { k },\mathbf {t_r}, \mathbf { e_i}]$ by the literal $(\lnot )( \mathbf { c_i \cdot x_i } + i_{ \mathbf { c_r \cdot x_r } }^p \bowtie c )$ where $\mathbf { x_i }$ are of type $\mathsf {Int}$, $\mathbf { x_r }$ are of type $\mathsf {Real}$, $i_{ \mathbf { c_r \cdot x_r } }^p$ is a fresh variable of type $\mathsf {Int}$ and p is one of $\{ +, - \}$. We define the interpretation of $i_{ \mathbf { c_r \cdot x_r } }^p$ in $\mathcal {I}'$ to be the result of rounding the value $(\mathbf { c_r \cdot x_r })^\mathcal {I}$ to an integer up if p is $+$ or down if p is −. If this variable occurs in a literal L that entails a lower bound on $i_{ \mathbf { c_r \cdot x_r } }^p$, then p is −, otherwise p is $+$. Notice that in either case, the interpretation of L remains unchanged by the transformation ${\small \mathsf {to\_lia}}$. After constructing ${\small \mathsf {to\_lia}}( \mathcal {I}, (\lnot \varphi [\mathbf { k },\mathbf {t_r}, \mathbf { e_i}] ) )$, the procedure calls the selection function $S_I$ on the resulting interpretation and formula, which returns a tuple of terms, call it $\mathbf {s_i}$. We then obtain a tuple of terms $\mathbf {t}_i$ by applying a second transformation, denoted ${\small \mathsf {to\_lira}}$, to $\mathbf {s}_i$, which replaces all $\mathrm {LIA}$-variables of the form $i_{t}^p$ in $\mathbf {s}_i$ with the $\mathrm {LIRA}$-term $\small \mathsf {to\_int}^p( t )$. Overall, we return the tuple $( \mathbf {t_r} \{ \mathbf { e_i } \rightarrow \mathbf {t_i } \}, \mathbf {t_i} )$, where integer variables $\mathbf {e_i}$ are replaced by $\mathbf {t_i}$ within the terms $\mathbf {t_r}$ selected for the real variables. When using this selection in the context of the procedure in Fig. 1, the instance ${\varphi [ \mathbf { k}, \mathbf {t_r} \{ \mathbf { e_i } \rightarrow \mathbf {t_i } \}, \mathbf {t_i}]}$ is added to ${\varGamma }$.

Fig. 7

A selection function $\mathcal {S}_{\mathrm {LIRA}}$ for quantifier-free $\mathrm {LIRA}$-formula $\varphi [\mathbf { k },\mathbf { e_r }, \mathbf { e_i}]$, where $\mathbf { e_r }$ are real variables and $\mathbf { e_i}$ are integer variables. In this procedure, ${\small \mathsf {to\_lia}}( \mathcal {I}, \psi )$ denotes the result of casting $\mathrm {LIRA}$-formula $\psi$ to a $\mathrm {LIA}$ one, and $\mathcal {I}'$ is an extension of $\mathcal {I}$ (see Example 8)

Example 8

Consider the formula $\forall x{:}\,\mathsf {Real}\,y{:}\mathsf {Int}\, (x - 2 \cdot y< b \vee y < a)$ where a and b are free constants of type $\mathsf {Real}$ and $\mathsf {Int}$ respectively. The negated Skolemized form of this formula is equivalent to $e_1 - 2 \cdot e_2 \ge b \wedge e_2 \ge a$, where $e_1$ and $e_2$ are fresh constants. A possible run of $\mathcal {P}_{\mathcal {S}_{\mathrm {LIRA}}}$ on this input is as follows.

#	${\varGamma }$	${\varGamma }'$	$\mathsf {e}$	$M_\ell$	$(S_R, S_I) \text { return}$	$\mathbf {t}[\mathbf { k}]$	$\text {Add to } {\varGamma }$
1	sat	sat	$e_1$	$\{ \underline{e_1 \ge b + 2 \cdot e_2} \}$	$(b + 2 \cdot e_2)$
			$e_2$	$\{ \underline{e_2 \ge i_{a}^+} \}$	$(i_{a}^+)$	$( b + 2 \cdot \small \mathsf {to\_int}^+(a), \small \mathsf {to\_int}^+(a))$	$\bot$
2	unsat

On the first iteration, we run $S_R$ which returns the term $b + 2 \cdot e_2$ for x based on the bound $e_1 \ge b + 2 \cdot e_2$. We then call ${\small \mathsf {to\_lia}}( \mathcal {I}, (( b + 2 \cdot e_2 ) - 2 \cdot e_2 \ge b \wedge e_2 \ge a) )$, which returns $( \mathcal {I}', \psi ' )$, where $\psi '$ is equivalent to $e_2 \ge i_{a}^+$, and $\mathcal {I}'$ interprets $i_{a}^+$ as $a^\mathcal {I}$ was rounded up to an integer value. We subsequently call $S_I$ on this interpretation and formula, which results in the selection of term $i_{a}^+$ for $e_2$. Thus, $S_I$ returns the tuple $( i_{a}^+ )$, where applying the transformation ${\small \mathsf {to\_lira}}$ gives us $( \small \mathsf {to\_int}^+(a))$. Overall, $\mathcal {S}_{\mathrm {LIRA}}$ returns the tuple $( b + 2 \cdot \small \mathsf {to\_int}^+(a), \small \mathsf {to\_int}^+(a))$, which we obtain by applying the substitution $\{ y \mapsto \small \mathsf {to\_int}^+(a) \}$ to our value for $e_1$ and appending our value $\small \mathsf {to\_int}^+(a)$ for $e_2$. Applying the substitution $\{ x \mapsto b + 2 \cdot \small \mathsf {to\_int}^{+}(a), y \mapsto \small \mathsf {to\_int}^{+}(a) \}$ to our input results in the formula $(b + 2 \cdot \small \mathsf {to\_int}^{+}(a) - 2 \cdot \small \mathsf {to\_int}^{+}(a)< b \vee \small \mathsf {to\_int}^{+}(a) < a)$, which after simplification is $(\small \mathsf {to\_int}^{+}(a) < a)$. After eliminating conversion functions, this formula is $i< a \wedge 0 \le i - a < 1$ where i is a fresh integer variable, which is $\mathrm {LIRA}$-unsatisfiable. This run shows that $\exists a{:}\,\mathsf {Real}\,b{:}\,\mathsf {Int}\, \forall x{:}\,\mathsf {Real}\,y{:}\,\mathsf {Int}\, (x - 2 \cdot y< b \vee y < a)$ is $\mathrm {LIRA}$-unsatisfiable. $\square$

It is straightforward that the use of this selection function in Fig. 1 gives a sound procedure for quantified $\mathrm {LIRA}$ due to Corollaries 1 and 2, and the transformation (3) preserves equivalence (up to variables $\mathbf {k}$). We do not provide a formal proof of completeness for this approach, although we note that quantifier elimination is possible for this fragment [65].

6 Boolean structure and nested quantification

This section presents a novel technique for establishing the T-satisfiability of formulas with Boolean structure and nested quantification. The technique generalizes the instantiation-based procedure as described in Sect. 2, and can be integrated within the solving architecture used by SMT solvers.

In the following, we show an approach for determining the T-satisfiability of closed T-formula $(\lnot )\varphi$. Without loss of generality, we assume $\varphi$ is a formula from the following grammar:

$$\begin{aligned} \varphi := \lnot \forall \mathbf {x}\, \varphi \mid G \mid \varphi _1 \vee \cdots \vee \varphi _m \end{aligned}$$

(4)

where G is quantifier-free. In other words, all quantification in our input occurs as a (negated) child of a disjunction. Notice this grammar is effectively a generalization of prenex normal form, since all formulas in prenex normal form are equivalent to a formula in a subset of the above grammar which restricts $m=1$.²

At its core, our approach for establishing the satisfiability of $\varphi$ is the following. Let $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$ be a sub-formula of our input, where this formula may occur beneath any number of negations and $\psi$ is quantifier-free. Using the procedure in Fig. 1, construct a set of instances $\{ \psi [ \mathbf {k}, \mathbf {t}_1[ \mathbf {k} ] ], \ldots , \psi [ \mathbf {k}, \mathbf {t}_n[ \mathbf {k} ] ] \}$ that is either unsatisfiable, or that collectively entail $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$. Note that the free variables $\mathbf {k}$ of this sub-formula are considered to be existentially quantified implicitly here. If this set is unsatisfiable, replace $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$ in the input by $\bot$. Otherwise, replace $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$ in the input by the (quantifier-free) formula $\psi [ \mathbf {k}, \mathbf {t}_1[ \mathbf {k} ] ] \wedge \cdots \wedge \psi [ \mathbf {k}, \mathbf {t}_n[ \mathbf {k} ] ]$. Repeat this process until our input is replaced by a quantifier-free formula. In this section, we describe an approach that is based on the above reasoning, but is amenable to the standard solving architecture used by SMT solvers. In particular, the approach will be based on incrementally constructing a set of quantifier-free formulas ${\varGamma }$ that approximate the input $\varphi$, where this set is periodically checked for T-satisfiability.

We begin with the following preliminaries. For each closed quantified T-formula, we associate a Boolean variable A called the positive guard of $\forall \mathbf {x}\, \varphi$, and unique set of Skolem variables $\mathbf {e}$ of the same sort as $\mathbf {x}$. We write $( A, \mathbf {e} ) \leftrightharpoons \forall \mathbf {x}\, \varphi$ to denote that A and $\mathbf {e}$ are associated with $\forall \mathbf {x}\, \varphi$. We write $\lfloor \varphi \rfloor$ for the result of replacing in $\varphi$ all closed quantified formulas (not occurring beneath other quantifiers in $\varphi$) with their corresponding positive guards. We write $\mathcal {A}(\varphi )$ to denote the set of positive guards in $\varphi$. Our approach maintains an evolving set of formulas ${\varGamma }$. We add formulas of the form $A \Rightarrow \phi$ to ${\varGamma }$, where $\phi$ is a quantifier-free formula that is entailed by $\forall \mathbf {x}\, \varphi$ and $(A, \mathbf {e} ) \leftrightharpoons \forall \mathbf {x}\, \varphi$. We call such formulas guarded instances. We write $\lfloor \psi \rfloor _{{\varGamma }}$ to denote the result of replacing in $\lfloor \psi \rfloor$ each positive guard A by the conjunction of formulas on the right hand sides of instances from ${\varGamma }$ that are guarded by A. Conceptually, the formula $\lfloor \psi \rfloor _{{\varGamma }}$ will correspond to the current quantifier-free approximation of $\psi$ in ${\varGamma }$ in our approach.

Example 9

Let $\varphi$ be $\lnot \forall x\, P( x ) \vee \lnot \forall y\, R( y ) \vee \lnot \forall z\, Q( z ) \vee G$ where G is quantifier-free, let $A_1 \leftrightharpoons (\forall x\, P( x ), e_1)$, $A_2 \leftrightharpoons (\forall y\, R( y ), e_2)$ and $A_3 \leftrightharpoons (\forall z\, Q( z ), e_3)$, and let ${\varGamma }$ be $\{ A_1 \Rightarrow P( a ), A_2 \Rightarrow R( b ), A_2 \Rightarrow R( c ) \}$. Then, $\lfloor \varphi \rfloor$ is $\lnot A_1 \vee \lnot A_2 \vee \lnot A_3 \vee G$, $\mathcal {A}(\lfloor \varphi \rfloor ) = \{ A_1, A_2, A_3 \}$, and $\lfloor \varphi \rfloor _{{\varGamma }}$ is $\lnot P( a ) \vee \lnot ( R( b ) \wedge R( c ) ) \vee \lnot \top \vee G$. $\square$

Fig. 8

Abstract procedure $\small \mathsf {solve}$ for establishing the T-satisfiability of $\forall \mathbf {x}\, \varphi [ \mathbf {x} ]$, which calls a counterexample-guided approach for quantifier instantiation $\small \mathsf {CEGQI}_T$. Instances are added to ${\varGamma }$ based on a selection function $\mathcal {S}_T$ for theory T. This procedure generalizes the one in Fig. 1

To determine the T-satisfiability of a closed T-formula $\forall \mathbf {x}\, \varphi [ \mathbf {x} ]$, we use the procedure $\small \mathsf {solve}_T$ in Fig. 8. This procedure incrementally refines an approximation of $\forall \mathbf {x}\, \varphi [ \mathbf {x} ]$, given by set ${\varGamma }$, until it is found to be (un)satisfiable in T. The procedure first invokes the recursive subprocedure $\small \mathsf {CEGQI}_T$, which takes as input a set ${\varGamma }$ initially containing the positive guard $A_0$ of $\forall \mathbf {x}\, \varphi [ \mathbf {x} ]$, and $A_0$ itself. This subprocedure adds formulas to ${\varGamma }$ in Step 3 until either ${\varGamma }$ is T-unsatisfiable (Step 1), in which case the input is unsatisfiable, or otherwise the procedure saturates (Step 2), in which case the input is satisfiable.

Formulas are added to ${\varGamma }$ based on the recursive procedure $\small \mathsf {rec}_T$. Recall that our input formula $\forall \mathbf {x}\, \varphi [ \mathbf {x} ]$ is a formula having a tree-like structure built from grammar (4). At a high level, the procedure $\small \mathsf {rec}_T$ returns a guarded instance of some quantified sub-formula in this tree whose satisfiability is yet to be determined, if one exists. In detail, this function takes as arguments ${\varGamma }$ and the positive guard A of a quantified formula $\forall \mathbf {y}. \psi [ \mathbf {k}, \mathbf {y} ]$, called initially with $A = A_0$. It first constructs the formula $\phi [ \mathbf {k}, \mathbf {e} ] = \lfloor \psi [ \mathbf {k},\mathbf {e} ] \rfloor _{{\varGamma }}$, which represents an approximation of the formula $\psi [ \mathbf {k},\mathbf {e} ]$ under the assumption of the current instances in ${\varGamma }$. If the current set of instances $\lfloor A \rfloor _{{\varGamma }}$ that are guarded by A and the negation of this formula are unsatisfiable, then it is the case that $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$ is equivalent to $\lfloor A \rfloor _{{\varGamma }}$ and the procedure returns the empty set. Otherwise, we consider the direct children of $\psi$, i.e. those whose positive guard $A'$ occurs in $\mathcal {A}( \lfloor \psi [ \mathbf {k}, \mathbf {e} ] \rfloor )$. If the recursive call to $\small \mathsf {rec}_T$ returns a guarded instance for some child $A'$, then the procedure returns that instance. Otherwise, it returns a guarded instance $A \Rightarrow {\phi [ \mathbf {k}, \mathbf {t}[\mathbf {k}] ]}$, where $\mathcal {I}$ is a model of theory T, $\lfloor A \rfloor _{{\varGamma }}$ and $\lnot \phi [ \mathbf {k},\mathbf {e} ]$, and terms $\mathbf {t}[ \mathbf {k}]$ are chosen by the selection function $\mathcal {S}_T$ for theory T.

The correctness of this procedure relies on the following facts, where recall from Sect. 1.1 two formulas are equivalent up to $\mathbf {k}$ if the are satisfied by the same set of models when restricted to the interpretation of variables from $\mathbf {k}$.

Lemma 10

Let $( A, \mathbf {e} ) \leftrightharpoons \forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$.

• 1. If $\small \mathsf {rec}_T( {\varGamma }, A)$ returns $\{ A \Rightarrow {\phi [ \mathbf {k}, \mathbf {t} ]} \}$, then $\phi [ \mathbf {k}, \mathbf {t} ]$ is equivalent to $\psi [ \mathbf {k}, \mathbf { t } ]$ up to $\mathbf {k}$.

• 2. If $\lfloor A \rfloor _{{\varGamma }} \wedge \lfloor \lnot \psi [ \mathbf {k}, \mathbf {e} ] \rfloor _{{\varGamma }}$ is T-unsat, then $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$ is equivalent to $\lfloor A \rfloor _{{\varGamma }}$ up to $\mathbf {k}$.

Proof

We prove both facts simultaneously by induction on the structure of $\psi$.

(Base case) When $\psi [ \mathbf {k}, \mathbf {y} ]$ is quantifier-free, then $\lfloor \psi [ \mathbf {k}, \mathbf {e} ] \rfloor _{{\varGamma }} = \psi [ \mathbf {k}, \mathbf {e} ]$ and $\small \mathsf {rec}_T( {\varGamma }, A)$ returns only sets of the form $\{ A \Rightarrow {\psi [ \mathbf {k}, \mathbf {t}[ \mathbf {k} ] ]} \}$. Thus, part 1 holds, and moreover we have that $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ] \models _T \lfloor A \rfloor _{{\varGamma }}$. To show part 2, assume $\lfloor A \rfloor _{{\varGamma }} \wedge \lfloor \lnot \psi [ \mathbf {k}, \mathbf {e} ] \rfloor _{{\varGamma }}$ is T-unsatisfiable, or in other words $\lfloor A \rfloor _{{\varGamma }} \models _T \psi [ \mathbf {k}, \mathbf {e} ]$. Since $\mathbf {e}$ does not occur in $\lfloor A \rfloor _{{\varGamma }}$, we have that $\lfloor A \rfloor _{{\varGamma }} \models _T \forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$, and thus $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$ is equivalent to $\lfloor A \rfloor _{{\varGamma }}$ up to $\mathbf {k}$.

(Inductive case) When $\psi [ \mathbf {k}, \mathbf {y} ]$ is $\lnot \forall \mathbf {x}_1\, \psi _1[ \mathbf {k}_1, \mathbf {x}_1 ] \vee \cdots \vee \lnot \forall \mathbf {x}_m\, \psi _m[ \mathbf {k}_m, \mathbf {x}_m ]$, for $i=1,\ldots ,m$, let $( A_i, \mathbf {e}_i ) \leftrightharpoons \forall \mathbf {x}_i\, \psi _i[ \mathbf {k}_i, \mathbf {x}_i ]$ if $\mathbf {x}_i$ is non-empty. To show part 1, assume $\small \mathsf {rec}_T( {\varGamma }, A)$ returns $\{ A \Rightarrow {\phi [ \mathbf {k}, \mathbf {t} ]} \}$, where $\phi [ \mathbf {k}, \mathbf {t} ]$ is $\lfloor \psi [ \mathbf {k}, \mathbf {t} ] \rfloor _{{\varGamma }}$. For each $i=1,\ldots ,m$ where $\mathbf {x}_i$ is non-empty, by definition of $\small \mathsf {rec}_T$ it must be that $\small \mathsf {rec}_T( {\varGamma }, A_i)$ returns $\emptyset$, and thus $\lfloor A_i \rfloor _{{\varGamma }} \wedge \lfloor \lnot \psi _i[ \mathbf {k}_i, \mathbf {e}_i ] \rfloor _{{\varGamma }}$ is T-unsatisfiable. Thus, by part 2 of the induction hypothesis, we have that $\lfloor A_i \rfloor _{{\varGamma }}$ is equivalent to $\forall \mathbf {x}_i\, \psi _i[ \mathbf {k}_i, \mathbf {x}_i ]$ up to $\mathbf {k}_i$ where $\mathbf {k}_i$ is a subset of $\mathbf {k}$. Thus, $\lfloor \psi [ \mathbf {k}, \mathbf {t} ] \rfloor _{{\varGamma }}$ is equivalent to $\psi [ \mathbf {k}, \mathbf { t } ]$ up to $\mathbf {k}$, and thus part 1 holds. To show part 2, we have by part 1 that $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ] \models _T \lfloor A \rfloor _{{\varGamma }}$. When $\lfloor A \rfloor _{{\varGamma }} \wedge \lfloor \lnot \psi [ \mathbf {k}, \mathbf {e} ] \rfloor _{{\varGamma }}$ is T-unsatisfiable, $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$ is equivalent to $\lfloor A \rfloor _{{\varGamma }}$ up to $\mathbf {k}$ for the same reasons as in the base case. $\square$

Theorem 4

Assume the satisfiability of quantifier-free T-formulas is decidable, and a selection function $\mathcal {S}_T$ exists that is finite and monotonic.

• 1. If $\small \mathsf {solve}_T( \forall \mathbf {x}\, \varphi [ \mathbf {x} ] )$ returns “unsat”, then $\forall \mathbf {x}\, \varphi [ \mathbf {x} ]$ is T-unsatisfiable.

• 2. If $\small \mathsf {solve}_T( \forall \mathbf {x}\, \varphi [ \mathbf {x} ] )$ returns “sat”, then $\forall \mathbf {x}\, \varphi [ \mathbf {x} ]$ is T-satisfiable.

• 3. $\small \mathsf {solve}_T( \forall \mathbf {x}\, \varphi [ \mathbf {x} ] )$ terminates.

Proof

To show 1, let $\lceil {\varGamma } \rceil$ denote the result of replacing the positive guards in ${\varGamma }$ with the quantified formula they respond to. By definition of $\small \mathsf {solve}_T$, we have that $\lceil {\varGamma } \rceil$ contains $\forall \mathbf {x}\,\varphi [ \mathbf {x} ]$, and additionally contains tautologies of the form $\forall \mathbf {x}\, \psi [ \mathbf {k}, \mathbf {y} ] \Rightarrow \phi [ \mathbf {k}, \mathbf {t} ]$ where by Lemma 10.1 $\phi [ \mathbf {k}, \mathbf {t} ]$ is equivalent to $\psi [ \mathbf {k}, \mathbf {t} ]$ up to $\mathbf {k}$. Thus, $\lceil {\varGamma } \rceil$ is equivalent to $\forall \mathbf {x}\,\varphi [ \mathbf {x} ]$. Furthermore, we have that $\lceil {\varGamma } \rceil \models _T {\varGamma }$, and ${\varGamma }$ is T-unsatisfiable. Thus, $\forall \mathbf {x}\,\varphi [ \mathbf {x} ]$ is T-unsatisfiable.

To show 2, by definition of $\small \mathsf {solve}_T$, we have that ${\varGamma }$ is T-satisfiable, and $\lfloor A_0 \rfloor _{{\varGamma }} \wedge \lnot \lfloor \varphi [ \mathbf {e} ] \rfloor _{{\varGamma }}$ is T-unsatisfiable, where $( A_0, \mathbf {e} ) \leftrightharpoons \forall \mathbf {x}\, \varphi [ \mathbf {x} ]$. By Lemma 10.2, we have that $\forall \mathbf {x}\, \varphi [ \mathbf {x} ]$ is equivalent to $\lfloor A_0 \rfloor _{{\varGamma }}$. Since $A_0 \in {\varGamma }$, we have that ${\varGamma }\models _T \lfloor A_0 \rfloor _{{\varGamma }}$, and thus $\forall \mathbf {x}\, \varphi [ \mathbf {x} ]$ is satisfied by a model of ${\varGamma }$.

To show 3, all individual steps in the procedure are terminating since the T-satisfiability of quantifier-free T-formulas is decidable. Furthermore, we show that the number of instances added to ${\varGamma }$ is finite. Let $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$ be a formula where $( A, \mathbf {e} ) \leftrightharpoons \forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$ and for which $\small \mathsf {rec}_T( {\varGamma }, A)$ is called. Assume that at least one instance of the form $\{ A \Rightarrow {\phi [ \mathbf {k}, \mathbf {t}_1[ \mathbf {k} ] ]} \}$ is added for some quantifier-free T-formula $\phi [ \mathbf {k}, \mathbf {e} ] = \lfloor \psi [ \mathbf {k}, \mathbf {e} ] \rfloor _{{\varGamma }}$. Since formulas are never removed from ${\varGamma }$, it must be the case that $\lfloor \psi [ \mathbf {k}, \mathbf {e} ] \rfloor _{{\varGamma }} = \lfloor \psi [ \mathbf {k}, \mathbf {e} ] \rfloor _{{\varGamma }\cup {\varGamma }'}$ for all formulas ${\varGamma }'$ added in subsequent recursive calls to $\small \mathsf {CEGQI}_T$. Thus, all instances returned by $\small \mathsf {rec}_T$ guarded by A are of the form $\{ A \Rightarrow {\phi [ \mathbf {k}, \mathbf {t}_i[ \mathbf {k} ] ]} \}$ for the same $\phi$. Since $\mathcal {S}_T$ is monotonic for $\exists \mathbf {k}\, \forall \mathbf {y}\,\phi [ \mathbf {k}, \mathbf {y} ]$, we are guaranteed to add a new instance to ${\varGamma }$ on each recursive call to $\small \mathsf {CEGQI}_T$. Thus, since $\mathcal {S}_T$ is finite for $\exists \mathbf {k}\, \forall \mathbf {y}\,\phi [ \mathbf {k}, \mathbf {y} ]$, only finitely many instances of this form are returned. Since there are only finitely many $\forall \mathbf {y}\, \psi [ \mathbf {k}, \mathbf {y} ]$ for which $\small \mathsf {rec}_T$ is called on, we have that only finitely many instances are added to ${\varGamma }$, finitely many recursive calls are made to $\small \mathsf {CEGQI}_T$, and thus $\small \mathsf {solve}_T( \forall \mathbf {x}\, \varphi [ \mathbf {x} ] )$ terminates. $\square$

By the previous theorem, assuming satisfiability of quantifier-free T-formulas is decidable and a finite and monotonic selection function exists for T, $\small \mathsf {solve}_T$ is a decision procedure for T-formulas containing arbitrary nested quantification.

Example 10

Consider the $\mathrm {LIA}$-formula $\forall x\, \varphi [ x ]$ where $\varphi [ x ]$ is $\lnot ( \forall y\, x> y \vee 0 > y ) \vee x < 0$. Let $(A_1, e_1) \leftrightharpoons \forall x\, \varphi [ x ]$ and let $( A_2, e_2 ) \leftrightharpoons \forall y\, e_1> y \vee 0 > y$. We call $\small \mathsf {CEGQI}$ where ${\varGamma }$ is initially $\{ A_1 \}$. A possible run of this procedure is summarized in the table below.

		$\small \mathsf {rec}_T$
#	${\varGamma }\text {?}$	A	$\lfloor \lnot \psi [ \mathbf {e}] \rfloor$	$\lfloor \lnot \psi [ \mathbf {e} ] \rfloor _{{\varGamma }}$	$\lfloor A \rfloor _{{\varGamma }} \wedge \lfloor \lnot \psi [ \mathbf {e}] \rfloor _{{\varGamma }}?$	$t[ \mathbf {k} ]$	return	return
1	sat	$A_1$	$A_2 \wedge e_1 \ge 0$	$\top \wedge e_1 \ge 0$	sat		$\small \mathsf {rec}_T( {\varGamma }, A_2 )$
		$A_2$	$e_1 \le e_2 \wedge 0 \le e_2$	$e_1 \le e_2 \wedge 0 \le e_2$	sat	$(e_1)$	$\{ A_2 \Rightarrow 0 > e_1 \}$
2	sat	$A_1$	$A_2 \wedge e_1 \ge 0$	$0 > e_1 \wedge e_1 \ge 0$	unsat		$\emptyset$	“sat”

On the first call to the procedure $\small \mathsf {CEGQI}$, ${\varGamma }$ is T-satisfiable. We call $\small \mathsf {rec}_T$ on ${\varGamma }$ and $A_1$, which first checks the satisfiability of $\lfloor A_1 \rfloor _{{\varGamma }} \wedge \lfloor ( \forall y\, e_1> y \vee 0 > y ) \wedge e_1 \ge 0 \rfloor _{{\varGamma }}$, which is $\top \wedge ( \top \wedge e_1 \ge 0 )$, which is satisfiable. It then checks if there exists an $A'$ among the positive guards in $\lfloor ( \forall y\, e_1> y \vee 0 > y ) \wedge e_1 \ge 0 \rfloor$ for which an instance can be returned. On the call to $\small \mathsf {rec}_T$ where $A' = A_2$, we find that $e_1 \le e_2 \wedge 0 \le e_2$ is satisfiable, and there are no positive guards in $\lfloor e_1> e_2 \vee 0 > e_2 \rfloor$, that is, $\forall y\, e_1> y \vee 0 > y$ contains no nested quantifiers. We use the selection function for linear integer arithmetic $\mathcal {S}_{\mathrm {LIA}}$ as given in Sect. 4, which given input $e_1 \le e_2 \wedge 0 \le e_2$ returns the tuple $t[ e_1 ] = (e_1)$, thus giving the instance $A_2 \Rightarrow 0 > e_1$ which we add to ${\varGamma }$. On the second call to $\small \mathsf {CEGQI}_T$, we have that ${\varGamma }= \{ A_1, A_2 \Rightarrow 0 > e_1 \}$ is satisfiable, and we again call $\small \mathsf {rec}_T$ on ${\varGamma }$ and $A_1$, where now $0 > e_1 \wedge e_1 \ge 0$ is unsatisfiable. This establishes that $\forall x\, \lnot ( \forall y\, x> y \vee 0 > y ) \vee x < 0$ is $\mathrm {LIA}$-satisfiable. $\square$

Example 11

We remark that treating formulas that are not in prenex normal form allows us to avoid unnecessary computation. Consider the $\mathrm {LIA}$-formula $\forall x\, \varphi [ x ]$, where $\varphi [ x ]$ is $(\lnot ( \forall y\, x > y ) \vee \lnot \forall z\, \psi [ x ] )$, and $\psi [ x ]$ is some $\mathrm {LIA}$-formula. Let $(A_1, e_1) \leftrightharpoons \forall x\, \varphi [ x ]$, let $( A_2, e_2 ) \leftrightharpoons \forall y\, e_1 > y$, and let $( A_3, e_3 ) \leftrightharpoons \forall z\, \psi [ e_1 ]$. A possible run of this procedure is summarized in the table below.

		$\small \mathsf {rec}_T$
#	${\varGamma }\text {?}$	A	$\lfloor \lnot \psi [ \mathbf {e}] \rfloor$	$\lfloor \lnot \psi [ \mathbf {e} ] \rfloor _{{\varGamma }}$	$\lfloor A \rfloor _{{\varGamma }} \wedge \lfloor \lnot \psi [ \mathbf {e}] \rfloor _{{\varGamma }}\text {?}$	$t[ \mathbf {k} ]$	return	return
1	sat	$A_1$	$A_2 \wedge A_3$	$\top \wedge \top$	sat		$\small \mathsf {rec}_T( {\varGamma }, A_2 )$
		$A_2$	$e_1 \le e_2$	$e_1 \le e_2$	sat	$(e_1)$	$\{ A_2 \Rightarrow e_1 > e_1 \}$
2	sat	$A_1$	$A_2 \wedge A_3$	$e_1 > e_1 \wedge \top$	unsat		$\emptyset$	“sat”

The first call to procedure $\small \mathsf {CEGQI}_T$, adds the formula $A_2 \Rightarrow e_1 > e_1$ to ${\varGamma }$. In the second call to $\small \mathsf {CEGQI}_T$, within the call to $\small \mathsf {rec}_T$ for $A=A_1$, we find that $\lfloor A_1 \rfloor _{{\varGamma }} \wedge \lfloor (\forall y\, e_1 > y) \wedge \forall z\, \psi [ e_1 ] \rfloor _{{\varGamma }}$, which is $\top \wedge ( e_1 > e_1 \wedge \top )$, is unsatisfiable. Thus, we conclude that $\forall x\, (\lnot ( \forall y\, x > y ) \vee \lnot \forall z\, \psi [ x ] )$ is $\mathrm {LIA}$-satisfiable. This was determined regardless of the content of $\psi$. $\square$

Example 12

Consider the $\mathrm {LIA}$-formula $\forall xy\, \varphi [ x, y ]$, where $\varphi [ x, y ]$ is $(\lnot ( \forall z\, z< x \vee y< z ) \vee x < y+5 )$. Let $(A_1, (e_1,e_2)) \leftrightharpoons \forall xy\, \varphi [ x, y ]$ and let $( A_3, e_3 ) \leftrightharpoons \forall z\, z< e_1 \vee e_2 < z$. We call $\small \mathsf {CEGQI}$ where ${\varGamma }$ is initially $\{ A_1 \}$. A possible run of this procedure is summarized in the table below.

		$\small \mathsf {rec}_T$
#	${\varGamma }\text {?}$	A	$\lfloor \lnot \psi [ \mathbf {e}] \rfloor$	$\lfloor \lnot \psi [ \mathbf {e} ] \rfloor _{{\varGamma }}$	$\lfloor A \rfloor _{{\varGamma }} \wedge \lfloor \lnot \psi [ \mathbf {e}] \rfloor _{{\varGamma }}\text {?}$	$t[ \mathbf {k} ]$	Return	Return
1	sat	$A_1$	$A_3 \wedge e_1 \ge e_2+5$	$\top \wedge e_1 \ge e_2+5$	sat		$\small \mathsf {rec}_T( {\varGamma }, A_3 )$
		$A_3$	$e_3 \ge e_1 \wedge e_2 \ge e_3$	$e_3 \ge e_1 \wedge e_2 \ge e_3$	sat	$(e_2)$	$\{ A_3 \Rightarrow e_1 > e_2 \}$
2	sat	$A_1$	$A_3 \wedge e_1 \ge e_2+5$	$e_1 > e_2 \wedge e_1 \ge e_2+5$	sat		$\ldots$
		$A_3$	$e_3 \ge e_1 \wedge e_2 \ge e_3$	$e_3 \ge e_1 \wedge e_2 \ge e_3$	unsat		$\emptyset$
		$A_1$	$\ldots$	$\ldots$	$\ldots$	(5, 0)	$\{ A_1 \Rightarrow \bot \}$
2	unsat							“unsat”

On the first call to $\small \mathsf {CEGQI}$, we find that ${\varGamma }$ is satisfiable, and the call to $\small \mathsf {rec}_T$ returns the guarded instance $A_3 \Rightarrow e_1 > e_2$, which we add to ${\varGamma }$. On the second call to $\small \mathsf {CEGQI}$, we find that ${\varGamma }$ is again satisfiable. The call to $\small \mathsf {rec}_T$ for $A=A_1$ first finds that ${\varGamma }\cup \{ A_3 \wedge e_1 \ge e_2+5 \}$ is also satisfiable, and invokes itself recursively on $A_3$. The call to $\small \mathsf {rec}_T$ for $A=A_3$ determines that $\lfloor A \rfloor _{{\varGamma }} \wedge \lfloor \lnot \psi [ \mathbf {e}] \rfloor _{{\varGamma }}$, which is $e_1 > e_2 \wedge ( e_3 \ge e_1 \wedge e_2 \ge e_3 )$, is unsatisfiable and thus returns the empty set. By Lemma 10.2, this indicates that $\forall z\, z< e_1 \vee e_2 < z$ is equivalent to $e_1 > e_2$, that is, the conjunction of instances in ${\varGamma }$ that are guarded by $A_3$. Returning to $\small \mathsf {rec}_T$ for $A=A_1$, we add an instance for $\forall xy\, \varphi [ x, y ]$ where $A_3$ is replaced by $e_1 > e_2$ in the construction of $\lfloor \lnot \varphi [ e_1, e_2 ] \rfloor _{{\varGamma }}$, which gives us $e_1 > e_2 \wedge e_1 \ge e_2+5$. Applying the selection function $\mathcal {S}_{\mathrm {LIA}}$ as given in Sect. 4 to this formula returns the tuple (5, 0) for $( e_1, e_2 )$, thus giving the instance $A_1 \Rightarrow \lnot ( 5 > 0 \wedge 5 \ge 0+5 )$, which is equivalent to $A_1 \Rightarrow \bot$. We add this instance to ${\varGamma }$, after which we find that it is unsatisfiable, and thus $\forall xy\, \varphi [ x, y ]$ is $\mathrm {LIA}$-unsatisfiable. $\square$

6.1 Implementation details

In practice, the approach in Fig. 8 can be accomplished by a single instance of an SMT solver. Although not shown here, we additionally associate a second Boolean variable B with each quantified formula, called its negative guard. For each quantified formula $\forall \mathbf {x}\, \varphi$ with negative guard B, we add the formula $B \Rightarrow \lnot \varphi [ \mathbf {e} ]$ to ${\varGamma }$. The function $\small \mathsf {rec}_T$ then can be simulated using a decision heuristic in the underlying SAT solver that decides positively on the negative guards of innermost quantified formulas first, and adds instances of quantified formulas only if their negative guards are not propagated to false at decision level 0. A formal description of this technique is the subject of future work.

An alternative strategy to Fig. 8 is to add instances of (top-most) quantified formulas that may have nested quantification. That is, for a quantified formula $\forall x\, \varphi [ x ]$, we may add instances of the form $A \Rightarrow \varphi [ t ]$, where $\varphi$ contains quantified formulas. In such a strategy, virtual terms in t ($\delta$ or $\infty$) that are substituted beneath quantifiers in $\varphi$ must be treated specially. Adding instances of this form may potentially allow us to discover unsatisfiable instances quicker, but also may introduce many quantified formulas that in turn degrade performance. In the latest version of our implementation, we do not use this strategy. However, an earlier version of our implementation (cvc4 from SMT COMP 2016) makes use of this strategy.

6.2 Comparison to existing approaches

We refer to the treatment of quantified formulas in Fig. 8 as counterexample-guided quantifier instantiation [50]. The algorithm is similar to existing instantiation-based approaches used by SMT solvers for quantified formulas [17, 25] in that it adds guarded instances of quantified formulas incrementally. Its instance selection is guided by models for the negation of quantified formulas, similar to model-based quantifier instantiation [26]. This approach differs in its scope, in that it primarily targets quantified formulas having uninterpreted functions, whereas the approach described in Fig. 8 targets quantified formulas having no uninterpreted functions. The approach of [26] also differs in that it uses a separate copy of the SMT solver as an oracle for checking the satisfiability of the negation of each quantified formula it instantiates, whereas our approach uses a single instance of the SMT solver for doing these tasks simultaneously in its main solving loop. Other approaches that are specialized for quantified linear arithmetic invoke separate instances of an SMT solver for each quantifier alternation [13, 19], and are often restricted to inputs where quantified formulas are in prenex normal form. In contrast, the approach in this section requires only one instance of the SMT solver and may be applied to inputs with Boolean structure in the grammar (4) described at the beginning of this section.

7 Instantiation as a synthesis procedure

The connection between quantifier elimination and synthesis has been shown fruitful in previous work [34]; it is one of our motivations for further improving quantified reasoning modulo theories. The instantiation procedure mentioned in this paper can be used to synthesize functions from certain classes of specifications. Consider (second-order) T-formulas of the form:

$$\begin{aligned} \exists \mathbf {f} \, \forall \mathbf {x} \, \varphi [\mathbf {f}, \mathbf {x}] \end{aligned}$$

(5)

where $\varphi$ is a quantifier-free formula, $\mathbf {x} = ( x_1, \ldots , x_n )$ is a tuple of variables of sort $\tau _i$ for $i = 1, \ldots , n$, and $\mathbf {f} = ( f_1, \ldots , f_m )$ is a tuple of functions of sort $\tau _1 \times \cdots \times \tau _n \rightarrow \tau _j$ for $j =1, \ldots , m$. We call such formulas synthesis conjectures. A synthesis conjecture is single invocation (over $\mathfrak {L}$) if it is equivalent to:

$$\begin{aligned} \exists \mathbf {f} \, \forall \mathbf {x} \, \psi [\mathbf {x}, \mathbf {f}( \mathbf {x} )] \end{aligned}$$

(6)

where $\psi [\mathbf {x}, \mathbf {y}] \in \mathfrak {L}$. That is, functions $\mathbf {f}$ are applied to the tuple $\mathbf {x}$ only. The formula (6) is equivalent to the (first-order) formula $\forall \mathbf {x} \, \exists \mathbf {y} \, \psi [ \mathbf {x},\mathbf {y}]$, whose negation

$$\begin{aligned} \exists \mathbf {x} \, \forall \mathbf {y} \, \lnot \psi [\mathbf {x}, \mathbf {y}] \end{aligned}$$

(7)

is suitable as an input to Fig. 1. As observed in [50], solutions for single invocation synthesis conjectures can be extracted from an unsatisfiable core of instantiations when proving the unsatisfiability of (7). In particular, let $\mathbf { \mathsf {k} }$ be a set of distinct fresh variables of the same sort as $\mathbf {x}$, and say the set $\{ {\lnot \psi [\mathbf { \mathsf {k} }, \mathbf {t}_1[ \mathbf { \mathsf {k} }] ]}, \ldots , {\lnot \psi [\mathbf { \mathsf {k} }, \mathbf {t}_n[ \mathbf { \mathsf {k} }] ]} \}$ is T-unsatisfiable where $\mathbf {t}_i = (t^1_i[ \mathbf { \mathsf {k} }], \ldots , t^m_i[ \mathbf { \mathsf {k} }] )$ for $i = 1, \ldots , n$. Then:

$$\begin{aligned} 1 \le j \le m{:} f_j = \lambda \mathbf {x}.\, \mathsf {ite}( \psi [\mathbf {x}, t^j_n[\mathbf {x}]], t^j_n[\mathbf {x}], (\,\cdots \, \mathsf {ite}( \psi [\mathbf {x}, t^j_2[\mathbf {x}]], t^j_2[\mathbf {x}], t^j_1[\mathbf {x}] ) )) \end{aligned}$$

(8)

is a solution for $\mathbf {f}$ in (6). The instantiation-based procedure in Fig. 1 can be used to discharge (7). It is important to note that the solution (8) does not necessarily belong to the language $\mathfrak {L}$, since there is no restriction on the selection functions for $\mathfrak {L}$ that restricts its return value $\mathbf {t}$ to terms in $\mathfrak {L}$. For example, in some of our approaches to linear real arithmetic, $\mathbf {t}$ may contain a free distinguished constants $\delta$ or $\infty$ which are outside of the typical language of linear real arithmetic. Different selection functions or post-processing may be required based on the restrictions for the solutions to synthesis conjectures.

In this paper, we have devised selection functions $\mathcal {S}$ for linear real and integer arithmetic that are finite and monotonic in Sects. 3 and 4. This implies a sound and complete method for synthesizing tuples of functions whose specification is a single invocation synthesis conjecture over linear real and integer arithmetic.

Example 13

Consider the second-order $\mathrm {LIA}$-formula $\exists f\, \forall xy\, (f( x, y ) \ge x \wedge f( x, y ) \ge y )$, which states that there exists a function f that is the maximum of its arguments x and y. This formula is equisatisfiable to the first-order $\mathrm {LIA}$-formula $\forall xy\, \exists z\, ( z \ge x \wedge z \ge y )$. We apply the instantiation-based procedure in Fig. 1 on the negation of this input, $\exists xy\, \forall z\, \lnot ( z \ge x \wedge z \ge y )$. The procedure may find the T-unsatisfiable set of instances based on $\{ \lnot ( x \ge x \wedge x \ge y ), \lnot ( y \ge x \wedge y \ge y ) \}$. Thus, a solution for f is $\lambda x_1 x_2.\, \mathsf {ite}( ( x_1 \ge x_1 \wedge x_1 \ge x_2 ), x_1, x_2 )$, which after simplification is $\lambda x_1 x_2.\, \mathsf {ite}( x_1 \ge x_2, x_1, x_2 )$. $\square$

8 Experimental evaluation

We have implemented the procedure in the SMT solver cvc4  [6] (version 1.5 pre-release). This section presents an evaluation of this implementation compared against other SMT solvers, first-order theorem provers and synthesis solvers.

We considered all quantified benchmarks over 6 classes in the $\mathrm {LRA}$ and $\mathrm {LIA}$ logics of the SMT library [7]. The class keymaera are verification conditions coming from the Keymaera verification tool [45], scholl were used for simplification of non-convex polyhedra in [54], psyco were used for weakest precondition synthesis for compiler optimizations in [37], uauto correspond to verification conditions in [28], and the tptp classes correspond to simple arithmetic conjectures coming from the TPTP library [58]. We also considered a class of benchmarks sygus corresponding to first-order formulations of the 71 single-invocation synthesis conjectures taken from the conditional linear integer track of the 2015 edition of the syntax-guided synthesis competition [1]. All benchmarks are in the SMT version 2 format. For comparisons with automated theorem provers, they were converted to the TPTP format by the SMTtoTPTP conversion tool [8]. We remark that all benchmarks consist purely of quantified formulas over linear arithmetic with very little, and in a majority of cases, no quantifier-free content. Of the 7 benchmark classes, only one (the scholl class from $\mathrm {LRA}$) had quantified formulas with nested quantification.³

Table 1 Results for $\mathrm {LRA}$ benchmarks, showing times (in seconds) and benchmarks solved by each solver and configuration over 3 benchmark classes with a 300s timeout

Table 2 Results for $\mathrm {LIA}$ benchmarks, showing times (in seconds) and benchmarks solved by each solver and configuration over 4 benchmark classes with a 300s timeout

The results for the linear real and integer benchmarks are in Tables 1 and 2 respectively. We considered all SMT solvers and theorem provers from the $\mathrm {LRA}$ and $\mathrm {LIA}$ divisions of SMT COMP 2016, and the TFA division of CASC J8 [59], the latest competitions in the SMT and automated theorem proving communities.⁴ We write cvc4-sc16 and z3-sc16 to denote solvers from SMT COMP 2016, where cvc4 implements an earlier version of the techniques from this paper and z3 (version 4.4.1) implements the techniques from [12]. We additionally considered Yices version 2.4.1 for $\mathrm {LRA}$, and z3 version 4.4.2 which implements the techniques from [13], which we denote yices and z3 respectively. For $\mathrm {LRA}$, we consider 4 configurations of CVC4 each using different variants of the selection function in Fig. 2:

• cvc4 uses the return value in Fig. 2,

• cvc4+lw uses the return value in Fig. 3 (Loos and Weispfenning),

• cvc4+fr uses the return value in Fig. 4 (Ferrante and Rackoff), and

• cvc4+nvt uses the return value in Fig. 5 (with no virtual terms).

By convention, all versions of cvc4 return instantiations for maximal lower bounds before minmial upper bounds, and do not use variable ordering heuristics for quantified formulas with multiple variables.

For both $\mathrm {LRA}$ and $\mathrm {LIA}$, the best configuration of cvc4 solves the most benchmarks overall (616 and 461 respectively). Among the configurations of cvc4, the configuration using a selection function based on Loos and Weispfenning’s method cvc4+lw performed the best. The performance of the latest version of z3 has comparable performance, solving one fewer benchmark in $\mathrm {LRA}$. The configuration cvc4+lw solves 5 benchmarks that z3 does not. z3 solves 4 benchmarks that cvc4+lw does not, and the virtual best of these solvers solves all but one benchmark within the timeout. Moreover, we note that cvc4+lw solves the aforementioned 5 benchmarks in an average of .4 s per benchmark. We believe that this is because cvc4 ’s strategy is not restricted to quantified formulas that are in prenex normal form, and thus it may terminate quickly by realizing large nested disjunctions are not relevant to the overall formula. We will comment more on this in the next section. cvc4 solves more benchmarks (616) from the scholl class than any other solver due to its techniques for formulas with nested quantification from Sect 6. A technique [19] in the SMT solver Yices (version 2.4.1) is able to solve all benchmarks from the keymaera and tptp classes of $\mathrm {LRA}$, but does not handle quantified formulas in $\mathrm {LIA}$ or with nested quantification.

For both benchmarks over $\mathrm {LIA}$ and $\mathrm {LRA}$, the automated theorem provers trail the performance of cvc4 (and z3) significantly. The best $\mathrm {LRA}$ automated theorem prover, Vampire, which uses a combination of a first-order theorem prover and an SMT solver [49], solves only 347 benchmarks, compared to 616 solved by cvc4-fr. The best $\mathrm {LIA}$ automated theorem prover was also Vampire, which solves 284 benchmarks, notably less than the 461 solved by cvc4. We conclude that recent lazy model-based techniques for quantified linear arithmetic, as implemented in cvc4 and z3, are highly effective for solving quantified linear arithmetic.

8.1 Comparison of strategies for quantifier alternation on crafted benchmarks

In this subsection, we demonstrate the effectiveness of our approach for handling nested quantification based on the strategy in Sect. 6. As mentioned, our strategy may be applied to quantified formulas in a grammar that is not restricted to prenex normal form, and may often avoid reasoning about irrelevant portions of quantified formulas, as demonstrated in Example 11. This gives us an advantage with respect to existing approaches, including the strategy used in z3  [13], which is limited to quantified formulas in prenex normal form.

To demonstrate this advantage, we constructed a set of benchmarks that are very easy if Boolean structure within quantifier scope is properly taken into account, and very hard otherwise. In detail, we randomly constructed 500 unique formula templates of the form $\varphi _1[ F ], \ldots , \varphi _{500}[ F ]$, where F occurs at some formula position in $\varphi _i$. Examples of formula templates of this form are $\bot \wedge F$, $\forall x\, \exists y\,( x > y \wedge F )$, $\exists xy\, x> y \wedge \exists z\, ( x> z \wedge z > y ) \wedge F$, and so on. These templates were constructed by recursively generating an abstract syntax tree where each formula node is given some probability of being one of $\forall , \exists , \lnot , \wedge , \vee ,>$, and each term node is given some probability of being either a bound variable or one of $+, 0, 1$. For each $i = 1, \ldots , 500$, we checked whether:

• The satisfiability result of $\varphi _i[ \top ]$ was the same as the satisfiability result of $\varphi _i[ \bot ]$, and

• The satisfiability of both $\varphi _i[ \top ]$ and $\varphi _i[ \bot ]$ could be quickly determined (in less than 5 s) by both cvc4 and z3.

Among the 500 templates, we found that 360 met the first criterion above and 497 met the second criterion.⁵ Overall, 357 met both criteria. Notice that for any such template that meets the first criteria, the satisfiability of $\varphi _i[ F ]$ can be determined independently of any closed formula we substitute for F. For each of these 357 templates, we measure the time taken by cvc4 and z3 to solve the formula obtained by replacing F with closed formulas corresponding to hard benchmarks from the previous section. Since F is irrelevant to the satisfiability of $\varphi _i[ F ]$, one might expect that the satisfiability of $\varphi _i[ F_{\text {hard}} ]$ should be determined relatively quickly, even if the satisfiability of $F_{\text {hard}}$ is hard to determine. However, we have that this is not necessarily the case, and that solving time can vary significantly from solver to solver.

Table 3 give the results of solvers cvc4 and z3 on template and instantiation pairs. We consider the 357 formula templates, as described above. The first two sets of columns give cvc4 and z3 ’s cumulative run time on the 357 templates where F is replaced by $\top$ and $\bot$ respectively. For the remaining three sets of columns, we replace F by formulas corresponding to benchmarks from the scholl class of SMT-LIB (rnd_6_39, rndpre_4_41, and rndpre_4_56). We chose these benchmarks since they are the three benchmarks that neither cvc4 nor z3 can solve within a two minute timeout. We found that no solver answered differently for two queries of the form $\varphi [ F_1 ]$ and $\varphi [ F_2 ]$ for $F_1 \ne F_2$. In this experiment, z3 timed out for 169 templates instantiated with $F_{\text {rnd}\_6\_39}$, and 2 templates instantiated with $F_{\text {rndpre}\_4\_41}$. Overall, z3 solved 71.2% benchmarks from the last three sets columns in less than 30 s. On the other hand, the results show that cvc4 solves each benchmark relatively quickly, regardless of the contents of F. The longest it took to solve any benchmark was 4.6 s. When comparing the average solving time for benchmarks in the last three sets of columns versus the first two sets, the average overhead was .13 s per benchmark.

Table 3 Results for 357 randomly constructed templates of the form $\varphi [ F ]$ whose satisfiability does not depend on F, for five cases of F

Table 4 Results for example crafted templates $\varphi [ F ]$ for three cases of F. The formula $F_{\text {rndpre}\_4\_8}$ corresponds to an easy satisfiable benchmark from the same class

For a closer look, Table 4 gives results for an additional five crafted templates, and the times taken by cvc4 and z3 to solve each (template, benchmark) pair. For all templates, we assume when applicable that free constants (e.g. a and b) are existentially quantified. The first four templates are unsatisfiable regardless of the content of F. The fifth template we considered was of the form $F_{\text {rndpre}\_4\_8} \vee F$, where $F_{\text {rndpre}\_4\_8}$ is the formula corresponding to a benchmark (also from the scholl class) which cvc4 and z3 both find to be satisfiable quickly, and thus this template is satisfiable for all F. For the first template, both cvc4 and z3 solve all three instances quickly. For the other templates, z3 ’s performance varies significantly. In fact, for some benchmarks such as the fourth template where F is $F_{\text {rnd}\_6\_39}$, z3 ’s performance is worse (${>}300$ s) than running on $F_{\text {rnd}\_6\_39}$ alone, which it solves in 226.3 s. Overall, cvc4 answers quickly for all benchmarks, solving almost all benchmarks in less than a second. It takes around 4 s to solve the second and third templates instantiated with rndpre_4_56, where it spends a majority of its time finding a model for the initial set of quantifier-free constraints and terminates after only two iterations of the loop in procedure $\small \mathsf {CEGQI}_T$ from Fig. 8. In our testing, we were unable to find a template $\varphi [ F ]$ for which cvc4 took more than 5 s longer to solve $\varphi [ F_{\text {hard}} ]$ when compared to the time it took to solve $\varphi [ \top ]$, where $F_{\text {hard}}$ is a formula corresponding to one of the benchmarks in the columns of Table 4. On the other hand, z3 ’s performance varied significantly on many of the non-trivial templates we considered.

We believe this indicates that a strategy for quantified linear arithmetic that does not require formulas to be in prenex normal form, such as the one from Sect. 6, can have significant performance advantages. We conjecture that this design decision accounts for the differences between cvc4 and z3 in our evaluation in the previous section, where we found that for 5 of the original benchmarks from the scholl class for which z3 timed out, at least one configuration of cvc4 was able to solve in less than 2 s.

8.2 Comparison with synthesis solvers

The techniques for solving quantified linear arithmetic in cvc4 have the additional advantage that they may produce solutions to synthesis conjectures as described in Sect. 7. In the 2015 edition of the syntax-guided synthesis (SyGuS) competition [2], an earlier version of cvc4 won the conditional linear arithmetic track, solving 70 of 73 benchmarks using techniques from [50]. The nearest solver ALCHEMIST [53] solved 43. cvc4 also won the conditional linear arithmetic track in the 2016 edition, solving all 73 synthesis conjectures, and a new approach in EUsolver [3] solved 72. The improvement in cvc4 in the latest edition is due to its use of a complete instantiation strategy for linear integer arithmetic when solving single invocation synthesis conjectures as described in Sect. 7.

8.3 Number of instantiations

We measured statistics on the number of instantiations cvc4 constructs while solving benchmarks in the previous section. Let $\#\mathsf {lits}( \psi , X )$ be the number of literals in $\psi$ containing a variable in set X. We approximate the number of possible instantiations of a quantified formula $\psi$ of the form $\forall x_1\,\ldots \,x_n\, \varphi$ where $\varphi$ is quantifier-free by the following calculation:

$$\begin{aligned} \#\mathsf {PInst}( \psi ) = {\varPi }_{i=1,\ldots ,n} \mathsf {max}( 1, \#\mathsf {lits}( \varphi , \{ x_i \} ) \end{aligned}$$

For each i, we add a factor corresponding to an approximation of the number of possible bounds for variable $x_i$. This measure is proportional to the worst-case behavior of the total number of instantiations required for the termination of the instantiation-based procedure in Fig. 1 when using the selection functions $\mathcal {S}_{\mathrm {LRA}}$ and $\mathcal {S}_{\mathrm {LIA}}$ for linear real and integer arithmetic. More precisely, each factor for variable $x_i$ is an approximation of the size of the set of possible terms returned by functions $S_{R0}$ and $S_{I0}$, as described in the proofs of Lemmas 3 and 6 respectively.

Table 5 Average number of instantiations and possible instantiations per benchmark for $\mathrm {LRA}$ and $\mathrm {LIA}$ benchmarks

Table 5 gives the average number of instantiations considered by cvc4 and the average possible number of instantiations considered by cvc4 across all benchmark families on benchmarks that all configurations of cvc4 solve. A few benchmark families (such as tptp and keymaera) had a very small number of possible instantiations, which can partially be attributed to the fact that cvc4 applies aggressive preprocessing techniques to eliminate variables from quantified formulas. Conversely, other benchmark families (such as scholl and psyco) had a very large number of possible instantiations. Many of the benchmarks in psyco contained formulas with quantifier prefixes up to 50 variables in length, and hence often had upwards of $2^{50}$ possible instantiations. Since the benchmarks in scholl contain nested quantification, we consider a very conservative estimate of the number of possible instantiations by only considering innermost quantified formulas in our computation. The number of instantiations cvc4 considers is on average considerably less the number of possible instantiations, demonstrating that a lazy approach for quantifier instantiation is beneficial, and often critical, to solving benchmarks in these libraries.

9 Conclusion

We have presented a class of instantiation-based procedures that are at the same time complete for quantified linear arithmetic and highly efficient in practice. Thanks to our framework we also obtain a simple and modular correctness argument for soundness and completeness on formulas with one quantifier alternation. This correctness argument is used in part for showing soundness and completeness on formulas with arbitrary quantifier alternations, as well as a complete and efficient method for solving single invocation synthesis conjectures. Our procedure for arbitrary quantifier alternations has advantages over approaches that are limited to formulas in prenex normal form.

For future work, we would like to extend the approach to new theories including fixed-width bit vectors, strings, and non-linear arithmetic, as well as for combinations of theories that admit quantifier elimination. We would like to focus on further heuristics for quantified linear arithmetic with arbitrary quantifier alternations, and for avoiding worst case performance for quantified integer arithmetic involving large coefficients. A longer term goal of this work is to develop an approach that is effective in practice for quantified formulas involving both background theories and uninterpreted functions. We plan to investigate the use of the framework described in this paper as a component of such an approach.