11institutetext: Massachusetts Institute of Technology
11email<EMAIL_ADDRESS>
11email<EMAIL_ADDRESS>
# Automatic Generation of Formula Simplifiers based on Conditional Rewrite
Rules

Rohit Singh  Armando Solar-Lezama

###### Abstract

This paper addresses the problem of creating simplifiers for logic formulas
based on conditional term rewriting. In particular, the paper focuses on a
program synthesis application where formula simplifications have been shown to
have a significant impact. We show that by combining machine learning
techniques with constraint-based synthesis, it is possible to synthesize a
formula simplifier fully automatically from a corpus of representative
problems, making it possible to create formula simplifiers tailored to
specific problem domains. We demonstrate the benefits of our approach for
synthesis benchmarks from the SyGuS competition and automated grading.

###### Keywords:

program synthesis, formula rewriting

##  1 Introduction

Formula simplification plays a key role in SMT solvers and solver-based tools.
SMT solvers, for example, often use local rewrite rules to reduce the size and
complexity of the problem before it is solved through some combination of
abstraction refinement and theory reasoning [13, 9]. Moreover, many
applications that rely on solvers often implement their own formula
simplification layer to rewrite formulas before passing them to the solver
[37, 38, 11, 17, 15].

In some cases, the motivation to build a simplifier in the application is to
be able to reduce the formula on the fly as it is being constructed, rather
than constructing a large formula that then gets simplified by the solver. A
more fundamental motivation, however, is that formulas generated by a
particular tool often exhibit patterns that can be easily exploited by a
custom formula simplifier but which would not be worthwhile to exploit in a
general solver.

One domain where this simplification is particularly important is constraint-
based synthesis. In particular, this paper will focus on the Sketch synthesis
system [35]. Sketch is an open source tool which has been used in systems
published in multiple top-tier conferences [19, 18, 32, 31, 12, 30, 36], and
it includes a publicly available benchmark suite of synthesis problems from
several important domains including storyboard programming [31], query
extraction [12] and automated grading (Autograder) [30], sketching Java
programs [18], as well as benchmarks available from the annual synthesis
competition (SyGuS) [4] . In particular, Sketch has hundreds of benchmarks for
Autograder problems obtained from student submissions to introductory
programming assignments on the edX platform.

The Sketch synthesis system includes a formula simplifier, that has a
tremendous impact on the size of the formulas. Without these simplifications,
problems that solve in seconds time-out instead. The simplification module in
Sketch has been under continuous development for eight years, so at this point
the code is quite mature and efficient, but it took significant effort to get
there, and many hard-to-identify bugs were introduced in the process of
developing it, as evidenced from the commit logs in the project repository
[2].

In this paper, we present a methodology for automatically generating a formula
simplifier from a corpus of benchmark problems. We also present Swapper, a
framework implements this methodology. The input to Swapper is a corpus of
formulas from problems in a particular domain. Given this corpus, Swapper
generates a formula simplifier tailored to the common recurring patterns
observed in this corpus.

The system operates in four phases. In the first phase, Swapper uses
representative sampling to identify common repeating sub-terms in the
different formulas in the corpus. In the second phase, these repeating sub-
terms are passed to the rule synthesizer which generates conditional
simplifications that can be applied to these sub-terms when certain local
conditions are satisfied. These conditional simplifications are the
simplification rules which in the third phase must be compiled to actual C++
code (the simplifier) that will implement these simplifications. Not all the
simplification rules discovered in the third phase will actually improve the
run-times for solving the formula. For example, some may reduce the formula
size without making it easier to solve, and some may actually prevent other
rules from being applied. In order to identify an optimal subset of rules to
incorporate into the final simplifier, the system relies on a fourth phase of
auto-tuning that evaluates combinations of rules based on their empirical
performance on a subset of the corpus (Training set). The resulting
synthesizer will be shown to work effectively not just for problems in the
corpus, but also for other problems from the same domain.

Overall, our work makes the following contributions:

  1. 1.

We demonstrate how to automate the process of generating conditional rewrite
rules specific to the common recurring patterns in formulas from a given
domain.

  2. 2.

We demonstrate the use of autotuning to select an optimal subset of rules and
generate an efficient simplifier.

  3. 3.

We evaluate our approach on multiple domains from the Sketch synthesis tool
and show that the generated simplifiers improve the performance (running
times) of Sketch tool by 30-50% than the existing hand-crafted simplifier in
Sketch.

##  2 Related Work

A pre-processing step in constraint solvers and solver-based tools (like Z3,
Boolector [9], Sketch etc) is an essential one and term rewriting has been
extensively used as a part this pre-processing step [27, 37, 38, 11, 17, 15].
These pre-processing steps are very important and can have a significant
impact on performance. As others have observed and our experiments confirm,
however, rewrites that help for one class of problems may not be effective for
problems for a different domain. The task of developing domain-specific
simplification rules is time consuming and error-prone, and our technique aims
to automate the discovery of such rules.

Each part of our framework solves an independent problem and is different from
the state of the art, specialized for our purposes. A recent paper introducing
Alive [23], a domain specific language for specifying, verifying, and
compiling peephole optimizations in LLVM is the closest to our framework as a
whole. Their rewrite rules are guarded by a predicate, they use static
analyses to find the validity of those guards, they verify the rules and then
compile them to efficient C++ code for rewriting LLVM code: all similar to our
phases. However, their system is targeted towards the compilers community and
relies upon the developers to discover and specify rewrite rules. Our work is
targeted towards the solver community and automatically synthesizes the
rewrite rules from benchmark problems of a given domain.

Identification of recurrent sub-graphs from benchmark DAGs is similar in
essence to the Motif discovery problem [28] which is famous because of its
application in DNA fingerprinting[20]. This is a very active area of research
and recently we have seen some attempts to use sampling [10], machine learning
[21] and distributed algorithms [22, 6, 29] to compute the Motifs
(statistically significant recurrent sub-graphs) as quickly as possible. Our
DAGs, on the other hand, have labeled nodes (labeled with operation types) and
our motifs have to account for the fact that some opperations are commutative
but not others, which makes direct translation to Motif discovery problem more
difficult.

In the superoptimization community, people explore all possible equivalent
programs and find the most optimal one. It would not make sense to do that for
formulas. But [7] came up with this idea of packaging the superoptimization
into multiple rewrite rules similar to what we are doing here. Although it
looks similar in spirit to our work, there are a few differences. Most
importantly, [7] uses enumeration of potential candidates for optimized
versions of instruction sequences and then checks if it is indeed the most
optimal version. Whereas, we use a hybrid approach that primarily relies on
constraint based synthesis for generating the rules, which offers a
possibility of specifying a structured grammar for the functions.

