linux_kernel-list.h

看linux的代码看到这段利用头文件实现的链表。这段写的确实经典，简洁（但不算易懂）且用到了C语言的一些奇技淫巧（误），跟数据结构书上的比起来不知道要高到哪去（不过其实我也没有很注意看书上的代码就是了）

写了下注释

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
/*-
 * Copyright (c) 2011 Felix Fietkau <nbd@openwrt.org>
 * Copyright (c) 2010 Isilon Systems, Inc.
 * Copyright (c) 2010 iX Systems, Inc.
 * Copyright (c) 2010 Panasas, Inc.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions
 * are met:
 * 1. Redistributions of source code must retain the above copyright
 *    notice unmodified, this list of conditions, and the following
 *    disclaimer.
 * 2. Redistributions in binary form must reproduce the above copyright
 *    notice, this list of conditions and the following disclaimer in the
 *    documentation and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
 * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
 * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
 * IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
 * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
 * NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
 * THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
#ifndef _LINUX_LIST_H_
#define _LINUX_LIST_H_

#include <stddef.h>
#include <stdbool.h>

#define	prefetch(x)

    /*很有趣的一个实现
    __typeof__(((type *) NULL)->member) *__mptr 把mptr初始化为任意结构体的member元素对应类型的指针
    ptr为结构体内某元素的指针
    offsetof(type, member) 返回type结构体的member成员相对type的偏移量
    因此该宏定义作用是传入一个结构体实例的成员指针，返回该结构体的头指针
    */
#ifndef container_of
#define container_of(ptr, type, member)					\
	({								\
		const __typeof__(((type *) NULL)->member) *__mptr = (ptr);	\
		(type *) ((char *) __mptr - offsetof(type, member));	\
	})
#endif

struct list_head {
	struct list_head *next;
	struct list_head *prev;
};

#define LIST_HEAD_INIT(name) { &(name), &(name) }	
           //这里用name的地址初始化prev和next，使name声明后本身是个回环
#undef LIST_HEAD
#define LIST_HEAD(name)	struct list_head name = LIST_HEAD_INIT(name)

static inline void
INIT_LIST_HEAD(struct list_head *list)
{
	list->next = list->prev = list;
}

static inline bool
list_empty(const struct list_head *head)
{
	return (head->next == head);
}

static inline bool
list_is_first(const struct list_head *list,
	      const struct list_head *head)
{
	return list->prev == head;			//如果前一个元素就是链表头
}

static inline bool
list_is_last(const struct list_head *list,
	     const struct list_head *head)
{
	return list->next == head;			//如果后一个元素是链表尾
}

static inline void
_list_del(struct list_head *entry)
{
	entry->next->prev = entry->prev;
	entry->prev->next = entry->next;
}

static inline void
list_del(struct list_head *entry)
{
	_list_del(entry);
	entry->next = entry->prev = NULL;
}					
		//这里没有free操作，说明这些函数不处理内存分配问题

static inline void
_list_add(struct list_head *_new, struct list_head *prev,
    struct list_head *next)
{

	next->prev = _new;
	_new->next = next;
	_new->prev = prev;
	prev->next = _new;
}						//同样没有malloc

static inline void
list_del_init(struct list_head *entry)
{
	_list_del(entry);
	INIT_LIST_HEAD(entry);
}
		/*假设list_head是一个容器（结构体）内的成员
		通过list_entry获取该容器对应实例的头指针
		ptr为指向list_head的指针*/
#define	list_entry(ptr, type, field)	container_of(ptr, type, field)
#define	list_first_entry(ptr, type, field)	list_entry((ptr)->next, type, field)
#define	list_last_entry(ptr, type, field)	list_entry((ptr)->prev, type, field)

#define	list_for_each(p, head)						\
	for (p = (head)->next; p != (head); p = p->next)

#define	list_for_each_safe(p, n, head)					\
	for (p = (head)->next, n = p->next; p != (head); p = n, n = p->next)

#define list_for_each_entry(p, h, field)				\
	for (p = list_first_entry(h, __typeof__(*p), field); &p->field != (h); \
	    p = list_entry(p->field.next, __typeof__(*p), field))
										//h为链表头

#define list_for_each_entry_safe(p, n, h, field)			\
	for (p = list_first_entry(h, __typeof__(*p), field),		\
	    n = list_entry(p->field.next, __typeof__(*p), field); &p->field != (h);\
	    p = n, n = list_entry(n->field.next, __typeof__(*n), field))

#define	list_for_each_entry_reverse(p, h, field)			\
	for (p = list_last_entry(h, __typeof__(*p), field); &p->field != (h); \
	    p = list_entry(p->field.prev, __typeof__(*p), field))

#define	list_for_each_prev(p, h) for (p = (h)->prev; p != (h); p = p->prev)
#define	list_for_each_prev_safe(p, n, h) for (p = (h)->prev, n = p->prev; p != (h); p = n, n = p->prev)

static inline void
list_add(struct list_head *_new, struct list_head *head)
{
	_list_add(_new, head, head->next);
            //这里的第三个参数结合list_init构造了一个循环链表
}

static inline void
list_add_tail(struct list_head *_new, struct list_head *head)
{
	_list_add(_new, head->prev, head);
}

static inline void
list_move(struct list_head *list, struct list_head *head)
{
	_list_del(list);
	list_add(list, head);
}

static inline void
list_move_tail(struct list_head *entry, struct list_head *head)
{
	_list_del(entry);
	list_add_tail(entry, head);
}

static inline void
_list_splice(const struct list_head *list, struct list_head *prev,
    struct list_head *next)
{
	struct list_head *first;
	struct list_head *last;

	if (list_empty(list))
		return;

	first = list->next;
	last = list->prev;
	first->prev = prev;
	prev->next = first;
	last->next = next;
	next->prev = last;
}	
		//将头为prev尾为next（其实头尾一样）的链表拼接到list链表内，注意拼接后list不再是链表头

