mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix java compilation bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-01-16 08:08:51 +05:30
parent 05b7aa3ebb
commit 41ad1d50f9
3 changed files with 55 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/java/Context.java
View file

@ -383,7 +383,7 @@ public class Context extends IDisposable
**/
public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
{
return Expr.Create
return Expr.create
(this,
Native.datatypeUpdateField
(nCtx(), field.getNativeObject(),

7
src/smt/theory_arith_core.h
View file

@ -1270,7 +1270,9 @@ namespace smt {
result = FC_GIVEUP;
break;
case FC_CONTINUE:
TRACE("final_check_arith", tout << "continue arith...\n";);
TRACE("final_check_arith",
tout << "continue arith..."
<< (get_context().inconsistent()?"inconsistent\n":"\n"););
return FC_CONTINUE;
}
}
@ -2333,7 +2335,8 @@ namespace smt {
b2->push_justification(ante, numeral(1), coeffs_enabled());
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, is_int(b1->get_var()), "farkas");
TRACE("arith_conflict", tout << "bound conflict\n";);
TRACE("arith_conflict", tout << "bound conflict v" << b1->get_var() << "\n";
tout << "bounds: " << b1 << " " << b2 << "\n";);
}
// -----------------------------------

71
src/smt/theory_arith_nl.h
View file

@ -897,31 +897,54 @@ namespace smt {
m_tmp_lit_set.reset();
m_tmp_eq_set.reset();
bool found_zero = false;
SASSERT(is_pure_monomial(m));
for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i);
if (!found_zero) {
theory_var _var = expr2var(arg);
if (is_fixed(_var)) {
bound * l = lower(_var);
bound * u = upper(_var);
if (l->get_value().is_zero()) {
/* if zero was found, then it is the explanation */
SASSERT(k.is_zero());
found_zero = true;
m_tmp_lit_set.reset();
m_tmp_eq_set.reset();
new_lower->m_lits.reset();
new_lower->m_eqs.reset();
}
accumulate_justification(*l, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
accumulate_justification(*u, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
}
}
}
bool found_zero = false;
for (unsigned i = 0; !found_zero && i < to_app(m)->get_num_args(); i++) {
expr * arg = to_app(m)->get_arg(i);
theory_var _var = expr2var(arg);
if (is_fixed(_var)) {
bound * l = lower(_var);
bound * u = upper(_var);
if (l->get_value().is_zero()) {
/* if zero was found, then it is the explanation */
SASSERT(k.is_zero());
found_zero = true;
m_tmp_lit_set.reset();
m_tmp_eq_set.reset();
new_lower->m_lits.reset();
new_lower->m_eqs.reset();
}
accumulate_justification(*l, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
TRACE("non_linear",
for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_lower->m_lits[j]);
tout << " ";
}
tout << "\n";);
accumulate_justification(*u, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set);
TRACE("non_linear",
for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_lower->m_lits[j]);
tout << " ";
}
tout << "\n";);
}
}
new_upper->m_lits.append(new_lower->m_lits);
new_upper->m_eqs.append(new_lower->m_eqs);
TRACE("non_linear",
tout << "lower: " << new_lower << " upper: " << new_upper << "\n";
for (unsigned j = 0; j < new_upper->m_lits.size(); ++j) {
ctx.display_detailed_literal(tout, new_upper->m_lits[j]);
tout << " ";
}
tout << "\n";);
return true;
}
@ -1887,6 +1910,10 @@ namespace smt {
derived_bound b(null_theory_var, inf_numeral(0), B_LOWER);
dependency2new_bound(d, b);
set_conflict(b.m_lits.size(), b.m_lits.c_ptr(), b.m_eqs.size(), b.m_eqs.c_ptr(), ante, is_lia, "arith_nl");
TRACE("non_linear",
for (unsigned i = 0; i < b.m_lits.size(); ++i) {
tout << b.m_lits[i] << " ";
});
}
/**