Lazy but Effective Functional Synthesis

Abstract

We present a new technique for generating a function implementation from a declarative specification formulated as a $\forall \exists$-formula in first-order logic. We follow a classic approach of eliminating existential quantifiers and extracting Skolem functions for the theory of linear arithmetic. Our method eliminates quantifiers lazily and produces a synthesis solution in the form of a decision tree. Compared to prior approaches, our decision trees have fewer nodes due to deriving theory terms that can be shared both within a single output as well as across multiple outputs. Our approach is implemented in a tool called AE-VAL, and its evaluation on a set of reactive synthesis benchmarks shows promise.

1 Introduction

The task of generating a function implementation from a specification of an input-output relation is commonly addressed by functional synthesis. Many prior approaches have been proposed for functional synthesis [10, 13, 16, 18, 20], with applications in various stages of software development, from prototyping to maintaining and repairing existing products. However, there is still a great need to make the synthesizers more robust and scalable, and the synthesized implementations more compact. We build this work on recent advances in lazy quantifier elimination methods [3, 6, 14, 17, 20] that enabled us to progress in both these dimensions.

Synthesis tasks are often formulated as quantified formulas. We consider formulas of the form $\forall \vec {x}\,.\,\exists \vec {y}\,.\,\psi (\vec {x}, \vec {y})$ (or $\forall \exists$-formulas in short¹). A simple example of a synthesis task formulated as a $\forall \exists$-formula to generate a max-function is shown below, where the two input variables $x_1$ and $x_2$ are universally quantified and the output y is existentially quantified:

$$\begin{aligned} \forall x_1, x_2 \,.\,\exists y \,.\,y \ge x_1 \wedge y \ge x_2 \wedge (x_1 = y \vee x_2 = y) \end{aligned}$$

The validity of this formula means that there always exists a maximum between two integers. A witness to the maximum value, i.e., a Skolem function $y = ite (x_1 \ge x_2, x_1, x_2)$, can then be generated (and suitably decoded as a statement in a program). In this paper, we consider the general case of synthesis of multi-output programs, i.e., with an arbitrary number of outputs. An example task is to generate a program that invokes both max and min-functions at the same time. An encoding of this task as a $\forall \exists$-formula is somewhat bulky, as shown below:

$$\begin{aligned} \forall x_1, x_2 \,.\,\exists y_1, y_2 \,.\,&y_1 \ge x_1 \wedge y_1 \ge x_2 \wedge (x_1 = y_1 \vee x_2 = y_1) \wedge \\&y_2 \le x_1 \wedge y_2 \le x_2 \wedge (x_1 = y_2 \vee x_2 = y_2) \end{aligned}$$

However, a solution for this synthesis task can still be formulated concisely: $ite (x_1 \ge x_2, y_1 = x_1 \wedge y_2 = x_2, y_1 = x_2 \wedge y_2 = x_1)$. In particular, note that the predicate $x_1 \ge x_2$ is shared between the two outputs $y_1$ and $y_2$ in the program, which respectively denote the values of the max and min functions.

Our synthesis procedure generates an implementation of a function while eliminating existential quantifiers in the formula, similar to prior work by Kuncak et al. [16]. However, quantifier elimination is an expensive iterative procedure in general. To lower the overall cost of functional synthesis, we propose to use a lazy procedure [6] for quantifier elimination in $\forall \exists$-formulas using Model-Based Projection (MBP) for linear arithmetic [14]. Unlike the prior work, our procedure does not require converting the formula into Disjunctive Normal Form (DNF), and thus often produces smaller and non-redundant implementations.

Along with the use of MBPs, we formulate criteria for an effective decomposition of a functional synthesis task. In particular, we aim at searching for a structured synthesis solution in the form of a decision tree, where each of the synthesis subtasks is defined in terms of a precondition and a set of Skolem constraints in a grammar, from which a function implementation is generated. While our notion of a precondition is similar to that in prior work [16], our MBP-based procedure results in fewer number of synthesis subtasks, thereby providing performance improvements and smaller implementations.

Our effective decomposition further enables optimization procedures for on-the-fly compaction of the generated function. In particular, we derive Skolem terms that can be re-used across multiple preconditions for a single output, and share the preconditions in a common decision tree across multiple outputs in the program. Our method identifies theory terms that can be shared both within and across outputs. While the motivation for such sharing is similar to optimization of Boolean gate-level circuits in the area of logic synthesis, our compaction is enabled by theory-specific reasoning (validity checks), not Boolean optimization at the propositional level. Our evaluation in a tool called AE-VAL demonstrates the benefits of our compaction algorithm, which further reduces the size of the resulting implementations by an average of two.

We have implemented our ideas in AE-VAL on top of our prior work [6], which described a procedure for determining the validity of $\forall \exists$-formulas using MBPs for linear arithmetic [14]. The focus of that effort was on deriving Skolem witnesses for a simulation relation between two given programs. However, there was no method described for functional synthesis, which requires deriving a Skolem function rather than a Skolem relation. Furthermore, it did not consider minimization or compaction of the generated implementations. Note again, that this minimization/compaction is not at the propositional level, but requires theory-specific reasoning. The required validity checks for compaction are built into the synthesis procedure and use the same MBP-based validity checker recursively. We provide a detailed evaluation of our tool on a selection of public benchmarks from SyGuS-COMP² and benchmark examples for reactive synthesis from Assume-Guarantee contracts [13].

We start by providing some background in Sect. 2. Next, in Sect. 3, we describe our criteria for effective decomposition and the MBP-based procedure for formulating the synthesis subtasks. In Sect. 4, we present a method for extracting Skolem functions from Skolem constraints. In Sect. 5, we describe our algorithm for compaction and re-use of theory terms within and across subtasks. We have implemented our procedure for functional synthesis for linear arithmetic and present a detailed evaluation in Sect. 6. Related work is described in Sect. 7 and conclusions in Sect. 8.

2 Background and Notation

A many-sorted first-order theory consists of disjoint sets of sorts , function symbols and predicate symbols . A set of terms is defined recursively as follows:

$$\begin{aligned} term \, {:}{:}\!= f( term , \dots , term ) \mid const \mid var \end{aligned}$$

where , $const$ is an application of some of zero arity, and $var$ is a variable uniquely associated with a sort in . A set of quantifier-free formulas is built recursively using the usual grammar:

$$\begin{aligned} formula \, {:}{:}\!=&\, true \mid false \mid p( term , \dots , term ) \mid Bvar \mid \\&\lnot formula \mid formula \wedge formula \mid formula \vee formula \, \end{aligned}$$

where true and false are Boolean constants, , and $Bvar$ is a variable associated with sort Bool.

In this paper, we consider theories of Linear Rational Arithmetic (LRA) and Linear Integer Arithmetic (LIA). In LRA, , , where $\cdot$ is a scalar multiplication (i.e., it does not allow multiplying two terms which both contain variables), and . In LIA, , , where div is an integer division³ , and . For both LRA and LIA, we use a shortcut , but do not include ite in .

Formula $\varphi$ is called satisfiable if there exists an interpretation m, called a model, of each element (i.e., a variable, a function or a predicate symbol), under which $\varphi$ evaluates to true (denoted $m\models \varphi$); otherwise $\varphi$ is called unsatisfiable. If every model of $\varphi$ is also a model of $\psi$, then we write $\varphi \implies \psi$. A formula $\varphi$ is called valid if $true \implies \varphi$.

For existentially-quantified formulas of the form $\exists y \,.\,\psi (\vec {x}, y)$, validity requires that each interpretation for variables in $\vec {x}$ and each function and predicate symbol in $\psi$ can be extended to a model of $\psi (\vec {x}, y)$. For a valid formula $\exists y \,.\,\psi (\vec {x}, y)$, a term $sk _{y}(\vec {x})$ is called a Skolem term, if $\psi (\vec {x}, sk _{y} (\vec {x}))$ is valid. More generally, for a valid formula $\exists \vec {y}\,.\,\psi (\vec {x}, \vec {y})$ over a vector of existentially quantified variables $\vec {y}$, there exists a vector of individual Skolem terms for every variable $\vec {y}[j]$, where $0 < j \le N$ and $N = |\vec {y}|$, such that:

$$\begin{aligned} true \implies \psi (\vec {x}, sk _{\vec {y}[1]} (\vec {x}),\ldots , sk _{\vec {y}[N]} (\vec {x})) \end{aligned}$$

(1)

In the paper, we assume that all free variables $\vec {x}$ are implicitly universally quantified. For simplicity, we omit the arguments and simply write $\varphi$ when the arguments are clear from the context.

3 Decomposing Functional Synthesis

A functional synthesis task aims at generating a function from a given input-output relation. We view this in terms of validity checking of $\forall \exists$-formulas and derive Skolem terms for the existentially-quantified variables. We propose to discover Skolem terms in stages: an original task is decomposed into subtasks, where each of the subtasks is solved in isolation, and the solution to the original problem is obtained as one common decision tree that combines the results from the subtasks.

3.1 Illustrative Example

Consider a given formula in Disjunctive Normal Form (DNF) (we defer a discussion of a general case until later in this section). Here, it is intuitively easy to see that the individual Skolem function for each $\vec {y}[j]$ can be represented in the form of a decision tree, as illustrated in the following example.

Example 1

Given a formula $\exists y_1, y_2 \,.\,\psi (x, y_1, y_2)$ in LIA, where

The formula is valid, which means that for every value of x there exist values of $y_1$ and $y_2$ that make either of two disjuncts true. Intuitively, the disjuncts correspond to two cases, when $x \le 2$ or $x \ge -1$. We call these formulas preconditions.

To extract Skolem terms for $y_1$ and $y_2$, this example permits considering two preconditions in isolation (however, it may not be true for other formulas, see Sect. 3.3). That is, if $x \le 2$, then $y_1$ should satisfy $y_1 > -3 \cdot x$ and $y_2$ should satisfy $y_2 < x$. In other words, the following two formulas are valid:

$$\begin{aligned} (x \le 2)&\implies \exists y_1 \,.\,(y_1 > -3 \cdot x) \\(x \le 2)&\implies \exists y_2 \,.\,(y_2 < x) \end{aligned}$$

Skolem terms for $y_1$ and $y_2$ assuming $x \le 2$ could be $-3 \cdot x + 1$ and $x-1$ respectively. Similarly, for the second precondition:

$$\begin{aligned} (x \ge -1)&\implies \exists y_1 \,.\,(y_1 < 5 \cdot x ) \\(x \ge -1)&\implies \exists y_2 \,.\,(y_2 > x) \end{aligned}$$

Assuming $x \ge -1$, a Skolem term for $y_1$ could again be $-3 \cdot x + 1$, but a Skolem term for $y_2$ is $x+1$. Combining these Skolem terms for both preconditions, we get Skolem terms for $\exists y_1, y_2 \,.\,\psi (x, y_1, y_2)$:

Note that this composition is possible because $(x \le 2) \vee (x \ge -1)$ is valid. In the next subsection, we describe this process formally.

3.2 Effective Decomposition

Our functional synthesis technique is based on a notion we call effective decomposition, defined below.

Definition 1

A decomposition of a valid formula $\exists \vec {y}\,.\,\psi (\vec {x}, \vec {y})$ is a tuple $\langle pre, \phi \rangle$, where pre (called preconditions) is a vector of formulas of length M and $\phi$ (called Skolem constraints) is a matrix of dimensions $M \times |\vec {y}|$, such that the following three conditions hold.

