mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

re-add model example

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-25 10:48:53 -07:00
parent 2c27056283
commit 7ed32f4315
1 changed files with 194 additions and 173 deletions
Download patch file Download diff file Expand all files Collapse all files

349
examples/c/test_capi.c
View file

@ -2769,72 +2769,72 @@ void fpa_example() {
double_sort = Z3_mk_fpa_sort(ctx, 11, 53); double_sort = Z3_mk_fpa_sort(ctx, 11, 53);
rm_sort = Z3_mk_fpa_rounding_mode_sort(ctx); rm_sort = Z3_mk_fpa_rounding_mode_sort(ctx);
// Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode). // Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode).
s_rm = Z3_mk_string_symbol(ctx, "rm"); s_rm = Z3_mk_string_symbol(ctx, "rm");
rm = Z3_mk_const(ctx, s_rm, rm_sort); rm = Z3_mk_const(ctx, s_rm, rm_sort);
s_x = Z3_mk_string_symbol(ctx, "x"); s_x = Z3_mk_string_symbol(ctx, "x");
s_y = Z3_mk_string_symbol(ctx, "y"); s_y = Z3_mk_string_symbol(ctx, "y");
x = Z3_mk_const(ctx, s_x, double_sort); x = Z3_mk_const(ctx, s_x, double_sort);
y = Z3_mk_const(ctx, s_y, double_sort); y = Z3_mk_const(ctx, s_y, double_sort);
n = Z3_mk_fpa_numeral_double(ctx, 42.0, double_sort); n = Z3_mk_fpa_numeral_double(ctx, 42.0, double_sort);
s_x_plus_y = Z3_mk_string_symbol(ctx, "x_plus_y"); s_x_plus_y = Z3_mk_string_symbol(ctx, "x_plus_y");
x_plus_y = Z3_mk_const(ctx, s_x_plus_y, double_sort); x_plus_y = Z3_mk_const(ctx, s_x_plus_y, double_sort);
c1 = Z3_mk_eq(ctx, x_plus_y, Z3_mk_fpa_add(ctx, rm, x, y)); c1 = Z3_mk_eq(ctx, x_plus_y, Z3_mk_fpa_add(ctx, rm, x, y));
args[0] = c1; args[0] = c1;
args[1] = Z3_mk_eq(ctx, x_plus_y, n); args[1] = Z3_mk_eq(ctx, x_plus_y, n);
c2 = Z3_mk_and(ctx, 2, (Z3_ast*)&args); c2 = Z3_mk_and(ctx, 2, (Z3_ast*)&args);
args2[0] = c2; args2[0] = c2;
args2[1] = Z3_mk_not(ctx, Z3_mk_eq(ctx, rm, Z3_mk_fpa_rtz(ctx))); args2[1] = Z3_mk_not(ctx, Z3_mk_eq(ctx, rm, Z3_mk_fpa_rtz(ctx)));
c3 = Z3_mk_and(ctx, 2, (Z3_ast*)&args2); c3 = Z3_mk_and(ctx, 2, (Z3_ast*)&args2);
and_args[0] = Z3_mk_not(ctx, Z3_mk_fpa_is_zero(ctx, y)); and_args[0] = Z3_mk_not(ctx, Z3_mk_fpa_is_zero(ctx, y));
and_args[1] = Z3_mk_not(ctx, Z3_mk_fpa_is_nan(ctx, y)); and_args[1] = Z3_mk_not(ctx, Z3_mk_fpa_is_nan(ctx, y));
and_args[2] = Z3_mk_not(ctx, Z3_mk_fpa_is_infinite(ctx, y)); and_args[2] = Z3_mk_not(ctx, Z3_mk_fpa_is_infinite(ctx, y));
args3[0] = c3; args3[0] = c3;
args3[1] = Z3_mk_and(ctx, 3, and_args); args3[1] = Z3_mk_and(ctx, 3, and_args);
c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3); c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3);
printf("c4: %s\n", Z3_ast_to_string(ctx, c4)); printf("c4: %s\n", Z3_ast_to_string(ctx, c4));
Z3_solver_push(ctx, s); Z3_solver_push(ctx, s);
Z3_solver_assert(ctx, s, c4); Z3_solver_assert(ctx, s, c4);
check(ctx, s, Z3_L_TRUE); check(ctx, s, Z3_L_TRUE);
Z3_solver_pop(ctx, s, 1); Z3_solver_pop(ctx, s, 1);
// Show that the following are equal: // Show that the following are equal:
// (fp #b0 #b10000000001 #xc000000000000) // (fp #b0 #b10000000001 #xc000000000000)
// ((_ to_fp 11 53) #x401c000000000000)) // ((_ to_fp 11 53) #x401c000000000000))
// ((_ to_fp 11 53) RTZ 1.75 2))) // ((_ to_fp 11 53) RTZ 1.75 2)))
// ((_ to_fp 11 53) RTZ 7.0))) // ((_ to_fp 11 53) RTZ 7.0)))
Z3_solver_push(ctx, s); Z3_solver_push(ctx, s);
c1 = Z3_mk_fpa_fp(ctx, c1 = Z3_mk_fpa_fp(ctx,
Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)), Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)),
Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)), Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)),
Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52))); Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)));
c2 = Z3_mk_fpa_to_fp_bv(ctx, c2 = Z3_mk_fpa_to_fp_bv(ctx,
Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)), Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)),
Z3_mk_fpa_sort(ctx, 11, 53)); Z3_mk_fpa_sort(ctx, 11, 53));
c3 = Z3_mk_fpa_to_fp_int_real(ctx, c3 = Z3_mk_fpa_to_fp_int_real(ctx,
Z3_mk_fpa_rtz(ctx), Z3_mk_fpa_rtz(ctx),
Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)), /* exponent */ Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)), /* exponent */
Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)), /* significand */ Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)), /* significand */
Z3_mk_fpa_sort(ctx, 11, 53)); Z3_mk_fpa_sort(ctx, 11, 53));
c4 = Z3_mk_fpa_to_fp_real(ctx, c4 = Z3_mk_fpa_to_fp_real(ctx,
Z3_mk_fpa_rtz(ctx), Z3_mk_fpa_rtz(ctx),
Z3_mk_numeral(ctx, "7.0", Z3_mk_real_sort(ctx)), Z3_mk_numeral(ctx, "7.0", Z3_mk_real_sort(ctx)),
Z3_mk_fpa_sort(ctx, 11, 53)); Z3_mk_fpa_sort(ctx, 11, 53));
args3[0] = Z3_mk_eq(ctx, c1, c2); args3[0] = Z3_mk_eq(ctx, c1, c2);
args3[1] = Z3_mk_eq(ctx, c1, c3); args3[1] = Z3_mk_eq(ctx, c1, c3);
args3[2] = Z3_mk_eq(ctx, c1, c4); args3[2] = Z3_mk_eq(ctx, c1, c4);
c5 = Z3_mk_and(ctx, 3, args3); c5 = Z3_mk_and(ctx, 3, args3);
printf("c5: %s\n", Z3_ast_to_string(ctx, c5)); printf("c5: %s\n", Z3_ast_to_string(ctx, c5));
Z3_solver_assert(ctx, s, c5); Z3_solver_assert(ctx, s, c5);
check(ctx, s, Z3_L_TRUE); check(ctx, s, Z3_L_TRUE);
Z3_solver_pop(ctx, s, 1); Z3_solver_pop(ctx, s, 1);
del_solver(ctx, s); del_solver(ctx, s);
Z3_del_context(ctx); Z3_del_context(ctx);
@ -2844,52 +2844,67 @@ void fpa_example() {
\brief Demonstrates some basic features of model construction \brief Demonstrates some basic features of model construction
*/ */
#if 0
void mk_model_example() { void mk_model_example() {
Z3_context ctx;
Z3_model m;
Z3_sort intSort;
Z3_symbol aSymbol, bSymbol, cSymbol;
Z3_func_decl aFuncDecl, bFuncDecl, cFuncDecl;
Z3_ast aApp, bApp, cApp;
Z3_sort int2intArraySort;
Z3_ast zeroNumeral, oneNumeral, twoNumeral, threeNumeral, fourNumeral;
Z3_sort arrayDomain[1];
Z3_func_decl cAsFuncDecl;
Z3_func_interp cAsFuncInterp;
Z3_ast_vector zeroArgs;
Z3_ast_vector oneArgs;
Z3_ast cFuncDeclAsArray;
Z3_string modelAsString;
printf("\nmk_model_example\n"); printf("\nmk_model_example\n");
Z3_context ctx = mk_context(); ctx = mk_context();
// Construct empty model // Construct empty model
Z3_model m = Z3_mk_model(ctx); m = Z3_mk_model(ctx);
Z3_model_inc_ref(ctx, m); Z3_model_inc_ref(ctx, m);
// Create constants "a" and "b" // Create constants "a" and "b"
Z3_sort intSort = Z3_mk_int_sort(ctx); intSort = Z3_mk_int_sort(ctx);
Z3_symbol aSymbol = Z3_mk_string_symbol(ctx, "a"); aSymbol = Z3_mk_string_symbol(ctx, "a");
Z3_func_decl aFuncDecl = Z3_mk_func_decl(ctx, aSymbol, aFuncDecl = Z3_mk_func_decl(ctx, aSymbol,
/*domain_size=*/0, /*domain_size=*/0,
/*domain=*/NULL, /*domain=*/NULL,
/*range=*/intSort); /*range=*/intSort);
Z3_ast aApp = Z3_mk_app(ctx, aFuncDecl, aApp = Z3_mk_app(ctx, aFuncDecl,
/*num_args=*/0, /*num_args=*/0,
/*args=*/NULL); /*args=*/NULL);
Z3_symbol bSymbol = Z3_mk_string_symbol(ctx, "b"); bSymbol = Z3_mk_string_symbol(ctx, "b");
Z3_func_decl bFuncDecl = Z3_mk_func_decl(ctx, bSymbol, bFuncDecl = Z3_mk_func_decl(ctx, bSymbol,
/*domain_size=*/0, /*domain_size=*/0,
/*domain=*/NULL, /*domain=*/NULL,
/*range=*/intSort); /*range=*/intSort);
Z3_ast bApp = Z3_mk_app(ctx, bFuncDecl, bApp = Z3_mk_app(ctx, bFuncDecl,
/*num_args=*/0, /*num_args=*/0,
/*args=*/NULL); /*args=*/NULL);
// Create array "c" that maps int to int. // Create array "c" that maps int to int.
Z3_symbol cSymbol = Z3_mk_string_symbol(ctx, "c"); cSymbol = Z3_mk_string_symbol(ctx, "c");
Z3_sort int2intArraySort = Z3_mk_array_sort(ctx, int2intArraySort = Z3_mk_array_sort(ctx,
/*domain=*/intSort, /*domain=*/intSort,
/*range=*/intSort); /*range=*/intSort);
Z3_func_decl cFuncDecl = Z3_mk_func_decl(ctx, cSymbol, cFuncDecl = Z3_mk_func_decl(ctx, cSymbol,
/*domain_size=*/0, /*domain_size=*/0,
/*domain=*/NULL, /*domain=*/NULL,
/*range=*/int2intArraySort); /*range=*/int2intArraySort);
Z3_ast cApp = Z3_mk_app(ctx, cFuncDecl, cApp = Z3_mk_app(ctx, cFuncDecl,
/*num_args=*/0, /*num_args=*/0,
/*args=*/NULL); /*args=*/NULL);
// Create numerals to be used in model // Create numerals to be used in model
Z3_ast zeroNumeral = Z3_mk_int(ctx, 0, intSort); zeroNumeral = Z3_mk_int(ctx, 0, intSort);
Z3_ast oneNumeral = Z3_mk_int(ctx, 1, intSort); oneNumeral = Z3_mk_int(ctx, 1, intSort);
Z3_ast twoNumeral = Z3_mk_int(ctx, 2, intSort); twoNumeral = Z3_mk_int(ctx, 2, intSort);
Z3_ast threeNumeral = Z3_mk_int(ctx, 3, intSort); threeNumeral = Z3_mk_int(ctx, 3, intSort);
Z3_ast fourNumeral = Z3_mk_int(ctx, 4, intSort); fourNumeral = Z3_mk_int(ctx, 4, intSort);
// Add assignments to model // Add assignments to model
// a == 1 // a == 1
@ -2899,25 +2914,25 @@ void mk_model_example() {
// Create a fresh function that represents // Create a fresh function that represents
// reading from array. // reading from array.
Z3_sort arrayDomain[] = {intSort}; arrayDomain[0] = intSort;
Z3_func_decl cAsFuncDecl = Z3_mk_fresh_func_decl(ctx, cAsFuncDecl = Z3_mk_fresh_func_decl(ctx,
/*prefix=*/"", /*prefix=*/"",
/*domain_size*/ 1, /*domain_size*/ 1,
/*domain=*/arrayDomain, /*domain=*/arrayDomain,
/*sort=*/intSort); /*sort=*/intSort);
// Create function interpretation with default // Create function interpretation with default
// value of "0". // value of "0".
Z3_func_interp cAsFuncInterp = cAsFuncInterp =
Z3_add_func_interp(ctx, m, cAsFuncDecl, Z3_add_func_interp(ctx, m, cAsFuncDecl,
/*default_value=*/zeroNumeral); /*default_value=*/zeroNumeral);
Z3_func_interp_inc_ref(ctx, cAsFuncInterp); Z3_func_interp_inc_ref(ctx, cAsFuncInterp);
// Add [0] = 3 // Add [0] = 3
Z3_ast_vector zeroArgs = Z3_mk_ast_vector(ctx); zeroArgs = Z3_mk_ast_vector(ctx);
Z3_ast_vector_inc_ref(ctx, zeroArgs); Z3_ast_vector_inc_ref(ctx, zeroArgs);
Z3_ast_vector_push(ctx, zeroArgs, zeroNumeral); Z3_ast_vector_push(ctx, zeroArgs, zeroNumeral);
Z3_func_interp_add_entry(ctx, cAsFuncInterp, zeroArgs, threeNumeral); Z3_func_interp_add_entry(ctx, cAsFuncInterp, zeroArgs, threeNumeral);
// Add [1] = 4 // Add [1] = 4
Z3_ast_vector oneArgs = Z3_mk_ast_vector(ctx); oneArgs = Z3_mk_ast_vector(ctx);
Z3_ast_vector_inc_ref(ctx, oneArgs); Z3_ast_vector_inc_ref(ctx, oneArgs);
Z3_ast_vector_push(ctx, oneArgs, oneNumeral); Z3_ast_vector_push(ctx, oneArgs, oneNumeral);
Z3_func_interp_add_entry(ctx, cAsFuncInterp, oneArgs, fourNumeral); Z3_func_interp_add_entry(ctx, cAsFuncInterp, oneArgs, fourNumeral);
@ -2925,82 +2940,89 @@ void mk_model_example() {
// Now use the `(_ as_array)` to associate // Now use the `(_ as_array)` to associate
// the `cAsFuncInterp` with the `cFuncDecl` // the `cAsFuncInterp` with the `cFuncDecl`
// in the model // in the model
Z3_ast cFuncDeclAsArray = Z3_mk_as_array(ctx, cAsFuncDecl); cFuncDeclAsArray = Z3_mk_as_array(ctx, cAsFuncDecl);
Z3_add_const_interp(ctx, m, cFuncDecl, cFuncDeclAsArray); Z3_add_const_interp(ctx, m, cFuncDecl, cFuncDeclAsArray);
// Print the model // Print the model
Z3_string modelAsString = Z3_model_to_string(ctx, m); modelAsString = Z3_model_to_string(ctx, m);
printf("Model:\n%s\n", modelAsString); printf("Model:\n%s\n", modelAsString);
// Check the interpretations we expect to be present // Check the interpretations we expect to be present
// are. // are.
Z3_func_decl expectedInterpretations[] = {aFuncDecl, bFuncDecl, cFuncDecl}; {
for (int index = 0; Z3_func_decl expectedInterpretations[] = {aFuncDecl, bFuncDecl, cFuncDecl};
index < sizeof(expectedInterpretations) / sizeof(Z3_func_decl); for (int index = 0;
++index) { index < sizeof(expectedInterpretations) / sizeof(Z3_func_decl);
Z3_func_decl d = expectedInterpretations[index]; ++index) {
if (Z3_model_has_interp(ctx, m, d)) { Z3_func_decl d = expectedInterpretations[index];
printf("Found interpretation for \"%s\"\n", if (Z3_model_has_interp(ctx, m, d)) {
Z3_ast_to_string(ctx, Z3_func_decl_to_ast(ctx, d))); printf("Found interpretation for \"%s\"\n",
} else { Z3_ast_to_string(ctx, Z3_func_decl_to_ast(ctx, d)));
printf("Missing interpretation"); } else {
printf("Missing interpretation");
exit(1);
}
}
}
{
// Evaluate a + b under model
Z3_ast addArgs[] = {aApp, bApp};
Z3_ast aPlusB = Z3_mk_add(ctx,
/*num_args=*/2,
/*args=*/addArgs);
Z3_ast aPlusBEval = NULL;
Z3_bool aPlusBEvalSuccess =
Z3_model_eval(ctx, m, aPlusB,
/*model_completion=*/Z3_FALSE, &aPlusBEval);
if (aPlusBEvalSuccess != Z3_TRUE) {
printf("Failed to evaluate model\n");
exit(1);
}
int aPlusBValue = 0;
Z3_bool getAPlusBValueSuccess =
Z3_get_numeral_int(ctx, aPlusBEval, &aPlusBValue);
if (getAPlusBValueSuccess != Z3_TRUE) {
printf("Failed to get integer value for a+b\n");
exit(1);
}
printf("Evaluated a + b = %d\n", aPlusBValue);
if (aPlusBValue != 3) {
printf("a+b did not evaluate to expected value\n");
exit(1); exit(1);
} }
} }
// Evaluate a + b under model {
Z3_ast addArgs[] = {aApp, bApp}; // Evaluate c[0] + c[1] + c[2] under model
Z3_ast aPlusB = Z3_mk_add(ctx, Z3_ast c0 = Z3_mk_select(ctx, cApp, zeroNumeral);
/*num_args=*/2, Z3_ast c1 = Z3_mk_select(ctx, cApp, oneNumeral);
/*args=*/addArgs); Z3_ast c2 = Z3_mk_select(ctx, cApp, twoNumeral);
Z3_ast aPlusBEval = NULL; Z3_ast arrayAddArgs[] = {c0, c1, c2};
Z3_bool aPlusBEvalSuccess = Z3_ast arrayAdd = Z3_mk_add(ctx,
Z3_model_eval(ctx, m, aPlusB, /*num_args=*/3,
/*model_completion=*/Z3_FALSE, &aPlusBEval); /*args=*/arrayAddArgs);
if (aPlusBEvalSuccess != Z3_TRUE) { Z3_ast arrayAddEval = NULL;
printf("Failed to evaluate model\n"); Z3_bool arrayAddEvalSuccess =
exit(1); Z3_model_eval(ctx, m, arrayAdd,
} /*model_completion=*/Z3_FALSE, &arrayAddEval);
int aPlusBValue = 0; if (arrayAddEvalSuccess != Z3_TRUE) {
Z3_bool getAPlusBValueSuccess = printf("Failed to evaluate model\n");
Z3_get_numeral_int(ctx, aPlusBEval, &aPlusBValue); exit(1);
if (getAPlusBValueSuccess != Z3_TRUE) { }
printf("Failed to get integer value for a+b\n"); int arrayAddValue = 0;
exit(1); Z3_bool getArrayAddValueSuccess =
} Z3_get_numeral_int(ctx, arrayAddEval, &arrayAddValue);
printf("Evaluated a + b = %d\n", aPlusBValue); if (getArrayAddValueSuccess != Z3_TRUE) {
if (aPlusBValue != 3) { printf("Failed to get integer value for c[0] + c[1] + c[2]\n");
printf("a+b did not evaluate to expected value\n"); exit(1);
exit(1); }
} printf("Evaluated c[0] + c[1] + c[2] = %d\n", arrayAddValue);
if (arrayAddValue != 7) {
// Evaluate c[0] + c[1] + c[2] under model printf("c[0] + c[1] + c[2] did not evaluate to expected value\n");
Z3_ast c0 = Z3_mk_select(ctx, cApp, zeroNumeral); exit(1);
Z3_ast c1 = Z3_mk_select(ctx, cApp, oneNumeral); }
Z3_ast c2 = Z3_mk_select(ctx, cApp, twoNumeral);
Z3_ast arrayAddArgs[] = {c0, c1, c2};
Z3_ast arrayAdd = Z3_mk_add(ctx,
/*num_args=*/3,
/*args=*/arrayAddArgs);
Z3_ast arrayAddEval = NULL;
Z3_bool arrayAddEvalSuccess =
Z3_model_eval(ctx, m, arrayAdd,
/*model_completion=*/Z3_FALSE, &arrayAddEval);
if (arrayAddEvalSuccess != Z3_TRUE) {
printf("Failed to evaluate model\n");
exit(1);
}
int arrayAddValue = 0;
Z3_bool getArrayAddValueSuccess =
Z3_get_numeral_int(ctx, arrayAddEval, &arrayAddValue);
if (getArrayAddValueSuccess != Z3_TRUE) {
printf("Failed to get integer value for c[0] + c[1] + c[2]\n");
exit(1);
}
printf("Evaluated c[0] + c[1] + c[2] = %d\n", arrayAddValue);
if (arrayAddValue != 7) {
printf("c[0] + c[1] + c[2] did not evaluate to expected value\n");
exit(1);
} }
Z3_ast_vector_dec_ref(ctx, oneArgs); Z3_ast_vector_dec_ref(ctx, oneArgs);
@ -3009,7 +3031,6 @@ void mk_model_example() {
Z3_model_dec_ref(ctx, m); Z3_model_dec_ref(ctx, m);
Z3_del_context(ctx); Z3_del_context(ctx);
} }
#endif
/*@}*/ /*@}*/
/*@}*/ /*@}*/
@ -3059,6 +3080,6 @@ int main() {
substitute_example(); substitute_example();
substitute_vars_example(); substitute_vars_example();
fpa_example(); fpa_example();
// mk_model_example(); mk_model_example();
return 0; return 0;
} }