static inline void
list_splice(const struct list_head *list, struct list_head *head)
{
	_list_splice(list, head, head->next);
}
										//list为待插入链表
static inline void
list_splice_tail(struct list_head *list, struct list_head *head)
{
	_list_splice(list, head->prev, head);
}

static inline void
list_splice_init(struct list_head *list, struct list_head *head)
{
	_list_splice(list, head, head->next);
	INIT_LIST_HEAD(list);
}

static inline void
list_splice_tail_init(struct list_head *list, struct list_head *head)
{
	_list_splice(list, head->prev, head);
	INIT_LIST_HEAD(list);
}
					//插入list后将list头指针初始化
#endif /* _LINUX_LIST_H_ */

函数功能总结

结构体

list_head 双向循环链表

宏

container_of( 指针,成员类型,成员名 ) 传入结构体某个成员的指针返回结构体头指针

函数

INIT_LIST_HEAD 初始化链表

list_empty 判断列表是否为空

list_is_first 判断当前元素是否为第一个

list_is_last 判断当前元素是否为最后一个

===================================

_list_del 删除元素通用实现

list_del 删除head指向元素

_list_add 添加元素通用实现

list_add 头插法，在链表头添加一个元素

list_add_tail 尾插法，链表尾添加一个元素

list_del_init 删除并初始化

list_move 移动list元素到链表头

list_move_tail 移动list到链表尾

===================================

list_entry 获取list_head所在容器的头指针

list_first_entry 上一个容器的头指针

list_last_entry 下一个容器的头指针

===================================

list_for_each

list_for_each_safe 向后遍历链表

list_for_each_prev

list_for_each_prev_safe 向前遍历链表

list_for_each_entry

list_for_each_entry_safe 遍历容器中的链表，p指向容器头

list_for_each_entry_reverse 反向遍历

===================================

_list_splice 链表拼接通用实现

list_splice 头插法将list插入head链表

list_splice_tail 尾插法

list_splice_init

list_splice_tail_init 插入后初始化

===================================

一个对于CONTAINER_OF和LIST_ENTRY解释得不错的链接

https://blog.csdn.net/hs794502825/article/details/10364977

几个比较有意思的宏

offsetof

出处：openwrt/libubox/list.h

1
#define offsetof(s,m)  (size_t)&(((s *)0)->m)

这个宏的作用是求结构体的一个成员相对结构体首地址的偏移量

1
((s *)0)->m

跟

1
((s *)NULL)->m

等价，这里做了件事，就是将数字0（NULL）强制转换成一个地址，使它的类型为指向结构体的指针s*
因此如果调用 offsetof(A,pointer)实际上调用了

1
(size_t) &((A *)NULL)->pointer

假设pointer成员相对A类型头指针的偏移量为n，那么上述运算的结果即为n
因为 &((A)NULL) 值为0，所以 &(((A )NULL)->pointer)值为n
这里注意符号&，原因我就不多说了

container_of

出处：openwrt/libubox/list.h

1
2
3
4
5
#define container_of(ptr, type, member)					\
({								\
	const __typeof__(((type *) NULL)->member) *__mptr = (ptr);	\
	(type *) ((char *) __mptr - offsetof(type, member));	\
})

这个宏用处在于假设定义了一个结构体

1
2
3
4
typedef struct mystruct{
    int num;
    list_head pointer;
} A;

这里list_head是双向链表的指针，定义如下

1
2
3
4
typedef struct _list_head{
	struct *list_head prev;
	struct *list_head next;
} list_head;

定义

1
2
A a;
int *p = (int*) &a.pointer.next;    //这里我强制转换成(int*)是省事而已，其实是个不好的做法

此时调用

1
2
void *p = NULL;
p = container_of(p,A,pointer);

会得到指向a的指针，原因如下，把宏展开

1
2
p = ({ const __typeof__( ( (A *)NULL ) ->pointer) *mptr = (p);
       (A*) ( (char*) __mptr - offsetof(A,pointer) ) })

还是有点难懂，拆分一下
第一个问题是，mptr的类型究竟是什么，答案是

1
const __typeof__( ( (A *)NULL ) ->pointer)

再拆分，typeof( ( (A )NULL ) ->pointer)是什么？，其实就是A类型的pointer这个成员的类型，即list_head
typeof是gnu C编译器的一个宏，返回变量的类型
所以mptr的类型是 const list_head
所以这个宏的第一步是

1
const list_head * mptr = (p);

再看第二步

1
(A*) ( (char*) __mptr - offsetof(A,pointer) )

第一步定义的mptr减去mptr指向的成员（在本例中是pointer）相对A结构体首地址的偏移
因此得到的就是该A结构体实例的首地址，即a，这也是为什么第二步的最外层是个(A*)的强制转换

#【翻译+整理】Bit Twiddling Hacks 位操作技巧

原文：http://graphics.stanford.edu/~seander/bithacks.html#OperationCounting

By Sean Eron Andersonseander@cs.stanford.edu

本文中出现的代码片段是公开的（除非有特别标注）——你可以把它们用在任何地方。这些资料是由© 1997-2005 Sean Eron Anderson 搜集整理的。本文给出了代码相应的说明并希望它们对你有所帮助。但本文不对内容提供担保并且不对代码是否适用于一些特定用途提供担保。截止2005.5.5，所有的代码都被完全测试过。上千人阅读了本文。此外，卡耐基梅隆大学计算机系的院长Randal Bryant教授使用它的Uclid代码测试系统测试了几乎所有代码。我也测试了32位机上所有可能的输入。对于第一个发现代码中bug的人，我将支付10美元（通过支票或paypal）（注：译者表示我不背锅（逃）），或是支付20美元用于慈善。

##关于复杂度计算方法