The third phase in Swapper automatically generates simplifier’s code
(representing an abstract reduction system) is similar to a term or graph
rewrite system like Stratego/XT [8, 24] or GrGEN.NET [14]. Stratego/XT is a
framework for the development of program transformation systems and GrGEN.NET
is a Graph Rewrite Generator. They offer declarative languages for graph
modeling, pattern matching, and rewriting. Both of these tools generate
efficient code for program/graph transformation based on rule control logic
provided by the user. We build upon their ideas and develop our own compiler
because we already had special input graphs (DAGs with operations as labels of
nodes) and an existing framework for simplification (Sketch’s DAG
simplification class). Our strategy can be compared with LALR parser
generation [16] where the next look-ahead symbol helps decide which rule to
use. In our case as well we keep around a set of rules that are potentially
applicable based on what the algorithm has seen.

##  3 Problem Overview

In order to describe the details of our approach, we first describe a few key
features of the Sketch synthesis system which will serve both as a component
and as a target for Swapper. Sketch is an open source system for synthesis
from partial programs. A partial program (also called a sketch) is a program
with holes, where the potential code to complete the holes is drawn from a
finite set of candidates, often defined as a set of expressions or a grammar.
Given a partial program with a set of assertions, the Sketch synthesizer finds
a completion for the holes that satisfies the assertions for all inputs from a
given input space.

Sketch uses symbolic execution to derive a predicate $P(x,c)$ that encodes the
requirement that given a choice $c$ for how to complete the program, the
program should be correct under all inputs $x$. The predicate $P(x,c)$ is
represented internally as a Directed Acyclic Graph. The DAG represents an
expression tree where equivalent nodes have been collapsed into a single node
by structural hashing [26]. The grammar for this language of expressions is
shown in Fig. 1. The formula simplification pass that is the subject of this
paper is applied to this predicate $P(x,c)$ as it is constructed and before
the predicate is solved in an abstraction refinement loop based on
counterexample guided inductive synthesis (CEGIS).

$\vspace{-10pt}\begin{array}[]{rlr}e=&boolop(e_{1},e_{2})&\mbox{apply a
boolean operator on }e_{1},e_{2}\\\ &arithop(e_{1},e_{2})&\mbox{apply an
arithmetic operator on }e_{1},e_{2}\\\ &src(id)&\mbox{universally quantified
input}\\\ &ctrl(id)&\mbox{existentially quantified control}\\\
&arr_{r}(e_{i},e_{a})&\mbox{read at index $e_{i}$ in array $e_{a}$}\\\
&arr_{w}(e_{i},e_{a},e_{v})&\mbox{write at index $e_{i}$ value $e_{v}$ in
array $e_{a}$}\\\ &arr_{create}(e_{0},...,e_{i})&\mbox{create a new array }\\\
&n(c)&\mbox{integer/Boolean constant with value $c$}\\\
&mux(e_{c},e_{0},\ldots e_{i})&\mbox{multiplexer chooses based on value
$e_{c}$}\\\ &assert(e)&\mbox{assertion of a boolean expression $e$}\\\
\end{array}$ Figure 1: The language of predicate expression in Sketch.

###  3.1 Formula Simplification using Conditional Rewrite Rules

A rewrite rule is a pattern matching rule that indicates that when the guard
predicate in the center is satisfied, one can replace the pattern on the left
with the pattern on the right without changing the semantics of the overall
formula. For example, a simple replacement rule is the following:

$mux(t,c,d)\xrightarrow{~{}~{}~{}c=d~{}~{}~{}}c$

This rule indicates that a term $mux$ that chooses between $c$ and $d$ based
on a condition $t$ can be replaced with the term $c$ as long as $c$ and $d$
can be proved to be always equal, which will be true, for example, if $c$ and
$d$ are identical subexpressions—this is easy to detect in the DAG
representation as the subexpressions will be represented by the same node
because of structural hashing.

The predicate may involve equality, as in the example above, or inequalities;
for example,

$or(lt(a,b),lt(a,d))\xrightarrow{~{}~{}~{}b<d~{}~{}~{}}lt(a,d)$

Note that in order to apply the rule, the system must be able to guarantee
that $b<d$ holds for all possible values of the inputs to the sub-formula. In
the Sketch simplifier, this is done by running a simple dataflow analysis over
the graph to infer ranges of values for every term [33].

###### Definition 1

A _Conditional Rewrite Rule_ is a triple $(LHS(x),\textit{pred}(x),RHS(x))$
where $x$ is a vector of input variables and $LHS$, $RHS$ are expressions that
include variables in $x$ as free variables and pred is a guard predicate
defined over the same input variables and drawn from a restricted grammar. The
triple satisfies the following formula:

$\forall x.\textit{pred}(x)\implies\left(LHS(x)=RHS(x)\right)$

We use the notation $LHS\xrightarrow{~{}~{}~{}pred~{}~{}~{}}RHS$ to denote the
rewrite rules.

The definition of the rule is symmetric with respect to $LHS$ and $RHS$, but
in practice the rule is going to be used by a system that searches for sub-
expressions that match $LHS$ and replaces them with the expression $RHS$ if it
can prove that the condition pred is guaranteed to be satisfied. For this
reason, our system will search for rules where $RHS$ is smaller than $LHS$
with the hope that this will help reduce the size of the overall formula.

There are two points about these rules that are important to highlight at this
point. First, there is a trade-off between the strength of the predicate and
the reduction that can be achieved by a rule: rules with weak predicates are
easier to match than rules with strong predicates, but rules with strong
predicates can offer more aggressive simplification. The second point,
however, is that the rules that give the most aggressive size reduction are
not necessarily the best ones; for example, a rule may replace a very large
$LHS$ expression with a small $RHS$ but in doing so it may prevent other rules
from being applied, resulting in a formula that is larger than what we would
have gotten if the rule had not been applied at all. For these reasons,
writing optimal simplifiers based on rewrite rules is a challenging task even
for human experts, which motivates our approach of using synthesis and
empirical autotuning methods to automatically discover optimal sets of
conditional rewrite rules.

##  4 Pattern Finding: Random Sampling based Clustering

We use a random sampling based clustering method to find “recurrent” pattern
sub-graphs (Definition 2) from a set of benchmark DAGs. We formalize the
intuitive requirement of “domain significance” (Definition 3), present our
algorithm (Algorithm 2 in the Appendix) that asymptotically finds “domain
significant” patterns and prove it’s correctness.

######  Definition 2 (Pattern, Sub-pattern, Sub-graph)

A pattern in the context of Swapper is a Directed Acyclic Graph (DAG) rooted
at a node that represent a computation of a single value with each node being
labeled by an SMT operation, constant or a typed variable. A sub-pattern or a
sub-graph $P$ of a larger DAG $G$ is a pattern such that there exists a graph
isomorphism between $P$ and $G$ that preserves the computation labels.

######  Definition 3 (Domain Significance)

Given a set $S$ of benchmark DAGs from a domain $D$, a sub-pattern DAG $P$ of
size $N$ (number of operation nodes in the DAG) is said to be domain
significant with probability $p$ where $p$ is the ratio of number of
occurrences of the pattern $P$ in $S$ and the total number of patterns of size
$N$ in $S$. The larger the value of $p$, more domain significant the pattern
$P$ would be.

###  4.1 Sampling Algorithm

To motivate the algorithm, we look at the requirement of approximating domain
significance:to approximate the distribution given by the actual domain
significance probabilities asymptotically (Definition 3). This will be
guaranteed if we ensure that every sample of size $N$ is equally likely to be
one of all patterns of size $N$ in the benchmark DAGs (allowing repetitions).
Because the benchmark set $S$ comprises of DAGs, we can always pick a node at
random from $S$ and then try to find a pattern of size $N$ rooted at that
node. If we can guarantee that for any fixed node in $S$, our sampling method
at that node picks a pattern of size $N$ with the same probability across all
patterns of size $N$ rooted at that node, and, that probability is independent
of the chosen node then we satisfy the original requirement. Our algorithm
maintains a boundary of collected nodes at any stage and picks another node
from all available parents (including some NULL parents) randomly at each
step. We present the algorithm in the appendix (Algorithm 2) and sketch a
proof of it’s correctness in Theorem 4.1 below.

###### Theorem 4.1

Given a set $S$ of benchmark DAGs and a number $N\geq 2$, Algorithm 2
asymptotically approximates the underlying order of patterns of size $N$ based
on the distribution of the domain significance probabilities.

###### Proof

As discussed above, it’s sufficient to show that the algorithm samples every
pattern of size $N$ rooted at a particular node with equal probability
irrespective of what the node is.

For simplicity, let’s first assume that instead of labeled DAGs representing
formulas, we have labeled directed binary trees in $S$. In this case, such a
sampling method is easy to construct. We randomly pick a node from $S$ and
then randomly pick from its (two) parents and at any stage pick randomly from
all available parents until we have $N$ nodes. If we hit a node with no
parents, we restart the sampling. Due to the fact that each node has equal
number of parents, at step $i$ (first step being the choice between two
parents), the number of available choices for picking will be $i+1$. This
ensures that the probability of picking any pattern (possibly after some
restarts) of size $N\geq 2$ is the same across the board i.e. is
$\frac{1}{2}\times\frac{1}{3}\times...\times\frac{1}{N}$. This idea can be
easily extended to $k$-ary trees.

Moreover, for trees with variable but bounded in-degrees we incorporate
“shadow” edges (represented by $NULL$ in the algorithm) to make sure that each
node has the same number of parents (the bound on in-degrees) and picking a
“shadow” edge will cause a restart of the sampling process. This will ensure
that if we pick a pattern of size $N$ (again, possibly after some restarts),
it will be equally likely to be any pattern of size $N$ from $S$.

Now, for DAGs instead of trees, where edges can point to the same node again,
we ensure this property by first picking a node from $S$ at random and then
considering only the breadth first search tree rooted at the first chosen node
for sampling - this ensures that for every DAG pattern rooted at this node,
there is only one way to pick it and hence equal probability of it being
picked as compared to any pattern rooted at that node. Once we find the nodes
of the pattern, we consider all the edges that were already there for
analysis, construct the pattern and count it appropriately in the samples.

Implementation of the algorithm incorporates the BFS tree construction on the
fly by maintaining a list of already seen nodes ($boundayNodes\cup nodes$) and
treating any new edge that leads to them as being a “shadow” edge (NULL in the
pseudo-code). It then extends the list of possible choices to
$size(nodes)\times(T-1)+1$ which is the number of valid possibilities one will
have if this were a $T$-ary tree. The probability for any pattern $P$ of size
$N\geq 2$ rooted at the first picked node ($n_{0}$ in the pseudo-code) to be
picked by the sampling algorithm (given that a pattern has been picked,
potentially after some restarts) is
$\frac{1}{T}\times\frac{1}{2*T-1}\times...\times\frac{1}{(N-1)*T-(N-2)}$
because each node will be picked randomly from a list ($boundaryNodes$) of
size $i\times(T-1)+1$ at step $i$ for $1\leq i\leq N-1$. Note that due to the
implicit BFS tree construction, there is only one way for a pattern to be
picked and the probability expression is independent of the pattern or the
node picked in the beginning.

###  4.2 Similarity Metrics

To group DAGs together into clusters, Swapper uses the following metrics. (1)
Signature of the DAG: To identify equivalent patterns, Swapper builds a
signature string of the DAG which is an encoding of the DAG with parenthesis
establishing the types of nodes, ordered names of input nodes and the parent-
child relationships. On top of this, the ordering of parents for commutative
operations is made lexicographic to ensure that patterns are mapped to the
same signature when they are equivalent because of commutativity. (2) Static
Analysis information from the benchmark DAGs: To check the pred part of the
rules, the generated simplifier performs a static analysis on the DAG and
identifies assumptions that are valid for each node. The assumptions for input
or source nodes are maintained with the DAG signature. Note that each DAG can
have multiple assumptions and all those assumptions are used later used during
the rule generation phase but are ignored for aggregating patterns.

###  4.3 Stopping Criterion

Swapper chooses a large number $M$ (starting with $50000$) but continues
sampling until the total number of patterns with probability of occurrence
greater than a threshold $\epsilon$ converges i.e. the next $M$ samples do not
result into a significant change in the number of such patterns. In our
experiments, we used $\epsilon=0.02$.

##  5 Rule Generation: Syntax-Guided Synthesis

In this phase, Swapper finds corresponding rewrite rules for the set of common
patterns obtained from the Pattern Finding phase. For each pattern, the
Pattern Finding phase also collects a set of predicates that can be valid for
the inputs of each pattern at different occurrences, as computed by a static
analysis on each benchmark in the corpus.

###  5.1 Problem Formulation

Swapper needs to find correct rewrite rules (3.1) which have a given LHS.
Additionally, we want to avoid rules with predicates that will never hold in
practice, so we focus on rules with predicates that are implied by the
predicates found by static analysis during the Pattern Finding Phase.

###### Problem 1

Given a function LHS(x), assumptions static(x) discovered by static analysis
for a given occurrence of the LHS pattern, and grammars for pred(x) and
RHS(x), find suitable candidates for pred(x) and RHS(x) which satisfy the
following constraints:

  1. 1.

$\forall x:static(x)\implies\textit{pred}(x)$

  2. 2.

$\forall x:\text{ }if\text{ }(\textit{pred}(x))\text{ }then\text{
}(LHS(x)==RHS(x))$

  3. 3.

$size($RHS$)$ < size($LHS$), where size($expr$) is the number of terms in the
expression $expr$

  4. 4.

$\textit{pred}(x)$ is the weakest predicate (most permissive) from the
predicate grammar that enables the $LHS$ to $RHS$ transformation

####  5.1.1 The space of predicates

For pred Swapper employs a simple Boolean expression generator that considers
conjunctions of equalities and inequalities among variables. These predicates
are inspired by existing predicates present in the rules in the Sketch’s hand-
crafted simplifier and are easier to check statically than more complicated
predicates.

####  5.1.2 Grammar for RHS

The template for RHS simulates the computation of a function using temporary
variables. This computation can be naturally interpreted as a DAG in
topologically sorted order. Essential grammar for the generator for RHS is
shown here:

$\begin{array}[]{rl}RHS(x)\equiv&let~{}t_{1}=\textbf{simpleOp}(x);\ldots
t_{k}=\textbf{simpleOp}(x,(t_{1},...,t_{k-1}));\\\
{}\hfil&in~{}t_{k}\end{array}$

where simpleOp represents a single operation node (e.g. AND, OR etc) with its
inputs being selected from the arguments. We put a strict upper bound on $k$
as the number of nodes in the LHS for which the RHS is being searched for. The
last computed temporary is interpreted as the output node of the DAG.

###  5.2 Correctness Constraint

Setting apart constraint number 4 regarding optimality of pred in the problem
definition 1, this problem can be seen as a classic synthesis problem. We will
enforce the fourth constraint on top of solutions to this synthesis problem.

$\exists c_{p}c_{r}\forall x\text{
}\left(static(x)\implies\textit{pred}(x,c_{p})\right)\wedge\textit{pred}(x,c_{p})\implies\left(LHS(x)=RHS(x,c_{r})\right)$

where $c_{p}$ and $c_{r}$ are the choices the solver needs to make to get a
concrete pred(x) or RHS(x). More concretely, these are the choices of: (i)
when to expand the grammar or when to use a terminal, and (ii) which subset of
inputs to choose for a particular operation (equality in pred and simpleOp in
RHS).

We explored two different techniques for synthesizing such rewrite rules: (1)
Symbolic Sketch based synthesis of rules, and (2) Enumerative search with
heuristics. Swapper uses a hybrid approach to get the best of the both
aforementioned techniques: scalability and exhaustiveness. We describe the
hybrid technique briefly.

###  5.3 Hybrid Enumerative/Sketch-based synthesis

Swapper breaks the SyGus Problem into two parts. (1) Constraints and
optimizations on predicates: Swapper uses the enumerative approach, generates
all possible candidate predicates from the specification grammar and checks
for their validity based on collected assumptions $static(x)$. It applies
various heuristics and optimizations including predicate refinement (5.3.1) on
top of the symbolic synthesis to scale the overall synthesis process while
maintaining it’s exhaustive nature. (2) Synthesis of $RHS$: Swapper hard-codes
a predicate and realizes the $RHS$ synthesis problem in Sketch using the
generator and minimize features ([34] [32]) of the Sketch language. Swapper
uses generators to recursively define the template for $RHS$, and minimize to
find the smallest possible RHS(x) for a fixed pred(x).

Figure 2: Comparison of performance of Sketch using the best Auto-generated
simplifiers from Hybrid and Enumerative techniques on Autograder benchmarks

input : LHS(x), allPreds

output : valid rewrite rules of the form $(LHS,\textit{pred}_{i},RHS_{i})$

$G_{\Rightarrow}\leftarrow$ ImplicationGraph(allPreds)

while  _$\neg\text{isEmpty}\left(G_{\Rightarrow}\right)$_ do

$\textit{pred}\leftarrow\text{popLeaf}\left(G_{\Rightarrow}\right)$

$RHS\leftarrow\textsc{Sketch}\text{Synth}\left(LHS,\textit{pred}\right)$

if  _$RHS=$ NULL_ then

foreach  _$\textit{pred}^{\prime}\in
G_{\Rightarrow}\wedge\textit{pred}\Rightarrow\textit{pred}^{\prime}$_ do

removePred$\left(\textit{pred}^{\prime},G_{\Rightarrow}\right)$

else

Output rule $(LHS,\textit{pred},RHS)$

Algorithm 1 Refinement method

####  5.3.1 Predicate Refinement

Swapper constructs the implication graph ($G_{\Rightarrow}$) of all available
predicates and iteratively finds $RHS$ for the least applicable predicates
(leaves in the graph $G_{\Rightarrow}$) at a given stage. Note that this
heavily reduces the synthesis time when there’s no possible simplification
rule for a leaf predicate and Swapper can prune out all predicates implied by
it. The procedure is shown in Algorithm 1.

This hybrid technique has the benefit of being able to exhaustively search for
rules of big sizes while making the core synthesis problem faster (fewer
constraints) and highly parallelizable (multiple Sketch instances with
different predicates are run in parallel). Figure 2 shows the improvement of
the auto-generated simplifier for AutoGrader benchmarks by using the Hybrid
technique over just the Enumerative one (excluding Sketch). Note that Sketch
does synthesis of rules guaranteeing their correctness for large but bounded
inputs, hence, we fully verify the generated rules with z3 [13] as well by
expressing them as SMT constraints before using them for code generation.

##  6 Efficient Simplifier Code Generation

There are no readability constraints to be satisfied by the simplifier code
since this is automatically generated by tool. This enables Swapper to do
certain optimizations. The most important one being that now it can share the
burden of pattern matching among all the rules which is particularly useful
when the $LHS$ is the same for multiple rules. First, using this idea and an
abstract predicate evaluation technique Swapper encodes the process of rule
application more efficiently than the earlier optimization phase. Second, to
help incorporate all the “symmetries” of the rules, Swapper enables pattern
matching with DAGs which differ only in the order of parent nodes at some
commutative operation(s).

Swapper hard-codes all aspects of the rule application including predicate
evaluation and the replacement procedure as C++ code. Because of the
engineered efficiency of rewriting, note that, in our experiments we will not
consider simplification time because of it being a one-time negligible (always
a fraction of a second) time-step as compared to further Sketch solving.

##  7 Auto-tuning Rules

