From 41ad1d50f9097b1c7c90fb84773702eacb946b2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 Jan 2015 08:08:51 +0530 Subject: [PATCH] fix java compilation bug Signed-off-by: Nikolaj Bjorner --- src/api/java/Context.java | 2 +- src/smt/theory_arith_core.h | 7 ++-- src/smt/theory_arith_nl.h | 71 +++++++++++++++++++++++++------------ 3 files changed, 55 insertions(+), 25 deletions(-) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index d52edfb82..a3b24c5d0 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -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(), diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index a97c82369..264eb0f10 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -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";); } // ----------------------------------- diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 6a7017a29..cace15db4 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -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] << " "; + }); } /**