mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
add API for setting variable activity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e4c6dcd84c
commit
89bf2d4368
|
@ -431,6 +431,15 @@ 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);
|
||||
|
|
|
@ -2245,6 +2245,7 @@ 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);
|
||||
|
||||
|
|
|
@ -6744,6 +6744,12 @@ class Solver(Z3PPObject):
|
|||
"""
|
||||
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()`.
|
||||
|
||||
|
|
|
@ -6236,6 +6236,12 @@ 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.
|
||||
|
|
|
@ -124,6 +124,7 @@ public:
|
|||
expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
|
||||
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override { m_solver.get_levels(vars, depth); }
|
||||
expr_ref_vector get_trail() override { return m_solver.get_trail(); }
|
||||
void set_activity(expr* lit, double act) override { m_solver.set_activity(lit, act); }
|
||||
|
||||
void push() override;
|
||||
void pop(unsigned n) override;
|
||||
|
|
|
@ -110,6 +110,7 @@ namespace opt {
|
|||
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) override;
|
||||
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override;
|
||||
expr_ref_vector get_trail() override { return m_context.get_trail(); }
|
||||
void set_activity(expr* lit, double act) override { m_context.set_activity(lit, act); }
|
||||
expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
|
||||
|
||||
void set_logic(symbol const& logic);
|
||||
|
|
|
@ -1619,6 +1619,12 @@ namespace sat {
|
|||
return tracking_assumptions() && m_assumption_set.contains(l);
|
||||
}
|
||||
|
||||
void solver::set_activity(bool_var v, unsigned act) {
|
||||
unsigned old_act = m_activity[v];
|
||||
m_activity[v] = act;
|
||||
m_case_split_queue.activity_changed_eh(v, act > old_act);
|
||||
}
|
||||
|
||||
bool solver::is_assumption(bool_var v) const {
|
||||
return is_assumption(literal(v, false)) || is_assumption(literal(v, true));
|
||||
}
|
||||
|
|
|
@ -387,6 +387,7 @@ namespace sat {
|
|||
char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
|
||||
bool check_clauses(model const& m) const;
|
||||
bool is_assumption(bool_var v) const;
|
||||
void set_activity(bool_var v, unsigned act);
|
||||
|
||||
lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level);
|
||||
|
||||
|
|
|
@ -341,6 +341,15 @@ public:
|
|||
return result;
|
||||
}
|
||||
|
||||
void set_activity(expr* var, double activity) override {
|
||||
m.is_not(var, var);
|
||||
sat::bool_var v = m_map.to_bool_var(var);
|
||||
if (v == sat::null_bool_var) {
|
||||
throw default_exception("literal does not correspond to a Boolean variable");
|
||||
}
|
||||
m_solver.set_activity(v, activity);
|
||||
}
|
||||
|
||||
proof * get_proof() override {
|
||||
UNREACHABLE();
|
||||
return nullptr;
|
||||
|
|
|
@ -80,6 +80,11 @@ namespace smt {
|
|||
m_queue.decreased(v);
|
||||
}
|
||||
|
||||
void activity_decreased_eh(bool_var v) override {
|
||||
if (m_queue.contains(v))
|
||||
m_queue.increased(v);
|
||||
}
|
||||
|
||||
void mk_var_eh(bool_var v) override {
|
||||
m_queue.reserve(v+1);
|
||||
SASSERT(!m_queue.contains(v));
|
||||
|
@ -167,6 +172,14 @@ namespace smt {
|
|||
m_delayed_queue.decreased(v);
|
||||
}
|
||||
|
||||
void activity_decreased_eh(bool_var v) override {
|
||||
act_case_split_queue::activity_decreased_eh(v);
|
||||
if (m_queue.contains(v))
|
||||
m_queue.increased(v);
|
||||
if (m_delayed_queue.contains(v))
|
||||
m_delayed_queue.increased(v);
|
||||
}
|
||||
|
||||
void mk_var_eh(bool_var v) override {
|
||||
m_queue.reserve(v+1);
|
||||
m_delayed_queue.reserve(v+1);
|
||||
|
@ -324,6 +337,8 @@ namespace smt {
|
|||
|
||||
void activity_increased_eh(bool_var v) override {}
|
||||
|
||||
void activity_decreased_eh(bool_var v) override {}
|
||||
|
||||
void mk_var_eh(bool_var v) override {}
|
||||
|
||||
void del_var_eh(bool_var v) override {}
|
||||
|
@ -509,6 +524,8 @@ namespace smt {
|
|||
|
||||
void activity_increased_eh(bool_var v) override {}
|
||||
|
||||
void activity_decreased_eh(bool_var v) override {}
|
||||
|
||||
void mk_var_eh(bool_var v) override {
|
||||
if (m_context.is_searching()) {
|
||||
SASSERT(v >= m_bs_num_bool_vars);
|
||||
|
@ -753,6 +770,8 @@ namespace smt {
|
|||
|
||||
void activity_increased_eh(bool_var v) override {}
|
||||
|
||||
void activity_decreased_eh(bool_var v) override {}
|
||||
|
||||
void mk_var_eh(bool_var v) override {}
|
||||
|
||||
void del_var_eh(bool_var v) override {}
|
||||
|
@ -1133,6 +1152,11 @@ namespace smt {
|
|||
m_queue.decreased(v);
|
||||
}
|
||||
|
||||
void activity_decreased_eh(bool_var v) override {
|
||||
if (m_queue.contains(v))
|
||||
m_queue.increased(v);
|
||||
}
|
||||
|
||||
void mk_var_eh(bool_var v) override {
|
||||
m_queue.reserve(v+1);
|
||||
m_queue.insert(v);
|
||||
|
|
|
@ -32,6 +32,7 @@ namespace smt {
|
|||
class case_split_queue {
|
||||
public:
|
||||
virtual void activity_increased_eh(bool_var v) = 0;
|
||||
virtual void activity_decreased_eh(bool_var v) = 0;
|
||||
virtual void mk_var_eh(bool_var v) = 0;
|
||||
virtual void del_var_eh(bool_var v) = 0;
|
||||
virtual void assign_lit_eh(literal l) {}
|
||||
|
|
|
@ -412,10 +412,19 @@ namespace smt {
|
|||
return m_activity[v];
|
||||
}
|
||||
|
||||
void set_activity(bool_var v, double & act) {
|
||||
void set_activity(bool_var v, double const & act) {
|
||||
m_activity[v] = act;
|
||||
}
|
||||
|
||||
void activity_changed(bool_var v, bool increased) {
|
||||
if (increased) {
|
||||
m_case_split_queue->activity_increased_eh(v);
|
||||
}
|
||||
else {
|
||||
m_case_split_queue->activity_decreased_eh(v);
|
||||
}
|
||||
}
|
||||
|
||||
bool is_assumption(bool_var v) const {
|
||||
return get_bdata(v).m_assumption;
|
||||
}
|
||||
|
|
|
@ -154,6 +154,13 @@ namespace smt {
|
|||
expr_ref_vector get_trail() {
|
||||
return m_kernel.get_trail();
|
||||
}
|
||||
|
||||
void set_activity(expr* lit, double act) {
|
||||
auto v = m_kernel.get_bool_var(lit);
|
||||
double old_act = m_kernel.get_activity(v);
|
||||
m_kernel.set_activity(v, act);
|
||||
m_kernel.activity_changed(v, act > old_act);
|
||||
}
|
||||
|
||||
failure last_failure() const {
|
||||
return m_kernel.get_last_search_failure();
|
||||
|
@ -412,5 +419,9 @@ namespace smt {
|
|||
return m_imp->get_trail();
|
||||
}
|
||||
|
||||
void kernel::set_activity(expr* lit, double activity) {
|
||||
m_imp->set_activity(lit, activity);
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
|
|
@ -229,6 +229,11 @@ namespace smt {
|
|||
*/
|
||||
expr_ref_vector get_trail();
|
||||
|
||||
/**
|
||||
\brief set activity of literal
|
||||
*/
|
||||
void set_activity(expr* lit, double activity);
|
||||
|
||||
/**
|
||||
\brief (For debubbing purposes) Prints the state of the kernel
|
||||
*/
|
||||
|
|
|
@ -203,6 +203,10 @@ namespace smt {
|
|||
return m_context.get_trail();
|
||||
}
|
||||
|
||||
void set_activity(expr* lit, double activity) override {
|
||||
m_context.set_activity(lit, activity);
|
||||
}
|
||||
|
||||
struct scoped_minimize_core {
|
||||
smt_solver& s;
|
||||
expr_ref_vector m_assumptions;
|
||||
|
|
|
@ -328,6 +328,11 @@ public:
|
|||
return m_solver2->get_trail();
|
||||
}
|
||||
|
||||
void set_activity(expr* lit, double activity) override {
|
||||
m_solver1->set_activity(lit, activity);
|
||||
m_solver2->set_activity(lit, activity);
|
||||
}
|
||||
|
||||
proof * get_proof() override {
|
||||
if (m_use_solver1_results)
|
||||
return m_solver1->get_proof();
|
||||
|
|
|
@ -251,6 +251,8 @@ public:
|
|||
|
||||
virtual void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) = 0;
|
||||
|
||||
virtual void set_activity(expr* lit, double activity) = 0;
|
||||
|
||||
class scoped_push {
|
||||
solver& s;
|
||||
bool m_nopop;
|
||||
|
|
|
@ -127,6 +127,10 @@ public:
|
|||
return m_base->get_trail();
|
||||
}
|
||||
|
||||
void set_activity(expr* var, double activity) override {
|
||||
m_base->set_activity(var, activity);
|
||||
}
|
||||
|
||||
lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
|
||||
SASSERT(!m_pushed || get_scope_level() > 0);
|
||||
m_proof.reset();
|
||||
|
|
|
@ -93,6 +93,11 @@ public:
|
|||
throw default_exception("cannot retrieve trail from solvers created using tactcis");
|
||||
}
|
||||
|
||||
void set_activity(expr* var, double activity) override {
|
||||
throw default_exception("cannot set activity for solvers created using tactcis");
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
ast_manager& tactic2solver::get_manager() const { return m_assertions.get_manager(); }
|
||||
|
|
|
@ -161,6 +161,10 @@ public:
|
|||
expr_ref_vector get_trail() override {
|
||||
return m_solver->get_trail();
|
||||
}
|
||||
void set_activity(expr* var, double activity) override {
|
||||
m_solver->set_activity(var, activity);
|
||||
}
|
||||
|
||||
model_converter* external_model_converter() const {
|
||||
return concat(mc0(), local_model_converter());
|
||||
}
|
||||
|
|
|
@ -186,6 +186,10 @@ public:
|
|||
return m_solver->get_trail();
|
||||
}
|
||||
|
||||
void set_activity(expr* var, double activity) override {
|
||||
m_solver->set_activity(var, activity);
|
||||
}
|
||||
|
||||
unsigned get_num_assertions() const override {
|
||||
return m_solver->get_num_assertions();
|
||||
}
|
||||
|
|
|
@ -96,6 +96,7 @@ public:
|
|||
if (mc) (*mc)(mdl);
|
||||
}
|
||||
}
|
||||
|
||||
void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
|
||||
m_solver->get_levels(vars, depth);
|
||||
}
|
||||
|
@ -104,9 +105,14 @@ public:
|
|||
return m_solver->get_trail();
|
||||
}
|
||||
|
||||
void set_activity(expr* var, double activity) override {
|
||||
m_solver->set_activity(var, activity);
|
||||
}
|
||||
|
||||
model_converter* external_model_converter() const{
|
||||
return concat(mc0(), local_model_converter());
|
||||
}
|
||||
|
||||
model_converter_ref get_model_converter() const override {
|
||||
model_converter_ref mc = external_model_converter();
|
||||
mc = concat(mc.get(), m_solver->get_model_converter().get());
|
||||
|
|
Loading…
Reference in a new issue