mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

check for 0

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-22 10:43:50 -07:00
parent 640cf1809d
commit dd5e2e8930
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/api/ml/z3.mli
View file

@ -2862,6 +2862,9 @@ sig
val get_decls : model -> FuncDecl.func_decl list
(** Evaluates an expression in the current model.
The Boolean argument indicates whether to apply model completion.
When model completion is true it will assign an interpretation for
constants and functions that do not have an interpretation in the model.
This function may fail if the argument contains quantifiers,
is partial (MODEL_PARTIAL enabled), or if it is not well-sorted.

3
src/sat/sat_solver.cpp
View file

@ -3974,7 +3974,8 @@ namespace sat {
double multiplier = m_config.m_reward_offset * (is_sat ? m_config.m_reward_multiplier : 1.0);
for (unsigned i = qhead; i < m_trail.size(); ++i) {
auto v = m_trail[i].var();
auto reward = multiplier / (m_stats.m_conflict - m_last_conflict[v] + 1);
auto d = std::max(1ull,m_stats.m_conflict - m_last_conflict[v] + 1);
auto reward = multiplier / d;
auto activity = m_activity[v];
set_activity(v, static_cast<unsigned>(m_step_size * reward + ((1.0 - m_step_size) * activity)));
}