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

fix maxsat compilation for maxsat example

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-29 09:00:37 -08:00
parent 09dc773658
commit 0a67f6ee9b
2 changed files with 10 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
examples/maxsat/maxsat.c
View file

@ -578,8 +578,9 @@ int smtlib_maxsat(char * file_name, int approach)
unsigned i; unsigned i;
Z3_optimize opt; Z3_optimize opt;
unsigned num_hard_cnstrs, num_soft_cnstrs; unsigned num_hard_cnstrs, num_soft_cnstrs;
Z3_ast * hard_cnstrs, * soft_cnstrs, soft; Z3_ast * hard_cnstrs, * soft_cnstrs;
Z3_ast_vector hard, objs; Z3_ast_vector hard, objs;
Z3_app soft;
unsigned result = 0; unsigned result = 0;
ctx = mk_context(); ctx = mk_context();
s = mk_solver(ctx); s = mk_solver(ctx);
@ -595,22 +596,16 @@ int smtlib_maxsat(char * file_name, int approach)
} }
objs = Z3_optimize_get_objectives(ctx, opt); objs = Z3_optimize_get_objectives(ctx, opt);
Z3_ast_vector_inc_ref(ctx, objs); Z3_ast_vector_inc_ref(ctx, objs);
num_soft_cnstrs = 0;
soft = Z3_ast_vector_get(ctx, objs, 0); // soft constraints are stored in a single objective which is a sum
while (Z3_get_decl_kind(ctx, Z3_get_app_decl(ctx, Z3_to_app(ctx, soft))) == Z3_OP_ITE) { // of if-then-else expressions.
++num_soft_cnstrs; soft = Z3_to_app(ctx, Z3_ast_vector_get(ctx, objs, 0));
soft = Z3_get_app_arg(ctx, Z3_to_app(ctx, soft), 1); num_soft_cnstrs = Z3_get_app_num_args(ctx, soft);
}
soft_cnstrs = (Z3_ast *) malloc(sizeof(Z3_ast) * (num_soft_cnstrs)); soft_cnstrs = (Z3_ast *) malloc(sizeof(Z3_ast) * (num_soft_cnstrs));
num_soft_cnstrs = 0; for (i = 0; i < num_soft_cnstrs; ++i) {
soft = Z3_ast_vector_get(ctx, objs, 0); soft_cnstrs[i] = Z3_get_app_arg(ctx, Z3_to_app(ctx, Z3_get_app_arg(ctx, soft, i)), 0);
while (Z3_get_decl_kind(ctx, Z3_get_app_decl(ctx, Z3_to_app(ctx, soft))) == Z3_OP_ITE) {
soft_cnstrs[num_soft_cnstrs] = Z3_get_app_arg(ctx, Z3_to_app(ctx, soft), 0);
++num_soft_cnstrs;
soft = Z3_get_app_arg(ctx, Z3_to_app(ctx, soft), 1);
} }
// soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs);
switch (approach) { switch (approach) {
case NAIVE_MAXSAT: case NAIVE_MAXSAT:
result = naive_maxsat(ctx, s, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs); result = naive_maxsat(ctx, s, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs);

2
src/api/z3_api.h
View file

@ -4299,7 +4299,7 @@ extern "C" {
/** /**
\brief Return the i-th argument of the given application. \brief Return the i-th argument of the given application.
\pre i < Z3_get_num_args(c, a) \pre i < Z3_get_app_num_args(c, a)
def_API('Z3_get_app_arg', AST, (_in(CONTEXT), _in(APP), _in(UINT))) def_API('Z3_get_app_arg', AST, (_in(CONTEXT), _in(APP), _in(UINT)))
*/ */