From 40e329fc92e91acc9efda668e8d6d034221fe887 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 27 Apr 2019 10:13:15 -0700 Subject: [PATCH] remove push/pop for fixedpoint objects from API #2249 Signed-off-by: Nikolaj Bjorner --- src/api/api_datalog.cpp | 17 ----------------- src/api/c++/z3++.h | 2 -- src/api/dotnet/Fixedpoint.cs | 20 -------------------- src/api/java/Fixedpoint.java | 19 ------------------- src/api/ml/z3.ml | 2 -- src/api/ml/z3.mli | 10 ---------- src/api/python/z3/z3.py | 8 -------- src/api/z3_fixedpoint.h | 23 ----------------------- 8 files changed, 101 deletions(-) diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 57037f1a8..e872bc12d 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -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, diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 6af38cb82..175fe87fc 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2787,8 +2787,6 @@ namespace z3 { array 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); } diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 51ee79b55..dc4de8925 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -161,26 +161,6 @@ namespace Microsoft.Z3 } } - /// - /// Creates a backtracking point. - /// - /// - public void Push() - { - Native.Z3_fixedpoint_push(Context.nCtx, NativeObject); - } - - /// - /// Backtrack one backtracking point. - /// - /// Note that an exception is thrown if Pop is called without a corresponding Push - /// - public void Pop() - { - Native.Z3_fixedpoint_pop(Context.nCtx, NativeObject); - } - - /// /// Update named rule into in the fixedpoint solver. /// diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 7bb0fda58..8560b6292 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -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. * diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 50735a57c..825f3606c 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -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 = diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 69dbfa23d..678f99443 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -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] - {!push} *) - val pop : fixedpoint -> unit - (** Update named rule into in the fixedpoint solver. *) val update_rule : fixedpoint -> Expr.expr -> Symbol.symbol -> unit diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 6d6220fb5..3bd0df612 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -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: diff --git a/src/api/z3_fixedpoint.h b/src/api/z3_fixedpoint.h index 54a42e9bf..33b970371 100644 --- a/src/api/z3_fixedpoint.h +++ b/src/api/z3_fixedpoint.h @@ -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(