LoopInvGen, a solver specialized for invariant generation problems.

tbl:solvers-authors lists the submitted solvers along with their authors,
and tbl:solvers-in-tracks shows the tracks in which each solver participated.
<TABLE>The \(\textsc {CVC4}_{2018}\)  solver is based on an approach for program synthesis that is implemented inside an SMT solver [1]}.
This approach extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures,
and uses counterexample-guided techniques for quantifier instantiation (CEGQI) that make finding such proofs practically feasible.
\(\textsc {CVC4}_{2018}\)  also combines enumerative techniques, and symmetry breaking techniques [2]}.
The DryadSynth solver combines enumerative and symbolic techniques.
It considers benchmarks in conditional linear integer arithmetic theory (LIA), and can therefore assume all have a solution in some pre-defined decision tree normal form.
It then tries to first get the correct height of a normal form decision tree, and then tries to synthesize a solution of that height.
It makes use of parallelization, using as many cores as are available, and of optimizations based on solutions of typical LIA SyGuS problems.
The \(\textsc {EUSolver}_{2017}\)  solver uses a divide-and-conquer strategy [3]} to find different expressions that satisfy different subsets of the input space,
and then unifies them into a solution that works well for the entire space of inputs.
Subexpressions are typically found using enumeration techniques
and are then unified into the final solutions using decision tree learning [4]}.
<TABLE>The Horndini solver extends the classical IC3 decision-tree algorithm with
the Horn implication counterexamples (Horn-ICE) framework [5]},
which extends the ICE-learning model.
The authors describe a decision-tree learning algorithm that learns from Horn-ICE samples,
works in polynomial time, and uses statistical heuristics to learn small trees that satisfy the samples.
The LoopInvGen solver [6]} for invariant synthesis extends the data-driven approach to inferring sufficient loop invariants
from a set of program states [7]}.
Previous approaches to invariant synthesis were restricted to using a fixed set, or a fixed template for features,
e.g., ICE-DT [8]} requires the shape of constraints (such as octagonal) to be fixed apriori.
Instead LoopInvGen starts with no initial features, and automatically learns features as necessary using program synthesis.
It reduces the problem of loop invariant inference to a series of precondition inference problems,
and uses a counterexample-guided inductive synthesis (CEGIS) loop to revise the current candidate.
Experimental Setup
The solvers were run on the StarExec platform [9]} with a dedicated cluster of 12 nodes,
where each node consisted of two 4-core 2.4 GHz Intel processors with 256 GB RAM and 1 TB hard-disk space.
The memory usage limit for each solver run was set to 128 GB, and the wall-clock time limit is set to 3600 seconds
(thus, a solver that used all 4 cores could consume at most 14400 seconds of CPU time).
The solutions that the solvers produced were checked for both syntactic and semantic correctness.
That is, a first postprocessor checked that the produced expression adhered to the grammar specified in the given benchmark,
and if this check passes, a second postprocessor checked that the solution adhered to semantic constraints
given in the benchmark (by invoking an SMT solver).

