c - C 中的符号模拟 C++

Question

我想知道是否可以看到 C 程序的循环展开形式。例如我有以下 for 循环

// The following code mimics functionality of a logic circuit whose
//inputs are a,b,c and d
//output f
//At every for loop iteration, fresh values of a,b,c and d are input
//to the code whereas k value is used from the previous iteration.

    bool k = 0;
    bool a,b,c,d;
    bool g,h,n,j,f;

    for(i = 1; i < 100; i++)
    {
    h = !(a | b);  //nor gate
    g =  (b & c);  //and gate
    n = !(c & d);  //nand gate
    f = (k==0) ? h : g;  //mux
    j = n ^ f;    //xor gate
    k = j;
    }

问题是“是否有可能以可读格式查看此程序的循环展开形式”。我很想知道 gcc 编译器如何表达 h99、g99、n99、f99、j99 和 k99(第 99 次循环迭代中 h、g、n、f、j 和 k 的值)是否可以这样做？或者应该如何查看 h99、g99、n99、f99、j99 和 k99 在输入 a99、b99、c99、d99 到 a1、b1、c1 和 d1 方面的表达式？

简而言之，我想在每次迭代“i”时进行符号模拟即，将输出 hi、gi、ni、fi、ji 和 ki 表示为输入 ai、bi、ci、di 到 a1、b1、c1 和 d1。

如果您有任何问题，请告诉我。

Answer 1

您应该考虑在正式的推理工具中编写循环的递归版本，例如 ACL2(搜索 ACL2 以下载它，在 tryacl2.org 上还有一个原始的交互式版本)。然后要求定理证明器为您展开循环，方法是要求它证明函数的调用等于未知的东西和 :expand 提示。类似于以下内容:

(defthm unroll-it
  (equal (my-fun 1 nil nil nil nil nil nil nil nil nil)
         xxx)
  :hints (("Goal" :expand (...some term that you need expanded))))

您可能需要 100 个展开提示，因为默认情况下 ACL2 不打开递归调用。无论如何，如果您真的开始走这条路，您可以联系 acl2-help 列表。有关 ACL2 声誉的声明，请参见维基百科。