当我们统计算法中共进行了几步操作时，所有C运算符被视为一步操作。所有不需要被写入内存中的中间步骤不计数。当然，这里的计算方法仅用于估算实际的机器指令数量和CPU时间。此外，假设所有的指令执行时间相同，虽然这不符合事实，但CPU的技术将朝这个方向发展。每个系统因为很多细微的差异，因此运行这些代码时的速度都各不相同，如高速缓存大小，内存带宽，指令集等的差异。最后，基准测试是判断一个算法比其他算法高效的最好方法，所以请在目标机器上测试，以确定是否使用下面技巧。

计算整数的符号

####类型定义：

1
2
3
4
int v;      // 我们希望确定v的符号
int sign;   // 结果存在这 

// CHAR_BIT 是一个字节的比特数（一般是8）

####算法1

1
sign = -(v < 0);  // 如果 v < 0 则sign=-1, 否则sign=0.

####算法2

如果希望避免指令执行时发生跳转（如IA32） （注：一般执行 v<0 ,会执行test eax,edx（假设eax和edx分别存放v和0），然后jge或jb）

1
sign = -(int)( (unsigned int)((int)v) >> (sizeof(int) * CHAR_BIT -1) );

####算法3

如果需要更少的指令数（但可移植性差） 

1
sign = v >> ( sizeof(int) * CHAR_BIT -1 );

最后一个表达式对于32位的整数相当于 sign = v >> 31。这明显比第一种要快。

算法4

如果你希望返回值是+1和-1 

1
sign = +1 | (v >> (sizeof(int) * CHAR_BIT - 1));

算法5

或者你希望返回值是+1,0和-1

#####5.1

1
sign = (v != 0) | -(int)((unsigned int)((int)v) >> (sizeof(int) * CHAR_BIT - 1));
5.2

可移植性较差但更快

1
sign = (v != 0) | (v >> (sizeof(int) * CHAR_BIT - 1)); // -1, 0, or +1
5.3

可移植性好且简洁（注：但跳转多）

1
sign = (v > 0) - (v < 0); // -1, 0, or +1

算法6

希望测试一个数是不是非负数，返回+1或0

1
sign = 1 ^ ((unsigned int)v >> (sizeof(int) * CHAR_BIT - 1)); // if v < 0 then 0, else 1

解释

算法3：当有符号整数右移时，当原数为负，最高位（最左一位）填充1，否则填充0。而当数字二进制位为全1时即为-1。不幸的是这个特点与架构有关（不可移植）。

####附注：

2003.3.7，Angus Duggan指出1989年的ANSI C标准没有对有符号数右移的结果给出明确的标准（ implementation-defined），所以在一些系统上这些代码可能不能用 。为了更好的可移植性，Toby Speight在2005.9.28建议加入CHAR_BIT而不是假设每个字节都是8个比特。Angus于2006.3.4推荐了上面这种更具移植性的算法。 Rohit Garg于2009.9.12推荐了判断非负数的算法。

译者注解

算法1不解释，v<0返回的是0或1

算法2和算法3原理类似。注意，算法有个前提就是C编译器对于有符号数位移操作采取算术右移 而非 逻辑右移 对于无符号数相反（附注中说明了这个行为其实取决于编译器）。对于算法2，先将v转换为无符号，之后位移。因为为无符号，因此高位补0，移位后v中只保留了原数的最高位，因为int型为补码存储，最高位为符号位，若原数小于0，则结果为000…001，反之为000…000，因此sign返回-1或0。

算法3因为v为有符号，因此如果符号位为1，右移高位补1，结果为111…111，即补码的-1，反之为000…000

算法4为算法3的结果 或+1，对于-1，-1 | +1 = 111…111 | 000…001 = 111…111 = -1，对于0，为+1

算法5.1和5.2与4原理相同，当v!=0时进行或运算的就是+1，否则为0.

算法5.3，若v>0，则 (v>0)-(v<0) = 1-0=1 若v<0为-1，若v=0为0

算法6改或为异或，当后一个式子为0时，即v>=0时结果为1；后一个式子为1时（注意这里为逻辑右移）结果0。

判断两数符号是否相反

1
2
3
int x, y;               // 待比较的数

bool f = ((x ^ y) < 0); // 如果x和y符号相反则为真

附注：

Manfred Weis于2009.11.26建议加入

译者注解

若x和y符号相反，即符号位不同。此时进行位异或运算，符号位为1，因此运算结果为一负数。

不使用跳转计算一个整数的绝对值

####定义

1
2
3
4
int v;           // 计算v的绝对值
unsigned int r;  // 结果

int const mask = v >> sizeof(int) * CHAR_BIT - 1;//定义一个掩码，值为v算术右移至仅保留最高位

####算法1

1
r = (v + mask) ^ mask;

####算法2 （已被申请专利）

1
r = (v ^ mask) - mask;

####解释：

一些CPU没有取整数绝对值的指令（或者编译器不支持）。在那些跳转开销较大的机器上，上面的程序要比

1
r = (v < 0) ? -(unsigned)v : v;

来的快，即使两者指令数相同。

附注：

2003.3.7，Angus Duggan指出1989年的ANSI C标准没有对有符号数右移的结果给出明确的标准（ implementation-defined），所以在一些系统上这些代码可能不能用 （好像很熟悉？是的跟第一个程序的附注是同样的）。我曾阅读ANSI C，里面并未要求整数必须用补码表示，所以程序也有可能因此不能用 。（在一些很古老的机子里用的可能是反码）。2004.3.14，Keith H. Duggar向我发送了上面提到的专利算法。这是我最早提出的算法

1
r=(+1|(v>>(sizeof(int)*CHAR_BIT-1)))*v

