mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

update model during Lex

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-07-06 17:33:54 +02:00
parent 519c9dba25
commit 53f82e3239
3 changed files with 11 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/opt/hitting_sets.cpp
View file

@ -204,7 +204,7 @@ namespace opt {
set_conflict(0, justification(justification::AXIOM));
}
else if (sz == 1) {
IF_VERBOSE(1, verbose_stream() << "unit literal : " << S[0] << " " << val << "\n";);
IF_VERBOSE(2, verbose_stream() << "unit literal : " << S[0] << " " << val << "\n";);
assign(S[0], val, justification(justification::AXIOM));
}
else {
@ -221,6 +221,7 @@ namespace opt {
inc_score(clause_id);
}
TRACE("opt", display(tout, j););
IF_VERBOSE(1, if (!sign) display(verbose_stream(), j););
if (!sign && m_enable_simplex) {
add_simplex_row(!sign, sz, S);
}
@ -246,6 +247,7 @@ namespace opt {
pop(scope_lvl());
IF_VERBOSE(1, verbose_stream() << "(hsmax.negated-size: " << fsz << ")\n";);
#if 0
// garbage collect agressively on exit.
// all learned clases for negative branches are

4
src/opt/opt_context.cpp
View file

@ -269,6 +269,9 @@ namespace opt {
if (r == l_true && !get_lower_as_num(i).is_finite()) {
return r;
}
if (r == l_true && i + 1 < m_objectives.size()) {
update_lower(true);
}
}
DEBUG_CODE(if (r == l_true) validate_lex(););
return r;
@ -841,6 +844,7 @@ namespace opt {
switch(obj.m_type) {
case O_MAXSMT: {
rational r = m_maxsmts.find(obj.m_id)->get_upper();
TRACE("opt", tout << "maxsmt: " << r << " negate: " << obj.m_neg << " offset: " << obj.m_offset << "\n";);
if (obj.m_neg) r.neg();
r += obj.m_offset;
return inf_eps(r);

8
src/opt/weighted_maxsat.cpp
View file

@ -701,9 +701,9 @@ namespace opt {
TRACE("opt", tout << "no more cores\n";);
m_lower = m_upper;
return l_true;
}
}
return l_true;
}
}
return l_true;
}
private:
@ -785,7 +785,7 @@ namespace opt {
switch (is_sat) {
case l_true:
if (lower > m_lower) {
m_lower = lower;
m_lower = lower;
}
return true;
case l_false: