mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove push/pop for fixedpoint objects from API #2249
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
fa88bdb075
commit
40e329fc92
|
@ -588,23 +588,6 @@ extern "C" {
|
|||
Z3_CATCH;
|
||||
}
|
||||
|
||||
void Z3_API Z3_fixedpoint_push(Z3_context c,Z3_fixedpoint d) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fixedpoint_push(c, d);
|
||||
RESET_ERROR_CODE();
|
||||
to_fixedpoint_ref(d)->ctx().push();
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
void Z3_API Z3_fixedpoint_pop(Z3_context c,Z3_fixedpoint d) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fixedpoint_pop(c, d);
|
||||
RESET_ERROR_CODE();
|
||||
to_fixedpoint_ref(d)->ctx().pop();
|
||||
Z3_CATCH;
|
||||
|
||||
}
|
||||
|
||||
void Z3_API Z3_fixedpoint_add_callback(Z3_context c, Z3_fixedpoint d,
|
||||
void *state,
|
||||
Z3_fixedpoint_new_lemma_eh new_lemma_eh,
|
||||
|
|
|
@ -2787,8 +2787,6 @@ namespace z3 {
|
|||
array<Z3_ast> qs(queries);
|
||||
return Z3_fixedpoint_to_string(ctx(), m_fp, qs.size(), qs.ptr());
|
||||
}
|
||||
void push() { Z3_fixedpoint_push(ctx(), m_fp); check_error(); }
|
||||
void pop() { Z3_fixedpoint_pop(ctx(), m_fp); check_error(); }
|
||||
};
|
||||
inline std::ostream & operator<<(std::ostream & out, fixedpoint const & f) { return out << Z3_fixedpoint_to_string(f.ctx(), f, 0, 0); }
|
||||
|
||||
|
|
|
@ -161,26 +161,6 @@ namespace Microsoft.Z3
|
|||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Creates a backtracking point.
|
||||
/// </summary>
|
||||
/// <seealso cref="Pop"/>
|
||||
public void Push()
|
||||
{
|
||||
Native.Z3_fixedpoint_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_fixedpoint_pop(Context.nCtx, NativeObject);
|
||||
}
|
||||
|
||||
|
||||
/// <summary>
|
||||
/// Update named rule into in the fixedpoint solver.
|
||||
/// </summary>
|
||||
|
|
|
@ -157,25 +157,6 @@ public class Fixedpoint extends Z3Object
|
|||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Creates a backtracking point.
|
||||
* @see #pop
|
||||
**/
|
||||
public void push() {
|
||||
Native.fixedpointPush(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* Backtrack one backtracking point.
|
||||
* Remarks: Note that an exception is thrown if {@code pop}
|
||||
* is called without a corresponding {@code push}
|
||||
*
|
||||
* @see #push
|
||||
**/
|
||||
public void pop() {
|
||||
Native.fixedpointPop(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
* Update named rule into in the fixedpoint solver.
|
||||
*
|
||||
|
|
|
@ -1883,8 +1883,6 @@ struct
|
|||
| L_FALSE -> Solver.UNSATISFIABLE
|
||||
| _ -> Solver.UNKNOWN
|
||||
|
||||
let push x = Z3native.fixedpoint_push (gc x) x
|
||||
let pop x = Z3native.fixedpoint_pop (gc x) x
|
||||
let update_rule x = Z3native.fixedpoint_update_rule (gc x) x
|
||||
|
||||
let get_answer x =
|
||||
|
|
|
@ -3256,16 +3256,6 @@ sig
|
|||
The query is unsatisfiable if there are no derivations satisfying any of the relations. *)
|
||||
val query_r : fixedpoint -> FuncDecl.func_decl list -> Solver.status
|
||||
|
||||
(** Creates a backtracking point.
|
||||
{!pop} *)
|
||||
val push : fixedpoint -> unit
|
||||
|
||||
(** Backtrack one backtracking point.
|
||||
|
||||
Note that an exception is thrown if Pop is called without a corresponding [Push]</remarks>
|
||||
{!push} *)
|
||||
val pop : fixedpoint -> unit
|
||||
|
||||
(** Update named rule into in the fixedpoint solver. *)
|
||||
val update_rule : fixedpoint -> Expr.expr -> Symbol.symbol -> unit
|
||||
|
||||
|
|
|
@ -7047,14 +7047,6 @@ class Fixedpoint(Z3PPObject):
|
|||
r = Z3_fixedpoint_query_from_lvl (self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
|
||||
return CheckSatResult(r)
|
||||
|
||||
def push(self):
|
||||
"""create a backtracking point for added rules, facts and assertions"""
|
||||
Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint)
|
||||
|
||||
def pop(self):
|
||||
"""restore to previously created backtracking point"""
|
||||
Z3_fixedpoint_pop(self.ctx.ref(), self.fixedpoint)
|
||||
|
||||
def update_rule(self, head, body, name):
|
||||
"""update rule"""
|
||||
if name is None:
|
||||
|
|
|
@ -334,29 +334,6 @@ extern "C" {
|
|||
Z3_fixedpoint f,
|
||||
Z3_string s);
|
||||
|
||||
/**
|
||||
\brief Create a backtracking point.
|
||||
|
||||
The fixedpoint solver contains a set of rules, added facts and assertions.
|
||||
The set of rules, facts and assertions are restored upon calling #Z3_fixedpoint_pop.
|
||||
|
||||
\sa Z3_fixedpoint_pop
|
||||
|
||||
def_API('Z3_fixedpoint_push', VOID, (_in(CONTEXT), _in(FIXEDPOINT)))
|
||||
*/
|
||||
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d);
|
||||
|
||||
/**
|
||||
\brief Backtrack one backtracking point.
|
||||
|
||||
\sa Z3_fixedpoint_push
|
||||
|
||||
\pre The number of calls to pop cannot exceed calls to push.
|
||||
|
||||
def_API('Z3_fixedpoint_pop', VOID, (_in(CONTEXT), _in(FIXEDPOINT)))
|
||||
*/
|
||||
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d);
|
||||
|
||||
/** \brief The following utilities allows adding user-defined domains. */
|
||||
|
||||
typedef void Z3_fixedpoint_reduce_assign_callback_fptr(
|
||||
|
|
Loading…
Reference in a new issue