的升级版，因为少用了一个乘法。不幸的是，这个算法于2000.6.6被 Vladimir Yu Volkonsky申请了专利并用到了Sun系统上。2006.8.13，Yuriy Kaminskiy告诉我专利可能是无效的，因为在申请专利之前这个方法就已经被公开发表，比如1996年11月9日Agner Fog的《How to Optimize for the Pentium Processor》（如何为奔腾处理器做优化）。Yuriy还提到这个文档1997年的时候被翻译成了俄文，Vladimir可能读过了。此外，网站时光倒流机器（The Internet Archive）也存在到这里的旧链接。2007.1.30，Peter Kankowski 给作者分享了一个版本的求绝对值，灵感来源于Microsoft’s Visual C++编译器的输出。在这里作为最终解决方案。2007.12.6 Hai Jin抱怨运算的结果是有符号的，所以当计算负数中的最大值时，得到的结果还是负数。2008.4.15 Andrew Shapira指出上述三元运算符的方法可能会出现溢出，因为缺少(unsigned)的类型说明；为了最佳的可移植性，他建议写作： (v < 0) ? (1 + ((unsigned)(-1-v))) : (unsigned)v。2008.7.9 Vincent Lefèvre说服作者删除了它（上述的式）而采用了原来的式（解释中提到的那个式子）。因为即使在非二进制补码的机器上，根据ISO C99规范， -(unsigned)v也是正确的。-(unsigned)v运算时，先通过加2^N转换为无符号数，得到v的补码表示，我们称为U。所以U=v+2^N，又因为

-v=2^N - (v+2^N) = 2^N - U = 0 - U = -U ，所以 -(unsigned)v = -U = -v

译者注解

若v<0，则mask=111…111，算法1=(v-1)^-1 =-v 算法2=(v^-1) +1 = -v

算法1因为v-1除符号位外其余各位都与v相反，又 ^-1相当于按位取反，因此运算完毕后符号位清零，其余各位保留-v的原码。

算法2更直接，就是平时常用的补码和原码转换。

若v>=0，则mask=000…000，算法1= (v+0) ^0 =v 算法2= (v^0) - 0=v

计算两个整数的最大值和最小值（无跳转）

定义

1
2
3
int x;  // 两个整数
int y;   
int r;  // 结果

算法1

1
2
r = y ^ ((x ^ y) & -(x < y)); // min(x, y)
r = x ^ ((x ^ y) & -(x < y)); // max(x, y)

在极少数的机器上，跳转开销很大且没有条件转移指令，上述代码可能比有跳转的实现要快

1
r = (x < y) ? x : y

即使它多使用了两个指令（但一般跳转实现更快）。

解释：

因为若 x<y，-(x<y)为-1（补码为111…111），所以相当于 r= y^( (x^y) & ~0) = y^x^y =x

若x>=y，-(x<y)为0，所以相当于 r=y^( (x^y) & 0) = y^0=y

max同理

####算法2

如果能保证 INT_MIN <= x-y <= INT_MAX，则可以使用下面的代码，因为只用算一次 x-y所以更快

1
2
r = y + ((x - y) & ((x - y) >> (sizeof(int) * CHAR_BIT - 1))); // min(x, y)
r = x - ((x - y) & ((x - y) >> (sizeof(int) * CHAR_BIT - 1))); // max(x, y)

附注

1989 ANSI C没有明确右移行为，所以代码可能无法移植。如果因为溢出抛出异常

Ref：

https://site.douban.com/196781/ God-Mode 豆瓣小站，在该站的奇技淫巧（emmm。。。）条目下有本文大概半篇多的翻译。本人的很多翻译也参考了站内大神的翻译。

emmmm

咕了4个月

终于找到友链为什么炸了

因为。。。我友链文件没按.yml的格式写

: (

其实是因为懒癌晚期

到今天才想着重新搞一下

把之前翻译的z3py发上来

然后开个坑

美滋滋（并不

Z3 API in Python

原文地址：http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examples.htm

Z3是微软研究院开发的一个高效的定理证明器。Z3可以被用于很多场景，例如：软件/硬件测试、约束求解、混合系统分析、安全、生物（药物设计）和几何问题。

这个教程展示了Z3Py的主要功能：python里的Z3 API。阅读此教程不需要Python基础。但学习Python很有用，同时也有很多的Python免费教程供我们学习（https://docs.python.org/3/tutorial/）

Z3同样包含了C、.net和OCaml的API。Z3Py的源代码可以在Z3发行版中看到，你可以按照你的需求进行修改。源代码也展示了如何使用Z3 4.0的新功能。其他酷炫的Z3前端有ScalaZ3和SBV。

###入门

让我们从下面这个例子开始：

1
2
3
x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

函数 Int(‘x’) 定义了一个叫x的Z3整型变量， solve 函数求解这一约束系统。上面的例子用到了两个变量 x 和 y ，还有三个约束。Z3Py和Python一样使用 = 赋值。运算符 <,<=,>,>=,==,!= 用于比较。在上述例子中，表达式 x+2*y==7 是一个Z3约束。Z3可以求解并处理该等式。

下一个例子展示了如何用Z3公式/表达式 simplifier

1
2
3
4
5
x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))

默认情况下，Z3Py（Web版）使用数学记号显示表达式。通常∧是逻辑与，∨是逻辑或。指令

1
set_option(html_mode=False)

使所有公式和表达式以Z3Py的记号显示。这也是Z3发行版的默认模式。

1
2
3
4
5
x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1py

Z3提供拆分表达式的函数

1
2
3
4
5
6
7
8
9
x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name:  ", n.decl().name()

Z3支持所有基础数学运算。Z3Py使用与Python相同的运算优先级。如Python中，**是乘幂。Z3可以求解非线性多项式约束。

1
2
3
x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)

Real(‘x’) 建立一个实变量x。Z3Py可以表示任意大的整数，有理数（如上面例子所示），代数数。代数数是指任何整系数多项式的复根。Z3内部精确的表示了每个数。无理数被显示为十进制使我们较容易读出结果。

1
2
3
4
5
6
7
x = Real('x')
y = Real('y')
solve(x**2 + y**2 == 3, x**3 == 2)

set_option(precision=30)
print "Solving, and displaying result with 30 decimal places"
solve(x**2 + y**2 == 3, x**3 == 2)

