关于SV产生约束的问题

静心聆听

目前遇到这样一个约束：两个动态数组A[]，B[]，A.size == B.size；他们构成链表，A中的是数据，B中的是索引，B中FF表示结束。例如
序号      A            B
  0        0x11       3
  1        0x22       4
  2        0x33       FF
  3        0x44       1
  4        0x55       2
给出起始索引0，将会依次找出数据 11,44,22,55,33 正常的是这样的，但不知道怎么来做约束，因为大概想了一下可能会出现这种情况：

序号      A            B

  0        0x11       3

  1        0x22       4

  2        0x33       FF

  3        0x44       2

  4        0x55       1

这样的话，给起始索引0：数据流将是：11，44，22，55，22，55，22，55，22......这样就会进入死循环，将会进入死循环，不知道要怎么写约束避免这个问题。

请大神指教一下

A1985

[ 本帖最后由 A1985 于 2019-11-20 23:08 编辑 ]\n\n思路对错自己判断：   
typedef struct node {
                         int data;
                         int cur_ptr;
                         int next_ptr;
                         } node_t;

    node_t A[];
    int B[];

    constraint c_s {
            
           foreach(A[k]) {
           A[k].cur_ptr == k++;
           A[k].next_ptr == B[k];
          }
        foreach(A[k])
                       foreach(A[j])
                          k != j -> { A[k].next_ptr != A[j].cur_ptr;  A[j].next_ptr != A[k].cur_ptr;}  
}
   
B其他数字约束自己加。。。
   

静心聆听

A1985 发表于 2019-11-20 22:55
[ 本帖最后由 A1985 于 2019-11-20 23:08 编辑 ]\n\n思路对错自己判断：   
typedef struct node {
       ...

这个约束好像还是有点问题，会约束失败。因为在
foreach(A[k])
                       foreach(A[j])
                          k != j -> { A[k].next_ptr != A[j].cur_ptr;  A[j].next_ptr != A[k].cur_ptr;}  
对任意一个A的next_ptr都不能与其他A的cur_ptr相等，那就只能与字节的cur_ptr相等，而我之前约束了不允许出现A[k].next_ptr == A[k].cur_ptr，故约束会失败。我改了一下：

foreach(A[k])

                       foreach(A[j])

                          A[k].next_ptr ==  A[j].cur_ptr -> { A[j].next_ptr != A[k].cur_ptr;}  

这样好像就可以了。
但是这样的话，如果B中的索引有重复将会出现：
序号      A       B
  0       0xaa    2
  1       0xbb    3
  2       0xcc    1
  3       0xdd    2
还是会出现循环在里面，所以就直接放弃B中有重复数据的想法，直接使用 unique {B}；使的数据不重复。
最后，谢谢您指点

A1985

静心聆听 发表于 2019-11-21 10:38
这个约束好像还是有点问题，会约束失败。因为在
foreach(A[k])
                       forea ...

foreach(A[k])
                       foreach(A[j])
                          k != j -> { A[k].next_ptr == A[j].cur_ptr -> A[j].next_ptr != A[k].cur_ptr;}  


B约束下就好。

A1985

静心聆听 发表于 2019-11-21 10:38
这个约束好像还是有点问题，会约束失败。因为在
foreach(A[k])
                       forea ...

大概就这样吧。。。