[Sketch]Sketch文档

The Sketch Programmers Manual

原作者：Armando Solar-Lezama

对于一段包含未知量的代码或者函数，当存在一些限制条件时，可以通过推理求出未知量。Sketch即是此种求解工具。它有自己的语法，但可以将补全后的程序按照C标准输出。

1. Overview

本章介绍了如何通过编译器来运行一个最简单的Sketch例子。

1.1. Hello world

harness void doubleSketch(int x){
  int t = x * ??;
  assert t == x + x;
}

以上即为一个最简单的Sketch代码，类似C或Java语言。但有所不同的是，程序中的??表示一个未知的常量，姑且称之为一个未知量。Sketch提供了一个合成器（synthesizer），程序中的harness关键字告诉合成器寻找满足程序要求的??值，并将其替换。在上面的例子中，??的值需要对任何的输入都满足程序中的assert语句。

Flag --bnd-inbits 指定输入的范围，如上面的例子中，输入x的值被限定在0到2^bnd-inbits。默认为5，不推荐设为更大的值。

1.2. Running the synthesizer

  > sketch test1.sk

上面的命令可以运行合成器，并直接在终端输出。

Flag --fe-output-code 可使输出为标准C++格式。

Flag --fe-output-test 可生成测试工具，随机生成一些输入数据测试生成的C++代码。

类似上述参数可以在命令行中指定，也可以直接写在文件的开头。

命令行写法：

  > sketch --fe-output-code test1.sk

文件内写法：

  pragma options " flags ";

需要注意的是，命令行的参数优先级是高于文件内部参数的。

1.3. Parallel Sovling

Sketch在某些问题上可以并行加速，需要指定flag --slv-parallel。使用该参数时，默认并行的CPU个数为当前CPU个数-1。
可以用flag --slv-p-cpus指定具体个数。并行不一定对所有问题都有提升，有些问题使用并行可能会更慢，具体见6.2节。

  Flag --slv-parallel 采用并行模式，cpu个数为当前机器的cpu个数-1

  Flag --slv-p-cpus 配合上一个参数，用来指定具体使用的cpu个数

2. Core language

核心语法借鉴了许多C和Java的语法

2.1. Primitive Types

基本类型有五个：bit，int，char，double，float。
子类型关系：bit $\subseteq$ char $\subseteq$ int。
即，能在所有使用char和int的地方用bit，bit可以表示bool型，0为false，1为true。
float和double能互相转换，但是不能和int等自动转换，即不能用1表示float，需要用1.0。

Modeling floating point 对于合成器而言，分析浮点数的值需要较多资源。Sketch提供了4种浮点数类型可供选择：AS_BIT，AS_FFIELD，AS_FIXPOINT，TO_BACKEND（区别详见官方英文manual）。
可用 Flag --fe-fpencoding 指定

2.2. Structs

Example 1. 定义和初始化一个结构体

struct Point{
  int x;
  int y;
}
void main(){
  Point p1 = new Point();
  assert p1.x == 0 && p1.y == 0; //默认初始化为0

  Point p2 = new Point(x=5,y=7);
  assert p2.x == 5 && p2.y == 7; //构造函数初始化
}

Example 2. 类似Java，结构体对象都是通过引用操作的。引用是类型安全的，并且可自动回收。一个类型T的引用总是指向null或者有效的对象。程序包含了隐式的null检查，因此对null的解引用会报错。

struct Car {
  int license;
}
void main(){
  Car c = new Car();
  Car d = c; // d points to c
  c.license = 123;
  assert d.license == 123;
  strange(c, d);
  assert d.license == 123;
  assert d == c;
}
void strange(Car x, Car y){
  x = new Car();
  y = new Car();
  x.license = 456;
  y.license = 456;
  assert x.license = y.license;
  assert x != y;
}

2.3. Temporary Structures

临时结构，不需要使用new申请内存，节约时间，可当做基本类型使用

• 赋值：赋值即复制（copy）
• 等号比较：两个临时结构的比较即为其对应数据的逐个比较

Example 3. 临时结构使用时须在类型外加竖线，构造时也需要加。例中结构体Point定义同上

  |Point| p1 = |Point|(x=5, y=3);
  Point p2 = new Point(x=3, y=7);
  |Point| p3 = p1; //内容拷贝
  p3.x = 10;
  Point p4 = p2;
  p4.x = 15;

  assert p1.x = 5;
  assert p2.x = 15;
  assert p3.x = 10;
  assert p4.x = 15;
  if(??) assert p1 == p2;// equivalent to p1.x == p2.x && p1.y==p2.y
  if(??) assert p1 != p2;// equivalent to !(p1==p2)

临时结构与引用结构的交互：相互赋值时（=）均为内容拷贝，比较时（==）均为内容比较。需要保证引用非空，否则会导致assertion错误。
限制条件：当前版本的临时结构只能为局部变量或者函数参数。并且，不允许定义临时结构的数组，不允许在结构体中定义临时结构，不允许临时结构中含有数组。

2.4. Final Types

类似Java的Final关键字，但是Sktch中没有该关键字，变量是否为final类型根据以下规则自动推断

• 用作左值的变量不为final，包括赋值语句左边的变量，前自增和后自增的变量，以及作为其他函数的引用参数
• 标准for循环中的循环变量，如果没有在循环内部改变，则在循环内部为final类型。for(int i=a; i<b; ++i)
• 数组不为final类型
• 全局变量如果是纯量，则只能为final类型。

final变量不允许赋值，必须在声明时即初始化。对于结构中的final字段（field），须在声明时通过名字初始化。

表达式也可以为final类型，如果其由final表达式组成

• Final变量为final表达式
• 如果a和b为final，则二值表达式 a op b 为final
• 如果a，b和c为final，则三元表达式 a ? b : c 为final
• 如果e是final表达式并且f是final字段，则字段解引用e.f为final。

2.5. Arrays

一个类型为T，长度为N，名字为a的数组应按以下方式定义：

T[N] a;

程序会自动检查 N$\ge$0

访问数组内元素的方式与其他语言类似，a[x]，x<N，每次访问数组时，程序会自动检查是否越界。

注意：当T可为数组类型时，即为多维数组，如：

 int[N][M] a;

对于任意的x<M，a[x]是int[N]类型。对于任意的y<N，int[x][y]为int类型（注意x和y的顺序）。

动态长度数组。长度可为任意的final表达式。

harness void main(int n, int[n] in){
  int[n] out = addone(n, in);
}
int[n] addone(int n, int[n] in){
  int[n] out;
  for(int i=0; i<n; i++){
    out[i] = in[i]+1;
  }
}

通常，输出数组的长度为输入参数或者final类型的全局变量（在声明时即初始化，并没有被修改过）。任何作为数组长度的表达式均应为final类型，不能用作函数调用。

当数组长度需要由函数本身确定时，可以通过两种方式处理：

• 直接设置为保证不会越界的较大的长度（Example 5）;
• 将数组打包为一个struct;

Example 5. filter函数，输入一个数组，返回数组中的偶数。

int[N] filter(int N, int[N] in, ref int outsz){
  outsz = 0;
  int[N] out;
  for (int i=0; i<N; i++){
    if(in[i]%2 == 0){
      out[outsz++] = in[i];
    }
  }
  return out;
}

//
int[N] tmp = filter(N, in, tsz);
int sz = tsz;
int[sz] filteredArray = tmp[0::sz];

该方法需要一个引用的参数tsz作为返回数组的长度输出。tmp[0::sz]表示从0开始到sz-1的子数组。

Array fields 数组字段，数组长度需要为final表达式，必须在声明时即初始化。

Example 6. 使用数组字段重写filter函数

struct Array{
  int sz;
  int [sz] A;
}
Array filter(Array arr){
  int outsz = 0;
  int[arr.sz] out;
  for(int i=0; i<arr.sz; i++){
    if(arr.A[i]%2==0){
      out[outsz++] = arr.A[i];
    }
  }
  return new Array(sz = outsz, A = out[0::outsz]);
}