Lemma 1

For every valid formula $\exists \vec {y}\,.\,\psi (\vec {x}, \vec {y})$, a decomposition exists.

Indeed, a decomposition could be constructed by the formula itself and a precondition true. We are not interested in such cases because they do not simplify a process of extracting Skolem terms from Skolem constraints $\phi$. Instead, we impose additional syntactic restrictions on $\phi$. In particular, we call a decomposition $\langle pre, \phi \rangle$ of $\exists \vec {y}\,.\,\psi (\vec {x}, \vec {y})$ -effective if all formulas $\phi$ are expressible in some grammar .

The task of extracting Skolem terms boils down to developing an algorithm that (1) produces Skolem constraints in , and (2) exploits to extract a matrix of Skolem terms from a matrix of Skolem constraints, i.e., the following holds:

Theorem 1

Let $\langle pre, \phi \rangle$ be a decomposition of $\exists \vec {y}\,.\,\psi (\vec {x}, \vec {y})$, and sk be a matrix of Skolem terms, such that (embedding) holds. Then $Sk _{j}$ is the Skolem term for $\vec {y}[j]$:

Fig. 1.

A decision tree.

A straightforward implementation of $Sk_j$ in the form of a decision tree is shown in Fig. 1.

In this work, we restrict to be the grammars of LIA/LRA (see Sect. 2) but allow neither disjunctions nor negations. In the next subsection, we outline an algorithm that creates a -effective decomposition while solving formulas for validity. Then, in Sect. 4, we present an algorithm for extracting Skolem terms from formulas in .

3.3 Witnessing Existential Quantifiers with AE-VAL

Obtaining preconditions in general requires quantifier elimination. However, it leads to expensive reasoning, which we would like to improve upon.

Example 2

Consider the following formula:

$$\begin{aligned} \exists y_1, y_2 \,.\,\big ( y_1> x_1 \vee y_2< -x_2 \big ) \wedge \big ( y_1 < x_2 \vee y_2 > -x_1 \big ) \end{aligned}$$

If we were running the algorithm from [16], we would need to convert this formula into DNF, which would give us four disjuncts. A complete quantifier-elimination procedure would be then required to produce four preconditions and four Skolem constraints.

Our lazy quantifier-elimination method, called AE-VAL, generates both preconditions and Skolem constraints while solving the given formula for validity. In contrast to the DNF translation, for the formula in Example 2, it generates only two preconditions and two Skolem constraints.

The pseudocode of AE-VAL is shown in Algorithm 1 (we refer the reader to [6] for more detail). AE-VAL produces a sequence of Model-Based Projections (MBPs, see the definition below) [14], each of which under-approximates quantifier elimination. It iterates until the disjunction of MBPs is valid and thus avoids a complete quantifier elimination.

Definition 2

An $MBP _{\vec {y}}$ is a function from models of $\psi (\vec {x},\vec {y})$ to $\vec {y}$-free formulas if it has a finite image and the following hold:

$$\begin{aligned} \text {if }m\models \psi (\vec {x},\vec {y}) \text { then } m\models MBP _{\vec {y}}(m,\psi ) \\ MBP _{\vec {y}}(m,\psi ) \implies \exists \vec {y}\,.\,\psi (\vec {x},\vec {y}) \end{aligned}$$

There are different algorithms for constructing MBPs for different theories. We follow a method from [3] for LIA and present it on the following example. Intuitively, it is based on finding models, testing them on literals of the original formula, and eliminating quantifiers from the conjunctions of literals that passed the test.

Example 3

Recall the formula $\exists y_1,y_2 \,.\,\psi (x_1, x_2, y_1, y_2)$ from Example 2. Its set of literals is $Lit = \{ y_1> x_1 , y_2< -x_2 , y_1 < x_2 , y_2 > -x_1\}$. In the first iteration, AE-VAL generates a model $m_1$ of $\psi$: $m_1 = \{x_1\mapsto 0, x_2 \mapsto -2, y_1 \mapsto 0, y_2 \mapsto 1\}$. An MBP of $\psi$ w.r.t. $m_1$ is then generated iteratively: by eliminating $y_1$ first, and eliminating $y_2$ then.

For $y_1$ and $m_1$, AE-VAL fills $\phi [1,1]$ with a set of literals $\{l \in Lit \mid y_1\in vars(l) \wedge m_1\models l\}$, i.e., $\{y_1 < x_2\}$. Then AE-VAL eliminates quantifiers from $\exists y_1 \,.\,\phi [1,1]$ and adds the result (i.e., true) to the MBP.

For $y_2$ and $m_1$, AE-VAL fills $\phi [1,2]$ with $\{l \in Lit \mid y_2\in vars(l) \wedge m_1\models l\}$, i.e., $\{y_2 < -x_2 , y_2 > -x_1\}$. It then eliminates quantifiers from $\exists y_2 \,.\,\phi [1,2]$ and adds the result (i.e., $x_1 - x_2 > 1$) to the MBP.

Thus, after the first iteration of AE-VAL, we get the precondition $pre[1] = x_1 - x_2 > 1$, and Skolem constraints $\phi [1,1]$ and $\phi [1,2]$. The second iteration proceeds similarly, and AE-VAL outputs $pre[2] = true$, $\phi [2,1] = y_1 > x_1$, and $\phi [2,2] = y_2> - x_1$, and terminates.

Lemma 2

If AE-VAL returns $\langle \textsc {valid}, pre, \phi \rangle$ for a formula $\exists \vec {y}\,.\,\psi (\vec {x}, \vec {y})$, then the formula is effectively decomposable by pre and $\phi$, i.e., (i-totality),

(under-approximation), and (j-totality) hold.

Intuitively, the sequence of MBPs provides a lazy disjunctive decomposition of the overall problem, where each precondition can capture an arbitrary subspace on the $\vec {x}$ variables (under which it is possible to derive a Skolem term for the $\vec {y}$ variables). It often requires far fewer decompositions than a DNF-based quantifier elimination approach, where each precondition can at best be a cube, i.e., a conjunction of predicates on $\vec {x}$. Note that the number of decompositions, M, corresponds directly to the depth of the decision tree in the generated implementations. Thus, our MBP-based procedure for quantifier elimination can potentially perform better and lead to smaller implementations. Our experimental results in Sect. 6 show promising support.

4 Extraction of Skolem Terms

In this section, we describe our procedure for extracting individual Skolem terms from a matrix of Skolem constraints $\phi [i,j]$ in linear arithmetic. As pointed out in (embedding), this procedure is performed independently of a precondition pre[i]. We first describe the procedure where each $\phi [i,j]$ has occurrence of only one variable $y = \vec {y}[j]$, and thus has form $\pi (\vec {x},y)$; and $pre[i](\vec {x}) \implies \exists y \,.\,\pi (\vec {x},y)$ is valid. In Sect. 4.3, we describe how to handle occurrences of multiple $\vec {y}$ variables.

Although the general extraction schema is similar for all background theories, specific algorithmic details of each theory need to be discussed. In the rest of this section, we separately consider algorithms for LRA and LIA.

4.1 Skolem Terms in LRA

In Algorithm 2, we show how to extract a Skolem term for a variable $y \in \vec {y}$ from constraints having form $\pi (\vec {x},y)$. Intuitively, Algorithm 2 constructs a graph of a function that is embedded in a relation specified by a conjunction of equalities, inequalities, and disequalities over y and $\vec {x}$. Thus, Algorithm 2 takes as input six vectors of clauses extracted from $\pi$: E, D, G, GE, L, and LE:

We do not consider constraints having the shape $\alpha \cdot y \sim f(\vec {x})$, because it is safe to normalize it to $y \sim \frac{f(\vec {x})}{\alpha }$ (assuming positive $\alpha$; a negative $\alpha$ requires swapping the operator $\sim$ between < and >, and $\le$ and $\ge$). Finally, we assume that at least one of the vectors of clauses is non-empty, otherwise a Skolem term could be arbitrary, and there is no need to run Algorithm 2.

Below we present several helper-operators needed to construct a term sk based on a lightweight analysis of clauses in E, D, G, GE, L, and LE (where $\sim \,\in \{<,\le ,=,\ne ,\ge ,>\}$):

In the case when there is at least one conjunct $(y = e(\vec {x})) \in E$ (line 1), the algorithm simply returns the exact term $e(\vec {x})$. Note that there could be two or more equalities in E, which are consistent with each other due to (j-totality). Thus, it does not matter which of them is used for extracting a Skolem term.

In the case when there are lower and upper bounds (lines 2 and 3 respectively), the algorithm extracts expressions that encode the maximal and minimal values that y can take. Technically, it is done by mapping sets G and GE (for $\textsc {MAX}$) and L and LE (for $\textsc {MIN}$) to results of applications of ASSM to elements of these sets. In the case when $D = \varnothing$ or when $\ell$ and u are semantically equal, the algorithm has sufficient information to extract a Skolem term. In particular, if both lower and upper bounds are extracted, the algorithm returns a symbolic midpoint (line 6). Otherwise, it returns a symbolic value which differs from the upper or lower bounds (whichever is present) by one (lines 7 and 8).

Example 4

Consider $\pi = (y > 4 \cdot x_1) \wedge (y \ge -3 \cdot x_2 + 1) \wedge (y < x_1 + x_2)$. Algorithm 2 aims at extracting a term sk such that $\big (y = sk(x_1, x_2)\big ) \implies \pi$. First, the algorithm extracts the lower bound from two inequalities with “>” and“$\ge$”: $\ell = max (4 \cdot x_1, -3 \cdot x_2 + 1) = ite(4 \cdot x_1 > -3 \cdot x_2 + 1, 4 \cdot x_1, -3 \cdot x_2 + 1)$. Second, the algorithm extracts the upper bound from the only “<”-inequality: $u = x_1 + x_2$. Finally, the algorithm extracts and returns the symbolic midpoint between $\ell$ and u. That is, $sk = \frac{ite(4 \cdot x_1 > -3 \cdot x_2 + 1, 4 \cdot x_1, -3 \cdot x_2 + 1) + (x_1 + x_2)}{2}$.

The rest of the algorithm handles disequalities, i.e., in the case when $D \ne \varnothing$ (line 9). It assumes that $\ell$ and u are extracted, otherwise any suitable $\ell$ and u could be selected (in lines 10–12, we use some particular but not the only possible choice).

Intuitively, if y is required to differ from some $h(\vec {x})$ and to be in a range $(\ell ,u)$, it is sufficient to pick two distinct terms $v_1$ and $v_2$ such that:

$$\begin{aligned} (y = v_1(\vec {x}))&\implies (\ell (\vec {x})< y< u(\vec {x})) \\(y = v_2(\vec {x}))&\implies (\ell (\vec {x})< y < u(\vec {x})) \\(v_1(\vec {x}) = v_2(\vec {x}))&\implies false \end{aligned}$$

Since each variable assignment m to $\vec {x}$ makes at most one formula from set $\{h(m) = v_1(m), h(m) = v_2(m)\}$ true, we can always extract a Skolem term $sk=ite(h = v_1,v_2,v_1)$ that satisfies $(y = sk(\vec {x})) \implies (y \ne h(\vec {x}))$.