set_option 指令用于设置Z3环境。它被用于设置全局属性，如结果如何显示等。指令

1
set_option(precision=30)

设置显示结果时显示的十进制数有几位。数值 1.2599210498? 中的 ? 标记表示输出是被截断的。

下面的例子展示了一个常见的错误。表达式 3/2 是个Python数值但不是Z3中的有理数。这个例子也展示了创建有理数的不同方法。函数 Q(num,den) 创建一个Z3有理数，其中num是分子，den是分母。RealVal(1) 创建一个表示数值1的Z3实数。

1
2
3
4
5
6
7
8
9
print 1/3
print RealVal(1)/3
print Q(1,3)

x = Real('x')
print x + 1/3
print x + Q(1,3)
print x + "1/3"
print x + 0.25

有理数也可以以十进制显示

1
2
3
4
5
6
7
8
x = Real('x')
solve(3*x == 1)

set_option(rational_to_decimal=True)
solve(3*x == 1)

set_option(precision=30)
solve(3*x == 1)

一个约束系统不一定有解，在这种情况下，我们称系统无法满足（unsatisfiable）

1
2
x = Real('x')
solve(x > 4, x < 0)

跟Python一样，单行注释使用 # ，但Z3Py不支持多行注释

1
2
3
# This is a comment
x = Real('x') # comment: creating x
print x**2 + 2*x + 2  # comment: printing polynomial

逻辑运算

Z3支持的逻辑运算符：And,Or,Not,Implies(蕴含),If(if-then-else)。双蕴含用 == 表示。下面的例子展示了如何求解一个布尔约束。

1
2
3
4
p = Bool('p')
q = Bool('q')
r = Bool('r')
solve(Implies(p, q), r == Not(q), Or(Not(p), r))

Python中的布尔常量 True 和 False 可以用于Z3表达式。

1
2
3
4
5
p = Bool('p')
q = Bool('q')
print And(p, q, True)
print simplify(And(p, q, True))
print simplify(And(p, False))

下面的例子同时使用了多项式和布尔表达式约束。

1
2
3
p = Bool('p')
x = Real('x')
solve(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))

求解器

Z3提供了不同的求解器。上述例子中使用的命令 solve 调用了Z3求解器的API。这些调用可以在Z3目录下的 z3.py 中找到。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
x = Int('x')
y = Int('y')

s = Solver()
print s

s.add(x > 10, y == x + 2)
print s
print "Solving constraints in the solver s ..."
print s.check()

print "Create a new scope..."
s.push()
s.add(y < 11)
print s
print "Solving updated set of constraints..."
print s.check()
	
print "Restoring state..."
s.pop()
print s
print "Solving restored set of constraints..."
print s.check()

Solver() 命令定义了一个通用的求解器。所有约束式可以通过 add 方法添加。我们称约束式在求解器中 被声明。check() 方法求解所有已添加进求解器的约束式。如果可以求得解，该方法返回 sat 。如果不能求出解则返回 unsat 。也有可能出现声明的约束式不成立的情况，这时求解器返回 unknown 。

在一些应用下，我们希望求解一些相似的问题，这些问题有部分同样的约束式。我们可以使用 push 和 pop 命令。在Z3中，每个求解器维护一个保存声明的栈， push 命令保存当前栈空间大小，并创建一个空间，压入新的声明。 pop 命令删除上一个 push 命令压入的所有声明。check 方法计算求解器栈内的所有约束式。

下面的展示了一个Z3不能求解的例子。这种情况下求解器返回unknown 。注意Z3可以求解非线性多项式约束，但 2**x 不是多项式。

1
2
3
4
x = Real('x')
s = Solver()
s.add(2**x == 3)
print s.check()

下面的例子展示了如何将声明的约束式传入求解器，以及如何通过check 方法获取求解器状态。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
x = Real('x')
y = Real('y')
s = Solver()
s.add(x > 1, y > 1, Or(x + y > 3, x - y < 2))
print "asserted constraints..."
for c in s.assertions():
    print c

print s.check()
print "statistics for the last check method..."
print s.statistics()
# Traversing statistics
for k, v in s.statistics():
    print "%s : %s" % (k, v)

当求解器找到解时， check 方法返回 sat 。我们称Z3求出满足约束式的解。我们称这个解为所声明的约束式的一个模型。一个模型是指一种解释，能使所有约束式满足。下面的例子展示了查看模型的基本方法。

1
2
3
4
5
6
7
8
9
10
11
x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
print s.check()

m = s.model()
print "x = %s" % m[x]

print "traversing model..."
for d in m.decls():
    print "%s = %s" % (d.name(), m[d])

在上面的例子中，函数 Reals(‘x y z’) 创建了变量 x，y和z。这是下述写法的简写：

1
2
3
x = Real('x')
y = Real('y')
z = Real('z')

表达式 m[x] 模型m中的返回x的值。表达式 “%s = %s” % (d.name(), m[d]) 返回一个字符串，其中第一个%s被d对象的name属性替换，第二个%s被m[d] 的值替换（注：Python语法）。Z3Py会自动地将Z3对象的值全部转换为文本。

计算

Z3支持实型和整型变量。在单个问题中两种变量可以混合使用。与大多数编程语言一样，当我们需要时，Z3Py会自动地将整型表达式强制转换为实型。下面的例子展示了各种声明整型和实型变量的方法。

1
2
3
4
5
6
x = Real('x')
y = Int('y')
a, b, c = Reals('a b c')
s, r = Ints('s r')
print x + y + 1 + (a + s)
print ToReal(y) + c

函数ToReal 将一个整型表达式转换为实型。

Z3Py支持所有的基本的运算符。

1
2
3
4
5
6
a, b, c = Ints('a b c')
d, e = Reals('d e')
solve(a > b + 2,
      a == 2*c + 10,
      c + b <= 1000,
      d >= e)

函数simplify 提供了一些方法，可以对Z3表达式进行简单变换。