Swapper uses OpenTuner [5] to auto-tune the set of rules according to a
performance metric (based on time, memory, size of DAGs etc). OpenTuner uses
an ensembles of disparate search techniques simultaneously and quickly builds
a model for the behavior of the optimization function treating it as a black
box.

###  7.1 Optimization Problem Setup

Swapper specifies the set of all rules to the tuner and creates the following
two configuration parameters: (1) A permutation parameter: for deciding the
order in which the rules will be checked. (2) Total number of rules to be
used.

A lot of rules do not directly interact with each other and hence Swapper
reduces the search space by creating multiple permutation parameters for each
set of rules that can interact with each other e.g. any two rules with
overlapping patterns can potentially affect each other’s applicability whereas
any two rules with different base nodes in $LHS$ will not interact with one
another and can therefore be ordered in any way as desired for pattern
checking.

The evaluation function (fopt) to be optimized takes as input a set of rules
and returns a real number. This number corresponds to performance improvement
of Sketch on Training set benchmarks after rewriting the benchmarks using the
simplifier generated (Section 6) from the input set. Intuitively, fopt
penalizes heavily for under-performing on any benchmark from the Training set
and rewards normally for over-performing. It returns the average of all these
rewards. The auto-tuner tries to maximize this reward by trying out various
subsets and orderings of rules provided to it as input while learning a model
of dependence of fopt on selection of rules.

##  8 Experiments

In order to test the effectiveness of our system, we focus on these three
questions: (1) Can Swapper generate good simplifiers in reasonable amounts of
time and with low cost of computational power? (2) How do the simplifiers
generated by Swapper affect SMT solving performance of Sketch relative to the
hand written simplifier in Sketch? (3) How domain specific are the simplifiers
generated by Swapper?

For evaluation of Swapper on Sketch domains, we compared the following three
simplifiers:

  1. 1.

Hand-coded: This is the default simplifier in Sketch that has been built over
a span of past eight years. It comprises of simplifications based on (a)
rewrite rules that can be expressed in our framework(Subsection 3.1) (b)
constant propagation (c) structure hashing [26] and (d) a few other complex
simplifications that cannot be expressed in our framework

  2. 2.

Baseline: This disables the rewrite rules that can be expressed in our
framework from the Hand-coded simplifier but applies the rest of the
simplifications (b)-(d).

  3. 3.

Auto-generated: This incorporates the Swapper’s auto-generated rewrite rules
on top of the Baseline simplifier.

In the sections that follow, we elaborate on the details of the experiments.

###  8.1 Domains and Benchmarks

Domain |  Benchmark DAGs Used |  Avg. Number of Terms
---|---|---
Storyboard |  34 |  4173
QBS |  14 |  6580
AutoGrader |  45 |  23289
Sygus |  22 |  68366
Figure 3: Domains and Benchmarks investigated for Swapper’s evaluation

We investigated benchmarks from various domains of Sketch applications.
Storyboard benchmarks correspond to specifications for storyboard programming
problems [31], QBS ones correspond to query extraction specifications [12],
Sygus corresponds to the SyGus competition benchmarks translated from SyGus
format to Sketch specification [4] and AutoGrader ones are obtained from
student’s assignment submissions in the introduction to programming online edX
course [30]. For each of these domains we picked suitable candidates for
Swapper’s application by (1) eliminating those benchmarks which did not have
more than 5000 terms in the formula represented by their DAGs and those which
took less than 5 seconds to solve - so that there’s enough patterns and
opportunity for improvement (2) removing those which took more than 5 minutes
to solve - this was done to keep Swapper’s running time reasonable because we
need to run each benchmark multiple times during auto-tuning phase. Using
these cutoffs, the total number of usable benchmarks for AutoGrader domain
were reduced from 2404 to 45 and for Sygus from 309 to 22. Only a few (3-4) of
the QBS and Storyboard benchmarks qualified in this screening process with
around 5000-6000 terms each. Swapper was not able to generate enough rules for
auto-tuning from this small set of terms in the benchmarks (Training set).

###  8.2 Synthesis Time and Costs are Realistic

To generate a simplifier, Swapper employs: (1) a single pass of Pattern
Finding (2) a single or multiple passes of Rule Generation depending on
whether the rules from first pass were satisfactory (3) multiple evaluations
made by the Auto-Tuning phase. Many of these computations can be parallelized,
especially, the rule generation (we may have up to 100,000 patterns to
analyze) and evaluation of benchmarks (Auto-Tuner will potentially call this
hundreds of times, this number was around 150 in our experiments).

We used a private cluster running Openstack as the infrastructure for
parallelized computations with parallelisms of 20-40 on two virtual machines
emulating 24 cores, 32GB RAM of processing power each.

We present a worst case estimate of CPU time and cost of computation taken by
these phases based on our experiments and the Amazon Web Services [1]
estimator (using On-demand pricing for the same instances we used on our
private cluster and rounding them up to account for volatility in the prices):

Domain |  Pattern Finding |  Rule Generation |  Auto-Tuning |  Total Time (in hours) |  Cost
---|---|---|---|---|---
AutoGrader |  3 hours |  $1\text{ hour }\times 5$ |  $0.08\times 150$ |  20 |  $22
Sygus |  2 hours |  $1\text{ hour }\times 5$ |  $0.1\times 150$ |  22 |  $24
Figure 4: Estimated CPU time (in hours) and cost of computation on the cloud

In essence, Swapper can be used to automatically synthesize a simplifier for
less than $\$50$ spent on computation (around what one would pay a good
developer for an hour’s worth of work). Note that these wait times (around
20-22 hours or a day to get a simplifier) can be improved significantly by:
(a) parallelization of the Pattern Finding phase (b) Setting a timeout for
evaluation runs that are guaranteed to be worst than existing good runs and
(c) increasing the parallelism available to Swapper.

###  8.3 Swapper Performance

To test the performance of Swapper on Sketch benchmarks from a particular
domain, we first divided the corpus into three disjoint sets randomly
$(\textsc{Search},\textsc{Train},\textsc{Test})$. The Search set was used to
find patterns in the domain and Train set was used in the auto-tuning phase
for evaluation. And finally, Test set was used to empirically confirm that the
generated simplifier is indeed optimal for the domain. Moreover, we used
$2$-fold cross validation to ensure that there was no over-fitting on Train
set. We achieved this by exchanging Train and Test sets and auto-tuning with
the Test set instead of the Train set. We obtained similar performing
simplifiers as a result and verified that there was no over-fitting.

We implemented the evaluation of benchmarks in Swapper as a python script that
takes a set of DAGs as input, runs Sketch on each of them multiple times (set
to 5 in our experiments) and obtain the median values for time taken or memory
consumed. In our experiments we limited the performance evaluation to time
because we observed empirically that memory and time are highly correlated on
these benchmarks.