Results Overview
The primary criterion for winning a track was the number of benchmarks solved,
but we also analyzed the time to solve and the the size of the generated expressions.
The overall score for each solver was computed as \(5N + 3F + S\) .
Here \(N\)  denotes the number of benchmarks solved by the solver,
\(F\)  denotes the number of benchmarks solved among the fastest,
and \(S\)  denotes the number of benchmarks for which the size of the generated solution was among the shortest.
We used a pseudo-logarithmic scale for \(F\)  and \(S\) .
For time to solve, the scale is: \([0,1)\) , \([1,3)\) , \([3,10)\) , \([10,30)\) , \([30, 100)\) ,
\([100,300)\) , \([300, 1000)\) , \([1000,3600)\) , \(\geqslant 3600\) .
That is, the first “bucket” refers to termination in less than one second,
the second to termination in one to three seconds and so on.
We say that a solver solved a certain benchmark among the fastest
if the time it took to solve that benchmark is in the same bucket
as that of the solver which solved that benchmark in minimum time.
Similarly, for expression sizes, the pseudo-logarithmic scale we use is:
\([1,10)\) , \([10,30)\) , \([30,100)\) , \([100,300)\) , \([300,1000)\) , \(\geqslant 1000\) ,
where expression size is the number of nodes in the SyGuS parse-tree.
We also report on the number of benchmarks solved uniquely by a solver,
i.e. the number of benchmarks which no solver other than the particular solver could solve.
In fig:resultsPerTrack, we show the number of benchmarks solved,
the number of benchmarks solved among the fastest,
and the number of synthesized expressions among the smallest size;
per solver per track.
<FIGURE>General Track
In the general track, \(\textsc {CVC4}_{2018}\)  solved the most number of benchmarks (448),
and \(\textsc {EUSolver}_{2017}\)  came second, solving 420.
We note that the new version \(\textsc {CVC4}_{2018}\)  is significantly better than the previous version \(\textsc {CVC4}_{2017}\) ,
which could only solve 398 benchmarks.
The same order appears in the number of benchmarks solved among the fastest:
\(\textsc {CVC4}_{2018}\)  with 366, \(\textsc {EUSolver}_{2017}\)  with 266, and \(\textsc {CVC4}_{2017}\)  with 252.
Finally, we note that \(\textsc {CVC4}_{2018}\)  is able to solve 12 benchmarks that no other solver could solve,
and similarly there are 9 benchmarks that only EUSolver could solve.
<TABLE>We partitioned the benchmarks of the general track to a number of categories,
each containing a set of related benchmarks.
The results per category are given in the Table REF .
We observe that \(\textsc {EUSolver}_{2017}\)  preformed significantly better in the “Multiple Functions” and “ICFP” categories.
While the \(\textsc {CVC4}_{2018}\)  solver preformed better in the other categories,
none of the solvers could solve any of the benchmarks from the “Instruction Selection” category.

Conditional Linear Arithmetic Track
In the CLIA track, \(\textsc {CVC4}_{2018}\)  and DryadSynth had a close competition.
\(\textsc {CVC4}_{2018}\)  solved 85 out of 88 benchmarks, DryadSynth solved 84 benchmarks, and \(\textsc {EUSolver}_{2017}\)  solved 81 benchmarks.
In terms of the time to solve, DryadSynth solved 79 benchmarks among the fastest, \(\textsc {CVC4}_{2018}\)  solved 74,
followed by \(\textsc {EUSolver}_{2017}\)  which solved 29 among the fastest.
There were two benchmarks that were solved uniquely by DryadSynth,
and one that was solved uniquely by \(\textsc {CVC4}_{2018}\) .

Invariant Generation Track
In the invariant generation track, the LoopInvGen solver solved 115 out of 127 benchmarks, \(\textsc {CVC4}_{2018}\)  solved 109,
DryadSynth solved 103, Horndini solved 68 and \(\textsc {EUSolver}_{2017}\)  solved 61 benchmarks.
In terms of the time to solve, LoopInvGen solved 102 benchmarks among the fastest, followed by \(\textsc {CVC4}_{2018}\)  which solved 82,
DryadSynth which solved 81, Horndini which solved 21, and \(\textsc {EUSolver}_{2017}\)  which solved 15.
There was one benchmark that was solved by a unique solver – the fib17n.sl benchmark solved by LoopInvGen.


Programming By Example (Bit Vectors) Track
In the PBE track on the theory of bit vectors, the \(\textsc {CVC4}_{2018}\)  solver solved 724 out of 750 benchmarks
and \(\textsc {EUSolver}_{2017}\)  solved 677 benchmarks.
In terms of the time to solve, \(\textsc {CVC4}_{2018}\)  solved 508 benchmarks among the fastest,
and \(\textsc {EUSolver}_{2017}\)  solved 468.
However, \(\textsc {EUSolver}_{2017}\)  generates shorter expressions than \(\textsc {CVC4}_{2018}\)  in significantly many cases.
There were four benchmarks that were solved uniquely by \(\textsc {CVC4}_{2018}\) ,
and one benchmark that was solved uniquely by \(\textsc {EUSolver}_{2017}\) .