1
2
3
4
5
6
7
x, y = Reals('x y')
# Put expression in sum-of-monomials form
t = simplify((x + y)**3, som=True)
print t
# Use power operator
t = simplify(t, mul_to_power=True)
print t

help_simplify 函数打印simplify 函数所有可用的参数。Z3Py允许用户以两种方式写入这些参数。Z3内部的参数名以: 开头并以- 隔开各个单词。这些参数可以被Z3Py使用。Z3Py也提供了一些符合Python变量命名规则的名字，在这里: 被移除，- 被_ 取代。下面的例子展示了怎样使用以这两种方式调用函数。

1
2
3
4
5
6
7
8
x, y = Reals('x y')
# Using Z3 native option names
print simplify(x == y + 2, ':arith-lhs', True)
# Using Z3Py option names
print simplify(x == y + 2, arith_lhs=True)

print "\nAll available options:"
help_simplify()

Z3Py可以支持任意大的数字。下面的例子展示了使用大数，有理数和无理数进行基本运算。无理数中，Z3Py只支持代数数。代数数已经足够表示多项式约束的解了。Z3Py总是以十进制显示无理数，因为这方便阅读。可以使用 sexpr() 方法提取Z3内部的表达式，它能以S-表达式（s-expression）的形式显示Z3内部的数学表达式。

1
2
3
4
5
6
7
8
x, y = Reals('x y')
solve(x + 10000000000000000000000 == y, y > 20000000000000000)

print Sqrt(2) + Sqrt(3)
print simplify(Sqrt(2) + Sqrt(3))
print simplify(Sqrt(2) + Sqrt(3)).sexpr()
# The sexpr() method is available for any Z3 expression
print (x + Sqrt(y) * 2).sexpr()

硬件相关的运算

（注：此处为意译）

现代CPU和主流的编程语言使用基于固定大小的位向量的进行运算（注：如32位CPU采用基于位宽为32的数据进行运算）。在Z3Py中可以以位向量的方式进行这样的运算。位向量使我们可以看到有符号与无符号数的精确的补码表示。

下面的例子展示了如何创建位向量变量和常数。函数 BitVec(‘x’,16) 在Z3中创建了一个16位，名字为 x 的变量。为了方便使用，整数常量可以用于初始化位向量。函数 BitVecVal(10,32) 创建了一个32位的，值为10 的位向量。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
x = BitVec('x', 16)
y = BitVec('y', 16)
print x + 2
# Internal representation
print (x + 2).sexpr()

# -1 is equal to 65535 for 16-bit integers 
print simplify(x + y - 1)

# Creating bit-vector constants
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print simplify(a == b)

a = BitVecVal(-1, 32)
b = BitVecVal(65535, 32)
# -1 is not equal to 65535 for 32-bit integers 
print simplify(a == b)

其他编程语言，如C，C++，C#，Java的有符号与无符号数的各种运算对应的实际操作没有什么区别。但在Z3中，有符号数与无符号数使用不同的运算操作。 <,<=,>,>=,/,%,>> 运算对应有符号数，相对应的无符号数运算符为 ULT,ULE,UGT,UGE,UDiv,URem,LShR 

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)

solve(x + y == 2, x > 0, y > 0)

# Bit-wise operators
# & bit-wise and
# | bit-wise or
# ~ bit-wise not
solve(x & y == ~y)

solve(x < 0)

# using unsigned version of < 
solve(ULT(x, 0))

运算符 >> 是算术右移， << 是算术左移。逻辑右移是 LShR 

1
2
3
4
5
6
7
8
# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)

solve(x >> 2 == 3)

solve(x << 2 == 3)

solve(x << 2 == 24)

函数

不像其他编程语言，函数可以抛出异常或者无法返回。Z3的函数是完全定义的，即，函数是被所有输入的值所定义的，其中输入的值可以是一个函数，如划分函数。Z3是基于一阶逻辑的。

当我们给出约束式，如 x+y>3 时，我们称 x 和 y 是变量。在很多书中，x 和 y 称为未定义常量。即，它们可以被赋值为任何满足约束式 x+y>3 的值。

准确地说，一阶逻辑中的函数和符号常量是未定义的。这与很多其他理论中的函数相反，如算法中的函数 + 拥有标准的定义（将两数相加）。未定义函数和常量可以提供最大限度的灵活性：只要符合约束式，允许对函数和常量做出任何定义。（注：此段感觉翻译有误）

为了解释未定义的函数和常量的含义，我们定义了两个整数常量x和y。然后声明一个未进行定义的函数，这个函数有一个整型参数且返回值为一个整型。这个例子展示了我们可以使嵌套调用两次的f(x)等于x，即f(f(x)) == x

1
2
3
4
x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
solve(f(f(x)) == x, f(x) == y, x != y)

返回的结果为：f函数的定义是：f(0)=1 f(1)=0 f(a)=1 当a≠0,1

（注：这段因为涉及到一阶逻辑的知识翻了好久还是一头雾水，不过看了下代码，这段大概的意思应该就是，Z3的输入可以是一个未定义具体内容的函数，它可以通过与该函数相关的一些约束式来求出符合要求的函数模型）

在Z3中，我们也可以计算在一系列约束式下的一些表达式的值。下面的例子说明了如何使用 evaluate 方法

1
2
3
4
5
6
7
8
9
x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
s = Solver()
s.add(f(f(x)) == x, f(x) == y, x != y)
print s.check()
m = s.model()
print "f(f(x)) =", m.evaluate(f(f(x)))
print "f(x)    =", m.evaluate(f(x))

###可满足性和有效性