A similar reasoning is applied to any set D of disequalities: it is enough to consider $|D| + 1$ terms, which are semantically distinct. Our algorithm can be parametrized by any routine that extracts semantically distinct terms belonging to a range between $\ell$ and u. Two of possible routines are inspired respectively by a binary search (which is used in line 13) and a linear scan.

Definition 3

Let n be the number of disequalities in D and H be the set of right sides of expressions of D, then the binary-search helper-operator is defined as follows:

Example 5

Consider $\pi = (y \ne x_1 \wedge y \ne x_2)$. Since there are no inequalities in $\pi$, the lower and upper bounds are obtained from an arbitrary range, say (0, 1). Otherwise, they are computed similarly to as in Example 4. Algorithm 2 uses BNSR and returns the following Skolem term:

$$\begin{aligned} sk = ite\Big (\frac{1}{2} = x_1 \vee \frac{1}{2} = x_2, ite\Big (\frac{1}{4} = x_1 \vee \frac{1}{4} = x_2, \frac{1}{8}, \frac{1}{4}\Big ), \frac{1}{2}\Big ) \end{aligned}$$

Definition 4

Let s be some number, then

Example 6

Consider formula $\pi$ from Example 5, for which $H = \{x_1, x_2\}$, $\ell = 0$, and $u = 1$. A Skolem term can be compiled using the call to

$\textsc {SCAN}(\ell + \frac{u - \ell }{|H| + 2}, \frac{u - \ell }{|H| + 2}, H, |H| + 1)$:

$$\begin{aligned} sk = ite\Big (\frac{1}{4} = x_1 \vee \frac{1}{4} = x_2, ite\Big (\frac{1}{2} = x_1 \vee \frac{1}{2} = x_2, \frac{3}{4}, \frac{1}{2}\Big ), \frac{1}{4}\Big ) \end{aligned}$$

4.2 Skolem Terms in LIA

In this subsection, we present an algorithm for extracting Skolem terms in LIA. Although the flow of the algorithm is similar to the flow of the algorithm for LRA, presented in Sect. 4.1, there are two differences. First, there is no need to calculate a midpoint in the case when both a lower bound $\ell$ and an upper bound u are given. Instead, because (j-totality) guarantees the existence of at least one integer value for all y, it is enough to choose either the least or the greatest integer value within the range $(\ell , u)$. Second, there are divisibility constraints, which have to be treated more carefully. Unlike the case of LRA, we consider four vectors of clauses in the Skolem constraints $\pi$ over LIA:

We can safely avoid clauses containing < and $\ge$ because of the following transformations:

We need these rules to simplify the normalization of inequalities by dividing their right sides by $\alpha$ (assuming positive $\alpha$; a negative $\alpha$ requires changing the operator $\sim$ accordingly). For example, it would not be correct to normalize an inequality $5 \cdot y \ge 9$ to $y \ge div (9,5)$. Instead, when $5 \cdot y \ge 9$ is rewritten to $5 \cdot y > 8$, the normalization works correctly: $y > div (8,5)$. Similarly, an inequality $5 \cdot y < 9$ should be rewritten to $5 \cdot y \le 8$ and normalized to $y \le div (8,5)$.

We also rewrite the divisibility constraints (i.e., $div(y,\alpha ) \sim f(\vec {x})$) using the following transformations (in addition to applying (3)):

An example for applying the first rule is $div (y, 3) = 0$: y could be either 0, 1, or 2; or in other words $0 \le y \wedge y < 3$. For the second rule, an example is $div (y, 3) > 0$: y could be anything greater or equal than 3, or alternatively greater than 2. Similarly, $div (y, 3) \le 0$ is equivalent to $y \le 2$. Finally, the rule for disequalities enumerates a finite number (equal to $\alpha$) of disequalities of form $y \ne f(x)$. For instance, $div (y, 3) \ne 1$ is equivalent to $y \ne 3 \wedge y \ne 4 \wedge y \ne 5$.

The pseudocode of the algorithm that extracts a Skolem term for $\pi$ in LIA is shown in Algorithm 3. It handles constraints using the following helper-operators.

Definition 5

Let $h[y/\ell ]$ denote the term h with term $\ell$ substituted for variable y. Then a helper-operator for the linear scan in LIA is implemented as follows.

For the case when there exists an equality $\alpha \cdot y = e(\vec {x})$ in $\pi$, it is sufficient to extract $div(e, \alpha )$ for sk, because requirement (j-totality) guarantees that e is divisible by $\alpha$. This is implemented in function $\textsc {ASSM}_{\mathbb {Z}}$. To handle disequalities, the algorithm can only perform a linear scan, i.e., starting from the lower bound to make the least possible increments (i.e., by one). As opposed to the binary search, the linear scan guarantees that enough semantically distinct terms are considered. We illustrate this in the following example.

Example 7

Consider $\pi = (5 \cdot y \ne 4 \cdot x)$. Since there is no lower bound and no upper bound, we allow $\ell = 0$ (alternatively, any other term can be chosen). Then, since $\pi$ has only one disequality, we get the final Skolem as a single if-then-else: $ite\Big (\big (5 \cdot 0 \ne 4 \cdot x), 0, 1\Big )$.

4.3 Putting It All Together

Theorem 2

For some i, let $\phi [i,j](\vec {x}, \vec {y})$ be in LRA (resp. LIA), and $|\vec {y}| = N$. Then for each $j \in [1, N]$, Algorithm 2 (resp. Algorithm 3.) extracts a term sk[i, j], such that (embedding) holds.

