mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 04:41:21 +00:00
Code Activity

remove invocation of debugger

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-12 17:07:44 -04:00
parent 559af09b07
commit 0bca2aabff
4 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/ast.cpp
View file

@ -1119,7 +1119,6 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
} }
std::ostringstream buffer; std::ostringstream buffer;
buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible"; buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible";
INVOKE_DEBUGGER();
throw ast_exception(buffer.str()); throw ast_exception(buffer.str());
} }

6
src/nlsat/nlsat_solver.cpp
View file

@ -995,7 +995,7 @@ namespace nlsat {
unsigned sz = cls.size(); unsigned sz = cls.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
literal l = cls[i]; literal l = cls[i];
SASSERT(m_atoms[l.var()] == 0); SASSERT(m_atoms[l.var()] == nullptr);
SASSERT(value(l) != l_true); SASSERT(value(l) != l_true);
if (value(l) == l_false) if (value(l) == l_false)
continue; continue;
@ -1085,13 +1085,13 @@ namespace nlsat {
checkpoint(); checkpoint();
if (value(l) == l_false) if (value(l) == l_false)
continue; continue;
TRACE("nlsat_inf_set", tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l); tout << "\n";);
SASSERT(value(l) == l_undef); SASSERT(value(l) == l_undef);
SASSERT(max_var(l) == m_xk); SASSERT(max_var(l) == m_xk);
bool_var b = l.var(); bool_var b = l.var();
atom * a = m_atoms[b]; atom * a = m_atoms[b];
SASSERT(a != nullptr); SASSERT(a != nullptr);
interval_set_ref curr_set(m_ism); interval_set_ref curr_set(m_ism);
TRACE("nlsat_inf_set", tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l); tout << "\n";);
curr_set = m_evaluator.infeasible_intervals(a, l.sign()); curr_set = m_evaluator.infeasible_intervals(a, l.sign());
TRACE("nlsat_inf_set", tout << "infeasible set for literal: "; display(tout, l); tout << "\n"; m_ism.display(tout, curr_set); tout << "\n";); TRACE("nlsat_inf_set", tout << "infeasible set for literal: "; display(tout, l); tout << "\n"; m_ism.display(tout, curr_set); tout << "\n";);
if (m_ism.is_empty(curr_set)) { if (m_ism.is_empty(curr_set)) {
@ -1151,7 +1151,7 @@ namespace nlsat {
If satisfy_learned is true, then (arithmetic) learned clauses are satisfied even if m_lazy > 0 If satisfy_learned is true, then (arithmetic) learned clauses are satisfied even if m_lazy > 0
*/ */
bool process_clause(clause const & cls, bool satisfy_learned) { bool process_clause(clause const & cls, bool satisfy_learned) {
TRACE("nlsat", display(tout << "processing clause: ", cls) << "sat: " << is_satisfied(cls) << "\n";); TRACE("nlsat", display(tout << "processing clause: ", cls) << " sat: " << is_satisfied(cls) << "\n";);
if (is_satisfied(cls)) if (is_satisfied(cls))
return true; return true;
if (m_xk == null_var) if (m_xk == null_var)

1
src/nlsat/tactic/goal2nlsat.cpp
View file

@ -251,6 +251,7 @@ struct goal2nlsat::imp {
} }
void operator()(goal const & g) { void operator()(goal const & g) {
TRACE("goal2nlsat", g.display(tout););
if (has_term_ite(g)) if (has_term_ite(g))
throw tactic_exception("eliminate term-ite before applying nlsat"); throw tactic_exception("eliminate term-ite before applying nlsat");
unsigned sz = g.size(); unsigned sz = g.size();

2
src/qe/nlqsat.cpp
View file

@ -165,7 +165,7 @@ namespace qe {
lits.push_back(~l); lits.push_back(~l);
break; break;
default: default:
UNREACHABLE(); lits.push_back(l);
break; break;
} }
} }