We obtained $301$ rules for AutoGrader domain and $105$ rules for Sygus
domain. The optimal simplifier for AutoGrader used $135$ of the rules and the
one for Sygus used $65$ rules.

##### Benefits over the existing simplifier in Sketch

Auto-generated simplifier reduced the size of the problem DAGs by 13.8%
(AutoGrader) and 1.1%(Sygus) on average as compared to the size of DAGs
obtained after running Hand-coded simplifier (Figure 5). On DAGs obtained
after using Auto-generated simplifier on average, Sketch solver performed
better than on those obtained by using Hand-coded simplifier (Figure 6): (1)
Auto-generated simplifier made Sketch run faster on 80% of the AutoGrader
benchmarks and 90% of the Sygus benchmarks (2) The average times taken by
Sketch to solve a benchmark simplified using Auto-generated simplifier were
13s (AutoGrader) and 8s (Sygus) as compared to 20s and 21s respectively for
the Hand-coded simplifier. Figures 5 and 6 show distribution of sizes and
times for Sketch solving after applying all three simplifiers with percentiles
on the x-axis. It clearly shows the consistent improvement in performance by
applying the Auto-generated simplifier.

|
---|---
Figure 5: Change in sizes with different simplifiers |
---|---
Figure 6: Median Sketch running time percentiles with Auto-generated
simplifiers

##### Benefits over the unoptimized version of Sketch

Auto-generated simplifier reduced the size of the problem DAGs by 38.6%
(AutoGrader) and 1.6%(Sygus) on average (Figure 5). Application of Auto-
generated simplifier results into huge improvements in running times for
Sketch solver on both AutoGrader and Sygus benchmarks as compared to
application of Baseline: the average time of solving a benchmark was reduced
from 27.5s (AutoGrader) and 22s (Sygus) to 13s and 8s respectively (Figure 6).

|
---|---
Figure 7: Domain specificity of Auto-generated simplifiers: Time distribution

##### Domain specificity

We took the Auto-generated simplifier obtained from one domain and used it to
simplify benchmarks from the other domain and then ran Sketch on the
simplified benchmarks. Application of Auto-generated simplifier obtained from
Sygus increased the Sketch running times drastically on a few AutoGrader
benchmarks when compared to the application of Baseline simplifier (Figure 7),
and, resulted into Sketch running slower than after application of Auto-
generated simplifier obtained from AutoGrader domain. Application of Auto-
generated simplifier generated for AutoGrader domain reduced the running times
of Sketch solver on average as compared to the Baseline on Sygus benchmarks
but the times were still far away from the performance gains obtained by
application of Auto-generated simplifier generated for the Sygus domain
(Figure 7). This validates our hypothesis of these generated simplifiers to be
very domain specific.

## References

  * [1] Amazon Web Services. Online, http://aws.amazon.com/
  * [2] Sketch-Backend: Repository on Bitbucket. Online, https://bitbucket.org/gatoatigrado/sketch-backend/
  * [3] Sketch: Working Manual. Online, http://people.csail.mit.edu/asolar/manual.pdf
  * [4] Alur, R., Bodik, R., Juniwal, G., Martin, M.M., Raghothaman, M., Seshia, S., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design (FMCAD), 2013. pp. 1–8. IEEE (2013)
  * [5] Ansel, J., Kamil, S., Veeramachaneni, K., Ragan-Kelley, J., Bosboom, J., O’Reilly, U., Amarasinghe, S.P.: Opentuner: an extensible framework for program autotuning. In: Amaral, J.N., Torrellas, J. (eds.) International Conference on Parallel Architectures and Compilation, PACT ’14, Edmonton, AB, Canada, August 24-27, 2014. pp. 303–316. ACM (2014), http://doi.acm.org/10.1145/2628071.2628092
  * [6] Baldwin, N.E., Collins, R.L., Langston, M.A., Symons, C.T., Leuze, M.R., Voy, B.H.: High performance computational tools for motif discovery. In: IPDPS. IEEE Computer Society (2004)
  * [7] Bansal, S., Aiken, A.: Automatic generation of peephole superoptimizers. In: Proceedings of the 12th international conference on Architectural support for programming languages and operating systems. pp. 394–403. ASPLOS XII, ACM, New York, NY, USA (2006), http://doi.acm.org/10.1145/1168857.1168906
  * [8] Bravenboer, M., Kalleberg, K.T., Vermaas, R., Visser, E.: Stratego/XT 0.17. A language and toolset for program transformation. Science of Computer Programming 72(1-2), 52–70 (2008)
  * [9] Brummayer, R., Biere, A.: Boolector: An efficient smt solver for bit-vectors and arrays. In: Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009,. pp. 174–177. TACAS ’09, Springer-Verlag, Berlin, Heidelberg (2009), http://dx.doi.org/10.1007/978-3-642-00768-2_16
  * [10] Chen, X., Jiang, T.: An improved gibbs sampling method for motif discovery via sequence weighting. In: Comput Syst Bioinformatics Conf. pp. 239–47. World Scientific (2006)
  * [11] Cheung, A., Solar-Lezama, A., Madden, S.: Partial replay of long-running applications. In: Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering. pp. 135–145. ESEC/FSE ’11, ACM, New York, NY, USA (2011), http://doi.acm.org/10.1145/2025113.2025135
  * [12] Cheung, A., Solar-Lezama, A., Madden, S.: Inferring sql queries using program synthesis. CoRR abs/1208.2013 (2012)
  * [13] De Moura, L., Bjørner, N.: Z3: an efficient smt solver. In: Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems. pp. 337–340. TACAS’08/ETAPS’08, Springer-Verlag, Berlin, Heidelberg (2008), http://dl.acm.org/citation.cfm?id=1792734.1792766
  * [14] Geiß, R., Batz, G.V., Grund, D., Hack, S., Szalkowski, A.M.: GrGen: A Fast SPO-Based Graph Rewriting Tool pp. 383 – 397 (2006)
  * [15] Hoder, K., BjÃ¸rner, N., de Moura, L.: muz - an efficient engine for fixed points with constraints. In: Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6806, pp. 457–462 (2011)
  * [16] Horspool, R.N.: Incremental generation of lr parsers. Computer languages 15, 205–233 (1989)
  * [17] Jackson, P.B., Passmore, G.O.: Proving SPARK verification Conditions with SMT solvers (Dec 2009), http://homepages.inf.ed.ac.uk/pbj/papers/vct-dec09-draft.pdf
  * [18] Jeon, J., Qiu, X., Foster, J.S., Solar-Lezama, A.: Jsketch: sketching for java. In: Nitto, E.D., Harman, M., Heymans, P. (eds.) Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2015, Bergamo, Italy, August 30 - September 4, 2015. pp. 934–937. ACM (2015), http://doi.acm.org/10.1145/2786805.2803189
  * [19] Jeon, J., Qiu, X., Solar-Lezama, A., Foster, J.S.: Adaptive concretization for parallel program synthesis. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II. Lecture Notes in Computer Science, vol. 9207, pp. 377–394. Springer (2015), http://dx.doi.org/10.1007/978-3-319-21668-3_22
  * [20] Jones, N.C., Pevzner, P.A.: An Introduction to Bioinformatics Algorithms (Computational Molecular Biology). The MIT Press (Aug 2004), http://www.worldcat.org/isbn/0262101068
  * [21] Kon, M.A., Fan, Y., Holloway, D., DeLisi, C.: Svmotif: A machine learning motif algorithm. In: Proceedings of the Sixth International Conference on Machine Learning and Applications. pp. 573–580. ICMLA ’07, IEEE Computer Society, Washington, DC, USA (2007), http://dx.doi.org/10.1109/ICMLA.2007.104
  * [22] Liu, Y., Schmidt, B., Maskell, D.L.: An ultrafast scalable many-core motif discovery algorithm for multiple gpus. In: Proceedings of the 2011 IEEE International Symposium on Parallel and Distributed Processing Workshops and PhD Forum. pp. 428–434. IPDPSW ’11, IEEE Computer Society, Washington, DC, USA (2011), http://dx.doi.org/10.1109/IPDPS.2011.183
  * [23] Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Provably correct peephole optimizations with alive. SIGPLAN Not. 50(6), 22–32 (Jun 2015), http://doi.acm.org/10.1145/2813885.2737965
  * [24] Luttik, B., Visser, E.: Specification of rewriting strategies. In: Sellink, M.P.A. (ed.) 2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF 1997). Electronic Workshops in Computing, Springer-Verlag, Berlin (November 1997)
  * [25] McKerns, M.M., Strand, L., Sullivan, T., Fang, A., Aivazis, M.A.: Building a framework for predictive science. In: van der Walt, S., Millman, J. (eds.) Proceedings of the 10th Python in Science Conference. pp. 67 – 78 (2011)
  * [26] Mishchenko, A., Chatterjee, S., Brayton, R.: Dag-aware aig rewriting a fresh look at combinational logic synthesis. In: Proceedings of the 43rd annual Design Automation Conference. pp. 532–535. ACM (2006)
  * [27] Leonardo de Moura, N.B.: Smt: Techniques, hurdles, applications. SAT/SMT Summer School, MIT (2011), http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf
  * [28] Sandve, G.K.K., Drabløs, F.: A survey of motif discovery methods in an integrated framework. Biology direct 1(1), 11+ (Apr 2006), http://dx.doi.org/10.1186/1745-6150-1-11
  * [29] Seeja, K.R., Alam, M.A., Jain, S.K.: Motifminer: A table driven greedy algorithm for dna motif mining. In: Huang, D.S., Jo, K.H., Lee, H.H., Kang, H.J., Bevilacqua, V. (eds.) ICIC (2). Lecture Notes in Computer Science, vol. 5755, pp. 397–406. Springer (2009)
  * [30] Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. SIGPLAN Not. 48(6), 15–26 (Jun 2013), http://doi.acm.org/10.1145/2499370.2462195
  * [31] Singh, R., Solar-Lezama, A.: Synthesizing data structure manipulations from storyboards. In: Gyimóthy, T., Zeller, A. (eds.) SIGSOFT FSE. pp. 289–299. ACM (2011)
  * [32] Singh, R., Singh, R., Xu, Z., Krosnick, R., Solar-Lezama, A.: Modular synthesis of sketches using models. In: McMillan, K.L., Rival, X. (eds.) Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings. Lecture Notes in Computer Science, vol. 8318, pp. 395–414. Springer (2014), http://dx.doi.org/10.1007/978-3-642-54013-4_22
  * [33] Solar Lezama, A.: Program Synthesis By Sketching. Ph.D. thesis, EECS Department, University of California, Berkeley (Dec 2008)
  * [34] Solar-Lezama, A.: Program Synthesis by Sketching. Ph.D. thesis, Berkeley, CA, USA (2008), aAI3353225
  * [35] Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) APLAS. Lecture Notes in Computer Science, vol. 5904, pp. 4–13. Springer (2009)
  * [36] Solar-Lezama, A., Jones, C.G., Bodík, R.: Sketching concurrent data structures. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008. pp. 136–148. ACM (2008), http://doi.acm.org/10.1145/1375581.1375599
  * [37] Wintersteiger, C.M., Hamadi, Y., de Moura, L.: Efficiently solving quantified bit-vector formulas. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design. pp. 239–246. FMCAD ’10, FMCAD Inc, Austin, TX (2010), http://dl.acm.org/citation.cfm?id=1998496.1998539
  * [38] Yang, J., Yessenov, K., Solar-Lezama, A.: A language for automatically enforcing privacy policies. In: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 85–96. POPL ’12, ACM, New York, NY, USA (2012), http://doi.acm.org/10.1145/2103656.2103669

##  9 Appendix

###  9.1 Implementation Details: Summary/Supplemental Materials

####  9.1.1 Random Sampling based Clustering

We built a custom parser for DAGs in Python and implemented the sampling
method among other book-keeping operations. This parser takes a corpus of
benchmark DAGs as an input and interacts with Sketch back-end ([2],
implemented in C++) to find common patterns and valid local assumptions on the
inputs to these patterns. This method is approximate but fairly simple and
works well for our purposes in reasonable amounts of time.

input : $S$: Set of benchmark DAGs, $N\geq 2$ : Size of pattern to be found

$M$: Number of samples to be considered

$T$: maximum in-degree of any node in $S$

output : $Samples$: patterns of size $N$ ordered by their approximate domain
significance

$i\leftarrow 0$, $Samples\leftarrow map()$

while  _i < M_ do

$n_{0}\leftarrow$ randomPick($S$) , nodes $\leftarrow List(n_{0})$

while  _$size($ nodes$)<N$_ do

boundaryNodes = $List()$, boundaryEdges = $List()$

foreach  _$n\leftarrow$ nodes_ do

for  _$e\leftarrow$ n.incomingEdges_ do

if  _$e.from\in\text{nodes}\cup boundaryNodes$_ then

boundaryEdges.append(NULL)

else

boundaryNodes.append(e.from)

boundaryEdges.append(e)

