key: cord-0060405-uyoe9ut9
authors: Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare
title: Syntax-Guided Quantifier Instantiation
date: 2021-02-26
journal: Tools and Algorithms for the Construction and Analysis of Systems
DOI: 10.1007/978-3-030-72013-1_8
sha: 93d77b27f2df61550c39a01f11ab3141bfa6eafe
doc_id: 60405
cord_uid: uyoe9ut9

This paper presents a novel approach for quantifier instantiation in Satisfiability Modulo Theories (SMT) that leverages syntax-guided synthesis (SyGuS) to choose instantiation terms. It targets quantified constraints over background theories such as (non)linear integer, reals and floating-point arithmetic, bit-vectors, and their combinations. Unlike previous approaches for quantifier instantiation in these domains which rely on theory-specific strategies, the new approach can be applied to any (combined) theory, when provided with a grammar for instantiation terms for all sorts in the theory. We implement syntax-guided instantiation in the SMT solver CVC4, leveraging its support for enumerative SyGuS. Our experiments demonstrate the versatility of the approach, showing that it is competitive with or exceeds the performance of state-of-the-art solvers on a range of background theories.

Modern Satisfiability Modulo Theories (SMT) solvers are highly efficient tools, capable of reasoning about constraints over a wide range of logical theories, including (non-linear) real and integer arithmetic, fixed-size bit-vectors, and floating-point arithmetic. Their core algorithms are designed primarily for quantifier-free constraints, but various extensions have been shown to work well also for quantified constraints in many cases. Quantified reasoning in SMT has many practical applications, including software verification, automated theorem proving, and synthesis.

Current SMT solvers handle quantified constraints in a variety of ways, with a degree of effectiveness that usually depends on the background theory. For instance heuristic instantiation techniques such as E-matching [15] are used for quantified formulas with heavy use of uninterpreted functions. These heuristic instantiation techniques are refutationally incomplete but they can be highly effective, in particular in the context of verification applications. For quantified constraints over a particular background theory, such as linear arithmetic or fixed-size bit-vectors, on the other hand, SMT solvers resort to an entirely different set of techniques. While also based on quantifier instantiation, these other techniques tend to be counterexample-guided and can be complete for theories and fragments of first-order logic that admit quantifier elimination.

Specific previous work in the latter direction includes counterexample-guided quantifier instantiation techniques for linear arithmetic [25] and fixed-size bitvectors [18, 20] . The key to developing each of them is to devise an appropriate, theory-specific selection function, which determines a term selection strategy for instantiating universal quantifiers. For some logics, e.g., linear arithmetic, selection functions can be based on the notion of elimination set found in classic algorithms for quantifier elimination [9, 14] . However, since many theories used in practice do not admit quantifier elimination, the design of a good selection function is usually non-trivial. These challenges are further magnified when reasoning in combinations of multiple theories.

We propose a novel, syntax-guided quantifier instantiation (SyQI) approach, which is both general-purpose and highly effective for quantified formulas in background theories such as (non)linear integer, reals and floating-point arithmetic, and their combinations. The new approach leverages an embedding of a solver for the syntax-guided synthesis (SyGuS) problem [1] within an SMT solver in order to choose terms for quantifier instantiation in a counterexample-guided manner. It is theory-agnostic and only requires the specification, via a grammar, of the set of terms to consider for each sort in the theory when instantiating quantifiers. 3 Since it can be applied to quantified formulas in any background theory, it is more general in scope than previous work [20] . Our approach is intended for logics such as quantified floating-point arithmetic, which would benefit from counterexample-guided quantifier instantiation, but for which appropriate selection function are not obvious. We show that the use of syntax-guided synthesis gives us the flexibility to develop variants of our approach that are highly competitive with the state of the art in SMT solving. More specifically, this paper makes the following contributions:

-We present and prove correct a simple yet novel quantifier instantiation approach that leverages syntax-guided synthesis for selecting instantiations. -We explore variants of the approach along several dimensions, including the choice of symbols to include in grammars for various background theories. -We implement this technique in the SMT solver CVC4 [5] and show that it performs remarkably well in a wide variety of SMT logics. In particular, it improves upon the state of the art for solving quantified formulas over floating-point arithmetic, and is highly competitive for non-linear integer arithmetic and certain combined logics that involve fixed-size bit-vectors.

