3

我是my_list这样定义的：

struct my_struct {
    comparator[2] : list of int(bits:16);
    something_else[2] : list of uint(bits:16);
};
...
my_list[10] : list of my_struct;

禁止comparators同一索引（0 或 1）在所有列表中相同。当我以这种方式约束它时（例如对于索引 0）：

 keep my_list.all_different(it.comparator[0]);

我得到编译错误：

*** Error: GEN_NO_GENERATABLE_NOTIF: 

    Constraint without any generatable element.
    ... 
    keep my_list.all_different(it.comparator[0]);

我怎样才能生成它们都不同？感谢任何帮助

4

2 回答 2

2

当您引用my_list.comparator它时，它并没有像您认为的那样做。发生的事情是将所有comparator列表连接到一个 20 位元素列表中。通过删除约束并打印它来尝试一下：

extend sys {
  my_list[10] : list of my_struct;

  run() is also {
    print my_list.comparator;
  };
};

在这种情况下，您可以做的是构建自己的comparator[0]元素列表：

extend sys {
  comparators0 : list of int;
  keep comparators0.size() == my_list.size();
  keep for each (comp) in comparators0 {
    comp == my_list.comparator[index * 2];
  };
  keep comparators0.all_different(it);

  // just to make sure that we've sliced the appropriate elements
  run() is also {
    print my_list[0].comparator[0], comparators0[0];
    print my_list[1].comparator[0], comparators0[1];
    print my_list[2].comparator[0], comparators0[2];
  };
};

您可以对这个新列表应用all_different()约束。为了确保它正常工作，添加以下约束应该会导致矛盾：

extend sys {
  // this constraint should cause a contradiction
  keep my_list[0].comparator[0] == my_list[1].comparator[0];
};
于 2014-11-18T13:02:09.327 回答
2

它也可以一次性使用：

keep for each (elem) in my_list {
  elem.comparator[0] not in my_list[0..max(0, index-1)].apply(.comparator[0]);
  elem.comparator[1] not in my_list[0..max(0, index-1)].apply(.comparator[1]);      
};
于 2014-11-19T10:03:17.723 回答