mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
remove internal referenes to set_activity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
fc4c162e31
commit
8893913c98
|
@ -124,7 +124,6 @@ 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,7 +110,6 @@ 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);
|
||||
|
|
|
@ -336,16 +336,6 @@ 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) {
|
||||
v = m_solver.add_var(true);
|
||||
m_map.insert(var, v);
|
||||
}
|
||||
m_solver.set_activity(v, static_cast<unsigned>(activity));
|
||||
}
|
||||
|
||||
proof * get_proof() override {
|
||||
UNREACHABLE();
|
||||
return nullptr;
|
||||
|
|
|
@ -203,10 +203,6 @@ 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,11 +328,6 @@ 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,8 +251,6 @@ 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,10 +127,6 @@ 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,10 +93,6 @@ 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");
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
|
|
@ -161,9 +161,6 @@ 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,10 +186,6 @@ 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();
|
||||
}
|
||||
|
|
|
@ -105,10 +105,6 @@ 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());
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue