CODEWITHSUNDEEP
z3
Shambo
Shambo

Reputation: 946

Use of context in C++ API

I have the following program , which transforms a string into a Boolean formula (string_to_formula), where I am defining expr_vector b(c). This code works, but I am not being able to reason about the context. What is the function of a context? Is there any way we can define the variable b just once? Why do we need to send the context to the function? And can this code be written in a more succinct way? 

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;
}

Upvotes: 2

Views: 8410

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

The context object is relevant for multi-threaded programs. Each execution thread can have its own context, and they can be accessed without using any form of synchronization (e.g., mutexes). Each expression belongs to a single context. We cannot use the same expression in two different contexts, but we can copy them from one context to another.

In Z3, expressions are maximally shared. For example, if we have an expressions such as (f T T) where T is a big term, then internally Z3 has only one copy of T. For implementing this feature, we use a hashtable. The hashtable is stored in the context. If we use the same context C in two different execution threads, Z3 will probably crash due to race conditions updating C.

If your program has only one execution thread, you can avoid "moving" the context around by having a global variable.

The idea of context/manager is present in many libraries. For example, in CUDD (BDD library), they have a DdManager. In the script language Lua, they have a lua_State. These are all instances of the same idea.

Upvotes: 6

Related Questions