mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix at-most-1 constraint compiler bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
23b9d3ef55
commit
e32e0d460d
|
@ -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);
|
||||
}
|
||||
|
||||
|
|
|
@ -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(); }
|
||||
|
|
|
@ -290,6 +290,33 @@ namespace Microsoft.Z3
|
|||
Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The set of asserted formulas.
|
||||
/// </summary>
|
||||
public BoolExpr[] Assertions
|
||||
{
|
||||
get
|
||||
{
|
||||
Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
|
||||
|
||||
ASTVector assertions = new ASTVector(Context, Native.Z3_optimize_get_assertions(Context.nCtx, NativeObject));
|
||||
return assertions.ToBoolExprArray();
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The set of asserted formulas.
|
||||
/// </summary>
|
||||
public Expr[] Objectives
|
||||
{
|
||||
get
|
||||
{
|
||||
Contract.Ensures(Contract.Result<Expr[]>() != null);
|
||||
|
||||
ASTVector objectives = new ASTVector(Context, Native.Z3_optimize_get_objectives(Context.nCtx, NativeObject));
|
||||
return objectives.ToExprArray();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/// <summary>
|
||||
|
|
|
@ -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."""
|
||||
|
|
|
@ -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);
|
||||
|
||||
|
||||
|
||||
/*@}*/
|
||||
|
|
|
@ -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 {
|
||||
|
|
Loading…
Reference in a new issue