From e32e0d460d8f7e393f28ade7b10f9bac6a13033c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Oct 2016 21:50:45 -0700 Subject: [PATCH] fix at-most-1 constraint compiler bug Signed-off-by: Nikolaj Bjorner --- src/api/api_opt.cpp | 19 +++++++++---------- src/api/c++/z3++.h | 2 ++ src/api/dotnet/Optimize.cs | 27 +++++++++++++++++++++++++++ src/api/python/z3/z3.py | 3 +-- src/api/z3_optimization.h | 17 ++++++----------- src/smt/theory_pb.cpp | 2 +- 6 files changed, 46 insertions(+), 24 deletions(-) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 20eb6d1d4..308db4081 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -311,19 +311,18 @@ extern "C" { RETURN_Z3(of_ast_vector(v)); Z3_CATCH_RETURN(0); } - - unsigned Z3_API Z3_optimize_get_num_objectives(Z3_context c, Z3_optimize o) { - RESET_ERROR_CODE(); - return to_optimize_ptr(o)->num_objectives(); - } - Z3_ast Z3_API Z3_optimize_get_objective(Z3_context c, Z3_optimize o, unsigned index) { + Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o) { Z3_TRY; - LOG_Z3_optimize_get_objective(c, o, index); + LOG_Z3_optimize_get_objectives(c, o); RESET_ERROR_CODE(); - expr_ref result = to_optimize_ptr(o)->get_objective(index); - mk_c(c)->save_ast_trail(result); - RETURN_Z3(of_expr(result)); + unsigned n = to_optimize_ptr(o)->num_objectives(); + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + for (unsigned i = 0; i < n; i++) { + v->m_ast_vector.push_back(to_optimize_ptr(o)->get_objective(i)); + } + RETURN_Z3(of_ast_vector(v)); Z3_CATCH_RETURN(0); } diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index b03e38b7e..2a9c771a1 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2053,6 +2053,8 @@ namespace z3 { check_error(); return expr(ctx(), r); } + expr_vector assertions() const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); } + expr_vector objectives() const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); } stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); } friend std::ostream & operator<<(std::ostream & out, optimize const & s); void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); } diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index e5982e4fc..036aaf2f2 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -290,6 +290,33 @@ namespace Microsoft.Z3 Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s); } + /// + /// The set of asserted formulas. + /// + public BoolExpr[] Assertions + { + get + { + Contract.Ensures(Contract.Result() != null); + + ASTVector assertions = new ASTVector(Context, Native.Z3_optimize_get_assertions(Context.nCtx, NativeObject)); + return assertions.ToBoolExprArray(); + } + } + + /// + /// The set of asserted formulas. + /// + public Expr[] Objectives + { + get + { + Contract.Ensures(Contract.Result() != null); + + ASTVector objectives = new ASTVector(Context, Native.Z3_optimize_get_objectives(Context.nCtx, NativeObject)); + return objectives.ToExprArray(); + } + } /// diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index bc5bd8153..abeee5ba3 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6802,8 +6802,7 @@ class Optimize(Z3PPObject): def objectives(self): """returns set of objective functions""" - num = Z3_optimize_get_num_objectives(self.ctx.ref(), self.optimize) - return [_to_expr_ref(Z3_optimize_get_objective(self.ctx.ref(), self.optimize, i), self.ctx) for i in range(num)] + return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx) def __repr__(self): """Return a formatted string with all added rules and constraints.""" diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index e78be7881..219f3ede8 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -249,21 +249,16 @@ extern "C" { Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o); /** - \brief Return number of objectives on the optimization context. - - def_API('Z3_optimize_get_num_objectives', UINT, (_in(CONTEXT), _in(OPTIMIZE))) - */ - unsigned Z3_API Z3_optimize_get_num_objectives(Z3_context c, Z3_optimize o); - - /** - \brief Return i'th objective function. If the objective function is a max-sat objective it is returned + \brief Return objectives on the optimization context. + If the objective function is a max-sat objective it is returned as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...) If the objective function is entered as a maximization objective, then return the corresponding minimizaiton objective. In this way the resulting objective function is always returned as a minimization objective. - - def_API('Z3_optimize_get_objective', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT))) + + def_API('Z3_optimize_get_objectives', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE))) */ - Z3_ast Z3_API Z3_optimize_get_objective(Z3_context c, Z3_optimize o, unsigned index); + Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o); + /*@}*/ diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 384c58d73..7b032dce9 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -520,7 +520,7 @@ namespace smt { } unsigned th = args.size()*log; c->m_compilation_threshold = th; - IF_VERBOSE(2, verbose_stream() << "(smt.pb setting compilation threshold to " << th << " " << c->k() << ")\n";); + IF_VERBOSE(2, verbose_stream() << "(smt.pb setting compilation threshold to " << th << ")\n";); TRACE("pb", tout << "compilation threshold: " << th << "\n";); } else {