mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

remove useless set-activity

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-16 20:24:51 +03:00
parent 483a973b37
commit 6e3f05b986
4 changed files with 0 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/api/api_solver.cpp
View file

@ -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);

1
src/api/c++/z3++.h
View file

@ -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);

6
src/api/python/z3/z3.py
View file

@ -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()`.

7
src/api/z3_api.h
View file

@ -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.