mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Fixed backwards compatibility problem in maxsat example

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-06-28 14:44:41 +00:00
parent 1a59123819
commit 1f29cebd4d
1 changed files with 13 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
examples/maxsat/maxsat.c
View file

@ -348,7 +348,15 @@ void assert_at_most_k(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits, un
*/ */
void assert_at_most_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits) void assert_at_most_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits)
{ {
assert_at_most_k(ctx, s, n, lits, 1); assert_at_most_k(ctx, s, n, lits, 1);
}
Z3_solver mk_solver(Z3_context ctx)
{
Z3_solver r = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, r);
return r;
} }
/** /**
@ -357,8 +365,7 @@ void assert_at_most_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits)
void tst_at_most_one() void tst_at_most_one()
{ {
Z3_context ctx = mk_context(); Z3_context ctx = mk_context();
Z3_solver s = Z3_mk_solver(ctx); Z3_solver s = mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast k1 = mk_bool_var(ctx, "k1"); Z3_ast k1 = mk_bool_var(ctx, "k1");
Z3_ast k2 = mk_bool_var(ctx, "k2"); Z3_ast k2 = mk_bool_var(ctx, "k2");
Z3_ast k3 = mk_bool_var(ctx, "k3"); Z3_ast k3 = mk_bool_var(ctx, "k3");
@ -460,7 +467,7 @@ int naive_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast *
printf("unsat\n"); printf("unsat\n");
return num_soft_cnstrs - k - 1; return num_soft_cnstrs - k - 1;
} }
m = Z3_solver_get_model(ctx, s); m = Z3_solver_get_model(ctx, s);
Z3_model_inc_ref(ctx, m); Z3_model_inc_ref(ctx, m);
num_disabled = get_num_disabled_soft_constraints(ctx, m, num_soft_cnstrs, aux_vars); num_disabled = get_num_disabled_soft_constraints(ctx, m, num_soft_cnstrs, aux_vars);
Z3_model_dec_ref(ctx, m); Z3_model_dec_ref(ctx, m);
@ -523,7 +530,7 @@ int fu_malik_maxsat_step(Z3_context ctx, Z3_solver s, unsigned num_soft_cnstrs,
unsigned j; unsigned j;
// check whether assumption[i] is in the core or not // check whether assumption[i] is in the core or not
for (j = 0; j < core_size; j++) { for (j = 0; j < core_size; j++) {
if (assumptions[i] == Z3_ast_vector_get(ctx, core, j)) if (assumptions[i] == Z3_ast_vector_get(ctx, core, j))
break; break;
} }
if (j < core_size) { if (j < core_size) {
@ -607,8 +614,7 @@ int smtlib_maxsat(char * file_name, int approach)
Z3_ast * hard_cnstrs, * soft_cnstrs; Z3_ast * hard_cnstrs, * soft_cnstrs;
unsigned result = 0; unsigned result = 0;
ctx = mk_context(); ctx = mk_context();
s = Z3_mk_solver(ctx); s = mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0); Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0);
hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs); hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs);
soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs); soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs);