3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

add push/pop to optimization context for convenience

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-01 14:58:58 -07:00
parent 75c114feab
commit 31f16d7aa4
5 changed files with 77 additions and 2 deletions

View file

@ -102,6 +102,23 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
void Z3_API Z3_optimize_push(Z3_context c,Z3_optimize d) {
Z3_TRY;
LOG_Z3_optimize_push(c, d);
RESET_ERROR_CODE();
to_optimize_ptr(d)->push();
Z3_CATCH;
}
void Z3_API Z3_optimize_pop(Z3_context c,Z3_optimize d) {
Z3_TRY;
LOG_Z3_optimize_pop(c, d);
RESET_ERROR_CODE();
to_optimize_ptr(d)->pop(1);
Z3_CATCH;
}
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o) {
Z3_TRY;
LOG_Z3_optimize_check(c, o);

View file

@ -1511,6 +1511,12 @@ namespace z3 {
handle minimize(expr const& e) {
return handle(Z3_optimize_minimize(ctx(), m_opt, e));
}
void push() {
Z3_optimize_push(ctx(), m_opt);
}
void pop() {
Z3_optimize_pop(ctx(), m_opt);
}
check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); }
model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }

View file

@ -111,6 +111,26 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Creates a backtracking point.
/// </summary>
/// <seealso cref="Pop"/>
public void Push()
{
Native.Z3_optimize_push(Context.nCtx, NativeObject);
}
/// <summary>
/// Backtrack one backtracking point.
/// </summary>
/// <remarks>Note that an exception is thrown if Pop is called without a corresponding <c>Push</c></remarks>
/// <seealso cref="Push"/>
public void Pop()
{
Native.Z3_optimize_pop(Context.nCtx, NativeObject);
}
/// <summary>
/// The model of the last <c>Check</c>.
/// </summary>

View file

@ -6382,6 +6382,14 @@ class Optimize(Z3PPObject):
"""Add objective function to minimize."""
return OptimizeObjective(Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()))
def push(self):
"""create a backtracking point for added rules, facts and assertions"""
Z3_optimize_push(self.ctx.ref(), self.optimize)
def pop(self):
"""restore to previously created backtracking point"""
Z3_optimize_pop(self.ctx.ref(), self.optimize)
def check(self):
"""Check satisfiability while optimizing objective functions."""
return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))

View file

@ -6007,7 +6007,7 @@ END_MLAPI_EXCLUDE
/**
\brief Add a maximiztion constraint.
\brief Add a maximization constraint.
\param c - context
\param o - optimization context
\param a - arithmetical term
@ -6016,7 +6016,7 @@ END_MLAPI_EXCLUDE
unsigned Z3_API Z3_optimize_maximize(Z3_context, Z3_optimize o, Z3_ast t);
/**
\brief Add a minimiztion constraint.
\brief Add a minimization constraint.
\param c - context
\param o - optimization context
\param a - arithmetical term
@ -6025,6 +6025,30 @@ END_MLAPI_EXCLUDE
*/
unsigned Z3_API Z3_optimize_minimize(Z3_context, Z3_optimize o, Z3_ast t);
/**
\brief Create a backtracking point.
The optimize solver contains a set of rules, added facts and assertions.
The set of rules, facts and assertions are restored upon calling #Z3_optimize_pop.
\sa Z3_optimize_pop
def_API('Z3_optimize_push', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
*/
void Z3_API Z3_optimize_push(Z3_context c,Z3_optimize d);
/**
\brief Backtrack one level.
\sa Z3_optimize_push
\pre The number of calls to pop cannot exceed calls to push.
def_API('Z3_optimize_pop', VOID, (_in(CONTEXT), _in(OPTIMIZE)))
*/
void Z3_API Z3_optimize_pop(Z3_context c,Z3_optimize d);
/**
\brief Check consistency and produce optimal values.
\param c - context