From 09dc773658b5cd997e4fcdcdc0b8f922aec1a34e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Nov 2017 08:50:35 -0800 Subject: [PATCH] fix maxsat compilation for maxsat example Signed-off-by: Nikolaj Bjorner --- examples/maxsat/maxsat.c | 72 ++++++++++++++++++---------------------- 1 file changed, 33 insertions(+), 39 deletions(-) diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c index a312e79ad..b5d8a6a8c 100644 --- a/examples/maxsat/maxsat.c +++ b/examples/maxsat/maxsat.c @@ -116,41 +116,6 @@ Z3_ast mk_binary_and(Z3_context ctx, Z3_ast in_1, Z3_ast in_2) } -/** - \brief Get hard constraints from a SMT-LIB file. We assume hard constraints - are formulas preceeded with the keyword :formula. - Return an array containing all formulas read by the last Z3_parse_smtlib_file invocation. - It will store the number of formulas in num_cnstrs. -*/ -Z3_ast * get_hard_constraints(Z3_context ctx, unsigned * num_cnstrs) -{ - Z3_ast * result; - unsigned i; - *num_cnstrs = Z3_get_smtlib_num_formulas(ctx); - result = (Z3_ast *) malloc(sizeof(Z3_ast) * (*num_cnstrs)); - for (i = 0; i < *num_cnstrs; i++) { - result[i] = Z3_get_smtlib_formula(ctx, i); - } - return result; -} - -/** - \brief Get soft constraints from a SMT-LIB file. We assume soft constraints - are formulas preceeded with the keyword :assumption. - Return an array containing all assumptions read by the last Z3_parse_smtlib_file invocation. - It will store the number of formulas in num_cnstrs. -*/ -Z3_ast * get_soft_constraints(Z3_context ctx, unsigned * num_cnstrs) -{ - Z3_ast * result; - unsigned i; - *num_cnstrs = Z3_get_smtlib_num_assumptions(ctx); - result = (Z3_ast *) malloc(sizeof(Z3_ast) * (*num_cnstrs)); - for (i = 0; i < *num_cnstrs; i++) { - result[i] = Z3_get_smtlib_assumption(ctx, i); - } - return result; -} /** \brief Free the given array of cnstrs that was allocated using get_hard_constraints or get_soft_constraints. @@ -610,14 +575,42 @@ int smtlib_maxsat(char * file_name, int approach) { Z3_context ctx; Z3_solver s; + unsigned i; + Z3_optimize opt; unsigned num_hard_cnstrs, num_soft_cnstrs; - Z3_ast * hard_cnstrs, * soft_cnstrs; + Z3_ast * hard_cnstrs, * soft_cnstrs, soft; + Z3_ast_vector hard, objs; unsigned result = 0; ctx = mk_context(); s = mk_solver(ctx); - 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); + opt = Z3_mk_optimize(ctx); + Z3_optimize_inc_ref(ctx, opt); + Z3_optimize_from_file(ctx, opt, file_name); + hard = Z3_optimize_get_assertions(ctx, opt); + Z3_ast_vector_inc_ref(ctx, hard); + num_hard_cnstrs = Z3_ast_vector_size(ctx, hard); + hard_cnstrs = (Z3_ast *) malloc(sizeof(Z3_ast) * (num_hard_cnstrs)); + for (i = 0; i < num_hard_cnstrs; i++) { + hard_cnstrs[i] = Z3_ast_vector_get(ctx, hard, i); + } + objs = Z3_optimize_get_objectives(ctx, opt); + Z3_ast_vector_inc_ref(ctx, objs); + num_soft_cnstrs = 0; + soft = Z3_ast_vector_get(ctx, objs, 0); + while (Z3_get_decl_kind(ctx, Z3_get_app_decl(ctx, Z3_to_app(ctx, soft))) == Z3_OP_ITE) { + ++num_soft_cnstrs; + soft = Z3_get_app_arg(ctx, Z3_to_app(ctx, soft), 1); + } + soft_cnstrs = (Z3_ast *) malloc(sizeof(Z3_ast) * (num_soft_cnstrs)); + num_soft_cnstrs = 0; + soft = Z3_ast_vector_get(ctx, objs, 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) { case NAIVE_MAXSAT: result = naive_maxsat(ctx, s, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs); @@ -633,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); + Z3_optimize_dec_ref(ctx, opt); return result; }