Related Work. Handling quantified formulas in SMT solvers is a long-standing challenge. Early approaches for quantified formulas were largely based on Ematching [8, 10, 15] . They have been later supplemented with techniques that rely on models for establishing satisfiability [11, 26] , and on conflict finding to accelerate the search for unsatisfiability [27] . Pragmatic enumerative approaches for quantifier instantiation have also been explored and shown to increase the precision of SMT solvers on inputs involving uninterpreted functions where Ematching is incomplete [21] . The approach we describe here is also enumerative in nature; however, it leverages syntax-guided synthesis for choosing instantiations and does not target inputs with uninterpreted functions. For quantified formulas over a single background theory, counterexampleguided approaches have been considered by Bjørner and Janota [6] and by Reynolds et al. [25] , targeting primarily quantified linear integer/real arithmetic. For theories of other data types (e.g., bit-vectors), most approaches use valuebased instantiation, where concrete variable assignments for a set of quantifierfree formulas derived from the negation of the input formula (the counterexamples) provide instantiations for the universal variables. In the SMT solver Z3 [16] , model-based quantifier instantiation (MBQI) [11] is combined with a templatebased model finding procedure [29] . A recent line of work by Niemetz et al. [18] leverages invertibility conditions in a counterexample-guided loop for quantifier instantiation of formulas in the theory of fixed-size bit-vectors. Brain et al. [7] lift the concept of invertibility conditions to the theory of floating-point arithmetic and presented a preliminary quantifier elimination procedure for a fragment of the theory based on these conditions. Another approach for lazy quantifier elimination for bit-vector formulas is explored by Vediramana Krishnan et al. [12] , based on iterative approximate quantifier elimination.

Reynolds et al. [24] leverage counterexample-guided quantifier instantiation (CEGQI) to efficiently solve a restricted but practically useful form of syntaxguided synthesis problems. In contrast, the work in this paper has the dual goal of leveraging enumerative syntax-guided synthesis to establish a strategy for quantifier instantiation of (first-order) quantified formulas.

SyGuS techniques to solve quantified problems were previously explored by Preiner et al. in [20] . However, instead of focusing on quantifier instantiation they combined enumerative syntax-guided synthesis with value-based quantifier instantiation to synthesize Skolem functions for existential variables.

We assume the usual notions and terminology of many-sorted first-order logic with equality (denoted by ≈). Let S be a set of sort symbols. For every σ ∈ S, let X σ be an infinite set of variables of sort σ. Let X = σ∈S X σ . Let Σ be a signature consisting of a set Σ s ⊆ S of sort symbols and a set Σ f of interpreted (and sorted) function symbols f σ1···σnσ with arity n ≥ 0 and σ 1 , ..., σ n , σ ∈ Σ s . We assume that Σ includes a Boolean sort Bool and the Boolean values (true) and ⊥ (false). Let I be a Σ-interpretation that maps: each sort σ ∈ Σ s to a nonempty set σ I (the domain of I), with Bool I = { , ⊥}; each variable x ∈ X σ to an element x I ∈ σ I ; and each function f σ1···σnσ ∈ Σ f to a total function f I : σ I 1 × ... × σ I n → σ I if n > 0, and to an element in σ I if n = 0. We assume the usual definition of well-sorted terms, literals, and formulas as Bool terms with variables in X and symbols in Σ, and refer to them as Σ-terms, Σ-atoms, and so on. A ground term/formula is a Σ-term/formula without variables. We define x = (x 1 , ..., x n ) as a tuple of variables and write Qx.ϕ with Q ∈ {∀, ∃} for a quantified formula Qx 1 . · · · Qx n .ϕ. A formula is universal if it has the form ∀x. P where P is a quantifier-free formula. For simplicity, we consider only universal quantifiers since existential quantifiers can be rewritten in terms of universal ones. We use Lit(ϕ) to denote the set of Σ-literals of Σformula ϕ. For a Σ-term or Σ-formula e, we use e[x] to indicate that the free variables of e are in x. For a tuple of Σ-terms t = (t 1 , ..., t n ), we write e[t] for the term or formula obtained from e by simultaneously replacing each occurrence of x i in e by t i . If t is a Σ-term/formula and I a Σ-interpretation, we write t I to denote the meaning of t in I. We use the usual inductive definition of a satisfiability relation |= between Σ-interpretations and Σ-formulas.

A theory T is a pair (Σ, I), where Σ is a signature and I is a non-empty class of Σ-interpretations (the models of T ) that is closed under variable reassignment, i.e., every Σ-interpretation that only differs from an I ∈ I in how it interprets variables is also in I. A Σ-formula ϕ is T -satisfiable (resp. T -unsatisfiable) if it is satisfied by some (resp. no) interpretation in I; it is T -valid if it is satisfied by all interpretations in I.

Enumerative SyGuS using an Embedding into Datatypes. A syntax-guided synthesis problem for an n-ary function f in a background theory T consists of a set of semantic restrictions (a specification) for f , given as a (second-order) T -formula of the form ∃f. ϕ[f ], and a set of syntactic restrictions on the solutions for f , typically expressed as a context-free grammar. A solution to such a problem is a term t[x 1 , . . . , x n ] that satisfies the syntactic restrictions and is such that the formula ϕ[λx 1 , . . . , x n .t] is T -valid.

As shown in previous work [24] , syntactic restrictions for the bodies of functions to synthesize can be conveniently represented as a set of (algebraic) datatypes. The setting in this paper is simpler. Instead of synthesizing terms corresponding to function bodies, we use context-free-grammars for defining a set of (first-order) terms in a given theory, possibly containing free function symbols. For instance, let a and b be free constants of sort Int. The context-free grammar R below specifies a set of integer (Z) and Boolean (B) terms:

Given such a grammar, our SyGuS solver generates the following mutually recursive datatypes:

Each datatype constructor, listed on the right-hand side of each equation, corresponds to a production rule of R, e.g., plus corresponds to the rule Z ::= Z + Z. Given a datatype value v, we write to term(v) to denote the term that v represents, e.g., to term(plus(a, b)) is the term a + b.

In previous work [22, 24] , a smart enumerative approach for syntax-guided synthesis was presented and implemented in CVC4. In that work, the generation of terms is based on finding solutions for an evolving set of constraints in an extension of the quantifier-free fragment of algebraic datatypes, for which some SMT solvers have dedicated decision procedures [3, 23] . In the remainder of this paper, we write T D to denote the theory of datatypes over a signature Σ D of constructor and selector symbols. The signature Σ D includes (parametric) datatype sorts that are interpreted as the universe of a term algebra over the constructors. Selectors are interpreted as functions that extract the immediate subterms of a constructor term.

In our setting, datatype constraints are used to express syntactic restrictions on the terms in the original theory. For instance, in case of the example theory and corresponding datatypes Z and B defined above, we can write a datatype constraint that is falsified by all terms of the form plus(zero, t) where t is a constructor term of sort Z. This corresponds to ruling out terms of the form (0 + . . .) in the original theory where s is a term of sort Int. In more detail, for a datatype term d, we write is C (d) to denote the discriminator predicate, which is satisfied exactly when d is interpreted as a datatype value whose top constructor is C. We write sel σ,n (d) to denote a shared selector [28] applied to d, interpreted as the n th child of d with sort σ if one exists, and as an arbitrary element of σ otherwise. These symbols are used for constructing blocking constraints. For example, we can write ¬is plus (d) ∨ ¬is zero (sel Z,1 (d)) to state the constraint above that d cannot be interpreted as any datatype value corresponding to an Int term of the form (0 + . . .). In the context of syntax-guided synthesis, a constraint like this is added, for instance, to filter out redundant terms (like 0 + . . .) or terms already known to falsify the synthesis conjecture.

Our approach for syntax-guided instantiation relies on a notion of evaluation variables. A related, more general, notion of evaluation functions was used in the context of syntax-guided synthesis (see Section 2 of [22] for details). Let d be a term of a datatype sort encoding a grammar over terms of sort σ. We write e d to denote a free constant of sort σ, which we call the evaluation variable for d. We use evaluation variables to determine which terms to use in instantiations of quantified formulas. The algorithm given in the following section will add constraints that force the interpretation of e d to be equal to to term(d I ) in interpretations I. A simple example of such a constraint is is a (d) ⇒ e d ≈ a, stating that the evaluation variable e d for d is equal to the free constant a of integer type when d is interpreted as the datatype value a.

Our new SyGuS-based instantiation approach combines counterexample-guided quantifier instantiation (CEGQI) with smart enumerative SyGuS techniques to synthesize terms for quantifier instantiation. In essence, it is an algorithm that tries to synthesize a term t for a variable x in a given formula ∀x. P [x] such that ¬P [t] holds. For synthesis purposes, each quantified variable is associated with Algorithm 1 Main algorithms of the SyQI approach. for

Let dx be a fresh global constant of datatype sort grammar S (x) 5:

G := G ∪ {lj ⇒ ¬P [ed x ]} with fresh Boolean constant lj and fresh e dx 6: repeat 7:

if check(G) = unsat then return unsat 8:

if r = unsat then return sat 10:

for lj ∈ {l1, . . . , ln} such that l I j = do 11:

G := G ∪ select lemmasL(Qj, I) for xi ∈ {x1, . . . , xp} do 15:

ti

return non-empty subset of {P [t1, . . . , tp]} ∪ L based on selection strategy L a SyGuS grammar based on the sort of the variable. For example, our algorithm uses a bit-vector-specific grammar to synthesize bit-vector terms as possible instantiations of quantified variables of bit-vector sort. Our SyGuS solver suggests instantiations based on such grammars and an evolving set of constraints on the instance term. The main advantage of this instantiation approach is that it does not require theory-specific quantifier instantiation algorithms. Its only theory-specific aspects are the construction of the grammar for each theory sort and the satisfiability checks performed on the generated instances. Algorithm 1 shows the two main procedures syqi and select lemmas L of our SyGuS instantiation approach. To simplify the exposition, we describe the restricted case where the quantified input formula are all universal. Our implementation in CVC4, however, applies to the general case through a lazy conversion to DNF and resolution of quantifier alternations.

Procedure syqi takes as argument a set {Q 1 , . . . , Q n } of universal (quantified) T -formulas and a set G of ground T -formulas. As an initial step, and prior to solving the problem, we generate a lemma for each quantified formula Q i as part of our counterexample-guided quantifier instantiation approach (lines 2-5). We first create a fresh datatype constant d x of sort grammar S (x) for each variable x ∈ x in each input formula ∀x. P [x]. The datatype sort grammar S (x) is constructed from a SyGuS grammar determined by the sort of variable x. The language generated by the grammar includes ground terms from Q i and G of the same sort. These terms are chosen following a selection strategy S, which we describe in Section 3.1. Apart from running check, used as a black box, grammar S implements the only theory-specific handling of our procedure. Finally, we add to G a lemma of the form l i ⇒ ¬P [e dx ] for each quantified for-mula, where l i is a fresh Boolean constant (the counterexample literal for Q i ). Thanks to l i being fresh, this preserves the satisfiability of G. The notation e dx is a shorthand for (e dx 1 , . . . , e dx m ), the tuple of evaluation variables for each d x of x ∈ x. The purpose of a counterexample lemma is twofold. First, it indicates whether a quantified formula Q i is active (l i assigned to true) or inactive (l i assigned to false). Second, it focuses on finding counterexamples that falsify the body of Q i .

The main loop of procedure syqi is provided in lines 6-11. Each iteration starts with a quantifier-free satisfiability check (performed by procedure check on line 7) on the current set of ground formulas G in the combined theory T ∪ T D . If G is unsatisfiable, procedure syqi returns unsat. If G is satisfiable, the procedure further checks whether it can find a counterexample for any of the quantified formulas Q 1 , . . . , Q n , which is done by checking the satisfiability of G∧(l 1 ∨. . .∨l n ). If the check returns unsat then no more counterexamples can be found; the algorithm concludes that input set is satisfiable and returns sat. The reason is that, in this case, the set G is satisfiable and entails each input formula, as proven later in this section. If the second call to check (line 8) returns sat, it additionally returns (a finite representation of) a model I for the current set of ground formulas G. Since I satisfies l 1 ∨ . . . ∨ l n , it does not satisfy at least one quantified formula in Q 1 , . . . , Q n . 4 For each active quantified formula in I, we generate new lemmas via procedure select lemmas L (lines 10-11), and repeat the main loop of the algorithm. Note that the second satisfiability check can be avoided by employing a special decision heuristic for counterexample literals l i in the SAT solver. The decision heuristic will always assign a counterexample literal l i to true on a decision. Consequently, l i can only be assigned to false in a candidate interpretation I if ¬l i is entailed by the set of ground formulas G.

Procedure select lemmas L takes a formula ∀x. P [x] and a model I as arguments and generates a set of lemmas based on I and selection strategy L. The procedure maintains the invariant of always returning a set of lemmas L where L \ G is non-empty. This set L includes a single instantiation lemma (of the form P [t]) and an evaluation unfolding lemmas (see below) for each variable x ∈ x. The returned lemmas are generated based on one of three lemma selection strategies: priority-inst, priority-eval, and interleave. Strategy interleave selects both the instantiation lemma and a set of evaluation unfolding lemmas at the same time. Strategies priority-inst and priority-eval give priority to instantiation lemmas and evaluation unfolding lemmas, respectively; i.e., strategy priority-inst selects the instantiation lemma and only selects evaluation unfolding lemmas if the instantiation lemma was already in G. Analogously, priority-eval gives priority to evaluation unfolding lemmas.

The various lemmas are constructed as follows. For each variable x ∈ x we use the model value d I

x of datatype constant d x to construct the corresponding term to term(d I x ) in the theory of variable x (line 15). The constructed term corresponds to a term synthesized by the SyGuS extension of our datatypes solver based on the grammar specified for x. 

) ⇒ e dx = a + b. As a last step, select lemmas L selects a non-empty subset of the generated instantiation lemma P [t 1 , . . . , t p ] (where each t i is to term(d I xi )) and the evaluation unfolding lemmas L according to the lemma selection strategy L.

We now discuss the correctness properties of our approach. In the following, we say a grammar R for sort σ is complete, if for all interpretations I and values v of sort σ, it generates at least one term t such that t I = v. Note that we only consider complete grammars in this paper. We say a lemma selection strategy L is fair wrt a set of formulas G if it returns a set of lemmas that contain at least one lemma inequivalent to each formula in G whenever such lemma exists. Theorem 1. Let T be a theory with signature Σ, let F be a set of universal formulas {Q 1 , . . . , Q n } and G 0 is a set of quantifier-free formulas. If all grammars constructed by the calls to grammar S in syqi are complete and the selection strategy L used for select lemmas L is fair, then the following statements hold:

3. (Progress) Let G i be the current state of the set of ground formulas G after i iterations of syqi (lines 6-11). Each iteration i + 1 adds at least one new formula to G i , so that G i+1 \ G i = ∅.

Conceptually, the proof of refutational soundness relies on the fact that all lemmas added to G are entailed by the input or maintain equisatisfiability with respect to the input. The proof of model soundness relies on the fact that when G collectively entails the negation of (all) quantified formulas, then the current model I for G must be a model for all quantified formulas. Procedure syqi is not terminating in general. However, the progress property guarantees that the algorithm does not get stuck in a single state and keeps making progress towards refining the set of possible models by ruling out at least one candidate model at each iteration of the procedure's main loop.

Proof. For brevity, we show these statements for the case of n = 1 and where Q 1 is ∀x. P [x]; the proof can be easily lifted to n > 1. When syqi(F, G 0 ) terminates, the internal set G is the union of: To show (1), assume that ϕ is satisfied by some Σ-interpretation J , where without loss of generality assume that l J is false. Let I be a Σ∪Σ D -interpretation that extends J such that for each evaluation variable e d , the interpretation of d in I is such that to term(d I ) I = e I d . Such a value exists since our grammars are complete by assumption. We show that I satisfies each formula ψ in G. If ψ ∈ G 0 , then this holds since J satisfies ϕ, and hence, by extension I does as well. If ψ ∈ G cex , then ψ is satisfied by I since it interprets l i as false. If ψ ∈ G inst is an instantiation lemma of some Q i , then it is satisfied by I since J also satisfies Q i . If ψ ∈ G ev is an evaluation lemma, this is satisfied by our construction of d I . Thus ϕ is T -satisfiable, then G must be (T ∪ T D )-satisfiable. Thus, since syqi(F, G 0 ) returns unsat when G is (T ∪ T D )-unsatisfiable, this means that F ∪ G 0 must be T -unsatisfiable as well.

To show (2), if syqi(F, G 0 ) returns sat, then the set G is satisfied by some Σ ∪Σ D -interpretation and G∪{l 1 } is unsatisfiable. Let J be the Σ-interpretation that interprets all symbols in Σ the same as in I.

To show (3), assume ad absurdum that G is satisfied by a T ∪ T D -interpretation I where to term(d x I ) = t and Q 1 is active in I. Also assume that G contains the evaluation unfolding lemmas for d x I and the instantiation lemma P [t]. Due to the former, we have that e dx I = t I . Since Q 1 is active in I, I satisfies ¬P [e dx ]. However, P [t] is also satisfied by I, a contradiction. Thus, at least one of the lemmas returned by select lemmas L for Q 1 must be inequivalent to the lemmas in G, due to our assumption that L is a fair selection strategy.

For quantifier instantiation, we focus on the theories of fixed-size bit-vectors, floating-point numbers, integers, and reals as defined by the SMT-LIB 2 standard [4] . The signature of the theory of fixed-size bit-vectors includes a unique sort for each positive bit-vector width n, denoted here as BV [n] . The signature of the theory of floating-point numbers includes a rounding-mode sort RM and a unique floating-point sort for each combination of positive exponent width e and significand width s, denoted here as FP [e,s] . The theories of Integers and Reals include the integer sort Int and the real sort Real, respectively. For each of these sorts we define a SyGuS grammar that includes the following operators and constants. , we use bit strings where the left-most bit indicates the sign, the following e bits represent the exponent, and the remaining bits the significand. For the theory of fixed-size bit-vectors, we use smax [n] or smin [n] for the maximum or minimum signed value of width n, e.g., smax [4] = 0111 and smin [4] = 1000, and ones [n] for the maximum unsigned value, e.g., ones [4] = 1111. For the theory of floating-point numbers, we use ±0 for positive and negative zero, ±∞ for positive and negative infinity, and NaN for not a number, e.g., −0 [3, 5] = 10000000 and +∞ [3, 5] = 01110000. We further use ±min s for the positive and negative smallest subnormal, ±max s for the positive and negative largest subnormal, ±min n for the positive and negative smallest normal, and ±max n for the positive and negative largest normal, e.g., −max s [3, 5] = 10001111 and +min n [3, 5] = 00010000. In the definition of grammar R FP above, we use symbol ± to indicate that both the positive and negative variant of a special value is included in the grammar.

We extend the above set of default grammars (grammar S in Algorithm 1) with ground terms that occur in an input set {Q 1 , . . . , Q n }∪G 0 based on the sort of variable x ∈ x in Q i = ∀x. P [x] and a term selection strategy. This strategy is based on the following two factors. We consider three modes for the scope of ground terms: (1) ground terms that occur in quantified formula Q i (strategy in) (2) ground terms that occur in the set of ground formulas G (strategy out), and (3) the union of (1) and (2) (strategy both). We consider three modes for the size of ground terms, defined as the number of subterms a term consists of: (a) terms of minimal size, i.e., constants that occur in a term (strategy min) (b) terms of maximal size (strategy max), and (c) the union of (a) and (b) (strategy both). For example, for a ground term a + b · c, strategy min will select a, b, c, max will select a + b · c, and both will select a, b, c, a + b · c. Each of the scope and size modes may be combined, giving 3 * 3 = 9 possible term selection strategies.

where x, a, b have integer type and suppose we run syqi({Q}, ∅). The algorithm first constructs the grammar grammar S (x) for x, where we assume term selection strategy S with scope in and size min, which considers ground terms that occur in Q and are of minimal size (2, a, and b) . This grammar is encoded as the following datatype Z:

The algorithm introduces a fresh datatype variable d x of type Z, a fresh integer variable e dx of integer type, and adds l ⇒ e dx · e dx ≈ a · a + b · b + 2 · a · b to the internal set G of ground formulas, where l is a fresh Boolean variable. In the first iteration of the loop, we have that G (and G ∪ {l}) are satisfiable. Hence, the algorithm calls select lemmas L on Q and a model I for G; assume that d I x = zero and e I dx = a I = b I = 0. Based on the lemma selection strategy, we may choose to add the instantiation lemma 0 · 0 ≈ a · a + b · b + 2 · a · b, or the evaluation lemma is zero (d x ) ⇒ e dx ≈ 0, or both lemmas to G. Assuming both lemmas are added to G, the next iteration of the loop will consider a new model I where d I x = zero and e I dx = 0. The algorithm will continue finding models with new values for d x , until it finds a model I where d I x = plus(a, b) . At this point the instantiation lemma (a + b) · (a + b) ≈ a · a + b · b + 2 · a · b will be added to G, which is equivalent to false, and syqi will terminate with unsat.

We implemented syntax-guided quantifier instantiation in the CVC4 [5] solver, which has support for a wide range of background theories, covering all those in the SMT-LIB standard library [2] . CVC4 is based on the CDCL(T ) (formerly DPLL(T )) framework [19] . This framework integrates a propositional SAT solver, which attempts to find a Boolean assignment that propositionally satisfies the input formula, with one or more specialize theory solvers, which monitor the assignments made by the SAT solver to theory literal and flag a conflict if the assignments are ever inconsistent in their theory.

Our SyQI technique is implemented as a module of the subsolver of CVC4 that handles quantified formulas. We leverage CVC4's support for smart enumerative SyGuS as described in Reynolds et al. [22] . Specifically, the check method in line 7 in Algorithm 1 involves calling the (combination) of quantifier-free theory solvers, which includes an extension of the theory of datatypes described in the following.

Symmetry Breaking for Smart Enumerative Synthesis. As described in previous work [22, 24] , CVC4 uses advanced techniques for symmetry breaking for the datatypes over which context-free grammars are embedded. The quantifier-free datatype theory solver in CVC4 is extended to issue symmetry blocking clauses based on reasoning about such datatypes, so that the models we generate for a datatype variable d are such that to term(d) is unique with respect to rewriting. For example, the terms a + b and b + a are equivalent, and in CVC4, one will be rewritten to the other. Thus, we know that we only have to consider one variant, e.g., a + b. Hence, the extended datatypes solver may issue the blocking clause ¬is plus (d) ∨ ¬is b (sel Z,1 (d)) ∨ ¬is a (sel Z,2 (d)), effectively stating that the term associated with d should not be b + a. This technique is highly valuable for syntax-guided synthesis, since it reduces the set of terms considered in the search for candidate solutions. In the context of this work, these techniques are of great importance, since they guarantee that our algorithm does not consider multiple instantiations over tuples of pairwise equivalent terms.

Quantified Formulas within Boolean Structure and Nested Quantification. As mentioned earlier, while not shown in Algorithm 1, our approach uses standard techniques for handling qeneral quantified formulas, in particular with quantifiers that occur below Boolean connectives. In the context of CDCL(T ), for each quantified formula Q i of the form ∀x. P [x], the propositional model of our Boolean structure may either assign Q i to true or false, or leave it unassigned. Quantified formulas that are assigned to false are Skolemized, i.e., a lemma of the form ¬Q i ⇒ ¬P [k], where k are fresh constants, is returned to the SAT solver. Quantified formulas that are unassigned are ignored. Quantified formulas that are assigned to true are either active or inactive based on the value assigned to their counterexample literals. Those that are active are processed via select lemmas L . In practice, instantiation lemmas are guarded so that Q i ⇒ P [t] is returned to the SAT solver, meaning that the conclusion only holds when Q i is assigned to true. Furthermore, each Q i may have nested quantification, that is, the formula P the counterexample lemma l i ⇒ ¬P [e dx ] may contain quantified subformulas. Those quantified formulas are then processed by our full algorithm in the same way as quantified formulas from the input.

We implemented our approach in the SMT solver CVC4 [5] . We provide here an extensive evaluation of the techniques and strategies described in Section 3. We first evaluate term and lemma selection strategies for grammar construction, and then compare the performance of our best configuration against Z3 [16] , the only state-of-the-art SMT solver besides CVC4 that supports all the logics supported by our implementation.

We performed all experiments on a cluster with Intel Xeon CPU E5-2620 CPUs with 2.1GHz and 128GB memory. We used a time limit of 300 seconds, and an 8GB memory limit for each solver/benchmark pair and count memory out as time out. We evaluate here all configurations on all quantified logics in SMT-LIB [2] that do not contain uninterpreted functions (UF). As an exception, we include the logic UFBV, since the benchmarks in this logic rely almost entirely on BV reasoning only. We generally exclude logics with UF since for such logics counterexample-guided techniques, as in our approach, are not expected to be more effective than heuristic instantiation techniques such as E-matching, which we confirmed in a preliminary evaluation. Overall, we in- Term Selection for Grammar Construction. As a first experiment, we determine the best combination of scope-based and size-based ground term selection strategies for grammar construction as introduced in Section 3.1. We combine strategies based on scope with strategies based on term size into nine selection strategies: in-min, in-max, in-both, out-min, out-max, out-both, both-min, both-max, both-both. The results for our SyGuS instantiation approach with these strategies enabled is shown in Table 2 . Note that preliminary experiments identified lemma selection strategy interleave as the best. Hence, we use strategy interleave as the lemma selection strategy for this experiment.

Overall, using strategy both for the scope performs best. Furthermore, for this strategy all three size-based strategies perform equally well. For the remaining experiments, we use strategy both-both as the term selection strategy for grammar construction, where both minimal and maximal ground terms are selected from both the quantified formula Q i (containing the variable we construct a grammar for) and the set of ground formulas G. Note that we choose the more general strategy both-both over strategy both-max even though both-max performs slightly better.

Lemma Selection. In our second experiment, we determine the best lemma selection strategy out of the three strategies priority-inst, priority-eval and interleave described in Section 3. The results are shown in Table 2 . Note that we use the previously determined best term selection strategy both-both in this experiment.

The best overall strategy is interleave, indicating that it is beneficial to consider instantiation lemmas and evaluation unfolding lemmas in parallel. On the other hand, prioritizing evaluation lemmas over instantiation lemmas (priorityeval) performed significantly worse than the other two configurations. Since this strategy prioritizes evaluation lemmas, it has the advantage over other configurations of delaying instantiations until we obtain an interpretation I where the interpretation of e dx is consistent with respect to d x , i.e., e I dx = to term(d x ) I . As a consequence, prioritizing evaluation lemmas puts more effort into finding terms in instantiation that are guaranteed to refine the current candidate model I. However, we conclude from these results that it is often effective to consider instantiations in an eager fashion, either in parallel or even before considering evaluation lemmas. This is likely because instantiation lemmas may often refine the set of possible models even when G does not yet force our evaluation variables to have an interpretation that is consistent with their corresponding datatype values. Nevertheless, we found that evaluation lemmas are often necessary in practice for ensuring our procedure does not get stuck on a single model. When only instantiation lemmas are used, our procedure often terminates the loop with no new lemmas. This is to be expected, as such a strategy violates the requirements for the progress property of Theorem 1.

In the remaining experiment, we use strategy interleave as the lemma selection strategy since it performs slightly better than priority-inst.

Comparison Against Other Techniques. Finally, we compare our SyGuS instantiation approach against other techniques implemented in CVC4, the stateof-the-art SMT solvers Z3 [16] (version 4.8.9) and Boolector [17] (version 3.2.1), and the superposition-based theorem prover Vampire [13] (version 4.5.1). Note that Boolector implements counterexample-guided model synthesis [20] but only supports the SMT-LIB logic BV, whereas Vampire supports LIA, LRA, NIA, and NRA. We consider the following four configurations of CVC4: ematch: with E-matching [15] enabled; cegqi: with CEGQI for linear arithmetic [25] and bit-vectors [18] enabled, falls back to value-based instantiation techniques for other theories; enum: with enumerative instantiation [21] enabled; syqi: with our SyGuS instantiation approach enabled. We use strategy both-both for term selection, and interleave for lemma selection.

The results are summarized in Table 3 . First, note that Z3 disagrees on 10 benchmarks in logic FP with the other four CVC4 configurations. This is due to a known problem in Z3 related to operator rem, where it answers sat instead of unsat. We do not count these 10 benchmarks as solved and give the number of disagreements in parenthesis marked with a * in Table 3 .

Overall, note that E-matching (ematch) performs very poorly on these benchmark sets. This is not surprising since it is designed with a focus on problems with uninterpreted functions. To a lesser extent, enumerative instantiation (enum) also performs poorly, probably also due to the fact that it is not designed for inputs without uninterpreted functions. In detail, both this configuration and BV  sat  269  411  203  204  566  620  -(5846)  unsat  4752  5039  3846  4699  4934  4889  unsolved  825  396  1797  943  346  337  -BVFP  sat  113  110  26  29  174  --(224)  unsat  14  4  4  14  11  -unsolved  97  110  194  181  39  --BVFPLRA sat  103  95  67  67  164  --(185)  unsat  5  5  5  6  5  -unsolved  77  85  113  112  16  --FP  sat  34  28  23  23 syqi are enumerative in nature. The former uses a selection strategy based on the evolving ground terms in the current context, whereas the latter uses a fixed grammar built from the initial set of terms. In a sense, syqi leverages the power of a grammar for discovering new terms, whereas enum adapts to what terms are generated by instantiations. Overall, syqi solves 556 more benchmarks than enumerative instantiation, justifying the need for a syntax-guided approach for instantiation for inputs that are rich in background theories.

