5.3.4 L Atom的约束求解过程
原始的字符串约束被转换为L Atom中的公式,由支持数组约束的约束求解器求解,由于L Atom中包含原子函数,所以需要在约束求解器中增加对于原子函数的处理方法。本节介绍约束求解的过程。
1.总体架构
图5-13 转换之后的约束求解过程
约束求解的整体架构如图5-13所示。转换之后的约束被分为两个部分:下标部分和数组部分。下标部分是一个线性算数表达式集合,包括下标的约束和字符串长度的约束。数组部分是字符串的字符成员的约束。下标部分是约束成立的必要条件,下标的改变会引起字符串的结构发生改变,因此需要先求解下标部分的约束。
下标约束中变量的赋值顺序为表示字符串长度的变量、N 、i和i。这个求解顺序由如下原因决定。
①确定字符串的长度使解的搜索空间变得有限。
②当约束公式中包含N、i和i时,约束公式中包含表示集合的变量,因此是二阶表达式,需要确定集合的数量来将约束公式变换为一阶表达式才能够进一步求解。若对下标变量的赋值导致了矛盾,则进行回溯重新赋值。
本书将对下标变量赋具体值导致的一个约束公式变换为多个约束公式的过程称为“增殖”(propagation),根据被赋值变量的不同可分为对N 的增殖(N-Propagation)和对i的增值(i-Propagation),具体过程如下。(https://www.daowen.com)
当N被赋值为一个具体值V n时,包含s N 的公式增殖为一系列包含s ni的公式,其中ni∈N,i∈[1,V n],ni为新增加的临时变量,这些临时变量受到N的属性N p中Δ和Γ的限制。
当i和i被赋值为具体值V i和 V i时 ,包含的公式增殖为一系列包含s[V i, V i+ 1,…,V i-1,V i]的公式,每一个字符数组成员都是新引入的字符变量,由下一阶段进行求解。在下一节对此过程进行形式化描述。
2.下标约束求解过程的形式化描述
在支持多模型的约束求解(SMT[26])领域中,不同数据模型的约束求解过程以统一的步骤进行描述,称为DPLL(L)形式。本节采用此形式对下标约束的求解过程进行形式化描述,具体规则如图5-14所示。
图5-14 位置约束的求解规则
一个状态包括当前为变量赋的具体值和约束集合,表示为M‖C,其中M表示赋值表,约束C被分为位置约束C p和数组成员约束C a,“∨”表示约束之间的析取。每一个转换规则以横线下方的状态作为输入,在右侧方框中的条件下,转换到横线上方的状态,当一个状态无法应用图中的任何一个规则时,此状态中所有的位置变量都已经有具体值,转到下一步骤进行数组约束的求解过程。对于每个规则的描述如下。
①N-Propagation:当N被赋一个确定值V n时,引入V n个下标变量以及V n个字符数组成员变量s[ni],并且将约束中包含s[N]的表达式增殖为V n个包含s[ni]的表达式,约束nj≤nj+1+Δ来保证下标之间的间隔要大于Δ。
②i-Propagation:与N-Propagation相似,当边界变量i和i确定值之后,每个约束表达式中的
都由一系列从
到
的连续位置的字符成员进行替换。
③位置回溯:若变换之后的约束表达式导致数组模型发生冲突,则意味着为下标变量的赋值存在错误,需要回溯到之前的状态,并且为下标变量记录导致矛盾的约束,以避免生成相同的导致冲突的取值。
