CODEWITHSUNDEEP
z3
silenceluo
silenceluo

Reputation: 3

Assign value to bool variable in Z3 C api

I am new to Z3.

I define a bool type variable a:
Z3_sort bool_type = Z3_mk_bool_sort(ctx);
Z3_ast a = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "a"), bool_type);

My question is how can I assign different value to a, seems I cannot assign Z3_L_TRUE to it directly.

Any suggestions? Thanks!

Upvotes: 0

Views: 622

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

My first suggestion is to use the C++ API instead of the C API. Using the C API is quite error prone. The distribution comes with examples of using both the C and the C++ API:

https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c

and

https://github.com/Z3Prover/z3/blob/master/examples/c++/example.cpp

You will there see examples of creating logical variables, like you are doing, and adding assertions that constrain logical variables. It is easier to understand logical modeling using the text based API. That is, I suggest you use the SMT-LIB format to model what you intend, and this gives you a way to extrapolate what to do with the programmatic APIs.

Regarding your question: there is no notion of "assignment" in logical modeling. You can assert equalities for sure. Furthermore Z3_L_TRUE is a return code used when you check satisfiability. You can create a logical constant "true" using the method Z3_mk_true.

Upvotes: 2

Related Questions