C++ API 中上下文的使用

Question

我有以下程序，它将字符串转换为布尔公式 ( string_to_formula)，我在其中定义expr_vector b(c)。这段代码有效，但我无法推理context. a 的作用是什么context？有什么方法可以b只定义一次变量吗？为什么我们需要将 发送context给函数？这段代码可以写得更简洁吗？

int main() { try {

  context c;
  expr form(c);
  form  = string_to_formula("x1x00xx011",c);
  expr form1(c);
  form1  = string_to_formula("1100x1x0",c);

  solver s(c);
  s.add(form && form1);
  s.check();
  model m = s.get_model();
  cout << m << "\n";
} 

expr string_to_formula(string str, context& c )
{
 expr_vector b(c) ;
 for ( unsigned i = 0; i < str.length(); i++)
 { stringstream b_name;
   b_name << "b_" << i;
   b.push_back(c.bool_const(b_name.str().c_str()));
  }

 expr formula(c);
 formula = c.bool_val(true);
 for( unsigned i = 0 ; i < str.length() ; ++i )
 {  char element = str.at(i) ;
    if ( element == '1' )
       formula = formula && ( b[i] == c.bool_val(true) ) ;
    else if ( element == '0' )
        formula = formula && ( b[i] == c.bool_val(false) ) ;
    else if ( element == 'x' )
        continue;
 }
 return formula;
}

Answer 1

该context对象与多线程程序相关。每个执行线程都可以有自己的上下文，并且可以在不使用任何形式的同步（例如互斥体）的情况下访问它们。每个表达式都属于一个上下文。我们不能在两个不同的上下文中使用相同的表达式，但我们可以将它们从一个上下文复制到另一个上下文。

在Z3中，表达式被最大限度地共享。例如，如果我们有一个表达式，例如(f T T)whereT是一个大项，那么 Z3 内部只有一个 的副本T。为了实现此功能，我们使用哈希表。哈希表存储在context. 如果我们在两个不同的执行线程中使用相同的内容context C，Z3 可能会由于竞争条件更新而崩溃C。

如果您的程序只有一个执行线程，则可以通过使用全局变量来避免“移动”上下文。

上下文/管理器的想法存在于许多库中。例如，在CUDD（BDD 库）中，它们有一个DdManager. 在脚本语言Lua中，他们有一个lua_State. 这些都是同一想法的实例。