注意out的长度为arr.sz，这会使结构arr和字段sz均为final类型。sz已经在结构内的数组作为长度，故已经为final类型。现在arr也为final类型，因此对arr的任何字段赋值均会产生报错。

Flag --bnd-arr-size 限制动态长度数组的大小，如果输入参数为N和int[N] x，则N最大为bnd-arr-size。另外，如果参数为T[N*N] x，则该数组最大长度为bnd-arr-size²。

Multi-dimensional arrays 多维数组的定义为：
T[sz0, sz1, …, szn] A;
访问多维数组的元素：
A[i0, i1, …, in], 0$\le$ij<szj
多维数组其实是个语法糖，内部即为嵌套数组实现，只是使得顺序与直观相同。

Bulk array access 数组块访问，a[x::M]，如果x$\ge$0并且x+M$\leq$N，则返回T[M]，包含a[x]，…，a[x+M-1]。如果不满足条件则会报错。注意，当M=0时，允许x=N。
Array assignment 使用赋值操作可将整个数组或数组中的某一块复制到另一个数组中

b = a; // 须保证b的长度大于等于a，否则报错。
b[2::4] = a[5::4]; // 允许块复制，先将右边的都读出来后再复制到左边。

Array constants 支持C风格的数组常量{a1, a2, …, ak}，并且允许在任何需要数组的地方使用。

int[3] x = {1, 2, 3};
x[{1, 2}[a]] = 3;
x[0] = {4, 5, 6}[b];
x[{0, 1}[a]::2] = {0, 1, 2, 3, 4, 5, 6}[b::2];

String literals 字符串常量，"a string"即{‘a’, ’ ', ‘s’, ‘t’, ‘r’, ‘i’, ‘n’, ‘g’, ‘\0’}
Nested array constants 嵌套数组常量，在内部数组元素个数不一致时，取最大的，其他填充。{{1, 2}, {1}, {1, 2, 3}, {1}}的类型为int[3][4]，并等同于{{1,2,0},{1,0,0},{1,2,3},{1,0,0}}。
Array Equality 数组相等比较，长度和内容均相等时，两个数组相等。
数组a == 数组b，则a和b类型均为T[n]且任意的i<n时，a[i]==b[i];
数组a == 常量b，则a的类型为T[n]，b的类型为T，且n==1，a[0]==b;
多维数组T[n][m] a，T[m][n] b，若a==b，则n==m;
多维数组T[p][n][m] a，T[t] b，若a==b，则t==m && n==1 && p==1;
Bit Vectors 对于位数组，位操作后的长度变化如下：
bit[N] & bit[M] → bit[max(N,M)]
bit[N] | bit[M] → bit[max(N,M)]
bit[N] ^ bit[M] → bit[max(N,M)]
bit[N] + bit[M] → bit[max(N,M)]
bit[N] >> int → bit[N]
bit[N] << int → bit[N]
!bit[N] → bit[N]

对于大部分的数组操作都允许数组的长度不一致，一般都是短的数组通过填充后，再与长的数组操作。

2.6. Automatic Padding and Typecasting

在数组赋值或者参数传递时，能够通过填充隐式的改变长度（不包括引用的参数）。
int和bit填充0，struct填充null

Example 8.

int[4] x = {1, 2}; // x = {1, 2, 0, 0}。

Example 9.

int[2][2] x = {{2, 2}, {2, 2}};
int[4][4] y = x; // x -> int[2][4]={{2,2}, {2,2}, {0,0}, {0,0}} -> {{2,2,0,0}, {2,2,0,0}, {0,0,0,0}, {0,0,0,0}}。

Example 10.

Car[4] x;
car t = new Car();
x = t; // t -> Car[1] -> Car[4]={t, null, null, null}

Example 11.

int[n] x;
x = 0; // 数组清零，即使n/==0也不会报错

Example 12. 多维数组的填充

struct Car{ ... }
...
Car[2] x = {new Car(), new Car()};
Car[4][3] y = x;
assert y[0][0] == x[0];
assert y[1][0] == x[1];
assert y[1][1::3] == {null, null, null};
assert y[2] == {null, null, null, null};

先隐式转换Car -> Car[4]，然后对y赋值，如下：

for(int i=0; i<N; i++){
  if(i<M)
    y[i] = x[i];
  else
    y[i] = pad(T); // null
}

2.7. Explicit Typecasting

Sketch提供四种显式转换

• T[N] -> T[M]: (T[M])a //T[N] a;当M<N时，直接截断
• bit[N]能转换成int，bit[0]为最低位，不允许int转bit[N]
• 如果浮点数使用–fe-fpencoding AS_FIXPOINT，则可与int互相转换
• 代数数据类型（algebraic data type）能转化为它的变体。程序会自动检查类型是否正确。

Example 13. 检查x中元素是否全为0。

int[N] x=...;
assert x == (bit[N])0; //当N大于1时，直接比较会报错，因此先将纯量0显式转换为数组。

Example 14. 把动态长度的数组复制到另一个数组里

int[N] x=...;
int[M] y = (bit[M])x; // M>N时，写y=x;当M<=N时，写y=x[0::M]。未知时，两种写法都可能报错

2.8. Algebraic Data types (ADTs)

代数数据类型ADTs，看下面例子

adt Tree{
  Leaf{ int value; }
  Branch{ Tree left; Tree right; }
}
// a simple Tree
Tree t1 = new Leaf(value=5);
Tree t2 = new Leaf(value=6);
Tree t3 = new Leaf(value=7);
Tree t = new Branch(left=t1, right=new Branch(left=t2, right=t3));

Tree是一个ADT，有两个变体Leaf和Branch，他们都是Tree的子类型，可以实例化，但是因此导致Tree变成抽象的，不能实例化。
可以通过switch语句判断Tree的具体类型

int sum(Tree t){
  int v=0;
  switch(t){ // There is an implicit assertion that t is not null.
    case Leaf:{
      /*t is now of type Leaf in this block */
      v = t.value;
    }
    case Branch:{
      /*t is now of type Branch is this block */
      v = sum(t.left)+sum(t.right);
    }
  }
  /*Outside the switch, t goes back to being of type Tree*/
  return v;
}

上面的swtich语句语法上类似C，但是语义上完全不同。case必须对应Tree的子类；该switch语句的case只会执行一个，不会像C连续下去；并且给swtich的参数不能为null。

ADT允许分层嵌套：

adt ASTNode{
  adt Expression{
    Plus {Expression left; Expression right;}
    Times {Expression left; Expression right;}
    Num{ int n; }
    Var{ int id; }
  }
  adt Statement{
    Assign{ int lhs; Expression rhs; }
    IfStmt{ Expression cond; Statement tpart; Statement epart; }
    WhileStmt{Expression cond; Statement body;}
  }
}

上面的例子中，能创建Plus，Times，IfStmt，WhileStmt的实例，但不能创建Expression和Statement的实例。

下面是ADT的一些其它属性：

• ADT的所有字段都不允许改变（immutable）。
• 一个ADT的记录（Records）可以有字段（fields），这些字段能被其他变体继承。
• 上层的ADT和其变体不能有相同名字的字段。
• ADT及其变体的定义不能跨包（package）。
• 传给switch的参数必须是变量，switch的case必须为该变量的变体，并且变量不能为null。
• switch语句应该包含所有的case。
• 从父类型到子类型会触发隐式类型转换。
• 显式转换只能用来将父类型转换到子类型，否则会报错。

Equality ADT类型的变量看起来与引用相同，并且大部分情况确实相同，但是在相等比较上却不同。

两个ADT的比较是值比较，只有所有字段的值都相等，两个ADT才相等。

Tree t1 = new Leaf(value=5);
Tree t2 = new Leaf(value=5);
assert t1 == t2;

Tree b1 = new Branch(left = t1, right= t2);
Tree b2 = new Branch(left = t1, right= t2);
assert b1 == b2;

对于递归类的ADT，sketch自动生成递归比较函数。并且未初始化的ADT变量值为null，可直接用null来判断一个ADT变量是否已经初始化。

if( t1 == null){
  ...
}

未初始化的ADT变量仅能与null比较，其他操作会报错。如访问某个字段，显式类型转换或者将其传给switch语句。

Flag --bnd-inline-amnt 限制递归深度

2.9. Struct inheritance

ADT定义后不能改变，而使用struct继承方式定义则不受此限制，且用法与ADT相同。

struct Tree{
  int x;
}
struct Leaf extends Tree{
  int value;
}
struct Branch extends Tree{
  Tree left;
  Tree right;
}

上面定义的Tree，Leaf和Branch与使用adt定义的用法一致。但是现在Leaf和Branch值在创建后可以改变。这可能会导致程序需要更多的时间。

2.10. Control Flow

sketch支持if-then, while, do-while, for，且语法和含义都与C一致。switch用来匹配类型，因此不支持类似C的用法。同时，continue和break语句也不支持。

合成器通过展开的方式来推理循环的次数。
Flag --bnd-unroll-amnt 控制展开次数上限

Example 15.

for(int i=0; i<N; ++i){...} // 展开次数受到bnd-unroll-amnt限制
for(int i=0; i<100; ++i){...} // 展开100次，常数不受bnd-unroll-amnt限制
for(int i=0; i<N && i<7; ++i){...} // 展开次数受到bnd-unroll-amnt限制，但不会超过7

2.11. Funtions

sketch支持函数，定义函数的语法与C相同。

ret _ type name ( args ){
  body
}

Recursion 合成器通过内联的方式推理函数调用。对于递归函数，需要限定内联的最大次数。
Flag --bnd-inline-amnt 限制函数能在栈中出现的最大次数
Flag --bnd-bound-mode 两种求解方式CALLSITE和CALLNAME。默认CALLNAME为栈中函数出现的次数，CALLSITE为每个函数单独计数（此处存疑）。

Reference Vs. Value Parameter Passing 默认为值传递，需要传递引用时，需要加关键字ref

Example 16.

void foo(int in, ref int out){
  in = in + 1; // changes to in are not visible to the caller
  out = in + 1; //changes to out are
}
harness void main(int x){
  int y = x;
  int z = y+10;
  foo(y, z); // call to foo can change z but not y
  assert y == x && z == x+2;
}

传递引用实际上也并不是真正的引用，而是copy-in-copy-out。如果传递的是局部变量并且没有对引用设置别名，那这种方式和真正的引用没有区别。但是，如果设置别名或者传递的是结构的某个字段，那么这种方式就和真正的引用有所区别。

Example 17. copy-in-copy-out和真正引用的区别：

void foo(ref int p1, ref int p2){
  int t = p1;
  p1 = p1+1;
  p2 = p2+2;
  assert p1 == t+1;
}
harness void main(int x){
  int z = x;
  foo(z, z);
  assert z == x+2;
}

copy-in-copy-out不关心传递进来几个参数，最后z的值是由最后的修改决定的。

Implicit size parameters 传递数组参数时，一般需要将数组的大小也传递进去。

double[n] foo(int n, double[n] in);

但也可以将大小参数用方括号括起来设为隐式参数，调用时就不需要传递了。

double[n/2] foo([int n], double[n] in){//brackets signify implicit parameter
  return in[0::n/2];
}
harness void main(int n, double[n] in){
  double[n/2] res = foo(in); //we don’t have to pass n.
  double[n] res = foo(2*n, in);//but we can if we want.
}

隐式参数必须要在参数列表的开始，并且所有的隐式参数用方括号括起来。另外对于隐式参数，其类型必须为int，且每个隐式参数的值都对应至少一个数组参数的大小。

Example 18. 隐式参数使用示例1

// legal uses
int[n] foo([int n, int m], int[n] a, int[m] b)...
int[m] foo([int n], int[n] a, int m, int[m] b)...
int[n+m] foo([int n, int m], int[n][m] a, int[m] b)...
int[n+m] foo([int n, int m], int[n][m] a, int[2*m] b)...
// illegal uses
int[n] foo([int n, int m], int[n] a)... // m is not used
int[n] foo([int n], int[n*2] a)... //n is not the size of any array param
int[n+m] foo([int n, int m], int[n][m*2] a, int[m-1] b)... //m is not the size of any array param

隐式参数要么全部传递，要么全部不传递，不能只传一部分。并且，如果一个隐式参数被多个数组使用，那么该参数值须保持一致。

Example 19. 隐式参数使用示例2

void foo([int n, int m], int[n] a, int[m][n] b)...

int[5] w;
int[5] x;
int[3][5] y;
int[10] z;
//正确用法
foo(x, y); // n==5, m==n
foo(w, x); // n==5, m==1
foo(10, 3, z, y); // Involves an implicit cast for y.
//错误用法
foo(z, y); //different value of n for the two arrays
foo(3, z, y); //Passes only a subset of implicit parameters

2.12. Function parameters

函数也能作为其他函数的参数使用，类型为fun

Example 20. 函数作为参数的示例

int apply(fun f, int x){
  return f(x);
}
int timesTwo(int x){
  return x+x;
}
harness void main(int x){
  assert apply(timesTwo, x) == 2*x;
}

指定函数类型的fun关键字只能作为参数使用。函数类型fun不能用来定义变量，不能创建函数数组，也不能作为返回值类型或者引用使用。
但是一个函数参数并没有指明该函数需要什么参数，这就给程序增加了灵活性，甚至可以弥补程序没有泛型的问题。

2.13. Local functions and closures

Sketch支持在函数内部定义函数，具体语法和在函数外部定义一样。内部函数可以访问外部函数内的变量。下面的例子说明了局部函数如何和高阶函数一起使用。

void ForLoop(fun f, int i, int N){
  if(i<N){
    f(i);
    ForLoop(f, i+1, N);
  }
}

harness void main(int N, int[N] A){
  int[N] B;
  void copy(int i){
    B[i] = A[i]
  }
  ForLoop(copy, 0, N);
  assert A==B;
}

在上面的例子中，ForLoop函数使用了包括copy函数及其局部环境的闭包。ForLoop函数的作用和直接将copy函数放入for循环中一样。因为函数类型无法被返回或者写入堆中，因此函数的闭包使得其可以修改定义在其外部函数的局部变量，并不引起任何歧义。
最后，局部函数只能在定义之后使用，因此不能循环调用。

2.14. Lambda Functions

Lambda函数是匿名函数。语法：(vars) -> expression。两个例子

Example 21. Lambda作为高阶函数参数

int apply(fun f, int x) {
  return f(x, 5);
}
harness void main() {
  int result = apply((x, y) -> x + y, 7);
  assert result == 12;
}

Example 22. 定义函数fun类型的变量

  harness void main(){
    int t = 3;
    fun foo = (x) -> t*x;
    assert foo(2) == 6;
  }

Lambda函数必须在局部环境中定义和使用。Lambda函数中的表达式可以是任何合法的表达式，但其形参不能用作左值。
Lambda函数不能定义在结构体内，也不能作为返回值，类似局部函数。fun类型的变量均为final类型，初始化后不能修改。

Example 23. 在局部函数内使用两个不同类型的局部变量构造

harness void main(){
  bit t = 1;
  int a = 2;
  int b = 3;

  int foo(){
    fun g = ()->$(bit)?5:$(int);
    return g();
  }
  assert foo() == 3;
}

Example 24.

int apply(fun f) {
  return f();
}
harness void main(int x) {
  int a = 1;
  int b = 2;
  int foo() {
    fun f = () -> $(int);
    return f();
  }
  int t = apply(foo) * ??;
  assert t == x + x;
}

2.15. Polymorphism

Sketch从1.7.1开始支持多态。定义如下
type name<typeParams>( type pname , … ){ … }

典型的多态函数示例：

void forall<T>([int n], fun f, ref T[n] x){
  for(int i=0; i<n; ++i){
    f(x[i]);
  }
}

调用forall函数时，T应使用数据类型代替，可以为基础类型，结构体，adt和数组,但不能是fun类型。

Example 25. 使用一个多态函数

harness void main(){
  int sum=0;
  generator void add(int t){
    sum += t;
  }
  forall(add, {1,2,3,4,5});
  assert sum == 15;
  sum = 0;
  forall( (u) -> forall(add, u),{ {1,2,0} , {3,4,5} } ); // 此处存疑
  assert sum == 15;
}

从1.7.5开始，Sketch支持结构和ADT的多态。使用多态时，在名字后面加<typeParams>

struct SArray<T>{
  int n;
  T[n] val;
}

Example 26. 使用多态结构

include "array.skh";

int len<T>(SArray<T> ar){ return ar.n; }

harness void main(){
  SArray<int> ar1 = new SArray<int>(n=5, val={1,2,3,4,5});
  SArray<SArray<int>> ar2 = new SArray<SArray<int>>(n=1, val={ar1});
  assert ar1.val[0] == 1;
  assert ar2.val[0] == ar1;
  assert len(ar1) == 5;
}

对于ADT类似。如list包中的List ADT

adt List<T>{
  Cons{T val; List<T> next;}
  Nil{}
}
// 前插
List<T> add<T>(List<T> lst, T val){
  return new Cons<T>(val=val, next=lst);
}

Limitations 当前实现的多态的一些限制

1. 对于结构和ADT，类型不能为数组
2. 结构和ADT的构造需要显式指定类型T，如上面的new Cons<T>
3. 对于函数的参数类型推理十分有限，举例如下

  //Consider the two functions below.
  T read<T>(List<T> in){ ... }
  List<T> gen<T>(){ ... }
  void foo(List<int> lst){
    int x = read(lst); // From the context it is clear that T=int;
    int y = read(gen()); //In this case too, the context is enough
    //to determine that T = int;
    read(gen()); // However, this would lead to a type error
    // because the type of T is ambiguous.
  }

4. 程序对参数类型的推理更倾向于选择更具体的类型，如传递数值0，可能推理为bit而不是int，需要显式转换（int）0,或者定义一个int变量赋值为0。

2.16. Uninterpreted Functions

未解释的函数，定义如下

ret_type name(args);

未解释的函数就是函数体未知，只知道是个纯函数，当给定相同输入时，输出相同。如果用未解释的函数建模某个过程，则须保证该过程为数学过程，不涉及堆或全局变量。因此，未解释的函数被限制不能涉及结构。（此处存疑）

2.17. Packages

Sketch支持定义包，语法如下

package PACKAGENAME;

定义在同一个文件内的所有函数和结构都必须属于同一个包，否则编译报错。如果一个文件没有package命令，则默认为package ANONIMOUS。包名不能包含句号或其它特殊符号。
在一个文件中使用其它包，需要使用include命令，引号内为包所在文件。

include "file.sk"

Flag --fe-inc 指定查找目录，可以多次使用以包含多个目录。

每个包为一个命名空间，以避免名字冲突。使用其它包中的函数或者结构时，应使用@符号，如foo@pk()，则使用包名为pk中的函数foo。类似的，Car@vehicles c = new Car@vehicles() 定义了一个Car类型的对象，该类型在包vehicles中定义。

如果没有显式指定包名，则系统会按照以下方法查找：

• 如果当前包内有定义，则使用当前包内的定义；
• 如果当前包内无定义，但在其它包（仅一个）内有定义，则使用该包内定义；
• 如果当前包内无定义，但在其它包（多个）有定义，则报错。必须显式指定包名。

Example 27. 使用包的示例

// Begin file farm.sk
package farm;
struct Goat{
  int weight; }
struct Ram{
  int age; }
struct Mouse{
  int age; }
// End file farm.sk

// Begin file computer.sk
package computer;
struct Cpu{
  int freq; }
struct Ram{
  int size; }
struct Mouse{
  bit isWireless; }
// End file computer.sk

//Begin file test.sk
include "computer.sk";
include "farm.sk";
struct Mouse{
  int t;
}
harness main(){
  Cpu c = new Cpu(); // No ambiguity here.
  Ram@farm r = new Ram@farm() //Without @farm, this would be an error.
  Ram@computer rc = new Ram@computer();
  Mouse m = new Mouse(); // Give preference to the locally defined mouse.
  m.t = 10;
}
//End file test.sk

2.18. Global variables

Sketch支持全局变量，但有以下限制：

• 全局变量总是定义它的包所私有的。尽管你可以在包内读写给定的全局变量，但他们依然不是公有的（public）。
• 标量的全局变量是final类型的，因此全局的数组变量长度只能是固定的。
• 全局变量的初始化只能使用无副作用（side-effect-free）的常量表达式或final类型的全局变量。new C(a=x)，只要x是无副作用的，则该表达式也是无副作用的。除法，数组访问和函数调用是为有副作用，因此可能报错。

2.19. Annotation System

注释系统，旨在简化添加语言扩展的过程。语法：
@Name(parameter-string)
Name是注释的名字，parameter-string是一个描述注释参数的字符串。当前注释只支持函数和结构的定义。
注释在整个编译链中一直保存到代码生成。这对于想写自定义的代码生成非常有用。你只需要在你的代码中添加注释，那么你的代码生成器就能通过自动查询来获得函数和结构的注释。以下是一些比较特别的注释说明：

• @Native(code) 能够重写注释函数的代码生成
• @NeedsInclude(inc) 告诉代码生成器该函数需要包含单独的头文件。
• @Immutable() 将某个结构声明为不可更改的结构
• @DontAnalyze() 告诉合成器某个harness不需要分析，当你的某个harness比较大且非常复杂，但又需要生成代码时非常有用。
• @Private() 表示某个函数不应该用在包外
• @Gen() 用来注释一个特殊的函数类，对分析引擎有特殊含义，一般不在自己代码中使用。

2.20. The @Native annotation

比较重要的两个注释是@Native和@NeedInclude，第一个允许用户重写标准的代码生成，并告诉合成器对于一个特定的函数应该生成什么代码。第二个则告诉代码生成器该函数需要包含特定的头文件。

Example 28.

int NDCNT = 0;

int getND_private(int i);
int getND(){
  // 每次调用会返回一个不确定的值
  return getND_private(NDCNT++);
}

struct FileHandle{
  int maxReads;
}

FildHandle getFile(){
  //文件中的值为不确定的值
  return new FileHandle(maxReads=getND());
}

bit moreValues(FileHandle fh){
  // maxReads应该不小于0
  assert fh.maxReads>=0;
  return fh.maxReads!=0;
}

int readInt(FileHandle fh){
  // 不允许读取文件末尾的内容
  assert fh.maxReads > 0;
  --fh.maxReads;
  return getND();
}

FileHandle初始化为要读取的次数。每次调用readInt时，合成器判断是否达到了最大读取次数，没有就再读一个不确定的值。这种定义在需要读取文件时非常有用，但是对于一个真实的文件，要从文件中生成代码，上面的定义还不够。

使用@Native重写上面的代码

// 额外的字段对分析引擎不可见，但是在代码生成时需要。
struct FileHandle{
  int maxReads;
  @NeedsInclude("#include <fstream>")
  @NeedsInclude("#include <string>")
  @Native("ifstream in;")
  @Native("int last;")
  @Native("bool goon;")
  @Native("FileHandle(const string& s):in(s.c_str()){ in>>last; goon = !in.eof() && !in.fail(); }")
  @Native("int readInt(){ int x = last; in>>last; goon = !in.eof() && !in.fail(); return x;}")
}

@Native("{ _out = fh->goon; }")
  bit moreValues(FileHandle fh){
  assert fh.maxReads >= 0;
  return fh.maxReads!=0;
}

@Native("{ _out = fh->readInt(); }")
int readInt(FileHandle fh){
  assert fh.maxReads > 0;
  --fh.maxReads;
  return getND();
}

在分析代码时，注释对于合成器是不可见的，合成器此时应关注高层的建模。但是在生成代码时，却需要按照注释中的指导生成。
@Native注释允许程序员使用简单的模型代替复杂或底层的函数。程序员应该确保模型能够匹配到正在生成的相关代码。
更一般的说，如果需要自定义的扩展Sketch合成器，使用注释可以在不影响已有结构的基础上，将信息传递到你自定义的扩展中。

2.21. Casting of Expressions

Sketch允许在高阶函数调用中投射（cast）表达式。这些表达式被投射为Lambda表达式。能够被自动投射的表达式不应使用函数内的形参，也就是说在Lambda函数执行时，传进去的参数是被忽略掉的。

这在高阶生成器（High-Order Genernators）中非常有用。

generator int rec(fun choices){
  if(??){
    return choices();
  }else{
    return {|rec(choices) (+|-|*) rec(choices)|};
  }
}

如果用户想给高阶生成器传递参数，需要使用局部变量构造。下面的表达式在传给高阶生成器之前会被转换为lambda表达式。

harness void sketch(int x, int y, int z){
  assert rec($(int)) == (x+x)*(y-z);
}

3. Constant Generators and Specs

Sketch通过允许在代码中留空来扩展程序。每个空都对应一个包含了填充该空的代码片段集合的生成器。Sketch提供了丰富的构造生成器的集合。但是所有这些生成器都是一个核心生成器的语法糖，该核心生成器就是由一个??代替的整数。
从程序员的视角看，一个整数生成器就是一个占位符。在程序合成时，合成器必须用常量替代它。合成器要确保在所有可能的输入中，生成的代码都不会产生assert错误。

harness void main(int x){
  int y = x * ??;
  assert y == x + x;
}

上面的程序可以看作一个Sketch的Hello Wrold。该程序说明了一个Sketch的基本要素：

• harness程序
• 被生成器标记的空
• assertions

harness程序是Sketch的入口，配合assertions来得到想要的程序。合成器的目标是寻找常数C取代??，使得程序对任意的输入都满足assertion条件。上面的例子中，合成器需要的常数为2。

3.1. Harnesses and function equivalence requirement

一个Sketch程序可以有多个harness，Sketch会保证每个harness函数对合法输入的正确性。harness函数的参数不允许为堆中的对象，并且在验证每个harness之前，所有的全局变量都会被重置为初始值。因此，每个harness的验证顺序就不重要了。
Sketch还允许程序员这样的操作：一个函数（implementation）必须在功能上和另一个函数（specification）相同，只要在implementation函数名字后面加上 implements fname。当实现函数（自己翻译的implementation）和参考函数（自己翻译的specification）都没有使用全局变量时，相等约束可以看成一个调用了这两个函数并且用assert比较结果的harness。但是对于这样的情况推荐使用implements，因为这样显式告诉生成器可以用实现函数代替参考函数，给了程序更强的约束。
如果实现函数或者参考函数访问了全局变量，那么对于这些全局变量的所有可能值（不仅仅是初始值）两个函数的结果都必须相等，且在两个函数运行结束后，全局变量的值也应一致。这样可以保证在使用实现函数替换参考函数后，总是能保留之前的语义。也因此实现函数和参考函数不能访问指向堆中的全局变量。

Example 29. 使用harness和implements的简单例子

int count = 0;
int twox(int x, int y){
  ++count;
  return x+x;
}

int expr1(int x, int y){
  return x*?? + y*??;
}

int expr2(int x, int y) implements twox{
  count = count + ??;
  return x*?? + y*??;
}

harness void foo(){
  assert expr1(5, 2)*expr2(2, 4) == 24;
}

harness对两个函数的乘积增加了限制。而expr2增加了需要作为twox的实现函数的限制条件。又因twox修改了全局变量count，那么expr2应该以相同的方式修改count。
Implementation note 当前Sketch版本中，需要保持参考函数中不能有任何的未知量。并且，编译器会默认参考函数应该比实现函数更简单，因此在分析阶段，编译器会把每个实现函数替换成原来的参考函数。这样替换对求解器的性能有巨大的提升，但是却可能在实现函数中有递归时，产生无法识别的无穷递归的bug。

3.2. Assumptions

Sketch1.6.7后支持assume语句，assume后面的条件为假时，程序终止，后续的assertion都会被忽略。但是当一个函数被另一个函数调用时，在调用者眼里，被调用函数内的assumptions可以当作assertions看，因为调用需要保证环境和传入的参数满足被调用的assumptions。但是需要注意的是，对于生成器函数而言却并非如此，因为生成器函数是直接内联到调用者内的（详见第四章）。

对于某个参考函数的实现函数而言，它的assumptions应该比参考函数更弱（子集），因为任何对于参考函数的合法输入也必须对实现函数合法。
Example 30. Assume和implements

harness int foo(int x){
  assume x > 10;
  int t = x-10;
  assert t > 0;
  return t;
}
int moo(int x) implements foo{
  assume x > 3;
  int t = x-??;
  assert t > 0;
  return t;
}
harness void main(int x){
  assume x > 5;
  int t = ??;
  moo(x+t);
  minimize(t);
}

在上面的例子中，harness foo函数中假定x>10，必定满足后面的assert条件。而在实现函数moo中，未知量??也会被定义为10，因为assert限制条件与foo中一致。看起来moo中的assume条件是不够强的，不能保证assert，但是因为moo是foo的实现函数，moo会继承foo的条件。

3.3. Types for Constant Generators

??能代表以下不同类型的常量，系统会使用简单的推理决定使用何种类型。

• int
• bit
• 常量大小的数组和嵌套的常量大小的数组

3.4. Ranges for holes

可以使用以下参数指定程序中所有的??的搜索范围。
Flag --bnd-ctrlbits 合成器对未知值的搜索范围会被限制在0-2^N。也可以使用??(N)对某个未知值单独作限制。

3.5. Minimizing Hole Values

许多情况下，合成器需要找到最小的满足条件的常量。此时可以使用minimize(e)函数，这样程序会使e尽可能的小。更具体的说，合成器会找到一个e的上界e<bnd，如果有多个最小状态，则合成器会找到局部最小的集合，包含所有情况。
Flag --bnd-mbits 指定用多少位表示的所有上界（默认5）。注意，e的值需要严格小于上界，也就是上界为N的话，e只能为N-1

Example 31. 考虑下面的程序

harness void main(int i, int j){
  int i_orig=i, j_orig=j;
  if(i > ??){ // we’ll call this unknown u1
    i = ??; // u2
  }
  if(j > ??){ // u3
    j = ??; // u4
  }
  if(i_orig > 3 && j_orig > 3)
    assert 2*i + j > 6;
  minimize(i);
  minimize(j);
}

在上面的程序中，合成器会分别寻找i和j最小的上界（称之为b1，b2）。一种情况u1=3,u2=4,u3=0,u4=0，此时(b1, b2)为(5, 1)；另一种情况u1=0,u2=0,u3=0,u4=7，此时(b1, b2)为(1, 8)。这两个解不能比较，不存在好坏区分。

除了一般的最小化，合成器有一些语法糖来支持推理最少的语句数量。例如，下面的程序会产生交换x和y需要的最小赋值次数。（此处存疑）

void swap(ref bit[W] x, ref bit[W] y){
  minrepeat{
    if(??){ x = x ^ y;}else{ y = x ^ y; }
  }
}
harness void main(bit[W] x, bit[W] y){
  bit[W] tx = x; bit[W] ty = y;
  swap(x, y);
  assert x==ty && y == tx;
}

4. Generator functions

一个生成器即一个可能的解空间，解为可以填补某个未知量的代码片段。常量生成器是最简单的，它的解空间（代码片段的空间）就是某个范围的所有整数。复杂的生成器可以利用简单的生成器构成生成器函数得到。
举例来说，考虑一个有两个参数x和y的线性函数的集合，所有可能的函数集合可由下面的生成器函数表示:

generator int legen(int i, int j){
  return ??*i + ??*j + ??;
}

生成器函数可以被当作一般函数使用，但其语义却和普通函数不同。每次对生成器函数的调用都会被一个具体填充后的函数代替，每次调用的填充可能都不相同。下面是个例子：

harness void main(int x, int y){
  assert legen(x,y) == 2*x + 3;
  assert legen(x,y) == 3*x + 2*y;
}

求解上面的代码输出如下：

void _main (int x, int y){
  assert ((((2 * x) + (0 * y)) + 3) == ((2 * x) + 3));
  assert (((3 * x) + (2 * y)) == ((3 * x) + (2 * y)));
}

生成器函数和普通函数非常不同。普通函数内即使有多个生成器，在求解生成器之后，每次调用都是相同的填充（解）。看下面例子：

int linexp(int x, int y){
  return ?? *x + ?? *y + ??;
}
harness void main(int x, int y){
  assert linexp(x,y) >= 2*x + y;
  assert linexp(x,y) <= 2*x + y+2;
}

对上面的例子，生成器会寻找同时满足两个条件的解（可能有多个），输出一个解如下：

void linexp (int x, int y, ref int _out){
  _out = 0;
  _out = (2 * x) + (1 * y);
  return;
}
void _main (int x, int y){
  int _out = 0;
  linexp(x, y, _out);
  assert (_out >= ((2 * x) + y));
  int _out_0 = 0;
  linexp(x, y, _out_0);
  assert (_out_0 <= (((2 * x) + y) + 2));
}

编译器总会把函数返回值替换为引用参数。

4.1. Recursive Generator Functions

生成器强大的表示能力大部分得自其可以递归的定义一个表达式空间。

Example 32. 递归生成器

generator int rec(int x, int y, int z){
  int t = ??;
  if(t == 0){return x;}
  if(t == 1){return y;}
  if(t == 2){return z;}
  int a = rec(x,y,z);
  int b = rec(x,y,z);
  if(t == 3){return a * b;}
  if(t == 4){return a + b;}
  if(t == 5){return a - b;}
}
harness void sketch( int x, int y, int z ){
  assert rec(x,y,z) == (x + x) * (y - z);
}

但是，在定义递归生成器时一定要十分小心，因为定义的方式会直接对求解时间产生巨大影响。特别的，在定义生成器时，尤其要注意递归和对称。
Recursion control in generators 编译器通过内联的方式处理递归生成器，内联次数受bnd-inline-amnt限制。

下例代码是上例的另一种不好的定义方式。
Example 33. Inefficient recursive generator

generator int rec(int x, int y, int z){
  int t = ??;
  if(t == 0){return x;}
  if(t == 1){return y;}
  if(t == 2){return z;}
  int a = rec(x,y,z);
  int b = rec(x,y,z);
  if(t == 3){return rec(x,y,z) * rec(x,y,z);}
  if(t == 4){return rec(x,y,z) + rec(x,y,z);}
  if(t == 5){return rec(x,y,z) - rec(x,y,z);}
}
harness void sketch( int x, int y, int z ){
  assert rec(x,y,z) == (x + x) * (y - z);
}

两个生成器定义了相同的语法，定义了相同的表达式空间。但是第二个生成器因为每次递归调用rec都会单独内联，所以每次调用程序会将变大6倍，而不是第一种的2倍。

还有一个问题，递归生成器的内联次数和一般函数内联共用一个参数，但是，递归生成器的调用次数一般远小于普通函数的递归。因此可以为生成器单独定义一个限制参数。

Example 34. Generator with manual inlining control

generator int rec(int x, int y, int z, int bnd){
  assert bnd >= 0;
  int t = ??;
  if(t == 0){return x;}
  if(t == 1){return y;}
  if(t == 2){return z;}

  int a = rec(x,y,z, bnd-1);
  int b = rec(x,y,z, bnd-1);
  ...
}

上面的例子中当参数bnd小于0时，合成器会停止内联。

Avoiding symmetries 另一个需要注意的是对称性，就是不同的赋值也会产生同样的结果。产生对称性的原因可能为可交换性(commutative)和关联(associative)。

Example 35. 生成器中的对称性举例

generator int sum(int x, int y, int z, int bnd){
  assert bnd > 0;
  generator int factor(){
    return {| x | y | z|} * {| x | y | z | ?? |};
  }
  if(??){ return factor(); }
  else{return sum(x,y,z, bnd-1) + sum(x,y,z, bnd-1);}
}
generator int sumB(int x, int y, int z, int bnd){
  assert bnd > 0;
  generator int factor(){
    return {| x | y | z|} * {| x | y | z | ?? |};
  }
  if(??){ return factor(); }
  else{ return factor() + sumB(x,y,z, bnd-1);}
}

两个都表示相同的表达式空间，但是生成器sumB对生成的表达式强制右关联（right-associativity），而生成器sum可能产生任意的关联，因此sumB比sum效率更高。另外，sumB的bnd参数意义明确，就是递归次数；而sum的bnd参数在此却是指递归树深度，可能与bnd参数的本意不太相符。

4.2. Regular Expression Generators

Sketch提供简单的表达式表示方法，基于正则表达式的正则表达式生成器。
{|regexp|}
竖线|表示选择，？定义可选择的子表达式，使用正则表达式更简洁的表示上面的例子：

generator int rec(int x, int y, int z){
  if(??){
    return {| x | y | z |};
  }else{
    return {| rec(x,y,z) (+ | - | *) rec(x,y,z)|};
  }
}
harness void sketch( int x, int y, int z ){
  assert rec(x,y, z) == (x + x) * (y - z);
}

正则表达式也可以和指针表达式一起使用。比如，假设你想创建一个可以把数据压入栈中的函数，使用链表表示。可以使用类似下面的方法：（此处存疑）

push(Stack s, int val){
  Node n = new Node();
  n.val = val;
  {| (s.head | n)(.next)? |} = {| (s.head | n)(.next)? |};
  {| (s.head | n)(.next)? |} = {| (s.head | n)(.next)? |};
}

4.3. Local Variables Construct

Sketch可以使用$(type)结构指导合成器在求解时只考虑当前范围内所有该类型的数据。

harness void main(int x) {
  int a = 2;
  double b = 2.3;
  assert x*$(int) == x + x; // $(int)==={|0|a|x|}
}

type可以是基础类型或者任何用户定义的类型，基础类型的默认值也会被考虑。当前范围内的局部变量和形参都会考虑。如果是在局部函数内，则在局部函数外的函数的局部变量和形参也会考虑。

4.4. High order generators

生成器可以作为其它生成器或者函数的参数，这样大大增加了生成器的灵活性。比如，上面的rec生成器有三个变量，但是有时候可能需要两个或者五个等，下面是个灵活运用高阶生成器的例子：

generator int rec(fun choices){
  if(??){
    return choices();
  }else{
    return {| rec(choices) (+ | - | *) rec(choices)|};
  }
}
harness void sketch( int x, int y, int z ){
  generator int F(){
    return {| x | y | z |};
  }
  assert rec(F) == (x + x) * (y - z);
}

在不同的上下文环境，可能表达式需要特别的子表达式，仍旧使用上面定义的生成器：

harness void sketch( int N, int[N] A, int x, int y ){
  generator int F(){
    return {| A[x] | x | y |};
  }
  if(x<N){
    assert rec(F) == (A[x]+y)*x;
  }
}

高阶表达式还能用来描述想得到的代码的模式（pattern），如下面的例子可以表示想要得到有重复结构的代码。

generator void rep(int n, fun f){
  if(n>0){
    f();
    rep(n-1, f);
  }
}

4.5. repeat construct

上面rep生成器可以表示代码中重复的模式，这种需求实际上非常普遍，因此Sketch提供了专门的实现该功能的结构

repeat(N){
  stmt
}

这种结构其实也是个语法糖，就是对应上面的rep递归生成器。一个主要区别就是，如果使用系统定义的，则重复次数受到bnd-unroll-amnt限制，如果自己写的话，展开次数受到bnd-inline-amnt限制。如果N不是常数或者未知的常数，那么该结构的结果会变成一系列嵌套的if语句。（此处存疑）

上面的结构还有一种简单的变体

repeat( i : N ){
  stmt
}

上面的i是个自动声明的新的整型变量，能够用在stmt中来跟踪当前正在执行的是第几次重复，第n次重复则i=n。举例如下：

generator int add([int n, int k], int[n] A, int idx, int[k] offst){
int res = 0;
  repeat(i: k){
    res += A[idx + offst[i]];
  }
  return res;
}
int[n] combine([int n], int[n] A){
  int[n] B;
  for(int i=1; i<n-1; ++i){
    int[3] offsts = {??-1, ??-1, ??-1};
    B[i] = add(A, i, offsts);
  }
  return B;
}
harness void main(){
  assert combine({2, 4, 5}) == {0, 11, 0};
}

上面??后面的-1是必须的，因为??只能表示非负整数。上面的代码输出如下：

void combine (int n, int[n] A, ref int[n] _out)
{
  _out = ((int[n])0);
  for(int i = 1; i < (n - 1); i = i + 1)
  {
    int _out_s3 = A[i];
    _out_s3 = _out_s3 + (A[i + -1]);
    _out_s3 = _out_s3 + (A[i + 1]);
    _out[i] = _out_s3;
  }
  return;
}

在上面的输出中，重复结构被展开成三个单独的语句，从A中读取数据，累加到输出变量。编译器知道累加第一个前，变量中为0,因此简化为了定义变量并初始化。

5. Regression tests and Benchmark Suite

Sketch软件包含了回归测试集，其中有许多极端的测试用例，如果需要对编译器修改的话，这些测试用例还是很重要的。如果使用的mercurial版本，测试用例在src/test/sk/seq，如果使用的easy-to-install版本，则位于test/sk/seq。安装了Sketch之后，可以使用make或者make long来进行测试。区别是make只是运行测试程序，确保合成器不会崩溃；而make long则运行所有的测试用例后，生成代码，并随机生成输入测试生成的代码是否正确。
软件还包含了一个基准工具，可以用来评价自己写的新的合成算法并和标准合成算法比较。在release_benchmarks（或者src/release_benchmarks）目录下运行bash perftest.sh OUTDIR，OUTDIR是日志文件（logs）保存位置。全部基准测试一遍大概需要一天，因为一个测试用例会跑15遍来计算统计结果，这个可以脚本在脚本里修改。测试开始后即可使用下面命令查看相关的统计数据。

cat OUTDIR/* | awk -f …/scripts/stats.awk

6. Advanced Usage and Diagnostics

6.1. Interpreting Synthesizer Output

使用参数 -V n 来指定合成器输出的详细程度，用以排查错误或者了解一个程序为什么会跑了那么久。
关于Sketch的运行，首先是先猜一个值，然后验证。如果验证错误，程序会生成一个反例，然后搜索该满足该反例的解，继续验证，重复此过程。-V 5就能看到这些推理和验证的步骤。合成器会在验证的开始和结束分别输出BEG CHECK和END CHECK，会在归纳推理阶段的开始和结束输出BEG FIND和END FIND。如果程序卡在某个地方，根据输出可以判断是卡在推理阶段还是验证阶段，因为推理和验证有不同的加速策略，所以知道这一点很重要。
如果合成器告诉你程序无解，可以通过指定–debug-cex参数输出在验证不同解时生成的反例。通常这些反例会提供一些没被考虑到的导致程序无解的极端情况。
Flag -V 输出的详细程度0-15，数字越大输出越多
Flag --debug-cex 输出反例，-V最少为3

6.2. Parallel Solving

并行时，Sketch会启动多个线程同时运行。每个线程使用随机（stochastic）和符号（suybolic）的组合搜索解。并不是所有问题并行时都会加速，但是如果并行可以加速的话，那一般提升会很大。
通常，并行只加速推理阶段，如果要求解的问题主要在验证阶段耗费的时间较长，那么并行就不会起到什么加速作用。相似的，如果程序中使用了较多的minimize，那么并行也不会加速很多。

6.3. Performance diagnostics

下面列举一些导致程序运行时间较长和内存耗尽的情况，以及如何检查程序是否出了这样的问题。
Too much inlining/unrolling 循环和内联函数都会展开，如果嵌套层数较多，即使限制了展开上限也会需要非常多的资源。-V > 12时，可以看到一些如下格式的输出：
CREATING funName
size = N
after ba size = N
每个这样的输出对应一个函数。N表示该函数中的操作数量，如果N很多，那么这个函数内部要么有个很大的生成器，要么有很多循环。
当后端读取了所有函数，就会开始内联，内联的输出如下：
Inlining functions in the sketch.
inlined n1 new size = s1
inlined n2 new size = s2
…
这些输出表示合成器有多少函数正在内联，以及随着内联的展开，程序在内部的表示所占用的空间的增长。如果增长的太大，如 >200K，则表示有太多的内联了。这种问题可以通过减小–bnd-inline-amnt，或者并行（parallelism）来解决。

Recursive generators are too large or have too much recursion 不同于递归函数的后端内联，递归生成器在前端内联。内联过多也有可能是由递归生成器造成的。递归生成器内联过多时，会同时导致未知量变多，表现如下：
control_ints = N1 control_bits = N2
inputSize = Nin ctrlSize = Nctrl
其中，Nin和Nctrl分别表示输入和未知量的总位数。如果Nctrl增长到几千，那可能就是生成器内联太多了。可以参考第四章的例子优化生成器。另外，并行可以加速生成器的选择太多的问题。

The range of some intermediate values is growing too large 中间变量的范围太大。通常Sketch使用的内部表示（representation）随着中间变量的最大值线性增长。在某些情况下，这会导致问题变得太大，内存不够用。在每个推理阶段，都会输出下面信息：
* TIME TO ADD INPUT : XX ms
如果这个数字超过了几百毫秒或者在每轮求解时内存消耗剧增，说明中间变量太大了，–bnd-int-range参数可以对计算中的输入数据强加一个最大值限制。

harness void main(int x){
  x = x * ??;
  if(x < 10){
    if(??){
      x = x * x;
    }
    if(??){
      x = x * x * x;
    }
    if(??){
      x = x * x * x;
    }
  }
  assert x < 100;
}

例如上面的例子，如果输入和未知量均为5位，那么上面的程序基本确定会耗尽内存。即使x最大为32，但在符号表示中，x能大到2^180（此处存疑）。但实际上，根据下面的assert，x是不可能超过100的。此时使用–bnd-int-range 100（推荐留有余量，如110）可以将x限制在100以内，此时很快就会得到解。

在某些情况中，因为最大值本来就很大，即使使用–bnd-int-range也很大。此时，可以使用–slv-nativeints参数，该参数将使用另一种专门为大数定制的求解方式，可能比默认的求解方式慢一点。如果在输入的范围内，给定输入的程序中的整数范围大约大于500时，那么使用此参数，可能会加速。

Flag --bnd-int-range 程序中整数绝对值的最大值。默认为MAX_INT，但是一般不会达不到最大值就会出现其它问题的。

Flag --slv-nativeints 用另一种更节约内存的方式取代标准求解方式，对大数更友好。

The problem is too hard to verify Sketch在推理和验证中迭代，有时会遇到合成器很简单的找到正确解，但是却难以验证，即使限制输入范围。使用参数–slv-lightverif 以尽力验证。如果在一定时间内没有找到反例，则默认正确。
另一种选择是使用更小的输入，–bnd-inbits或者–bnd-arr-size。如果小的输入不足以验证正确性，可以将小数和大数分成两个harness，一个检查所有的小数，另一个显式指定一些大数输入，如下：

int foo(int x){
  x = x + ??;
  while({| x (> | >=) 1000 |} ){
    x = {| x (- | + ) 1000 |};
  }
  return x;
}
harness void main(int x){
  assert ((x + 5) % 1000) == foo(x);
}

使用上面的例子，输入的x应保证最小10位。如果输入位数不够大，也可以选择自己挑选一些大数，用类似下面的例子的方式构造。此时如果–bnd-inbits为5,那么main的x为[0,31]，而largeVal的范围为[1090,1121]。这种方式也可能会漏掉一些对于正确与否十分关键的输入。

harness void largeVal(int x){
  main(1090 + x);
}

对于包含数组的，Sketch会检查数组所有元素的所有可能值。有时这可能不必要，使用参数–slv-sparsearray x，只验证稀疏数组，也就是大部分为0的数组。x=0.05表示对于长度1000的数组，最多5个非0元素。

最后，Sketch中的验证器（checker）会采用随机测试和符号验证的组合来检查错误。如果使用参数–slv-lightverif降低符号验证的有效性，那么可以通过参数–slv-simiters N来增加随即测试的力度，N默认为3，最大150。当进行随机测试时，会周期性的通过学习来简化验证过程，N越大，简化程度可能越高，因此，N够大时，简化到一定程度，可能完全不需要使用–slv-lightverif参数。

6.4. Custom Code Generators

有时候可能不需要C代码，可以自定义代码生成器，在Sketch编译器的最后代码生成时调用。

自定义代码生成器，必须实现FEVisitor接口（包sketch.compiler.ast.core中），并且有编译器可以用来实例化的默认的构造器，同时需要使用@CodeGenerator注释。然后使用参数–fe-custom-codegen指定自定义的代码生成器的jar文件（包含代码生成器和所有用到的类）。
Flag --fe-custom-codegen 指定自定义代码生成器的jar文件名，替换编译器自带的代码生成。

关于如何自定义代码生成器，在sketch-frontend/customcodegen目录下，包含了一个名为CSP的自定义代码生成器的示例。CSP将排版后输出到终端。通过以下步骤使用CSP：

• 在sketch-frontend目录下，编译javac -cp sketch-1.7.5-noarch.jar customcodegen/SCP.java
• 创建jar包：jar -cvf customcodegen.jar customcodegen/
• 使用CSP：sketch --fe-custom-codegen customcodegen.jar test/sk/seq/miniTest1.sk

运行成功后会输出以下信息：
Class customcodegen.SCP is a code generator.
Generating code with customcodegen.SCP
(followed by the pretty-printed version of your code).

6.5. Temporary Files and Frontend Backend Communication

前端通过临时文件和求解器通讯，文件以要求解的文件命名，保存在临时目录，用完即删。因此，如果在一个文件（或两个同名文件）上同时运行两个sketch实例，临时文件可能会冲突，导致编译失败。可以使用以下参数解决。
Flag --fe-output 指定临时文件的输出目录
其它关于临时文件的参数：
Flag --fe-keep-tmp 临时文件不删除
Flag --debug-fake-solver 不运行后端求解，直接使用上次运行的结果（可能会有错误）。（此处存疑）

6.6. Extracting the intermediate representation

Flag --debug-output-dag 加上一个文件名来保存中间表示。该表示的格式可以轻易转换为其他求解器的格式，可以用以比较求解性能。

（略）Figure 1: Format for intermediate representation.

7. Standard Library

7.1. Package math

math包含了标准的数学函数，这些函数对浮点数的编码有特定要求，使用math包会默认指定参数–fe-fpencoding TO_BACKEND。
这些函数看似未解释的函数，实际上后端能理解他们的语义。
包名：math.skh
函数：

• uninterp float sin (float v)/math.skh:15/
• uninterp float cos (float v)/math.skh:17/
• uninterp float tan (float v)/math.skh:19/
• uninterp float sqrt (float v)/math.skh:21/
• float abs (float v)/math.skh:23/
• uninterp float log (float v)/math.skh:28/
• uninterp float arctan (float v)/math.skh:33/
• uninterp float _cast_int_float (int v)/math.skh:40/
• generator double _cast_int_double (int v)/math.skh:46/
• generator float Pi ()/math.skh:51/

7.2. Package generics

包含了常用生成器函数，会在调用处内联。
包名：generics.skh
函数：

• generator T[n] map ([int n], T[n] in, fun f)/generics.skh:17/
  标准的map函数，将函数f应用到数组中的每个元素，产生新的数组。f的参数默认为T->T
• generator int len ([int n], T[n] ar)/generics.skh:29/
  返回数组长度
• generator void foreach ([int n], ref T[n] in, fun f)/generics.skh:38/
  与map语义相同，但是f的参数为T->Avoid
• generator void forall (int a, int b, fun f)/generics.skh:49/
  把一个函数应用到a和b之间的所有整数，f的参数int->void

7.3. Package generators

算数运算的生成函数。
包名：generators.skh
函数：

• generator int linexp ([int N], int[N] vals)/generators.skh:19/
  生成系数在-2到(2^cbits-2)之间的线性表达式
• generator int plinexp ([int N], int[N] vals)/generators.skh:35/
  生成系数在0到2^cbits之间的线性表达式
• generator int expr ([int N, int T], int[N] pars, int[T] ops)/generators.skh:51/
  生成包含N个操作数和T个运算符的整型表达式
• generator int exprG ([int T], fun chose, int[T] ops)/generators.skh:68/
  生成基于一个选择生成函数和T个运算符的整型表达式。选择函数chose应该有一个引用的整型参数表示要选择的ID。这样可以避免对称性。
• generator int expr_cost ([int N, int T], int[N] pars, int[T] ops, ref int cost)/generators.skh:83/
  生成包含N个操作数和T个运算符的表达式。引用参数cost跟表达式的长度成正比
• generator int expr_noc_cost ([int N], int[N] pars, int T, int[T] ops, ref int cost)/generators.skh:98/
  生成包含N个操作数和T个运算符的表达式
• generator bit exprBool ([int N, int T], int[N] pars, int[T] ops)/generators.skh:117/
  生成包含N个操作数和T个运算符的布尔表达式。运算符是算数表达式，布尔表达式通过算数表达式的不等比较组合生成。
• generator bit exprBoolG ([int T], fun choices, int[T] ops)/generators.skh:126/

7.4. Package array

包含定长和变长的数组。使用该包的函数可以使得数组长度不再是类型的一部分。
包名：array.skh
结构：
Structure SArray 固定长度（static sized）数组。包含了数组长度信息。

struct SArray<T> {
  int n;
  T[n] val;
}

Structure Array 长度变便数组，类似C++的vector。

struct Array<T> {
  SArray<T> inner;
  int sz;
}

函数：

• Array newArray ()/array.skh:33/
  创建长度为0的新数组
• T last (Array in)/array.skh:40/
  返回数组最后一个元素
• void add (Array in, T val)/array.skh:48/
  在数组最后添加一个元素

7.5. Package list

包含了链表类型（ADT）和一些帮助函数
包名：list.skh
结构：基于ADT的链表

struct List<T> {
  @Immutable()
}
struct Cons<T> extends List@list {
  T val;
  List<T> next;
}
struct Nil<T> extends List@list {
}

函数：

• List empty ()/list.skh:20/
  返回空链表
• List single (T x)/list.skh:28/
  创建一个单元素的链表并返回
• T head (List l)/list.skh:35/
  返回链表第一个元素，需要保证链表非空
• List add (List lst, T val)/list.skh:42/
  在链表头添加一个元素

7.6. Package stack

不可更改的通用栈数据类型
包名：stack.skh
结构：Structure Stack，抽象类型，只能通过下面的Empty函数创建

struct Stack<T> {
  @Immutable()
}

函数：

• Stack Empty ()/stack.skh:20/
  创建空的栈
• Stack push (Stack prev, T val)/stack.skh:27/
  入栈，并返回栈
• Stack pop (Stack st)/stack.skh:34/
  出栈，并返回栈
• T peek (Stack st)/stack.skh:42/
  返回栈顶元素

8. Credits

略

9. Glossary of Flags

Sketch参数汇总
–bnd-arr-size
–bnd-bound-mode
–bnd-ctrlbits
–bnd-inbits
–bnd-inline-amnt
–bnd-int-range
–bnd-mbits
–bnd-unroll-amnt
–debug-cex
–debug-fake-solver
–debug-output-dag
–fe-custom-codegen
–fe-fpencoding
–fe-inc
–fe-keep-tmp
–fe-output-code
–fe-output-test
–fe-output
–slv-nativeints
–slv-p-cpus
–slv-parallel
-V