mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

fix bitrot in maxsat example reference management #1116

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-26 09:36:53 -07:00
parent 404db5759a
commit 7db1847f51
2 changed files with 13 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

12
examples/maxsat/maxsat.c
View file

@ -358,6 +358,7 @@ void tst_at_most_one()
{
Z3_context ctx = mk_context();
Z3_solver s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_ast k1 = mk_bool_var(ctx, "k1");
Z3_ast k2 = mk_bool_var(ctx, "k2");
Z3_ast k3 = mk_bool_var(ctx, "k3");
@ -376,7 +377,9 @@ void tst_at_most_one()
if (result != Z3_L_TRUE)
error("BUG");
m = Z3_solver_get_model(ctx, s);
Z3_model_inc_ref(ctx, m);
printf("model:\n%s\n", Z3_model_to_string(ctx, m));
Z3_model_dec_ref(ctx, m);
Z3_solver_assert(ctx, s, mk_binary_or(ctx, k2, k3));
Z3_solver_assert(ctx, s, mk_binary_or(ctx, k1, k6));
printf("it must be sat...\n");
@ -384,12 +387,15 @@ void tst_at_most_one()
if (result != Z3_L_TRUE)
error("BUG");
m = Z3_solver_get_model(ctx, s);
Z3_model_inc_ref(ctx, m);
printf("model:\n%s\n", Z3_model_to_string(ctx, m));
Z3_solver_assert(ctx, s, mk_binary_or(ctx, k4, k5));
printf("it must be unsat...\n");
result = Z3_solver_check(ctx, s);
if (result != Z3_L_FALSE)
error("BUG");
Z3_model_dec_ref(ctx, m);
Z3_solver_dec_ref(ctx, s);
Z3_del_context(ctx);
}
@ -455,7 +461,9 @@ int naive_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast *
return num_soft_cnstrs - k - 1;
}
m = Z3_solver_get_model(ctx, s);
Z3_model_inc_ref(ctx, m);
num_disabled = get_num_disabled_soft_constraints(ctx, m, num_soft_cnstrs, aux_vars);
Z3_model_dec_ref(ctx, m);
if (num_disabled > k) {
error("BUG");
}
@ -506,6 +514,7 @@ int fu_malik_maxsat_step(Z3_context ctx, Z3_solver s, unsigned num_soft_cnstrs,
}
else {
core = Z3_solver_get_unsat_core(ctx, s);
Z3_ast_vector_inc_ref(ctx, core);
core_size = Z3_ast_vector_size(ctx, core);
block_vars = (Z3_ast*) malloc(sizeof(Z3_ast) * core_size);
k = 0;
@ -531,6 +540,7 @@ int fu_malik_maxsat_step(Z3_context ctx, Z3_solver s, unsigned num_soft_cnstrs,
}
}
assert_at_most_one(ctx, s, k, block_vars);
Z3_ast_vector_dec_ref(ctx, core);
return 0; // not done.
}
}
@ -598,6 +608,7 @@ int smtlib_maxsat(char * file_name, int approach)
unsigned result = 0;
ctx = mk_context();
s = Z3_mk_solver(ctx);
Z3_solver_inc_ref(ctx, s);
Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0);
hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs);
soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs);
@ -615,6 +626,7 @@ int smtlib_maxsat(char * file_name, int approach)
}
free_cnstr_array(hard_cnstrs);
free_cnstr_array(soft_cnstrs);
Z3_solver_dec_ref(ctx, s);
return result;
}

2
src/util/lp/sparse_matrix_instances.cpp
View file

@ -2,8 +2,8 @@
Copyright (c) 2017 Microsoft Corporation
Author: Lev Nachmanson
*/
#include "util/vector.h"
#include <memory>
#include "util/vector.h"
#include "util/lp/lp_settings.h"
#include "util/lp/lu.h"
#include "util/lp/sparse_matrix.hpp"