From 6e3f05b98657f7ff6d5a2671002b85cbb1b9f1fa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 16 May 2019 20:24:51 +0300
Subject: [PATCH] remove useless set-activity

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_solver.cpp  | 9 ---------
 src/api/c++/z3++.h      | 1 -
 src/api/python/z3/z3.py | 6 ------
 src/api/z3_api.h        | 7 -------
 4 files changed, 23 deletions(-)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index fb7a937cc..83bf8a33f 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -428,15 +428,6 @@ extern "C" {
         Z3_CATCH;
     }
 
-    void Z3_API Z3_solver_set_activity(Z3_context c, Z3_solver s, Z3_ast a, double activity) {
-        Z3_TRY;
-        LOG_Z3_solver_set_activity(c, s, a, activity);
-        RESET_ERROR_CODE();
-        init_solver(c, s);
-        to_solver_ref(s)->set_activity(to_expr(a), activity);
-        Z3_CATCH;
-    }
-
     Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s) {
         Z3_TRY;
         LOG_Z3_solver_get_trail(c, s);
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 60d5afecd..8bacf8dbc 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -2292,7 +2292,6 @@ namespace z3 {
             check_error(); 
             return result; 
         }
-        void set_activity(expr const& lit, double act) { Z3_solver_set_activity(ctx(), m_solver, lit, act); }
         expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
         friend std::ostream & operator<<(std::ostream & out, solver const & s);
 
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 042cdde6f..2fa85a7cd 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6781,12 +6781,6 @@ class Solver(Z3PPObject):
         """Return trail of the solver state after a check() call. 
         """
         return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
-
-    def set_activity(self, lit, act):
-        """Set activity of literal on solver object.
-        This influences the case split order of the variable.
-        """
-        Z3_solver_set_activity(self.ctx.ref(), self.solver, lit.ast, act)
         
     def statistics(self):
         """Return statistics for the last `check()`.
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 0d9f548ef..f3fc1ed7e 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6351,13 +6351,6 @@ extern "C" {
     */
     void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz,  unsigned levels[]);
 
-    /**
-       \brief set activity score associated with literal.
-
-       def_API('Z3_solver_set_activity', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST), _in(DOUBLE)))
-     */
-    void Z3_API Z3_solver_set_activity(Z3_context c, Z3_solver s, Z3_ast l, double activity);
-
     /**
        \brief Check whether the assertions in a given solver are consistent or not.