Programming By Example (Strings) Track
In the PBE track on the theory of strings, the \(\textsc {CVC4}_{2018}\)  solver solved 102 out of 118 benchmarks,
and \(\textsc {EUSolver}_{2017}\)  solved 79 benchmarks.
In terms of the time to solve, \(\textsc {CVC4}_{2018}\)  solved 98 benchmarks among the fastest,
and \(\textsc {EUSolver}_{2017}\)  solved 79.
We note again that \(\textsc {EUSolver}_{2017}\)  generates shorter expressions than \(\textsc {CVC4}_{2018}\)  in several cases.
There were 21 benchmarks that were solved uniquely by \(\textsc {CVC4}_{2018}\) .

Detailed Results
In this section we show the results of the competition from the benchmark's perspective.
For a given benchmark we would like to know:
how many solvers solved it

what are the minimum and maximum times required to solve

what are the minimum and maximum sizes of solutions generated

which solver solved the benchmark the fastest, and

which solver produced the smallest expression.
We present the results in groups organized per track and category.
For instance, the top plot in fig:prog-rep-icfp presents the details for program repair benchmarks from the general track.
The black bars above the \(y\) -axis show the range of time taken to solve across the various solvers, in our pseudo logarithmic scale.
Inspect for instance benchmark t2.sl.
The black bar indicates that the fastest solver takes less than 1 second, and the slowest one takes between 100 to 300 seconds.
The black number above the black bar indicates the exact number of seconds (floor-rounded to the nearest second)
it took the slowest solver to solve a benchmark (and \(\infty \)  if at least one solver exceeded the time bound).
Thus, we can see that for t2.sl, the slowest solver took 138 seconds.
The white number at the lower part of the bar indicates the time taken by the fastest solver.
Thus, we can see that for t2.sl, the fastest solver required less than 1 second.
The colored squares/rectangles below the black bar indicate which solvers were among the fastest to solve that benchmark
(according to the solvers' legend at the top).
For instance, we can see that \(\textsc {CVC4}_{2018}\)  and \(\textsc {EUSolver}_{2017}\)  were the fastest to solve t2.sl,
solving it in less than a second, and that among the solvers that solved t4.sl only \(\textsc {EUSolver}_{2017}\)  solved it in less than a second.
Similarly, the gray bars below the \(y\) -axis indicate the range of expression sizes in pseudo-logarithmic scales,
where the size of an expression is determined by the number of nodes in its parse tree.
The black number at the bottom of the gray bar indicates the exact size of the largest solution (or \(\infty \)  if it exceeded 1000),
and the white number at the top of the gray bar indicates the exact size of the smallest solution.
When the smallest and largest size of expressions are in the same pseudo-logarithmic bucket, as is the case in t2.sl),
we indicate the expression size only in black.
The colored squares/rectangles above the gray bar indicate which solvers were amongst the ones that produced the smallest expression
(according to the solvers' legend at the top).
For instance, for t20.sl the smallest expression produced had size 3,
which is produced only by \(\textsc {EUSolver}_{2017}\) .
Finally, the top \(x\) -axis indicates the number of solvers that solved a particular benchmark.
For instance, in fig:prog-rep-icfp, only one solver solved t6.sl, two solvers solved t14.sl,
three solvers solved t2.sl, and no solver solved t13.sl.
Note that for the benchmarks that no solver is able to solve, the black bars indicate the range of time taken by solvers to terminate.
When no solver produces a correct result, there are no colored squares/rectangles below the black bars, as is the case for t13.sl.
<FIGURE><FIGURE><FIGURE><FIGURE><FIGURE><FIGURE><FIGURE><FIGURE><FIGURE><FIGURE><FIGURE><FIGURE>Summary
This year's competition consisted of over 1600 benchmarks, 107 of which where contributed this year.
Five solvers competed this year, one of which was submitted by developers creating a tool for SyGuS-Comp for the first time.
All tools preformed remarkably well, on both existing and new benchmarks.
In particular, more than 74% of the current set of benchmarks from the general track are now solved.
However, there are several classes of problems that are still challenging for the current solvers,
especially the “Instruction Selection” and “Multiple Functions” categories;
and we hope the developers would continue to improve their SyGuS techniques and advance the state of the art.