while  _size(boundaryEdges) < $size(nodes)\times(T-1)+1$_ do

boundaryEdges.append(NULL)

$e^{*}\leftarrow\text{randomPick}(boundaryEdges)$

if  _$e^{*}=$ NULL_ then

break

else

nodes.append($e^{*}.from$)

if  _$size(nodes)==N$_ then

$Samples[Pattern(\text{nodes}))]$ += $1$

$i=i+1$

$sortByValues(Samples)$

Algorithm 2 Probabilistic DAG Sampling

Input: The input to this phase are benchmark DAG files and the size of the
patterns to be found. We use the standard Sketch back-end DAG specification
[3]. A snippet of an example input file is provided here:

⬇

543 = ARR_W INT_ARR 429 536 542

544 = ARR_W INT_ARR 428 543 5

545 = NOT BOOL 482

546 = AND BOOL 361 545

547 = AND BOOL 481 546

Here the first entry in each line is the node ID followed by the type of
operation, the output type of the operation and respective operands (maximum
number of operands in our experiments = in-degree of any node in the DAG was
3)

Output:  The output from this phase is a list of patterns sorted by their
number of occurrence in the samples. We have attached one sample output file
for two different domains in the supplemental materials. The list contains the
rule signature to identify the rule. Here is an example snippet of such an
output:

⬇

(AND|(AND|(S:N_3:BOOL)|(S:N_4:BOOL)|)

|(EQ|(S:N_1:INT)|(S:N_2:INT)|)|) 1966 246

(AND|(AND|(S:N_1:BOOL)|(S:N_2:BOOL)|)

|(AND|(S:N_3:BOOL)|(S:N_4:BOOL)|)|) 1702 3

(AND|(AND|(AND|(S:N_3:BOOL)|(S:N_4:BOOL)|)

|(S:N_2:BOOL)|)|(S:N_1:BOOL)|) 1230 4

The second column is the number of times this pattern occurred in the sampling
phase and the third column is the number of different static analyses
configurations it found at those locations where the pattern was found. This
phase also produces a list of different static analysis configurations for the
same domain. For example, for the pattern

(AND|(AND|(S:N_3:BOOL)|(S:N_4:BOOL)|)|(EQ|(S:N_1:INT)|(S:N_2:INT)|)|),

some static analysis configurations are:

⬇

(AND|(AND|(S:N_3:BOOL:R(0-1))|(S:N_4:BOOL:R(0-1))|)

|(EQ|(S:N_1:INT:L(|-1|0|1|2|3|4|))|(S:N_2:INT:L(|-1|

))|)|)

##(AND|(AND|(S:N_3:BOOL:R(0-1))|(S:N_4:BOOL:R(0-1))|)

|(EQ|(S:N_1:INT:L(|-1|0|2|3|4|5|6|7|8|9|10|11|12|13|)

)|(S:N_2:INT:L(|-1|))|)|)

##(AND|(AND|(S:N_3:BOOL:R(0-1))|(S:N_4:BOOL:R(0-1))|)

|(EQ|(S:N_1:INT:L(|-1|0|1|2|3|5|29|30|31|32|34|35|36|

37|44|45|52|53|60|61|68|69|103|104|105|106|113|114|

115|116|118|))|(S:N_2:INT:L(|-1|))|)|)

Each source or “S” node is appended with interval analysis results i.e. it can
be in a Range R(3-10) or a in a list L(|3|5|7|) or just be “anything” T.

####  9.1.2 Rule Generation: Hybrid technique

We implemented the enumerative part of the technique in Python and
parallelized the Sketch calls using Pathos library [25]. We also augmented the
Sketch back-end to implement some enumerative search heuristics and
optimizations for generated rules in C++.

Optimizations for the Hybrid Technique: The synthesis search space is pruned
using the following heuristics:

  * •

Constrain the number of operation nodes in $RHS$ based on nodes found in $LHS$
e.g. if $LHS$ doesn’t contain any nodes that write to an array then $RHS$
shouldn’t either or if $LHS$ contains only Boolean operations then limit the
$RHS$ grammar to Boolean operations as well. This helps reduce Sketch solving
time.

  * •

Maintain signatures of each $(LHS,\textit{pred})$ pair accounting for
symmetries so that solving for rules containing equivalent pairs never happens
more than once.

  * •

In Sketch specification, use the expected data-type of output nodes to pick
the final operation in $RHS$.

We attach all generated rules in supplemental materials. The rules are
arranged in folders with all files “*.aux” corresponding to DAGs representing
the LHS (d.aux), RHS (f.aux) and predicate (p.aux).

⬇

$ cat ./119/d.aux

0 = S BOOL N_3

1 = S BOOL N_4

2 = S BOOL N_2

3 = S BOOL N_1

4 = OR BOOL 0 1

5 = OR BOOL 4 2

6 = OR BOOL 5 3

7 = AND BOOL 6 1

7

$ cat ./119/f.aux

0 = S BOOL N_3

1 = S BOOL N_4

2 = S BOOL N_2

3 = S BOOL N_1

1

$ cat ./119/p.aux

0 = S BOOL N_3

1 = S BOOL N_4

2 = S BOOL N_2

3 = S BOOL N_1

4 = CONST BIT 1

4

####  9.1.3 Code Generation

We implemented the code generation component in the Sketch back-end. The Code
Generation phase takes the rules provided to it as an input (rule signature
strings or separate pattern DAGs in files) and generates C++ code that
implements efficient matching of LHS of all the rules together and hard-codes
all symmetries of the rules for matching. The generated C++ code is complied
again with minimal libraries from Sketch back-end to produce a binary for the
simplifier. The simplifier is then run on existing set of DAGs to produce
reduced simplified DAGs.

We attach auto-generated code in files names “matches.cpp” which is compiled
with existing Sketch back-end code.

####  9.1.4 Auto-tuning Rules

We implemented the evaluation function using calls to multiple parallel
instances of Sketch for Testing set benchmarks in Python. The tuner interacts
with a MySQL database to store and analyze existing information about the
experiments (run-times, configurations of rules, etc). Note that because

We attach the auto-tuner specification code as python scripts that show the
evaluation function.

###  9.2 Conclusion

We conclude by reiterating the contributions made in this paper. We presented
a framework Swapper that automates generation of domain specific simplifiers,
for Solvers and other tools employing Solvers, based on conditional rewrite
rules. We also tested it for multiple domains in Sketch showing that Swapper
can generate good simplifiers in reasonable amounts of time and with low cost
of computational power. Simplifiers generated by Swapper perform better than
the Hand-coded simplifier on average in Sketch and are very domain specific
i.e. a simplifier obtained for a particular domain will most likely not work
well on another different domain.