当一个约束式/公式 F的值在任何有效取值下始终为真，称该公式为普遍有效公式（即恒真公式）。当约束式在一些取值下为真则称公式为可满足的。验证有效性时，即需要找出命题为永真的证明。验证可满足性则是求出一个满足式子的集合。考虑一个包含 a 和 b 的公式 F 。F 是否普遍有效即是否在 a 和 b 的所有取值下F 都为真。如果F 是有效的，则Not(F) 为永假的，即Not(F) 在任何取值下都不为真，即，Not(F) 是不可满足的。所以公式F 在Not(F) 不可满足时为永真的。 同样，当且仅当 Not(F) 不为永真时，F 是可满足的。下面的例子证明了德摩根定理 。

下面的例子定义了一个Z3Py函数，它接收了一个公式作为参数。这个函数创建一个Z3求解器，并添加了传入参数的公式的非 ，检查这个公式的非是否是不可满足的。下述的函数是Z3Py的命令prove 的简化版。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
p, q = Bools('p q')
demorgan = And(p, q) == Not(Or(Not(p), Not(q)))
print demorgan

def prove(f):
    s = Solver()
    s.add(Not(f))
    if s.check() == unsat:
        print "proved"
    else:
        print "failed to prove"

print "Proving demorgan..."
prove(demorgan)

列表解析式

Python支持列表解析式。列表解析式为创建列表提供了一个简便的方法。它们可以用于创建Z3表达式。下面的例子展示了如何在Z3Py中使用过列表解析式。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
 Create list [1, ..., 5] 
print [ x + 1 for x in range(5) ]

# Create two lists containg 5 integer variables
X = [ Int('x%s' % i) for i in range(5) ]
Y = [ Int('y%s' % i) for i in range(5) ]
print X

# Create a list containing X[i]+Y[i]
X_plus_Y = [ X[i] + Y[i] for i in range(5) ]
print X_plus_Y

# Create a list containing X[i] > Y[i]
X_gt_Y = [ X[i] > Y[i] for i in range(5) ]
print X_gt_Y

print And(X_gt_Y)

# Create a 3x3 "matrix" (list of lists) of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(3) ] 
      for i in range(3) ]
pp(X)

上面的例子中，表达式 “x%s” %i 返回一个由i的值替换%s的字符串。

命令pp 与print 类似，但它使用Z3用于格式化元组和列表的格式化字符串，而不是Python的。

Z3Py也提供创建布尔、整型和实型向量的函数，这些函数可以在列表解析式中被执行。

1
2
3
4
5
6
7
8
X = IntVector('x', 5)
Y = RealVector('y', 5)
P = BoolVector('p', 5)
print X
print Y
print P
print [ y**2 for y in Y ]
print Sum([ y**2 for y in Y ])

（注：下面内容为Z3在一些领域应用的示例）

###运动方程

在高中中，我们学习过运动方程。这些等式描述了位移、时间、加速度、初速度和末速度的关系。在Z3Py中可以表示为：

1
2
d == v_i * t + (a*t**2)/2
v_f == v_i + a*t

例题1

Ima Hurryin以30m/s的速度靠近红绿灯。此时灯变黄，Ima踩下刹车。如果Ima的加速度为-8.00m/s^2，请计算车辆在减速过程中的位移。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
d, a, t, v_i, v_f = Reals('d a t v__i v__f')

equations = [
   d == v_i * t + (a*t**2)/2,
   v_f == v_i + a*t,
]
print "Kinematic equations:"
print equations

# Given v_i, v_f and a, find d
problem = [
    v_i == 30,
    v_f == 0,
    a   == -8
]
print "Problem:"
print problem 

print "Solution:"
solve(equations + problem)

例题2

Ben Rushin在等红绿灯。当灯变绿时，Ben以6.00m/s^2的加速度加速4.10秒。请计算这段时间Ben的位移。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
d, a, t, v_i, v_f = Reals('d a t v__i v__f')

equations = [
   d == v_i * t + (a*t**2)/2,
   v_f == v_i + a*t,
]

# Given v_i, t and a, find d
problem = [
    v_i == 0,
    t   == 4.10,
    a   == 6
]

solve(equations + problem)

# Display rationals in decimal notation
set_option(rational_to_decimal=True)

solve(equations + problem)

###位运算技巧

一些底层的位运算技巧在C程序员中很流行。我们试着用Z3实现其中一些技巧。

2的幂

这个技巧常用于C程序（包括Z3源码）中测试一个整数是否是2的幂。我们可以用Z3证明这个算法的正确性。此处即证明 x != 0 && !(x & (x - 1)) 为真，当且仅当x 为2的幂。

1
2
3
4
5
6
7
8
9
10
x      = BitVec('x', 32)
powers = [ 2**i for i in range(32) ]
fast   = And(x != 0, x & (x - 1) == 0)
slow   = Or([ x == p for p in powers ])
print fast
prove(fast == slow)

print "trying to prove buggy version..."
fast   = x & (x - 1) == 0
prove(fast == slow)

####相反数

下面的技巧用于测试两个数是否互为相反数。

1
2
3
4
5
6
7
8
9
10
11
x      = BitVec('x', 32)
y      = BitVec('y', 32)

# Claim: (x ^ y) < 0 iff x and y have opposite signs
trick  = (x ^ y) < 0

# Naive way to check if x and y have opposite signs
opposite = Or(And(x < 0, y >= 0),
              And(x >= 0, y < 0))

prove(trick == opposite)

数学问题

猫狗和老鼠

我们花费100美元要购买100只动物。每只狗15美元，猫1美元，老鼠25美分。且必须每种至少买一只，求购买方案。

1
2
3
4
5
6
7
8
9
10
11
12
# Create 3 integer variables
dog, cat, mouse = Ints('dog cat mouse')
solve(dog >= 1,   # at least one dog
      cat >= 1,   # at least one cat
      mouse >= 1, # at least one mouse
      # we want to buy 100 animals
      dog + cat + mouse == 100,  
      # We have 100 dollars (10000 cents):
      #   dogs cost 15 dollars (1500 cents), 
      #   cats cost 1 dollar (100 cents), and 
      #   mice cost 25 cents 
      1500 * dog + 100 * cat + 25 * mouse == 10000)

数独

下面的例子展示了如何用Z3求解数独问题。其中instance 定义了数独矩阵。这个例子大量使用了Python中的列表解析式。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ] 
      for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9) 
             for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ Distinct([ X[i][j] for i in range(9) ]) 
             for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j] 
                        for i in range(3) for j in range(3) ]) 
             for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,9,4,0,3,0),
            (0,0,0,5,1,0,0,0,7),
            (0,8,9,0,0,0,0,4,0),
            (0,0,0,0,0,0,2,0,8),
            (0,6,0,2,0,1,0,5,0),
            (1,0,2,0,0,0,0,0,0),
            (0,7,0,0,0,0,5,2,0),
            (9,0,0,0,6,5,0,0,0),
            (0,4,0,9,7,0,0,0,0))

instance_c = [ If(instance[i][j] == 0, 
                  True, 
                  X[i][j] == instance[i][j]) 
               for i in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
    m = s.model()
    r = [ [ m.evaluate(X[i][j]) for j in range(9) ] 
          for i in range(9) ]
    print_matrix(r)
else:
    print "failed to solve"

八皇后问题

八皇后问题：在8×8格的国际象棋上摆放八个皇后，使其不能互相攻击。即任意两个皇后都不能处于同一行、同一列或同一斜线上的摆法。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
Q = [ Int('Q_%i' % (i + 1)) for i in range(8) ]

# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Q[i], Q[i] <= 8) for i in range(8) ]

# At most one queen per column
col_c = [ Distinct(Q) ]

# Diagonal constraint
diag_c = [ If(i == j, 
              True, 
              And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i)) 
           for i in range(8) for j in range(i) ]

solve(val_c + col_c + diag_c)

应用：解决安装问题

常常用软件的安装问题通常是因为无法在系统上安装一组新包。Z3的这个应用适用于使用包管理器的系统。很多包都有其依赖。每个软件的发行版都包含一个meta-data文件用于指明该软件的依赖。meta-data 文件内包含依赖包的名字、版本等。更重要的是，它指明了软件的依赖包和有冲突的包。系统中不能安装那些有冲突的包。

Z3可以方便地解决安装问题。思路就是给每个包定义一个布尔变量。如果这个包必须被安装，则值为True。如果a包依赖于b，c和z，我们可以写为：

1
DependsOn(a, [b, c, z])

DependsOn 用于获取依赖包的条目：

1
2
def DependsOn(pack, deps):
   return And([ Implies(pack, dep) for dep in deps ])

因此，DependsOn(a, [b, c, z])返回下式的值

1
And(Implies(a, b), Implies(a, c), Implies(a, z))

即，如果用户安装a包，则他们应该安装b，c和z。

如果d包与e包冲突，我们可以写为Conflict(d, e)

其中

1
2
def Conflict(p1, p2):
    return Or(Not(p1), Not(p2))

函数返回表达式 Or(Not(d), Not(e)) 。

通过这两个函数，我们可以把该问题描述为：

1
2
3
4
5
6
7
8
9
10
11
12
13
def DependsOn(pack, deps):
    return And([ Implies(pack, dep) for dep in deps ])

def Conflict(p1, p2):
    return Or(Not(p1), Not(p2))

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')

solve(DependsOn(a, [b, c, z]),
      DependsOn(b, [d]),
      DependsOn(c, [Or(d, e), Or(f, g)]),
      Conflict(d, e),
      a, z)

注意这个例子隐含了约束

1
DependsOn(c, [Or(d, e), Or(f, g)])

意思就是要安装c，必须安装d或e，和f或g。

现在，我们优化一下上面的代码。首先我们定义了DependsOn ，可以通过DependsOn(b, d) 调用。我们还定义了 install_check ，用于返回必须在系统上安装的包的列表，即计算的结果。函数Conflict 用于检测冲突，可以接收多个参数。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
def DependsOn(pack, deps):
    if is_expr(deps):
        return Implies(pack, deps)
    else:
        return And([ Implies(pack, dep) for dep in deps ])

def Conflict(*packs):
    return Or([ Not(pack) for pack in packs ])

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')

def install_check(*problem):
    s = Solver()
    s.add(*problem)
    if s.check() == sat:
        m = s.model()
        r = []
        for x in m:
            if is_true(m[x]):
                # x is a Z3 declaration
                # x() returns the Z3 expression
                # x.name() returns a string
                r.append(x())
        print r
    else:
        print "invalid installation profile"

print "Check 1"
install_check(DependsOn(a, [b, c, z]),
              DependsOn(b, d),
              DependsOn(c, [Or(d, e), Or(f, g)]),
              Conflict(d, e),
              Conflict(d, g),
              a, z)

print "Check 2"
install_check(DependsOn(a, [b, c, z]),
              DependsOn(b, d),
              DependsOn(c, [Or(d, e), Or(f, g)]),
              Conflict(d, e),
              Conflict(d, g),
              a, z, g)

在本地使用Z3Py

Z3Py是Z3发行版的一部分。在z3文件夹中python 子目录。为了在本地使用，必须在Python脚本中声明

from Z3 import *

z3 python的目录必须在环境变量PYTHONPATH 中。Z3Py会自动地搜索Z3运行库（z3.dll（WIN），libz3.so（Linux）或libz3.dylib（OSX））。你也可以使用下述命令手动初始化Z3Py：

1
init("z3.dll")

ref:

原文：http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/guide-examples.htm

ScalaZ3：http://lara.epfl.ch/~psuter/ScalaZ3/

SBV：http://hackage.haskell.org/package/sbv

README

##HEY GUYS

##Welcome To My Blog

##I Share And Record My Notes Here

##You Can Download or Repaint Everything on This Blog

##And Please Annotate The Author When You Repaint My Blog

##Have Fun Guys

emmm

好像配友链配爆炸了呢。。。

编码炸了= =
辣鸡win
总不用utf-8

啊。。。今天不想配了