如何使用boolector为我的代码生成模型？

Question

我正在尝试boolector，所以我试图为简单的代码创建模型。假设我有以下伪代码：

int a = 5;
int b = 4;
int c = 3;

对于这组简单的说明，我可以创建模型，并且一切正常。问题是当我之后还有其他说明时，例如

b = 10;
c = 20;

显然，由于同一模块中的b不能等于4和10，因此无法生成模型。一位维护人员建议我使用boolector_push和boolector_pop，以便在需要时创建新的Context。

boolector_push的代码是：

void
boolector_push (Btor *btor, uint32_t level)
{
  BTOR_ABORT_ARG_NULL (btor);
  BTOR_TRAPI ("%u", level);
  BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
              "incremental usage has not been enabled");

  if (level == 0) return;

  uint32_t i;
  for (i = 0; i < level; i++)
  {
    BTOR_PUSH_STACK (btor->assertions_trail,
                     BTOR_COUNT_STACK (btor->assertions));
  }
  btor->num_push_pop++;
}

代替boolector_pop是

void
boolector_pop (Btor *btor, uint32_t level)
{
  BTOR_ABORT_ARG_NULL (btor);
  BTOR_TRAPI ("%u", level);
  BTOR_ABORT (!btor_opt_get (btor, BTOR_OPT_INCREMENTAL),
              "incremental usage has not been enabled");
  BTOR_ABORT (level > BTOR_COUNT_STACK (btor->assertions_trail),
              "can not pop more levels (%u) than created via push (%u).",
              level,
              BTOR_COUNT_STACK (btor->assertions_trail));

  if (level == 0) return;

  uint32_t i, pos;
  BtorNode *cur;

  for (i = 0, pos = 0; i < level; i++)
    pos = BTOR_POP_STACK (btor->assertions_trail);

  while (BTOR_COUNT_STACK (btor->assertions) > pos)
  {
    cur = BTOR_POP_STACK (btor->assertions);
    btor_hashint_table_remove (btor->assertions_cache, btor_node_get_id (cur));
    btor_node_release (btor, cur);
  }
  btor->num_push_pop++;
}

[我认为，这两个函数保持对使用boolector_assert生成的断言的跟踪，因此考虑到约束将相同的情况，如何使用boolector_push和boolector_pop获得最终且正确的模型？

我想念什么？

谢谢

Answer 1

您怀疑，求解器的push和pop方法不是您想要的。相反，您必须将要建模的程序转换为所谓的SSA（静态单一分配）表格。这是关于它的维基百科文章，内容丰富：https://en.wikipedia.org/wiki/Static_single_assignment_form

基本思想是，您将可变变量作为时变值“处理”，并在对它们进行多次分配时为其赋予唯一的名称。因此，以下内容：

a = 5
b = a + 2
c = b + 3
c = c + 1
b = c + 6

成为：

a0 = 5
b0 = a0 + 2
c0 = b0 + 3
c1 = c0 + 1
b1 = c1 + 6

等请注意，条件处理起来很棘手，并且通常需要所谓的phi-nodes。 （即合并分支的值。）大多数编译器会自动为您执行这种转换，因为它可以进行许多优化。您可以手动执行此操作，也可以使用算法为您执行此操作，具体取决于您的特定问题。

这里是关于堆栈溢出的另一个问题，本质上是在要求类似的内容：Z3 Conditional Statement

希望这会有所帮助！