Our results show that syqi is remarkably competitive when compared to cegqi, which uses the best known theory-specific instantiation strategies. The performance of syntax-guided instantiation matches or exceeds counterexampleguided instantiation on logics BVFP, BVFPLRA, FP, FPLRA, NIA, NRA, and UFBV. In particular, for quantified floating-point arithmetic (FP), the performance of syqi significantly outperforms cegqi, where it solves 224 more bench-marks. We attribute this to the fact that cegqi only performs value-based instantiation, whereas the use of grammars is effective in determining useful symbolic terms to use in instantiations for this theory. Interestingly, syqi solves the only satisfiable benchmark in the NIA category that is unsolved by cegqi, meaning that in a portfolio setting with all available configurations, CVC4 solves all benchmarks in this category. On the other hand, counterexample-guided instantiation outperforms syqi on logics such as LIA, LRA, and BV, where wellestablished instantiation strategies exist. Syntax-guided techniques are especially ineffective for linear real arithmetic, since it is often important to construct specific real constants based on solving sets of linear (in)equalities [25] .

Comparing all configurations of CVC4 with Z3, Boolector, and Vampire, we see that in some logics like LIA and NIA, counterexample-guided instantiation in CVC4 outperforms Z3 and Vampire, whereas in other logics like NRA, UFBV, and many logics that combine BV, FP and LRA, Z3 performs best. For the logic BV, Boolector outperforms CVC4 and Z3; however, CVC4 solves the most unsatisfiable instances. The syqi configuration performs best on the floatingpoint benchmarks, where it solves 181 more than the closest competitor. When comparing the four CVC4 configurations in terms of uniquely solved instances, cegqi uniquely solves 660 instances, syqi 119 instances, enum 117 instances, and ematch not a single one. Between configurations cegqi and syqi, the former uniquely solves 1479 instances, and the latter 402 instances.

In summary, theory-specific approaches as implemented in CVC4, Z3, and Boolector outperform syqi in categories where instantiation strategies are highly mature, such as linear integer and real arithmetic, and fixed-width bit-vectors. Nevertheless, our evaluation demonstrates the versatility of the approach, especially for benchmarks using quantified floating-point arithmetic or combined theories where no good approach to quantifier instantiation was known.

We have presented a syntax-guided approach for quantifier instantiation and implemented it in the SMT solver CVC4. Our experiments show that our approach is a viable alternative to theory-specific quantifier instantiation techniques and can be applied to a wide range of logics. In particular, for the theory of floatingpoint arithmetic, syntax-guided instantiation in CVC4 significantly outperforms the state of the art. In future work, we plan to tune our grammar construction based on an analysis of which terms are more likely to appear in conflicts, which can potentially be done automatically. Another direction of future work is to provide an interface that would allow users to supply their own grammars for use in SyQI, similarly to the user-provided triggers for E-matching. We also plan to use our approach as a baseline for quantified logics in recent (and future) new theories. Currently, support in SMT solvers is highly limited, for instance, for quantified formulas involving the theory of strings and regular expressions. Syntax-guided instantiation can serve as a baseline for potential user applications that rely on quantified formulas in these theories.

Syntax-guided synthesis

The Satisfiability Modulo Theories Library (SMT-LIB) (2020)

An abstract decision procedure for satisfiability in the theory of recursive data types

The SMT-LIB Standard: Version 2.0

Computer Aided Verification -23rd International Conference

Playing with quantified satisfaction

Invertibility conditions for floating-point formulas

Simplify: a theorem prover for program checking

A decision procedure for the first order theory of real addition with order

Solving quantified verification conditions using satisfiability modulo theories

Complete instantiation for quantified formulas in satisfiabiliby modulo theories

Word level property directed reachability

First-order theorem proving and vampire

Applying linear quantifier elimination

Efficient e-matching for SMT solvers

Tools and Algorithms for the Construction and Analysis of Systems

Boolector 2.0

On solving quantified bit-vector constraints using invertibility conditions. Formal Methods in System Design pp

Solving SAT and SAT Modulo Theories: from an abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)

Counterexample-guided model synthesis

Revisiting enumerative instantiation

cvc4sy: Smart and fast term enumeration for syntax-guided synthesis

A decision procedure for (co)datatypes in SMT solvers

Counterexampleguided quantifier instantiation for synthesis in SMT

Solving quantified linear arithmetic by counterexample-guided instantiation

Quantifier instantiation techniques for finite model finding in SMT

Finding conflicting instances of quantified formulas in SMT

Datatypes with shared selectors

Efficiently solving quantified bit-vector formulas

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use