Hello,
I was experimenting with Z3 by using the C API, when I noticed that the generated model did not satisfy the supplied constraints. I have pasted the contents of a C file demonstrating the problem, along with the runtime output, below. Is there a bug somewhere, or do I not understand what Z3 does for model generation?
Is it possible to generate a model which complies with the supplied constraints? If so, how should it be done?
Source Code:
#include <z3.h> int main( int argc, char* argv[] ) { //Setup Z3 Z3_config cfg = Z3_mk_config(); Z3_set_param_value(cfg, "MODEL", "true"); Z3_context ctxt = Z3_mk_context(cfg); Z3_del_config(cfg); //Create symbols and variables Z3_type_ast real = Z3_mk_real_type(ctxt); Z3_symbol symbol_X = Z3_mk_string_symbol(ctxt, "X" ); Z3_symbol symbol_Y = Z3_mk_string_symbol(ctxt, "Y" ); Z3_symbol symbol_a = Z3_mk_string_symbol(ctxt, "a" ); Z3_symbol symbol_b = Z3_mk_string_symbol(ctxt, "b" ); Z3_symbol symbol_c = Z3_mk_string_symbol(ctxt, "c" ); Z3_symbol symbol_d = Z3_mk_string_symbol(ctxt, "d" ); Z3_symbol symbol_t = Z3_mk_string_symbol(ctxt, "t" ); Z3_symbol symbol_u = Z3_mk_string_symbol(ctxt, "u" ); Z3_ast X = Z3_mk_const(ctxt, symbol_X, real); Z3_ast Y = Z3_mk_const(ctxt, symbol_Y, real); Z3_ast a = Z3_mk_const(ctxt, symbol_a, real); Z3_ast b = Z3_mk_const(ctxt, symbol_b, real); Z3_ast c = Z3_mk_const(ctxt, symbol_c, real); Z3_ast d = Z3_mk_const(ctxt, symbol_d, real); Z3_ast t = Z3_mk_const(ctxt, symbol_t, real); Z3_ast u = Z3_mk_const(ctxt, symbol_u, real); //Convenience functions Z3_ast add2(Z3_ast lhs, Z3_ast rhs) { const Z3_ast args[2] = {lhs,rhs}; return Z3_mk_add(ctxt,2,args); } Z3_ast sub2(Z3_ast lhs, Z3_ast rhs) { const Z3_ast args[2] = {lhs,rhs}; return Z3_mk_sub(ctxt,2,args); } Z3_ast mult2(Z3_ast lhs, Z3_ast rhs) { const Z3_ast args[2] = {lhs,rhs}; return Z3_mk_mul(ctxt,2,args); } //Create logic constraints Z3_ast show = NULL; show = Z3_mk_eq(ctxt,add2(t,u),Z3_mk_numeral(ctxt,"1",real)); Z3_assert_cnstr(ctxt,show); printf("%s\r\n",Z3_ast_to_string(ctxt,show)); show = Z3_mk_eq(ctxt,c,t); Z3_assert_cnstr(ctxt,show); printf("%s\r\n",Z3_ast_to_string(ctxt,show)); show = Z3_mk_eq(ctxt,d,u); Z3_assert_cnstr(ctxt,show); printf("%s\r\n",Z3_ast_to_string(ctxt,show)); show = Z3_mk_eq(ctxt,a,u); Z3_assert_cnstr(ctxt,show); printf("%s\r\n",Z3_ast_to_string(ctxt,show)); show = Z3_mk_eq(ctxt,b, sub2(Z3_mk_numeral(ctxt,"0",real),t)); Z3_assert_cnstr(ctxt,show); printf("%s\r\n",Z3_ast_to_string(ctxt,show)); show = Z3_mk_le(ctxt, add2(mult2(X,c),mult2(Y,d)), Z3_mk_numeral(ctxt,"10",real) ); Z3_assert_cnstr(ctxt,show); printf("%s\r\n",Z3_ast_to_string(ctxt,show)); show = Z3_mk_ge(ctxt, add2(mult2(X,c),mult2(Y,d)), Z3_mk_numeral(ctxt,"5",real) ); Z3_assert_cnstr(ctxt,show); printf("%s\r\n",Z3_ast_to_string(ctxt,show)); show = Z3_mk_le(ctxt, add2(mult2(X,a),mult2(Y,b)), Z3_mk_numeral(ctxt,"10",real) ); Z3_assert_cnstr(ctxt,show); printf("%s\r\n",Z3_ast_to_string(ctxt,show)); show=Z3_mk_ge(ctxt, add2(mult2(X,a),mult2(Y,b)), Z3_mk_numeral(ctxt,"5",real) ); Z3_assert_cnstr(ctxt,show); printf("%s\r\n",Z3_ast_to_string(ctxt,show)); //Check and show results Z3_model model; Z3_lbool result = Z3_check_and_get_model(ctxt,&model); printf("\r\nResult=%s\r\n\r\n", result==Z3_L_FALSE?"False": (result==Z3_L_TRUE?"True":"Undefined") ); if( !model ) printf("No model generated.\r\n"); else { printf("%s\r\n",Z3_model_to_string(ctxt,model)); Z3_del_model(model); } Z3_del_context(ctxt); return 0; }
Output:
(= (+ t u) 1)(= c t)(= d u)(= a u)(= b (- 0 t))(<= (+ (* X c) (* Y d)) 10)(>= (+ (* X c) (* Y d)) 5)(<= (+ (* X a) (* Y b)) 10)(>= (+ (* X a) (* Y b)) 5)Result=Truepartitions:*2 {t c b Y X} -> 0:real*3 {u d a} -> 1:real
I expected to see that the constraint "(>= (+ (* X c) (* Y d)) 5)", which should be "(X*c)+(Y*d) >= 5", would evaluate to be true when substituting the results from the model. From the resulting model, "X", "Y", and "c" are all 0, and then "d" is 1. Through substitution, the constraint evaluates to "(0 * 0)+(0 * 1) >= 5", which is false. Is this correct?
The reason for what you are seeing is that Z3 is not a decision procedure for non-linear arithmetic.
Your constraints contain non-linear terms, th terms X*c and Y*d contain multiplication of the uninterpreted constants X, Y, d, and d.
Z3 approximates X*c by treating it as an uninterpreted function applied to arguments X and c.
If you write X*5+Y*3, on the other hand, it is still a linear term. Z3 is complete for inequalities between linear terms.
I ran across what seems to be another implication of this.I modified my example slightly, so that it would logically conjoin the expressions, and then assert the conjoined expression. Checking the results from Z3 results in the value Z3_L_TRUE. Next, I modified the program so that it negated the conjoined equations before asserting it. Checking this negated expression also resulted in the value Z3_L_TRUE.Is this the appropriate behavior, that Z3_L_UNDEF is returned for both for an expression and the negation of that expression?If this is the expected behavior, is there a simple way to detect when conditions resulting in this are occurring, without having to test each expression individually?
What you describe sounds like the following:
Z3 will return Z3_L_TRUE when the constraints you pass are satisfiable.It is possible for a constraint and its negation to be satisfiable.
Example: "x = 1" and "not (x = 1)" is satisfiable. Z3 returns Z3_L_TRUE for both queries.