For proving this theorem, it remains to show how we obtain $\pi (\vec {x}, \vec {y}[j])$ that Algorithm 2 (resp. Algorithm 3) should take as input with each $\vec {y}[j]$. Indeed, the MBPs constructed in Sect. 3.3 allow occurrences of multiple variables from $\vec {y}$ in a clause in $\phi [i,j]$. However, by construction, a variable $\vec {y}[j]$ can appear in all $\phi [i,k], 1 \le k \le j$, but a variable $\vec {y}[j]$ cannot appear in any $\phi [i,k], j < k \le N$. In particular, term $\phi [i,N]$ is only over the variables $\vec {x}$ and $\vec {y}[N]$. Therefore, we first apply Algorithm 2 (resp. Algorithm 3) to $\phi [i,N]$, to derive the Skolem term sk[i, N]. It is then substituted in all appearances of $\vec {y}[N]$ in other constraints $\phi [i,N-1], \ldots , \phi [i,1]$. Continuing such reasoning over the remaining variables leads to obtaining suitable inputs for Algorithm 2 (resp. Algorithm 3) and each $\vec {y}[j]$.

5 Synthesis of Compact Skolem Terms

Recall that Theorem 1 gives a way to construct a global Skolem term from preconditions and relations, and Sect. 4 describes algorithms to extract a local term sk[i, j] from a relation $\phi [i,j]$. So far, this provides a procedure that invokes Algorithm 2 or Algorithm 3 as soon as possible, i.e., when $\phi [i,j]$ has just been produced by the MBP-based procedure AE-VAL together with some pre[i]. However, for large formulas it is often the case that the number M of generated MBPs is large, and so is a vector of tuples $\langle pre[i], \bigwedge \limits _{0 < j \le N}\phi [i,j] \rangle$ where $0 < i \le M$.

In this section, we propose to leverage the output of AE-VAL for producing compact Skolem terms. We first describe how to reduce the number of distinct Skolem terms among the tuples generated by AE-VAL for each $y\in \vec {y}$. Next, we aim to reduce the depth of the overall decision tree in case of multiple outputs $\vec {y}$, i.e., extracting a common if-then-else (ite) block which is shared among all outputs.

Fig. 2.

Optimized decision tree.

5.1 Optimizing Decision Trees by Combining Preconditions

Our goal is to decrease the depth of a decision tree that combines Skolem terms for M different preconditions. Recall that at each node i, where $0 < i \le M$ and for variable $y = \vec {y}[j]$, the Skolem term sk[i, j] and the precondition pre[i] should be connected via (j-totality) and (embedding), i.e.:

$$\begin{aligned}&pre[i](\vec {x}) \implies \exists y \,.\,\phi [i,j](\vec {x}, \vec {y}) \\&y = sk[i,j](\vec {x}) \implies \phi [i,j](\vec {x}, \vec {y}) \end{aligned}$$

Note that preconditions in the decision tree could potentially guard the same Skolem terms, in which case we could compact the size. This is illustrated pictorially in Fig. 2 for the example shown earlier in Fig. 1. In particular, if sk[1, j] and sk[2, j] in Fig. 1 could be replaced by a common $sk'$, then the preconditions pre[1] and pre[2] can be merged using a disjunction, thereby decreasing the depth of the decision tree. The challenge is that $sk'$ might not necessarily be obtained by Algorithm 2 or Algorithm 3, because Skolem constraints $\phi [1,j]$ or $\phi [2,j]$, taken in isolation, are in general not restrictive enough. However, $sk'$ could be produced by Algorithm 2 or Algorithm 3 if $\phi [1,j] \wedge \phi [2,j]$ is given as input.

Generalizing this idea further, we consider an expensive minimization algorithm to search over all partitions of the set and find the best partition such that each index in a class of the partition can share the same Skolem term. More formally, for each partition of $\mathbb {M}$, for each class $p_k$ in the partition, we check that:

If all r implications hold, then $\mathbb {P}$ is a valid candidate partition, associated with r Skolem terms $sk',\ldots , sk^{(r)}$ derived from $\bigwedge \limits _{i\in p_1}\phi [i,j](\vec {x}, y)$, ..., $\bigwedge \limits _{i\in p_r}\phi [i,j](\vec {x}, y)$, respectively. We then select the best partition among the valid candidate partitions, based on size of resulting Skolem terms (or other cost criteria). Clearly, examining all possible partitions would have exponential cost, with the check for each partition class also being an expensive validity check.

Instead of the expensive exact minimization, we adopt a greedy strategy for finding a good (but not necessarily the best) valid candidate partition, possibly within a predetermined number of iterations. The routine for identifying each partition class $p_k$ is shown in Algorithm 4. First, $p_1$ is selected from $\mathbb {M}$, then $p_2$ is selected from $\mathbb {M}\setminus p_1$, and so on.

Algorithm 4 is based on iteratively guessing a set of indices $p_k$ and checking an implication of the form (4). The guessing proceeds in two phases: first it checks if all eligible indices from a set $\mathbb {I} \subseteq \mathbb {M}$ are in $p_k$. If so, the algorithm terminates. Otherwise, it iteratively tries to strengthen the left side of (4) by removing some of the disjuncts (line 3). After removing a disjunct $pre[i']$ from the left side, the Skolem constraint $\phi [i',j]$ should also be removed from the right side, and the validity check repeats. This way, the algorithm is guaranteed to find the set of indices $p_k$ (possibly, empty) in a finite number of iterations.

The second phase of the guessing aims at strengthening $p_k$. It simply traverses the set of indices $\mathbb {I} \setminus p_k$ (line 5), adds $pre[i']$ and $\phi [i', j]$ to the left and right sides of 4 respectively and checks validity. The motivation behind the second phase is that the first phase could be too aggressive in practice, thus removing more indices from $p_k$ than needed.

Example 8

Recall our formula from Example 1. For generating a Skolem term for $y_1$, we create the following $\forall \exists$-formula and check its validity:

$$\begin{aligned} (x \ge -1 \vee x \le 2) \implies \exists y_1 \,.\,( y_1 < 5 \cdot x \wedge y_1 > -3 \cdot x) \end{aligned}$$

Since this formula is valid, our algorithm creates a single Skolem term $sk[1,1] = sk[1,2] = -3 \cdot x + 1$.

For generating a Skolem term for $y_2$, the corresponding $\forall \exists$-formula is invalid, and our algorithm generates two different Skolem terms sk[2, 1] and sk[2, 2]:

$$\begin{aligned} (x \ge -1 \vee x \le 2) \implies \exists y_2 \,.\,( y_2 < x \wedge y_2 > x ) \end{aligned}$$

5.2 Minimizing the Depth of the Common Decision Tree

To allow re-use of theory terms among multiple outputs $\vec {y}$, a common ite-block could be pulled outside of the individual decision trees for each output, denoted $Sk _{\vec {y}} (\vec {x}, \vec {y})$:

In general, depending on the cost criteria, it may be advantageous to not have a common ite-block at all or to have it be common to a subset of the outputs rather than all outputs. In this section, we consider a simple case where a common ite-block is shared among all outputs. Then, the remaining goal is to reduce the depth of this block by finding redundant branches.

Recall that Algorithm 4 can be used per output to find a good partition among the tuples, i.e., to decide which branches of the ite-block can share the same Skolem term. We view the results from this algorithm in the form of a matrix of Skolem terms, with a row for each ite-branch and a column for each output. Then, it is straightforward to identify redundant branches, which correspond to identical rows in the matrix. We illustrate this process in an example.

Example 9

Consider a formula with four existentially quantified variables $\vec {y}$ and four preconditions. Suppose the algorithm from Sect. 5 returns the partitions of the set $\{1,2,3,4\}$ for each variable in $\vec {y}$, as shown in the following matrix.

For instance, $\vec {y}[1]$ requires a partition $\{p_1\}$ where $p_1 = \{1,2,3,4\}$. Variable $\vec {y}[2]$ requires partition $\{q_1, q_2\}$ where $q_1 = \{1\}$ and $q_2 = \{2,3,4\}$. Variable $\vec {y}[3]$ requires partition $\{r_1, r_2\}$ where $r_1 = \{1,2,4\}$ and $q_2 = \{3\}$. Variable $\vec {y}[4]$ requires partition $\{s_1, s_2, s_3\}$ where $s_1 = \{1\}$, $s_2 = \{2,4\}$ and $s_3 = \{3\}$.

We can easily identify identical rows $A_1,\ldots A_k$ in the matrix, such that for all $0< j < M$, elements $A_1[j] = A_2[j] = \ldots = A_k[j]$ are equal.

In this example, row $A_1$ corresponds to pre[2], and row $A_2$ corresponds to pre[4]. Thus, individual Skolem terms for all variables for pre[2] and pre[4] can be combined, and the depth of the common ite-block is reduced by one.

6 Evaluation

We implemented our synthesis algorithms on top of the AE-VAL tool [6] which is in turn built on top of the Z3 SMT solver [5]. Note that the previous implementation of AE-VAL was already able to solve quantified formulas for validity via an iterative MBP construction and to extract Skolem constraints. However, it did not provide procedures to extract Skolem functions (described in Sect. 4) or to compact them (described in Sect. 5). In particular, note that during our compaction procedure, we use AE-VAL recursively to solve subsidiary quantified formulas of the form (4).

6.1 Results on Benchmark Examples

We considered 134 $\forall \exists$-formulas originated from various Assume-Guarantee contracts written in the Lustre programming language [13]⁴. The majority of benchmarks are derived from industrial projects, such as a Quad-Redundant Flight Control System, a Generic Patient Controlled Analgesia infusion pump, as well as a Microwave model, a Cinderella-Stepmother game, and several hand-written examples. Since the original set of benchmarks include minor variations of the same tasks, we identified 80 distinct benchmarks⁵ for presentation in Table 1.

All the $\forall \exists$-formulas had more than one existentially-quantified variable. Table 1 presents the statistics and results on the benchmarks. The formulas are over 5–100 universally-quantified variables and 2–49 existentially-quantified variables. The highest depth of the common ite-block in the produced Skolem⁶ is 7. AE-VAL was able to terminate on all of them within a timeout of 60 s. The solving stage (including construction of MBPs and collecting Skolem constraints) took less than a second for all benchmarks. Compiling Skolem$_1$ (i.e., without compaction) took insignificant time, but compacting Skolem$_2$ took much longer for 11 outliers (the most crucial one is №16). This can be explained by many iterations for greedily finding a good partition, as explained in Sect. 5.

Table 1. Concrete evaluation data.

Fig. 3.

Size of Skolems terms (i.e., total numbers of Boolean and arithmetic operators).

Figure 3 visualizes the effect of the Skolem compaction. Each point in the plot corresponds to a pair of runs of AE-VAL: the x-axis shows the size of the compacted Skolem (i.e., extracted with the use of both techniques from Sect. 5), and the y-axis shows the size of the naively created Skolem. The geometric mean for the ratio is 2.06, and the largest improvement is 6.95 – seen for the benchmark №38. In nearly half of the cases (35 out of 80), the depth of the ite-structure in the Skolem decreased at least by one. However, what proved to be the most effective for compaction is the factoring out of individual Skolem terms for particular variables, i.e., AE-VAL found a function which is good for all preconditions by greedy partitioning.

Fig. 4.

Benefits of AE-VAL over CVC4.

6.2 Comparison with CVC4

We also compared AE-VAL with state-of-the-art tool CVC4 [20], version 1.7-prerelease [git master 464470c3], the winner of the general track of the fifth SyGuS-COMP. Like AE-VAL and unlike most of the synthesizers based on an enumerative search (e.g. [2]), the refutation-based synthesizer in CVC4 does not enforce any syntactic restrictions on its solutions, e.g., formal grammars or templates, and it is more efficient than an enumerative synthesizer also implemented in CVC4.

Among 80 benchmarks from Table 1, CVC4 was able to solve 55, and it exceeded a timeout of 60 s for the remaining 25 benchmarks. In Fig. 4(a), we report the ratio of depths of the ite-blocks generated in the implementations. In most of the cases, our implementations have shorter depths.

Note that due to reasonings of encoding [19], CVC4 solved slightly different problems, in which it extracted only individual Skolems for each output variable. It is unable to combine them in one relation or share them, as opposed to what our tool does. Thus, we are unable to compare the overall size of the implementations produced by CVC4 and our method.

In addition, we performed comparison experiments on isolated groups of benchmarks from SyGuS-COMP, in which the formal grammars were ignored by both tools. In particular, we considered nearly fifty single-invocation benchmarks from groups array_sum, array_search, and max. The performance of both AE-VAL and CVC4 on array_sum and array_search is similar – both tools converge in less than a second. Figure 4(b) shows a comparison of AE-VAL with CVC4 on a sequence of max-benchmarks, in which the number of arguments n for the function max being synthesized varies from 2 to 16. AE-VAL and CVC4 both converge with similar results, but the synthesis time varies significantly. Note that for $n < 10$, both tools require less than 1 s (and CVC4 is slightly faster), but for larger n, the performance of CVC4 gets worse almost exponentially, while the performance of AE-VAL remains reasonable. In particular, CVC4 is unable to synthesize a max function with 17 inputs after two hours, but AE-VAL synthesizes a solution in just forty seconds.

7 Related Work

Our approach follows the classical flow of functional synthesis for unbounded domains proposed in [16]. Their main idea is to enhance quantifier-elimination procedures with a routine to generate witnesses. However, in practice, it requires an expensive conversion of the specification to DNF and applying quantifier elimination for each disjunct. With our MBP-based lazy quantifier-elimination procedure AE-VAL, we have made the approach more scalable and robust, while keeping the elegance and improving generality of the witness generation procedures. Furthermore, our approach benefits from additional optimization stages to make the final implementations compact.

As mentioned earlier, an older version of AE-VAL was built and successfully used for solving the validity of $\forall \exists$-formulas [6]. It has been successfully used in many applications:

• Realizability checking and synthesis from Assume-Guarantee contracts [13],

• Non-termination checking, and (potentially) synthesis of never-terminating lasso-shaped programs [9],

• Synthesis of simulation relations between pairs of programs [6, 7],

• Synthesis of (candidates of) inductive invariants [8].

However, it did not include any procedures to generate terms for a pure functional synthesis setting, or to compact the Skolems and share terms. We believe our new procedures can further improve the above-listed and other applications of AE-VAL.

An alternative way to quantifier elimination for solving functional synthesis tasks is implemented in CVC4 [20]. Their refutation-based approach aims at determining the unsatisfiability of the negated form of $\forall \exists$-formula. A solution is then directly obtained from an unsatisfiable set of ground instances of the negated synthesis conjecture. Similarly to AE-VAL, CVC4 proceeds lazily and creates a decision tree. However, as confirmed by our evaluation, their decision trees are often larger than the decision trees produced by AE-VAL for the same tasks.

Laziness in the search-space exploration allows viewing both AE-VAL and CVC4 as instances of Counterexample-Guided Inductive Synthesis (CEGIS [21]). Typically, the CEGIS-based algorithms, e.g., [1, 2, 21, 22], perform a guided search over the syntax tree of the program being synthesized. Our approach to synthesis, as well as [16] and [20], is driven by the logical structure of a background theory and does not put any restriction on the syntax tree size. This allows generating large and expressive implementations (such as max-functions over dozens of inputs) quickly.

There is a rich body of work on logic synthesis, i.e., synthesis of Boolean gate-level functions from specifications in propositional logic [12]. This considers synthesis of two-level (e.g., sum of products) or multi-level circuits, with minimization of various cost criteria (size, delay, power, etc.), and with sharing Boolean gates across multiple outputs. While our motivation for sharing “logic” is similar, note that we identify theory terms that can be shared within the implementation of an output, and across implementations of multiple outputs. Thus, our minimization/compaction is not at the Boolean-level, but requires theory-specific reasoning (validity checks). Furthermore, most logic synthesis efforts start with functional specifications. There have been some efforts in considering relational specifications [4, 15], but these are fairly straightforward extensions of well-known functional techniques.

Finally, a procedure similar to Model-Based Projection has also been used for existential quantification in Boolean formulas [11], where it was called circuit-cofactoring. The application considered there was SAT-based model checking, where a pre-image of a given set of states is computed by existential quantification of a set of variables. The main idea was to use a model on the quantified variables to derive a circuit-cofactor (including disjunctions), which can capture many more states than a generalized cube on the remaining variables. This resulted in far fewer enumerations than cube-based enumeration techniques.

8 Conclusions

We have presented a novel approach to functional synthesis based on lazy quantifier elimination. While checking realizability of the given specification, our algorithm produces a system of synthesis subtasks through effective decomposition. Individual solutions for these subtasks generate a decision tree based implementation, which is further eligible for optimizations. Compared to the existing approaches, our generated solutions are more compact, and the average running time for their synthesis is reasonably small. We have implemented the approach in a tool called AE-VAL and evaluated it on a set of reactive synthesis benchmarks and benchmarks from SyGuS-COMP. We have identified classes of programs when AE-VAL outperformed its closest competitor CVC4 both on running time and on ite-depth of implementations. In the future, we wish to extend AE-VAL to other first-order theories, to support (whenever applicable) enumeration-based reasoning, which utilizes grammars and results in even more compact solutions, and to leverage specifications enhanced with input-output examples.