From 31e16c7d60fd6b8e540414d79b1addaa7ab21599 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Apr 2020 20:20:33 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/smt/theory_utvpi_def.h | 123 ++++++++++++++----------------------- src/util/vector.h | 4 +- 2 files changed, 48 insertions(+), 79 deletions(-) diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index bac0114d7..1d72d5e1c 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -47,8 +47,7 @@ Revision History: --*/ -#ifndef THEORY_UTVPI_DEF_H_ -#define THEORY_UTVPI_DEF_H_ +#pragma once #include "smt/theory_utvpi.h" #include "util/heap.h" #include "ast/ast_pp.h" @@ -59,20 +58,20 @@ namespace smt { template theory_utvpi::theory_utvpi(ast_manager& m): - theory(m.mk_family_id("arith")), - a(m), - m_arith_eq_adapter(*this, m_params, a), - m_izero(null_theory_var), - m_rzero(null_theory_var), - m_nc_functor(*this), - m_asserted_qhead(0), - m_agility(0.5), - m_lia(false), - m_lra(false), - m_non_utvpi_exprs(false), - m_test(m), - m_factory(nullptr) { - } + theory(m.mk_family_id("arith")), + a(m), + m_arith_eq_adapter(*this, m_params, a), + m_izero(null_theory_var), + m_rzero(null_theory_var), + m_nc_functor(*this), + m_asserted_qhead(0), + m_agility(0.5), + m_lia(false), + m_lra(false), + m_non_utvpi_exprs(false), + m_test(m), + m_factory(nullptr) { + } template theory_utvpi::~theory_utvpi() { @@ -150,7 +149,7 @@ namespace smt { template void theory_utvpi::new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just) { - rational k; + rational k(0); th_var s = expand(true, v1, k); th_var t = expand(false, v2, k); context& ctx = get_context(); @@ -168,26 +167,23 @@ namespace smt { // Create equality ast, internalize_atom // assign the corresponding equality literal. // + // t1 - s1 = k + // app_ref eq(m), s2(m), t2(m); app* s1 = get_enode(s)->get_owner(); app* t1 = get_enode(t)->get_owner(); s2 = a.mk_sub(t1, s1); t2 = a.mk_numeral(k, m.get_sort(s2.get())); - // t1 - s1 = k eq = m.mk_eq(s2.get(), t2.get()); - TRACE("utvpi", - tout << v1 << " .. " << v2 << "\n"; - tout << mk_pp(eq.get(), m) <<"\n";); + TRACE("utvpi", tout << v1 << " .. " << v2 << "\n" << eq << "\n";); - if (!internalize_atom(eq.get(), false)) { - UNREACHABLE(); - } + VERIFY (internalize_atom(eq.get(), false)); literal l(ctx.get_literal(eq.get())); if (!is_eq) { - l = ~l; + l.neg(); } ctx.assign(l, b_justification(&eq_just), false); } @@ -207,22 +203,8 @@ namespace smt { inc_conflicts(); literal_vector const& lits = m_nc_functor.get_lits(); context & ctx = get_context(); - IF_VERBOSE(2, - verbose_stream() << "conflict:\n"; - for (unsigned i = 0; i < lits.size(); ++i) { - ast_manager& m = get_manager(); - expr_ref e(m); - ctx.literal2expr(lits[i], e); - verbose_stream() << mk_pp(e, m) << "\n"; - } - verbose_stream() << "\n";); - TRACE("utvpi", - tout << "conflict: "; - for (unsigned i = 0; i < lits.size(); ++i) { - ctx.display_literal_info(tout, lits[i]); - } - tout << "\n"; - ); + IF_VERBOSE(2, ctx.display_literals_smt2(verbose_stream() << "conflict:\n", lits)); + TRACE("utvpi", ctx.display_literals_smt2(tout << "conflict:\n", lits);); if (m_params.m_arith_dump_lemmas) { symbol logic(m_lra ? (m_lia?"QF_LIRA":"QF_LRA") : "QF_LIA"); @@ -248,14 +230,15 @@ namespace smt { template void theory_utvpi::found_non_utvpi_expr(expr* n) { - if (!m_non_utvpi_exprs) { - std::stringstream msg; - msg << "found non utvpi logic expression:\n" << mk_pp(n, get_manager()) << "\n"; - TRACE("utvpi", tout << msg.str();); - warning_msg("%s", msg.str().c_str()); - get_context().push_trail(value_trail(m_non_utvpi_exprs)); - m_non_utvpi_exprs = true; + if (m_non_utvpi_exprs) { + return; } + std::stringstream msg; + msg << "found non utvpi logic expression:\n" << mk_pp(n, get_manager()) << "\n"; + TRACE("utvpi", tout << msg.str();); + warning_msg("%s", msg.str().c_str()); + get_context().push_trail(value_trail(m_non_utvpi_exprs)); + m_non_utvpi_exprs = true; } template @@ -283,8 +266,8 @@ namespace smt { */ template void theory_utvpi::negate(coeffs& coeffs, rational& weight) { - for (unsigned i = 0; i < coeffs.size(); ++i) { - coeffs[i].second.neg(); + for (auto& c : coeffs) { + c.second.neg(); } weight.neg(); } @@ -303,8 +286,8 @@ namespace smt { void theory_utvpi::mk_coeffs(vector > const& terms, coeffs& coeffs, rational& w) { coeffs.reset(); w = m_test.get_weight(); - for (unsigned i = 0; i < terms.size(); ++i) { - coeffs.push_back(std::make_pair(mk_var(terms[i].first), terms[i].second)); + for (auto const& t : terms) { + coeffs.push_back(std::make_pair(mk_var(t.first), t.second)); } } @@ -475,8 +458,8 @@ namespace smt { template void theory_utvpi::display(std::ostream& out) const { - for (unsigned i = 0; i < m_atoms.size(); ++i) { - m_atoms[i].display(*this, out); out << "\n"; + for (auto const& a : m_atoms) { + a.display(*this, out); out << "\n"; } m_graph.display(out); } @@ -775,12 +758,9 @@ namespace smt { TRACE("utvpi", tout << "Disparity: " << v1 << "\n"; - for (auto v : zero_v) { - tout << "decrement: " << v << "\n"; - } + tout << "decrement: " << zero_v << "\n"; display(tout); ); - SASSERT(m_graph.is_feasible()); for (auto v : zero_v) { m_graph.inc_assignment(v, numeral(-1)); @@ -788,8 +768,9 @@ namespace smt { if (!is_parity_ok(k)) { todo.push_back(k); } - } + } TRACE("utvpi", display(tout);); + SASSERT(m_graph.is_feasible()); } DEBUG_CODE( for (unsigned i = 0; i < sz; ++i) { @@ -820,8 +801,8 @@ namespace smt { void theory_utvpi::model_validate() { context& ctx = get_context(); unsigned sz = m_atoms.size(); - for (unsigned i = 0; i < sz; ++i) { - bool_var b = m_atoms[i].get_bool_var(); + for (auto const& a : m_atoms) { + bool_var b = a.get_bool_var(); if (!ctx.is_relevant(b)) { continue; } @@ -841,20 +822,11 @@ namespace smt { CTRACE("utvpi", !ok, tout << "validation failed:\n"; tout << "Assignment: " << assign << "\n"; - m_atoms[i].display(*this, tout); + a.display(*this, tout); tout << "\n"; display(tout); m_graph.display_agl(tout); ); - if (!ok) { - std::cout << "validation failed:\n"; - std::cout << "Assignment: " << assign << "\n"; - m_atoms[i].display(*this, std::cout); - std::cout << "\n"; - display(std::cout); - m_graph.display_agl(std::cout); - - } // CTRACE("utvpi", ok, tout << "validation success: " << mk_pp(e, get_manager()) << "\n";); SASSERT(ok); } @@ -888,16 +860,12 @@ namespace smt { } if (a.is_add(e)) { r.reset(); - for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { - r += eval_num(to_app(e)->get_arg(i)); - } + for (expr* arg : *to_app(e)) r+= eval_num(arg); return r; } if (a.is_mul(e)) { r = rational(1); - for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { - r *= eval_num(to_app(e)->get_arg(i)); - } + for (expr* arg : *to_app(e)) r*= eval_num(arg); return r; } if (a.is_uminus(e, e1)) { @@ -986,5 +954,4 @@ namespace smt { }; -#endif diff --git a/src/util/vector.h b/src/util/vector.h index 9e2e35acc..4ba5d929b 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -32,11 +32,13 @@ using char_vector = old_svector; using signed_char_vector = old_svector; using double_vector = old_svector; -inline std::ostream& operator<<(std::ostream& out, unsigned_vector const& v) { +template +inline std::ostream& operator<<(std::ostream& out, old_svector const& v) { for (unsigned u : v) out << u << " "; return out; } + template struct vector_hash_tpl { Hash m_hash;