From 988e8afc2ec98013a3c83a71b55a4a943ceb99f1 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Mon, 3 Dec 2018 13:50:48 +0100 Subject: [PATCH 01/16] support for logging congruence closure equality explanations when commutativity is used --- src/smt/smt_quantifier.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index f74c9d4c9..f7af9bd51 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -172,7 +172,12 @@ namespace smt { break; } else { - out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n"; + + // The e-graph only supports commutativity for binary functions + out << "[eq-expl] #" << en->get_owner_id() + << " cg (#" << en->get_arg(0)->get_owner_id() << " #" << target->get_arg(1)->get_owner_id() + << ") (#" << en->get_arg(1)->get_owner_id() << " #" << target->get_arg(0)->get_owner_id() + << ") ; #" << target->get_owner_id() << "\n"; break; } case smt::eq_justification::kind::JUSTIFICATION: From 0870760eb5d8c160dd2423fed77a53635e04e3ae Mon Sep 17 00:00:00 2001 From: Nils Becker Date: Mon, 3 Dec 2018 22:39:29 +0100 Subject: [PATCH 02/16] logging meaning of theory specific constants --- src/ast/arith_decl_plugin.cpp | 27 ++++++++++++++++++++++-- src/ast/ast.cpp | 17 +++++++++++++++ src/ast/ast.h | 11 ++++++++++ src/ast/bv_decl_plugin.cpp | 39 ++++++++++++++++++++++++++++++++++- src/ast/bv_decl_plugin.h | 4 +++- src/ast/fpa_decl_plugin.cpp | 8 ++++++- src/smt/smt_quantifier.cpp | 2 +- 7 files changed, 102 insertions(+), 6 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index cdf18875c..926e515e2 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -89,7 +89,14 @@ app * arith_decl_plugin::mk_numeral(algebraic_numbers::anum const & val, bool is parameter p(idx, true); SASSERT(p.is_external()); func_decl * decl = m_manager->mk_const_decl(m_rootv_sym, m_real_decl, func_decl_info(m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM, 1, &p)); - return m_manager->mk_const(decl); + app * r = m_manager->mk_const(decl); + + if (log_constant_meaning_prelude(r)) { + am().display_root(m_manager->trace_stream(), val); + m_manager->trace_stream() << "\n"; + } + + return r; } } @@ -415,7 +422,12 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { r = m_manager->mk_const(m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p))); m_manager->inc_ref(r); m_small_ints.setx(u_val, r, 0); + + if (log_constant_meaning_prelude(r)) { + m_manager->trace_stream() << u_val << "\n"; + } } + return r; } else { @@ -425,6 +437,10 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { r = m_manager->mk_const(m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p))); m_manager->inc_ref(r); m_small_reals.setx(u_val, r, 0); + + if (log_constant_meaning_prelude(r)) { + m_manager->trace_stream() << u_val << "\n"; + } } return r; } @@ -436,7 +452,14 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { decl = m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p)); else decl = m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p)); - return m_manager->mk_const(decl); + app * r = m_manager->mk_const(decl); + + if (log_constant_meaning_prelude(r)) { + val.display(m_manager->trace_stream()); + m_manager->trace_stream() << "\n"; + } + + return r; } func_decl * arith_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity) { diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 067c4d127..178113ea7 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -662,6 +662,23 @@ ast* ast_table::pop_erase() { // // ----------------------------------- +/** + \brief Checks wether a log is being generated and, if necessary, adds the beginning of an "[attach-meaning]" line + to that log. The theory solver should add some description of the meaning of the term in terms of the theory's + internal reasoning to the end of the line and insert a line break. + + \param a the term that should be described. + + \return true if a log is being generated, false otherwise. +*/ +bool decl_plugin::log_constant_meaning_prelude(app * a) { + if (m_manager->has_trace_stream()) { + m_manager->trace_stream() << "[attach-meaning] #" << a->get_id() << " " << m_manager->get_family_name(m_family_id).str() << " "; + return true; + } + return false; +} + func_decl * decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range) { ptr_buffer sorts; diff --git a/src/ast/ast.h b/src/ast/ast.h index b81db5196..9c6c811b0 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -998,6 +998,17 @@ protected: virtual void inherit(decl_plugin* other_p, ast_translation& ) { } + /** + \brief Checks wether a log is being generated and, if necessary, adds the beginning of an "[attach-meaning]" line + to that log. The theory solver should add some description of the meaning of the term in terms of the theory's + internal reasoning to the end of the line and insert a line break. + + \param a the term that should be described. + + \return true if a log is being generated, false otherwise. + */ + bool log_constant_meaning_prelude(app * a); + friend class ast_manager; public: diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 6bbe3ce13..1ad25dc46 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -864,7 +864,15 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const { app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { parameter p[2] = { parameter(val), parameter(static_cast(bv_size)) }; - return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr); + app * r = m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr); + + if (m_plugin->log_constant_meaning_prelude(r)) { + m_manager.trace_stream() << "(" << bv_size << " #d"; + val.display(m_manager.trace_stream()); + m_manager.trace_stream() << ")\n"; + } + + return r; } sort * bv_util::mk_sort(unsigned bv_size) { @@ -883,3 +891,32 @@ app * bv_util::mk_bv2int(expr* e) { parameter p(s); return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e); } + + +app * bv_util::mk_bv(unsigned n, expr* const* es) { + app * r = m_manager.mk_app(get_fid(), OP_MKBV, n, es); + + if (m_plugin->log_constant_meaning_prelude(r)) { + m_manager.trace_stream() << "(" << n << " #x"; + + m_manager.trace_stream() << std::hex; + uint8_t hexDigit = 0; + unsigned curLength = (4 - n % 4) % 4; + for (unsigned i = 0; i < n; ++i) { + hexDigit << 1; + ++curLength; + if (m_manager.is_true(es[i])) { + hexDigit |= 1; + } + if (curLength == 4) { + m_manager.trace_stream() << hexDigit; + hexDigit = 0; + } + } + m_manager.trace_stream() << std::dec; + + m_manager.trace_stream() << ")\n"; + } + + return r; + } \ No newline at end of file diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 0d4d4d8be..3e087f63f 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -238,6 +238,8 @@ protected: func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity); void get_offset_term(app * a, expr * & t, rational & offset) const; + + friend class bv_util; public: bv_decl_plugin(); @@ -432,7 +434,7 @@ public: app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); } app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); } - app * mk_bv(unsigned n, expr* const* es) { return m_manager.mk_app(get_fid(), OP_MKBV, n, es); } + app * mk_bv(unsigned n, expr* const* es); }; diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index c0caaa3ca..2baf4b158 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -92,7 +92,13 @@ func_decl * fpa_decl_plugin::mk_numeral_decl(mpf const & v) { } app * fpa_decl_plugin::mk_numeral(mpf const & v) { - return m_manager->mk_const(mk_numeral_decl(v)); + app * r = m_manager->mk_const(mk_numeral_decl(v)); + + if (log_constant_meaning_prelude(r)) { + m_manager->trace_stream() << "(" << m_fm.to_string(v) << ")\n"; + } + + return r; } bool fpa_decl_plugin::is_numeral(expr * n, mpf & val) { diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index f7af9bd51..4c855a71d 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -210,7 +210,7 @@ namespace smt { get_stat(q)->update_max_generation(max_generation); fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def); if (f) { - if (has_trace_stream()) { + if (has_trace_stream() && pat != nullptr) { std::ostream & out = trace_stream(); obj_hashtable already_visited; From 6d2cf4f464d5fec4dbae1afe907c9d077664ee81 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Mon, 10 Dec 2018 22:49:08 +0100 Subject: [PATCH 03/16] smt-like logging of theory specific meaning of constants --- src/ast/arith_decl_plugin.cpp | 5 +- src/ast/bv_decl_plugin.cpp | 129 ++++++++++++++++++++++++++++------ src/ast/fpa_decl_plugin.cpp | 3 +- src/util/mpz.h | 2 + src/util/rational.h | 2 + 5 files changed, 115 insertions(+), 26 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 926e515e2..883e004a7 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -92,7 +92,7 @@ app * arith_decl_plugin::mk_numeral(algebraic_numbers::anum const & val, bool is app * r = m_manager->mk_const(decl); if (log_constant_meaning_prelude(r)) { - am().display_root(m_manager->trace_stream(), val); + am().display_root_smt2(m_manager->trace_stream(), val); m_manager->trace_stream() << "\n"; } @@ -427,7 +427,6 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { m_manager->trace_stream() << u_val << "\n"; } } - return r; } else { @@ -455,7 +454,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { app * r = m_manager->mk_const(decl); if (log_constant_meaning_prelude(r)) { - val.display(m_manager->trace_stream()); + val.display_smt2(m_manager->trace_stream()); m_manager->trace_stream() << "\n"; } diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 1ad25dc46..ce75cd90e 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -17,12 +17,22 @@ Revision History: --*/ #include +#include +#include #include "ast/bv_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "util/warning.h" #include "ast/ast_pp.h" #include "ast/ast_smt2_pp.h" +#if defined(_MP_INTERNAL) +#include "util/mpn.h" +#elif defined(_MP_GMP) +#include +#else +#error No multi-precision library selected. +#endif + bv_decl_plugin::bv_decl_plugin(): m_bv_sym("bv"), m_concat_sym("concat"), @@ -867,9 +877,71 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { app * r = m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr); if (m_plugin->log_constant_meaning_prelude(r)) { - m_manager.trace_stream() << "(" << bv_size << " #d"; - val.display(m_manager.trace_stream()); - m_manager.trace_stream() << ")\n"; + std::ios fmt(nullptr); + fmt.copyfmt(m_manager.trace_stream()); + SASSERT(val.is_int()); + if (val.is_small()) { + if (bv_size % 4 == 0) { + m_manager.trace_stream() << "#x" << std::hex << std::setw(bv_size/4) << std::setfill('0') << val << "\n"; + } else { + m_manager.trace_stream() << "#b" << std::bitset(val.get_unsigned()).to_string().substr(sizeof(unsigned)*8 - bv_size) << "\n"; + } + return r; + } +#ifndef _MP_GMP + digit_t *digits = mpz_manager::digits(val.to_mpq().numerator()); + unsigned size = mpz_manager::size(val.to_mpq().numerator()); + if (bv_size % 4 == 0) { + m_manager.trace_stream() << "#x" << std::hex; + unsigned bitSize = size * sizeof(digit_t) * 8; + if (bv_size > bitSize) { + for (unsigned i = 0; i < (bv_size - bitSize)/4; ++i) { + m_manager.trace_stream() << 0; + } + } + m_manager.trace_stream() << digits[size-1] << std::setw(sizeof(digit_t)*2) << std::setfill('0'); + for (unsigned i = 1; i < size; ++i) { + m_manager.trace_stream() << digits[size-i-1]; + } + m_manager.trace_stream() << "\n"; + } else { + m_manager.trace_stream() << "#b"; + const unsigned digitBitSize = sizeof(digit_t) * 8; + unsigned bitSize = size * digitBitSize; + unsigned firstDigitLength; + if (bv_size > bitSize) { + firstDigitLength = 0; + for (unsigned i = 0; i < (bv_size - bitSize)/4; ++i) { + m_manager.trace_stream() << 0; + } + } else { + firstDigitLength = bv_size % digitBitSize; + } + for (unsigned i = 0; i < size; ++i) { + if (i == 0 && firstDigitLength != 0) { + m_manager.trace_stream() << std::bitset(digits[size-1]).to_string().substr(digitBitSize - firstDigitLength); + } else { + m_manager.trace_stream() << std::bitset(digits[size-i-1]); + } + } + m_manager.trace_stream() << "\n"; + } +#else + // GMP version + const unsigned base = bv_size % 4 == 0 ? 16 : 2; + size_t sz = mpz_sizeinbase(*(val.to_mpq().numerator().m_ptr), base) + 2; + unsigned requiredLength = bv_size / (base == 16 ? 4 : 1); + unsigned padding = requiredLength > sz ? requiredLength - sz : 0; + sbuffer buffer(sz, 0); + mpz_get_str(buffer.c_ptr(), base, *(val.to_mpq().numerator().m_ptr)); + m_manager.trace_stream() << (base == 16 ? "#x" : "#b"); + for (unsigned i = 0; i < padding; ++i) { + m_manager.trace_stream() << 0; + } + m_manager.trace_stream() << buffer.c_ptr() << "\n"; +#endif + m_manager.trace_stream().copyfmt(fmt); + m_manager.trace_stream() << std::dec; } return r; @@ -892,30 +964,43 @@ app * bv_util::mk_bv2int(expr* e) { return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e); } - app * bv_util::mk_bv(unsigned n, expr* const* es) { app * r = m_manager.mk_app(get_fid(), OP_MKBV, n, es); - if (m_plugin->log_constant_meaning_prelude(r)) { - m_manager.trace_stream() << "(" << n << " #x"; - - m_manager.trace_stream() << std::hex; - uint8_t hexDigit = 0; - unsigned curLength = (4 - n % 4) % 4; + if (m_manager.has_trace_stream()) { for (unsigned i = 0; i < n; ++i) { - hexDigit << 1; - ++curLength; - if (m_manager.is_true(es[i])) { - hexDigit |= 1; - } - if (curLength == 4) { - m_manager.trace_stream() << hexDigit; - hexDigit = 0; - } - } - m_manager.trace_stream() << std::dec; + if (!m_manager.is_true(es[i]) && !m_manager.is_true(es[i])) + return r; + } - m_manager.trace_stream() << ")\n"; + if (m_plugin->log_constant_meaning_prelude(r)) { + if (n % 4 == 0) { + m_manager.trace_stream() << " #x"; + + m_manager.trace_stream() << std::hex; + uint8_t hexDigit = 0; + unsigned curLength = (4 - n % 4) % 4; + for (unsigned i = 0; i < n; ++i) { + hexDigit << 1; + ++curLength; + if (m_manager.is_true(es[i])) { + hexDigit |= 1; + } + if (curLength == 4) { + m_manager.trace_stream() << hexDigit; + hexDigit = 0; + } + } + m_manager.trace_stream() << std::dec; + } else { + m_manager.trace_stream() << " #b"; + for (unsigned i = 0; i < n; ++i) { + m_manager.trace_stream() << (m_manager.is_true(es[i]) ? 1 : 0); + } + } + + m_manager.trace_stream() << ")\n"; + } } return r; diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 2baf4b158..1e693b29a 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -95,7 +95,8 @@ app * fpa_decl_plugin::mk_numeral(mpf const & v) { app * r = m_manager->mk_const(mk_numeral_decl(v)); if (log_constant_meaning_prelude(r)) { - m_manager->trace_stream() << "(" << m_fm.to_string(v) << ")\n"; + m_fm.display_smt2(m_manager->trace_stream(), v, false); + m_manager->trace_stream() << "\n"; } return r; diff --git a/src/util/mpz.h b/src/util/mpz.h index 2df03666f..c258a1e62 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -99,6 +99,7 @@ class mpz { friend class mpbq; friend class mpbq_manager; friend class mpz_stack; + friend class bv_util; mpz & operator=(mpz const & other) { UNREACHABLE(); return *this; } public: mpz(int v):m_val(v), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {} @@ -134,6 +135,7 @@ inline void swap(mpz & m1, mpz & m2) { m1.swap(m2); } template class mpz_manager { + friend class bv_util; mutable small_object_allocator m_allocator; mutable omp_nest_lock_t m_lock; #define MPZ_BEGIN_CRITICAL() if (SYNCH) omp_set_nest_lock(&m_lock); diff --git a/src/util/rational.h b/src/util/rational.h index 3403848c4..dc805511f 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -93,6 +93,8 @@ public: void display_decimal(std::ostream & out, unsigned prec, bool truncate = false) const { return m().display_decimal(out, m_val, prec, truncate); } + void display_smt2(std::ostream & out) const { return m().display_smt2(out, m_val, false); } + bool is_uint64() const { return m().is_uint64(m_val); } bool is_int64() const { return m().is_int64(m_val); } From 58def55796aa53f8c000629024431cf4ff82bcf1 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Sat, 5 Jan 2019 14:44:06 +0100 Subject: [PATCH 04/16] mbqi support --- src/ast/ast.cpp | 4 +- src/smt/smt_quantifier.cpp | 76 +++++++++++++++++++++----------------- 2 files changed, 45 insertions(+), 35 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 178113ea7..305d91c97 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -28,6 +28,7 @@ Revision History: #include "ast/ast_smt2_pp.h" #include "ast/array_decl_plugin.h" #include "ast/ast_translation.h" +#include "util/z3_version.h" // ----------------------------------- @@ -1364,6 +1365,7 @@ ast_manager::ast_manager(proof_gen_mode m, char const * trace_file, bool is_form if (trace_file) { m_trace_stream = alloc(std::fstream, trace_file, std::ios_base::out); m_trace_stream_owner = true; + *m_trace_stream << "[tool-version] Z3 " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "\n"; } if (!is_format_manager) @@ -2346,7 +2348,7 @@ var * ast_manager::mk_var(unsigned idx, sort * s) { var * r = register_node(new_node); if (m_trace_stream && r == new_node) { - *m_trace_stream << "[mk-var] #" << r->get_id() << "\n"; + *m_trace_stream << "[mk-var] #" << r->get_id() << " " << idx << "\n"; } return r; } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 4c855a71d..7098f2d9c 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -210,44 +210,52 @@ namespace smt { get_stat(q)->update_max_generation(max_generation); fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def); if (f) { - if (has_trace_stream() && pat != nullptr) { - std::ostream & out = trace_stream(); - - obj_hashtable already_visited; - - // In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables - // is used. We need to make sure that all of these equalities appear in the log. - for (unsigned i = 0; i < num_bindings; ++i) { - log_justification_to_root(out, bindings[i], already_visited); - } - - for (auto n : used_enodes) { - enode *orig = std::get<0>(n); - enode *substituted = std::get<1>(n); - if (orig != nullptr) { - log_justification_to_root(out, orig, already_visited); - log_justification_to_root(out, substituted, already_visited); + if (has_trace_stream()) { + if (pat == nullptr) { + trace_stream() << "[mbqi-triggered] " << static_cast(f) << " #" << q->get_id(); + for (unsigned i = 0; i < num_bindings; ++i) { + trace_stream() << " #" << bindings[num_bindings - i - 1]->get_owner_id(); } - } + trace_stream() << "\n"; + } else { + std::ostream & out = trace_stream(); - // At this point all relevant equalities for the match are logged. - out << "[new-match] " << static_cast(f) << " #" << q->get_id() << " #" << pat->get_id(); - for (unsigned i = 0; i < num_bindings; i++) { - // I don't want to use mk_pp because it creates expressions for pretty printing. - // This nasty side-effect may change the behavior of Z3. - out << " #" << bindings[i]->get_owner_id(); - } - out << " ;"; - for (auto n : used_enodes) { - enode *orig = std::get<0>(n); - enode *substituted = std::get<1>(n); - if (orig == nullptr) - out << " #" << substituted->get_owner_id(); - else { - out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")"; + obj_hashtable already_visited; + + // In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables + // is used. We need to make sure that all of these equalities appear in the log. + for (unsigned i = 0; i < num_bindings; ++i) { + log_justification_to_root(out, bindings[i], already_visited); } + + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig != nullptr) { + log_justification_to_root(out, orig, already_visited); + log_justification_to_root(out, substituted, already_visited); + } + } + + // At this point all relevant equalities for the match are logged. + out << "[new-match] " << static_cast(f) << " #" << q->get_id() << " #" << pat->get_id(); + for (unsigned i = 0; i < num_bindings; i++) { + // I don't want to use mk_pp because it creates expressions for pretty printing. + // This nasty side-effect may change the behavior of Z3. + out << " #" << bindings[num_bindings - i - 1]->get_owner_id(); + } + out << " ;"; + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig == nullptr) + out << " #" << substituted->get_owner_id(); + else { + out << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")"; + } + } + out << "\n"; } - out << "\n"; } m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO m_num_instances++; From 3620dfee5e513925a52245715c21db303bb188bc Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Tue, 8 Jan 2019 22:09:32 +0100 Subject: [PATCH 05/16] logging names of quantified variables and updating inst-possible line --- src/ast/ast.cpp | 5 +++++ src/smt/smt_quantifier.cpp | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 305d91c97..ab37a9f40 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2477,6 +2477,11 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s if (m_trace_stream && r == new_node) { trace_quant(*m_trace_stream, r); + *m_trace_stream << "[attach-var-names] #" << r->get_id(); + for (unsigned i = 0; i < num_decls; ++i) { + *m_trace_stream << " " << decl_names[num_decls - i - 1].str(); + } + *m_trace_stream << "\n"; } return r; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 7098f2d9c..a22889b24 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -212,7 +212,7 @@ namespace smt { if (f) { if (has_trace_stream()) { if (pat == nullptr) { - trace_stream() << "[mbqi-triggered] " << static_cast(f) << " #" << q->get_id(); + trace_stream() << "[inst-possible] MBQI " << static_cast(f) << " #" << q->get_id(); for (unsigned i = 0; i < num_bindings; ++i) { trace_stream() << " #" << bindings[num_bindings - i - 1]->get_owner_id(); } From bfb554c0b8e87b094ecde74196061ef1744dc150 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Mon, 14 Jan 2019 21:28:06 +0100 Subject: [PATCH 06/16] logging sorts of quantified variables logging proof objects seperately form regular terms renaming inst-possible -> inst-discovered --- src/ast/ast.cpp | 11 +++++++++-- src/smt/smt_quantifier.cpp | 2 +- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index ab37a9f40..ba5ee5d5a 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2202,7 +2202,14 @@ app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const } if (m_trace_stream && r == new_node) { - *m_trace_stream << "[mk-app] #" << r->get_id() << " "; + if (is_proof(r)) { + if (decl == mk_func_decl(m_basic_family_id, PR_UNDEF, 0, nullptr, 0, static_cast(nullptr))) + return r; + *m_trace_stream << "[mk-proof] #"; + } else { + *m_trace_stream << "[mk-app] #"; + } + *m_trace_stream << r->get_id() << " "; if (r->get_num_args() == 0 && r->get_decl()->get_name() == "int") { ast_ll_pp(*m_trace_stream, *this, r); } @@ -2479,7 +2486,7 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s trace_quant(*m_trace_stream, r); *m_trace_stream << "[attach-var-names] #" << r->get_id(); for (unsigned i = 0; i < num_decls; ++i) { - *m_trace_stream << " " << decl_names[num_decls - i - 1].str(); + *m_trace_stream << " (" << decl_names[num_decls - i - 1].str() << " ; " << decl_sorts[num_decls - i -1]->get_name().str() << ")"; } *m_trace_stream << "\n"; } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index a22889b24..65a6db875 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -212,7 +212,7 @@ namespace smt { if (f) { if (has_trace_stream()) { if (pat == nullptr) { - trace_stream() << "[inst-possible] MBQI " << static_cast(f) << " #" << q->get_id(); + trace_stream() << "[inst-discovered] MBQI " << static_cast(f) << " #" << q->get_id(); for (unsigned i = 0; i < num_bindings; ++i) { trace_stream() << " #" << bindings[num_bindings - i - 1]->get_owner_id(); } From 279413412d9c4fca03569d0ebb37f44457f9d479 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Tue, 15 Jan 2019 01:09:44 +0100 Subject: [PATCH 07/16] preventing operations during MBQI search from being logged --- src/smt/smt_context.cpp | 10 ++++++---- src/smt/smt_context.h | 2 ++ 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 7ee6d4a92..7e7ed14b5 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -59,6 +59,7 @@ namespace smt { m_b_internalized_stack(m), m_e_internalized_stack(m), m_final_check_idx(0), + m_is_auxiliary(false), m_cg_table(m), m_dyn_ack_manager(*this, p), m_is_diseq_tmp(nullptr), @@ -238,6 +239,7 @@ namespace smt { context * context::mk_fresh(symbol const * l, smt_params * p, params_ref const& pa) { context * new_ctx = alloc(context, m_manager, p ? *p : m_fparams, pa); + new_ctx->m_is_auxiliary = true; new_ctx->set_logic(l == nullptr ? m_setup.get_logic() : *l); copy_plugins(*this, *new_ctx); return new_ctx; @@ -1941,7 +1943,7 @@ namespace smt { */ void context::push_scope() { - if (m_manager.has_trace_stream()) + if (m_manager.has_trace_stream() && !m_is_auxiliary) m_manager.trace_stream() << "[push] " << m_scope_lvl << "\n"; m_scope_lvl++; @@ -2392,7 +2394,7 @@ namespace smt { unsigned context::pop_scope_core(unsigned num_scopes) { try { - if (m_manager.has_trace_stream()) + if (m_manager.has_trace_stream() && !m_is_auxiliary) m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n"; TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";); @@ -3326,7 +3328,7 @@ namespace smt { Return true if succeeded. */ bool context::check_preamble(bool reset_cancel) { - if (m_manager.has_trace_stream()) + if (m_manager.has_trace_stream() && !m_is_auxiliary) m_manager.trace_stream() << "[begin-check] " << m_scope_lvl << "\n"; if (memory::above_high_watermark()) { @@ -3941,7 +3943,7 @@ namespace smt { << mk_pp(bool_var2expr(l.var()), m_manager) << "\n"; }); - if (m_manager.has_trace_stream()) { + if (m_manager.has_trace_stream() && !m_is_auxiliary) { m_manager.trace_stream() << "[conflict] "; display_literals(m_manager.trace_stream(), num_lits, lits); m_manager.trace_stream() << "\n"; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 6f382a5f6..7657795bd 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -106,6 +106,8 @@ namespace smt { unsigned m_final_check_idx; // circular counter used for implementing fairness + bool m_is_auxiliary; // used to prevent unwanted information from being logged. + // ----------------------------------- // // Equality & Uninterpreted functions From 28c03ed1de3410bb9d62cae11860db58c79bb286 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Thu, 21 Feb 2019 19:29:35 +0100 Subject: [PATCH 08/16] logging support for theory axioms --- src/ast/ast.cpp | 2 +- src/ast/bv_decl_plugin.cpp | 2 +- src/ast/datatype_decl_plugin.cpp | 41 +++++++ src/ast/datatype_decl_plugin.h | 5 +- src/ast/rewriter/th_rewriter.cpp | 23 ++++ src/smt/smt_internalizer.cpp | 8 -- src/smt/smt_quantifier.cpp | 186 +++++++++++++++---------------- src/smt/smt_quantifier.h | 5 + src/smt/smt_theory.h | 62 +++++++++++ src/smt/theory_arith_aux.h | 4 + src/smt/theory_arith_core.h | 5 + src/smt/theory_arith_int.h | 13 ++- src/smt/theory_arith_nl.h | 3 + src/smt/theory_array_base.cpp | 6 + src/smt/theory_array_full.cpp | 2 + src/smt/theory_bv.cpp | 26 ++++- src/smt/theory_datatype.cpp | 26 +++++ src/smt/theory_diff_logic_def.h | 5 + src/smt/theory_dl.cpp | 4 + src/smt/theory_fpa.cpp | 2 + src/smt/theory_jobscheduler.cpp | 51 ++++++++- src/smt/theory_lra.cpp | 68 ++++++++++- src/smt/theory_recfun.cpp | 17 ++- src/smt/theory_seq.cpp | 62 +++++++++-- src/smt/theory_seq.h | 1 + src/smt/theory_str.cpp | 6 + 26 files changed, 508 insertions(+), 127 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index ba5ee5d5a..0f6a81a59 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2486,7 +2486,7 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s trace_quant(*m_trace_stream, r); *m_trace_stream << "[attach-var-names] #" << r->get_id(); for (unsigned i = 0; i < num_decls; ++i) { - *m_trace_stream << " (" << decl_names[num_decls - i - 1].str() << " ; " << decl_sorts[num_decls - i -1]->get_name().str() << ")"; + *m_trace_stream << " (|" << decl_names[num_decls - i - 1].str() << "| ; |" << decl_sorts[num_decls - i -1]->get_name().str() << "|)"; } *m_trace_stream << "\n"; } diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index ce75cd90e..c4bada552 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -981,7 +981,7 @@ app * bv_util::mk_bv(unsigned n, expr* const* es) { uint8_t hexDigit = 0; unsigned curLength = (4 - n % 4) % 4; for (unsigned i = 0; i < n; ++i) { - hexDigit << 1; + hexDigit <<= 1; ++curLength; if (m_manager.is_true(es[i])) { hexDigit |= 1; diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 9cb685ccc..db3c0e2a0 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -400,6 +400,47 @@ namespace datatype { sort_ref_vector ps(*m_manager); for (symbol const& s : m_def_block) { new_sorts.push_back(m_defs[s]->instantiate(ps)); + if (m_manager->has_trace_stream()) { + symbol const& family_name = m_manager->get_family_name(get_family_id()); + for (constructor const* c : *m_defs[s]) { + func_decl_ref f = c->instantiate(new_sorts.back()); + const unsigned num_args = f->get_arity(); + if (num_args == 0) continue; + for (unsigned i = 0; i < num_args; ++i) { + m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; + ++m_id_counter; + } + const unsigned constructor_id = m_id_counter; + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name(); + for (unsigned i = 0; i < num_args; ++i) { + m_manager->trace_stream() << " " << family_name << "#" << constructor_id - num_args + i; + } + m_manager->trace_stream() << "\n"; + ++m_id_counter; + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n"; + ++m_id_counter; + m_axiom_bases.insert(f->get_name(), constructor_id + 4); + std::ostringstream var_sorts; + for (accessor const* a : *c) { + var_sorts << " (;" << a->range()->get_name() << ")"; + } + std::string var_description = var_sorts.str(); + unsigned i = 0; + for (accessor const* a : *c) { + func_decl_ref acc = a->instantiate(new_sorts.back()); + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n"; + ++m_id_counter; + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i + << " " << family_name << "#" << m_id_counter - 1 << "\n"; + ++m_id_counter; + m_manager->trace_stream() << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 + << " " << family_name << "#" << m_id_counter - 1 << "\n"; + m_manager->trace_stream() << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; + ++m_id_counter; + ++i; + } + } + } } return true; } diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index fc98c97e7..736cc0875 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -249,13 +249,15 @@ namespace datatype { class plugin : public decl_plugin { mutable scoped_ptr m_util; map m_defs; + map m_axiom_bases; + unsigned m_id_counter; svector m_def_block; unsigned m_class_id; void inherit(decl_plugin* other_p, ast_translation& tr) override; public: - plugin(): m_class_id(0) {} + plugin(): m_id_counter(0), m_class_id(0) {} ~plugin() override; void finalize() override; @@ -290,6 +292,7 @@ namespace datatype { def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); } def& get_def(symbol const& s) { return *(m_defs[s]); } bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); } + unsigned get_axiom_base_id(symbol const& s) { return m_axiom_bases[s]; } util & u() const; private: diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index eb819c988..4fa8c4074 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -562,6 +562,29 @@ struct th_rewriter_cfg : public default_rewriter_cfg { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = nullptr; br_status st = reduce_app_core(f, num, args, result); + + if (st != BR_FAILED && m().has_trace_stream()) { + family_id fid = f->get_family_id(); + if (fid == m_b_rw.get_fid()) { + decl_kind k = f->get_decl_kind(); + if (k == OP_EQ) { + SASSERT(num == 2); + fid = m().get_sort(args[0])->get_family_id(); + } + else if (k == OP_ITE) { + SASSERT(num == 3); + fid = m().get_sort(args[1])->get_family_id(); + } + } + app_ref tmp(m()); + tmp = m().mk_app(f, num, args); + m().trace_stream() << "[inst-discovered] theory-solving " << static_cast(nullptr) << " " << m().get_family_name(fid) << "# ; #" << tmp->get_id() << "\n"; + tmp = m().mk_eq(tmp, result); + m().trace_stream() << "[instance] " << static_cast(nullptr) << " #" << tmp->get_id() << "\n"; + m().trace_stream() << "[attach-enode] #" << tmp->get_id() << " 0\n"; + m().trace_stream() << "[end-of-instance]\n"; + } + if (st != BR_DONE && st != BR_FAILED) { CTRACE("th_rewriter_step", st != BR_FAILED, tout << f->get_name() << "\n"; diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 4a6cd086c..5f9e031e5 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1019,15 +1019,7 @@ namespace smt { sort * s = term->get_decl()->get_range(); theory * th = m_theories.get_plugin(s->get_family_id()); if (th) { - if (m_manager.has_trace_stream()) { - m_manager.trace_stream() << "[theory-constraints] " << m_manager.get_family_name(s->get_family_id()) << "\n"; - } - th->apply_sort_cnstr(e, s); - - if (m_manager.has_trace_stream()) { - m_manager.trace_stream() << "[end-theory-constraints]\n"; - } } } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 65a6db875..01a9353f7 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -32,6 +32,96 @@ namespace smt { quantifier_manager_plugin * mk_default_plugin(); + /** + \brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its + equivalence class are in the log and up-to-date. + */ + void quantifier_manager::log_justification_to_root(std::ostream & log, enode *en, obj_hashtable &already_visited, context &ctx, ast_manager &m) { + enode *root = en->get_root(); + for (enode *it = en; it != root; it = it->get_trans_justification().m_target) { + if (already_visited.find(it) == already_visited.end()) already_visited.insert(it); + else break; + + if (!it->m_proof_is_logged) { + log_single_justification(log, it, already_visited, ctx, m); + it->m_proof_is_logged = true; + } else if (it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) { + + // When the justification of an argument changes m_proof_is_logged is not reset => We need to check if the proofs of all arguments are logged. + const unsigned num_args = it->get_num_args(); + enode *target = it->get_trans_justification().m_target; + + for (unsigned i = 0; i < num_args; ++i) { + log_justification_to_root(log, it->get_arg(i), already_visited, ctx, m); + log_justification_to_root(log, target->get_arg(i), already_visited, ctx, m); + } + it->m_proof_is_logged = true; + } + } + if (!root->m_proof_is_logged) { + log << "[eq-expl] #" << root->get_owner_id() << " root\n"; + root->m_proof_is_logged = true; + } + } + + /** + \brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log + equalities needed by the step (e.g. argument equalities for congruence steps). + */ + void quantifier_manager::log_single_justification(std::ostream & out, enode *en, obj_hashtable &already_visited, context &ctx, ast_manager &m) { + smt::literal lit; + unsigned num_args; + enode *target = en->get_trans_justification().m_target; + theory_id th_id; + + switch (en->get_trans_justification().m_justification.get_kind()) { + case smt::eq_justification::kind::EQUATION: + lit = en->get_trans_justification().m_justification.get_literal(); + out << "[eq-expl] #" << en->get_owner_id() << " lit #" << ctx.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n"; + break; + case smt::eq_justification::kind::AXIOM: + out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n"; + break; + case smt::eq_justification::kind::CONGRUENCE: + if (!en->get_trans_justification().m_justification.used_commutativity()) { + num_args = en->get_num_args(); + + for (unsigned i = 0; i < num_args; ++i) { + log_justification_to_root(out, en->get_arg(i), already_visited, ctx, m); + log_justification_to_root(out, target->get_arg(i), already_visited, ctx, m); + } + + out << "[eq-expl] #" << en->get_owner_id() << " cg"; + for (unsigned i = 0; i < num_args; ++i) { + out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")"; + } + out << " ; #" << target->get_owner_id() << "\n"; + + break; + } else { + + // The e-graph only supports commutativity for binary functions + out << "[eq-expl] #" << en->get_owner_id() + << " cg (#" << en->get_arg(0)->get_owner_id() << " #" << target->get_arg(1)->get_owner_id() + << ") (#" << en->get_arg(1)->get_owner_id() << " #" << target->get_arg(0)->get_owner_id() + << ") ; #" << target->get_owner_id() << "\n"; + break; + } + case smt::eq_justification::kind::JUSTIFICATION: + th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory(); + if (th_id != null_theory_id) { + symbol const theory = m.get_family_name(th_id); + out << "[eq-expl] #" << en->get_owner_id() << " th " << theory.str() << " ; #" << target->get_owner_id() << "\n"; + } else { + out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n"; + } + break; + default: + out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n"; + break; + } + } + struct quantifier_manager::imp { quantifier_manager & m_wrapper; context & m_context; @@ -105,96 +195,6 @@ namespace smt { return m_plugin->is_shared(n); } - /** - \brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its - equivalence class are in the log and up-to-date. - */ - void log_justification_to_root(std::ostream & log, enode *en, obj_hashtable &already_visited) { - enode *root = en->get_root(); - for (enode *it = en; it != root; it = it->get_trans_justification().m_target) { - if (already_visited.find(it) == already_visited.end()) already_visited.insert(it); - else break; - - if (!it->m_proof_is_logged) { - log_single_justification(log, it, already_visited); - it->m_proof_is_logged = true; - } else if (it->get_trans_justification().m_justification.get_kind() == smt::eq_justification::kind::CONGRUENCE) { - - // When the justification of an argument changes m_proof_is_logged is not reset => We need to check if the proofs of all arguments are logged. - const unsigned num_args = it->get_num_args(); - enode *target = it->get_trans_justification().m_target; - - for (unsigned i = 0; i < num_args; ++i) { - log_justification_to_root(log, it->get_arg(i), already_visited); - log_justification_to_root(log, target->get_arg(i), already_visited); - } - it->m_proof_is_logged = true; - } - } - if (!root->m_proof_is_logged) { - log << "[eq-expl] #" << root->get_owner_id() << " root\n"; - root->m_proof_is_logged = true; - } - } - - /** - \brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log - equalities needed by the step (e.g. argument equalities for congruence steps). - */ - void log_single_justification(std::ostream & out, enode *en, obj_hashtable &already_visited) { - smt::literal lit; - unsigned num_args; - enode *target = en->get_trans_justification().m_target; - theory_id th_id; - - switch (en->get_trans_justification().m_justification.get_kind()) { - case smt::eq_justification::kind::EQUATION: - lit = en->get_trans_justification().m_justification.get_literal(); - out << "[eq-expl] #" << en->get_owner_id() << " lit #" << m_context.bool_var2expr(lit.var())->get_id() << " ; #" << target->get_owner_id() << "\n"; - break; - case smt::eq_justification::kind::AXIOM: - out << "[eq-expl] #" << en->get_owner_id() << " ax ; #" << target->get_owner_id() << "\n"; - break; - case smt::eq_justification::kind::CONGRUENCE: - if (!en->get_trans_justification().m_justification.used_commutativity()) { - num_args = en->get_num_args(); - - for (unsigned i = 0; i < num_args; ++i) { - log_justification_to_root(out, en->get_arg(i), already_visited); - log_justification_to_root(out, target->get_arg(i), already_visited); - } - - out << "[eq-expl] #" << en->get_owner_id() << " cg"; - for (unsigned i = 0; i < num_args; ++i) { - out << " (#" << en->get_arg(i)->get_owner_id() << " #" << target->get_arg(i)->get_owner_id() << ")"; - } - out << " ; #" << target->get_owner_id() << "\n"; - - break; - } else { - - // The e-graph only supports commutativity for binary functions - out << "[eq-expl] #" << en->get_owner_id() - << " cg (#" << en->get_arg(0)->get_owner_id() << " #" << target->get_arg(1)->get_owner_id() - << ") (#" << en->get_arg(1)->get_owner_id() << " #" << target->get_arg(0)->get_owner_id() - << ") ; #" << target->get_owner_id() << "\n"; - break; - } - case smt::eq_justification::kind::JUSTIFICATION: - th_id = en->get_trans_justification().m_justification.get_justification()->get_from_theory(); - if (th_id != null_theory_id) { - symbol const theory = m().get_family_name(th_id); - out << "[eq-expl] #" << en->get_owner_id() << " th " << theory.str() << " ; #" << target->get_owner_id() << "\n"; - } else { - out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n"; - } - break; - default: - out << "[eq-expl] #" << en->get_owner_id() << " unknown ; #" << target->get_owner_id() << "\n"; - break; - } - } - bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, @@ -225,15 +225,15 @@ namespace smt { // In the term produced by the quantifier instantiation the root of the equivalence class of the terms bound to the quantified variables // is used. We need to make sure that all of these equalities appear in the log. for (unsigned i = 0; i < num_bindings; ++i) { - log_justification_to_root(out, bindings[i], already_visited); + log_justification_to_root(out, bindings[i], already_visited, m_context, m()); } for (auto n : used_enodes) { enode *orig = std::get<0>(n); enode *substituted = std::get<1>(n); if (orig != nullptr) { - log_justification_to_root(out, orig, already_visited); - log_justification_to_root(out, substituted, already_visited); + log_justification_to_root(out, orig, already_visited, m_context, m()); + log_justification_to_root(out, substituted, already_visited, m_context, m()); } } diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 4f14c6853..a126407d7 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -52,6 +52,11 @@ namespace smt { quantifier_stat * get_stat(quantifier * q) const; unsigned get_generation(quantifier * q) const; + static void log_justification_to_root(std::ostream & log, enode *en, obj_hashtable &already_visited, context &ctx, ast_manager &m); + private: + static void log_single_justification(std::ostream & out, enode *en, obj_hashtable &already_visited, context &ctx, ast_manager &m); + public: + bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index 66bb3e14b..ebce8df6f 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -20,6 +20,7 @@ Revision History: #define SMT_THEORY_H_ #include "smt/smt_enode.h" +#include "smt/smt_quantifier.h" #include "util/obj_hashtable.h" #include "util/statistics.h" #include @@ -358,6 +359,67 @@ namespace smt { std::ostream& display_var_flat_def(std::ostream & out, theory_var v) const { return display_flat_app(out, get_enode(v)->get_owner()); } + protected: + void log_axiom_instantiation(app * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector> & used_enodes = vector>()) { + ast_manager & m = get_manager(); + symbol const & family_name = m.get_family_name(get_family_id()); + if (pattern_id == UINT_MAX) { + m.trace_stream() << "[inst-discovered] theory-solving " << static_cast(nullptr) << " " << family_name << "#"; + if (axiom_id != UINT_MAX) + m.trace_stream() << axiom_id; + for (unsigned i = 0; i < num_bindings; ++i) { + m.trace_stream() << " #" << bindings[i]->get_id(); + } + if (used_enodes.size() > 0) { + m.trace_stream() << " ;"; + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + SASSERT(orig == nullptr); + m.trace_stream() << " #" << substituted->get_owner_id(); + } + } + } else { + SASSERT(axiom_id != UINT_MAX); + obj_hashtable already_visited; + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig != nullptr) { + quantifier_manager::log_justification_to_root(m.trace_stream(), orig, already_visited, get_context(), get_manager()); + quantifier_manager::log_justification_to_root(m.trace_stream(), substituted, already_visited, get_context(), get_manager()); + } + } + m.trace_stream() << "[new-match] " << static_cast(nullptr) << " " << family_name << "#" << axiom_id << " " << family_name << "#" << pattern_id; + for (unsigned i = 0; i < num_bindings; ++i) { + m.trace_stream() << " #" << bindings[i]->get_id(); + } + m.trace_stream() << " ;"; + for (auto n : used_enodes) { + enode *orig = std::get<0>(n); + enode *substituted = std::get<1>(n); + if (orig == nullptr) { + m.trace_stream() << " #" << substituted->get_owner_id(); + } else { + m.trace_stream() << " (#" << orig->get_owner_id() << " #" << substituted->get_owner_id() << ")"; + } + } + } + m.trace_stream() << "\n"; + m.trace_stream() << "[instance] " << static_cast(nullptr) << " #" << r->get_id() << "\n"; + } + + void log_axiom_instantiation(expr * r, unsigned axiom_id = UINT_MAX, unsigned num_bindings = 0, app * const * bindings = nullptr, unsigned pattern_id = UINT_MAX, const vector> & used_enodes = vector>()) { log_axiom_instantiation(to_app(r), axiom_id, num_bindings, bindings, pattern_id, used_enodes); } + + void log_axiom_instantiation(app * r, unsigned num_blamed_enodes, enode ** blamed_enodes) { + vector> used_enodes; + for (unsigned i = 0; i < num_blamed_enodes; ++i) { + used_enodes.push_back(std::make_tuple(nullptr, blamed_enodes[i])); + } + log_axiom_instantiation(r, UINT_MAX, 0, nullptr, UINT_MAX, used_enodes); + } + + public: /** \brief Assume eqs between variable that are equal with respect to the given table. Table is a hashtable indexed by the variable value. diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index f70e50ece..bac82b083 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1239,6 +1239,10 @@ namespace smt { farkas.add(abs(pa.get_rational()), to_app(tmp)); } tmp = farkas.get(); + if (m.has_trace_stream()) { + log_axiom_instantiation(tmp); + m.trace_stream() << "[end-of-instance]\n"; + } // IF_VERBOSE(1, verbose_stream() << "Farkas result: " << tmp << "\n";); atom* a = get_bv2a(m_bound_watch); SASSERT(a); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index f3a3e9238..72bb263d0 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -447,7 +447,10 @@ namespace smt { tout << l_ante << "\n" << l_conseq << "\n";); // literal lits[2] = {l_ante, l_conseq}; + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ante, conseq)); mk_clause(l_ante, l_conseq, 0, nullptr); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (ctx.relevancy()) { if (l_ante == false_literal) { ctx.mark_as_relevant(l_conseq); @@ -517,7 +520,9 @@ namespace smt { expr_ref mod_j(m); while(j < k) { mod_j = m.mk_eq(mod, m_util.mk_numeral(j, true)); + if (m.has_trace_stream()) log_axiom_instantiation(mod_j); ctx.internalize(mod_j, false); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; literal lit(ctx.get_literal(mod_j)); lits.push_back(lit); ctx.mark_as_relevant(lit); diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index afe527a98..f4e901de4 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -199,6 +199,7 @@ namespace smt { void theory_arith::branch_infeasible_int_var(theory_var v) { SASSERT(is_int(v)); SASSERT(!get_value(v).is_int()); + ast_manager & m = get_manager(); m_stats.m_branches++; numeral k = ceil(get_value(v)); rational _k = k.to_rational(); @@ -206,13 +207,15 @@ namespace smt { display_var(tout, v); tout << "k = " << k << ", _k = "<< _k << std::endl; ); - expr_ref bound(get_manager()); + expr_ref bound(m); expr* e = get_enode(v)->get_owner(); bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e))); - TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(to_app(bound), m.mk_not(to_app(bound)))); + TRACE("arith_int", tout << mk_bounded_pp(bound, m) << "\n";); context & ctx = get_context(); ctx.internalize(bound, true); ctx.mark_as_relevant(bound.get()); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -365,6 +368,7 @@ namespace smt { mk_polynomial_ge(pol.size(), pol.c_ptr(), unsat_row[0]+rational(1), p2); context& ctx = get_context(); + if (get_manager().has_trace_stream()) log_axiom_instantiation(get_manager().mk_or(p1, p2)); ctx.internalize(p1, false); ctx.internalize(p2, false); literal l1(ctx.get_literal(p1)), l2(ctx.get_literal(p2)); @@ -372,6 +376,7 @@ namespace smt { ctx.mark_as_relevant(p2.get()); ctx.mk_th_axiom(get_id(), l1, l2); + if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n"; TRACE("arith_int", tout << "cut: (or " << mk_pp(p1, get_manager()) << " " << mk_pp(p2, get_manager()) << ")\n"; @@ -400,7 +405,9 @@ namespace smt { bool _is_int = m_util.is_int(e); expr * bound = m_util.mk_ge(e, m_util.mk_numeral(rational::zero(), _is_int)); context & ctx = get_context(); + if (get_manager().has_trace_stream()) log_axiom_instantiation(bound); ctx.internalize(bound, true); + if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n"; ctx.mark_as_relevant(bound); result = true; } @@ -646,7 +653,9 @@ namespace smt { TRACE("gomory_cut", tout << "new cut:\n" << bound << "\n"; ante.display(tout);); literal l = null_literal; context & ctx = get_context(); + if (get_manager().has_trace_stream()) log_axiom_instantiation(bound); ctx.internalize(bound, true); + if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n"; l = ctx.get_literal(bound); ctx.mark_as_relevant(l); dump_lemmas(l, ante); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 24e1020fd..457c6e068 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -789,7 +789,10 @@ namespace smt { bound = m_util.mk_eq(var2expr(v), m_util.mk_numeral(rational(0), true)); TRACE("non_linear", tout << "new bound:\n" << mk_pp(bound, get_manager()) << "\n";); context & ctx = get_context(); + ast_manager & m = get_manager(); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(bound, m.mk_not(bound))); ctx.internalize(bound, true); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; ctx.mark_as_relevant(bound); literal l = ctx.get_literal(bound); SASSERT(!l.sign()); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index c024c0da0..9ba520c9d 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -111,7 +111,9 @@ namespace smt { if (m.proofs_enabled()) { literal l(mk_eq(sel, val, true)); ctx.mark_as_relevant(l); + if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var())); assert_axiom(l); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } else { TRACE("mk_var_bug", tout << "mk_sel: " << sel->get_id() << "\n";); @@ -189,7 +191,9 @@ namespace smt { TRACE("array_map_bug", tout << "axiom2:\n"; tout << mk_ismt2_pp(idx1->get_owner(), m) << "\n=\n" << mk_ismt2_pp(idx2->get_owner(), m); tout << "\nimplies\n" << mk_ismt2_pp(conseq_expr, m) << "\n";); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(ante.var()), conseq_expr)); assert_axiom(ante, conseq); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } } @@ -331,7 +335,9 @@ namespace smt { literal sel1_eq_sel2 = mk_eq(sel1, sel2, true); ctx.mark_as_relevant(n1_eq_n2); ctx.mark_as_relevant(sel1_eq_sel2); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(n1_eq_n2.var())), m.mk_not(ctx.bool_var2expr(sel1_eq_sel2.var())))); assert_axiom(n1_eq_n2, ~sel1_eq_sel2); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } bool theory_array_base::can_propagate() { diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index d0a37175d..20aba9436 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -777,8 +777,10 @@ namespace smt { else { m_eqs.insert(v1, v2, true); literal eq(mk_eq(v1, v2, true)); + if (get_manager().has_trace_stream()) log_axiom_instantiation(get_context().bool_var2expr(eq.var())); get_context().mark_as_relevant(eq); assert_axiom(eq); + if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n"; // m_eqsv.push_back(eq); return true; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 33207d15a..36cddb1cc 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -229,9 +229,12 @@ namespace smt { enode * e2 = get_enode(v2); literal l = ~(mk_eq(e1->get_owner(), e2->get_owner(), true)); context & ctx = get_context(); + ast_manager & m = get_manager(); + expr * eq = ctx.bool_var2expr(l.var()); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_eq(mk_bit2bool(get_enode(v1)->get_owner(), idx), m.mk_not(mk_bit2bool(get_enode(v2)->get_owner(), idx))), m.mk_not(eq))); ctx.mk_th_axiom(get_id(), 1, &l); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (ctx.relevancy()) { - expr * eq = ctx.bool_var2expr(l.var()); relevancy_eh * eh = ctx.mk_relevancy_eh(pair_relevancy_eh(e1->get_owner(), e2->get_owner(), eq)); ctx.add_relevancy_eh(e1->get_owner(), eh); ctx.add_relevancy_eh(e2->get_owner(), eh); @@ -440,11 +443,13 @@ namespace smt { e1 = mk_bit2bool(o1, i); e2 = mk_bit2bool(o2, i); literal eq = mk_eq(e1, e2, true); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var())))); ctx.mk_th_axiom(get_id(), l1, ~l2, ~eq); ctx.mk_th_axiom(get_id(), ~l1, l2, ~eq); ctx.mk_th_axiom(get_id(), l1, l2, eq); ctx.mk_th_axiom(get_id(), ~l1, ~l2, eq); ctx.mk_th_axiom(get_id(), eq, ~oeq); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; eqs.push_back(~eq); } eqs.push_back(oeq); @@ -612,7 +617,9 @@ namespace smt { ); ctx.mark_as_relevant(l); + if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var())); ctx.mk_th_axiom(get_id(), 1, &l); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } void theory_bv::internalize_int2bv(app* n) { @@ -653,7 +660,9 @@ namespace smt { literal l(mk_eq(lhs, rhs, false)); ctx.mark_as_relevant(l); + if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var())); ctx.mk_th_axiom(get_id(), 1, &l); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; TRACE("bv", tout << mk_pp(lhs, m) << " == \n"; @@ -674,7 +683,9 @@ namespace smt { TRACE("bv", tout << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";); l = literal(mk_eq(lhs, rhs, false)); ctx.mark_as_relevant(l); + if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var())); ctx.mk_th_axiom(get_id(), 1, &l); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } } @@ -1126,8 +1137,10 @@ namespace smt { unsigned num_bool_vars = ctx.get_num_bool_vars(); #endif literal_vector & lits = m_tmp_literals; + ptr_vector exprs; lits.reset(); - lits.push_back(mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true)); + literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true); + lits.push_back(eq); literal_vector const & bits1 = m_bits[v1]; literal_vector::const_iterator it1 = bits1.begin(); literal_vector::const_iterator end1 = bits1.end(); @@ -1147,9 +1160,12 @@ namespace smt { ctx.internalize(diff, true); literal arg = ctx.get_literal(diff); lits.push_back(arg); + exprs.push_back(diff); } m_stats.m_num_diseq_dynamic++; + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_or(exprs.size(), exprs.c_ptr()))); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; TRACE_CODE({ static unsigned num = 0; static unsigned new_bool_vars = 0; @@ -1237,6 +1253,7 @@ namespace smt { m_stats.m_num_bit2core++; context & ctx = get_context(); + ast_manager & m = get_manager(); SASSERT(ctx.get_assignment(antecedent) == l_true); SASSERT(m_bits[v2][idx].var() == consequent.var()); SASSERT(consequent.var() != antecedent.var()); @@ -1253,8 +1270,11 @@ namespace smt { literal_vector lits; lits.push_back(~consequent); lits.push_back(antecedent); - lits.push_back(~mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false)); + literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false); + lits.push_back(~eq); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_implies(ctx.bool_var2expr(consequent.var()), ctx.bool_var2expr(antecedent.var())))); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (m_wpos[v2] == idx) find_wpos(v2); diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 6aa49efae..9209d8b5d 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -140,7 +140,14 @@ namespace smt { args.push_back(acc); } expr * mk = m.mk_app(c, args.size(), args.c_ptr()); + app_ref ax(m); + ax = m.mk_eq(n->get_owner(), mk); + if (antecedent != null_literal) { + ax = m.mk_implies(get_context().bool_var2expr(antecedent.var()), ax); + } + if (m.has_trace_stream()) log_axiom_instantiation(ax, 1, &n); assert_eq_axiom(n, mk, antecedent); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } /** @@ -157,11 +164,22 @@ namespace smt { func_decl * d = n->get_decl(); ptr_vector const & accessors = *m_util.get_constructor_accessors(d); SASSERT(n->get_num_args() == accessors.size()); + ptr_vector bindings; + vector> used_enodes; + used_enodes.push_back(std::make_tuple(nullptr, n)); + for (unsigned i = 0; i < n->get_num_args(); ++i) { + bindings.push_back(n->get_arg(i)->get_owner()); + } + unsigned base_id = get_manager().has_trace_stream() && accessors.size() > 0 ? m_util.get_plugin()->get_axiom_base_id(d->get_name()) : 0; unsigned i = 0; for (func_decl * acc : accessors) { app * acc_app = m.mk_app(acc, n->get_owner()); enode * arg = n->get_arg(i); + app_ref eq(m); + eq = m.mk_eq(arg->get_owner(), acc_app); + if (m.has_trace_stream()) log_axiom_instantiation(eq, base_id + 3*i, bindings.size(), bindings.c_ptr(), base_id - 3, used_enodes); assert_eq_axiom(arg, acc_app, null_literal); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; ++i; } } @@ -218,10 +236,18 @@ namespace smt { arg = ctx.get_enode(acc_app); } app * acc_own = m.mk_app(acc1, own); + app_ref imp(m); + imp = m.mk_implies(rec_app, m.mk_eq(arg->get_owner(), acc_own)); + if (m.has_trace_stream()) log_axiom_instantiation(imp, 1, &n); assert_eq_axiom(arg, acc_own, is_con); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } // update_field is identity if 'n' is not created by a matching constructor. + app_ref imp(m); + imp = m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_owner(), arg1)); + if (m.has_trace_stream()) log_axiom_instantiation(imp, 1, &n); assert_eq_axiom(n, arg1, ~is_con); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } theory_var theory_datatype::mk_var(enode * n) { diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 48991da8e..b7bd9adf1 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -598,7 +598,9 @@ void theory_diff_logic::new_edge(dl_var src, dl_var dst, unsigned num_edges le = m_util.mk_le(m_util.mk_add(n2,n1), n3); le = get_manager().mk_not(le); } + if (get_manager().has_trace_stream())log_axiom_instantiation(le); ctx.internalize(le, false); + if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n"; ctx.mark_as_relevant(le.get()); literal lit(ctx.get_literal(le)); bool_var bv = lit.var(); @@ -1007,6 +1009,7 @@ void theory_diff_logic::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v t2 = m_util.mk_numeral(k, m.get_sort(s2.get())); // t1 - s1 = k eq = m.mk_eq(s2.get(), t2.get()); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_eq(m.mk_eq(m_util.mk_add(s1, t2), t1), eq)); TRACE("diff_logic", tout << v1 << " .. " << v2 << "\n"; @@ -1015,6 +1018,8 @@ void theory_diff_logic::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v if (!internalize_atom(eq.get(), false)) { UNREACHABLE(); } + + if (m.has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n"; literal l(ctx.get_literal(eq.get())); if (!is_eq) { diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 824bd1d9e..be99b1234 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -256,6 +256,7 @@ namespace smt { lt = u().mk_lt(x,y); le = b().mk_ule(m().mk_app(r,y),m().mk_app(r,x)); context& ctx = get_context(); + if (m().has_trace_stream()) log_axiom_instantiation(m().mk_eq(lt, le)); ctx.internalize(lt, false); ctx.internalize(le, false); literal lit1(ctx.get_literal(lt)); @@ -266,12 +267,15 @@ namespace smt { literal lits2[2] = { ~lit1, ~lit2 }; ctx.mk_th_axiom(get_id(), 2, lits1); ctx.mk_th_axiom(get_id(), 2, lits2); + if (m().has_trace_stream()) m().trace_stream() << "[end-of-instance]\n"; } void assert_cnstr(expr* e) { TRACE("theory_dl", tout << mk_pp(e, m()) << "\n";); context& ctx = get_context(); + if (m().has_trace_stream()) log_axiom_instantiation(e); ctx.internalize(e, false); + if (m().has_trace_stream()) m().trace_stream() << "[end-of-instance]\n"; literal lit(ctx.get_literal(e)); ctx.mark_as_relevant(lit); ctx.mk_th_axiom(get_id(), 1, &lit); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 42d90c242..559615340 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -409,7 +409,9 @@ namespace smt { if (get_manager().is_true(e)) return; TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";); context & ctx = get_context(); + if (get_manager().has_trace_stream()) log_axiom_instantiation(e); ctx.internalize(e, false); + if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n"; literal lit(ctx.get_literal(e)); ctx.mark_as_relevant(lit); ctx.mk_th_axiom(get_id(), 1, &lit); diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index 3b218f56d..802455683 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -306,6 +306,9 @@ namespace smt { literal end_ge_lo = mk_ge(ji.m_end, clb); // Initialization ensures that satisfiable states have completion time below end. VERIFY(clb <= get_job_resource(j, r).m_end); + ast_manager& m = get_manager(); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var()))); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; region& r = ctx.get_region(); ctx.assign(end_ge_lo, ctx.mk_justification( @@ -376,6 +379,9 @@ namespace smt { lits.push_back(mk_eq_lit(end_e->get_owner(), rhs)); context& ctx = get_context(); ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr); + ast_manager& m = get_manager(); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(ctx.bool_var2expr(lits[0].var()), ctx.bool_var2expr(lits[1].var()), ctx.bool_var2expr(lits[2].var())), ctx.bool_var2expr(lits[3].var()))); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; return true; } @@ -707,7 +713,9 @@ namespace smt { // start(j) <= end(j) lit = mk_le(ji.m_start, ji.m_end); + if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var())); ctx.mk_th_axiom(get_id(), 1, &lit); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; time_t start_lb = std::numeric_limits::max(); time_t runtime_lb = std::numeric_limits::max(); @@ -735,11 +743,15 @@ namespace smt { // start(j) >= start_lb lit = mk_ge(ji.m_start, start_lb); + if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var())); ctx.mk_th_axiom(get_id(), 1, &lit); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; // end(j) <= end_ub lit = mk_le(ji.m_end, end_ub); + if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var())); ctx.mk_th_axiom(get_id(), 1, &lit); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; // start(j) + runtime_lb <= end(j) // end(j) <= start(j) + runtime_ub @@ -754,7 +766,10 @@ namespace smt { void theory_jobscheduler::assert_last_end_time(unsigned j, unsigned r, job_resource const& jr, literal eq) { job_info const& ji = m_jobs[j]; literal l2 = mk_le(ji.m_end, jr.m_end); - get_context().mk_th_axiom(get_id(), ~eq, l2); + context& ctx = get_context(); + if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var()))); + ctx.mk_th_axiom(get_id(), ~eq, l2); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } // resource(j) = r => start(j) <= lst(j, r, end(j, r)) @@ -762,11 +777,16 @@ namespace smt { context& ctx = get_context(); time_t t; if (lst(j, r, t)) { - ctx.mk_th_axiom(get_id(), ~eq, mk_le(m_jobs[j].m_start, t)); + literal le = mk_le(m_jobs[j].m_start, t); + if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(le.var()))); + ctx.mk_th_axiom(get_id(), ~eq, le); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } else { eq.neg(); + if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_not(ctx.bool_var2expr(eq.var()))); ctx.mk_th_axiom(get_id(), 1, &eq); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } } @@ -777,7 +797,10 @@ namespace smt { if (!first_available(jr, m_resources[r], idx)) return; vector& available = m_resources[r].m_available; literal l2 = mk_ge(m_jobs[j].m_start, available[idx].m_start); - get_context().mk_th_axiom(get_id(), ~eq, l2); + context& ctx = get_context(); + if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var()))); + ctx.mk_th_axiom(get_id(), ~eq, l2); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } // resource(j) = r => start(j) <= end[idx] || start[idx+1] <= start(j); @@ -788,7 +811,11 @@ namespace smt { SASSERT(resource_available(jr, available[idx])); literal l2 = mk_ge(m_jobs[j].m_start, available[idx1].m_start); literal l3 = mk_le(m_jobs[j].m_start, available[idx].m_end); - get_context().mk_th_axiom(get_id(), ~eq, l2, l3); + context& ctx = get_context(); + ast_manager& m = get_manager(); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var())))); + ctx.mk_th_axiom(get_id(), ~eq, l2, l3); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } // resource(j) = r => end(j) <= end[idx] || start[idx+1] <= start(j); @@ -799,7 +826,11 @@ namespace smt { SASSERT(resource_available(jr, available[idx])); literal l2 = mk_le(m_jobs[j].m_end, available[idx].m_end); literal l3 = mk_ge(m_jobs[j].m_start, available[idx1].m_start); - get_context().mk_th_axiom(get_id(), ~eq, l2, l3); + context& ctx = get_context(); + ast_manager& m = get_manager(); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var())))); + ctx.mk_th_axiom(get_id(), ~eq, l2, l3); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } /** @@ -808,6 +839,7 @@ namespace smt { bool theory_jobscheduler::split_job2resource(unsigned j) { job_info const& ji = m_jobs[j]; context& ctx = get_context(); + ast_manager& m = get_manager(); if (ji.m_is_bound) return false; auto const& jrs = ji.m_resources; for (job_resource const& jr : jrs) { @@ -818,6 +850,8 @@ namespace smt { if (ctx.is_diseq(e1, e2)) continue; literal eq = mk_eq_lit(e1, e2); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(eq.var()), m.mk_not(ctx.bool_var2expr(eq.var())))); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (ctx.get_assignment(eq) != l_false) { ctx.mark_as_relevant(eq); if (assume_eq(e1, e2)) { @@ -826,14 +860,19 @@ namespace smt { } } literal_vector lits; + ptr_vector exprs; for (job_resource const& jr : jrs) { unsigned r = jr.m_resource_id; res_info const& ri = m_resources[r]; enode* e1 = ji.m_job2resource; enode* e2 = ri.m_resource; - lits.push_back(mk_eq_lit(e1, e2)); + literal eq = mk_eq_lit(e1, e2); + lits.push_back(eq); + exprs.push_back(ctx.bool_var2expr(eq.var())); } + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(exprs.size(), exprs.c_ptr())); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; return true; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0b25aa626..2fad2f97b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1038,9 +1038,14 @@ public: expr_ref rem(a.mk_rem(dividend, divisor), m); expr_ref mod(a.mk_mod(dividend, divisor), m); expr_ref mmod(a.mk_uminus(mod), m); - literal dgez = mk_literal(a.mk_ge(divisor, zero)); - mk_axiom(~dgez, th.mk_eq(rem, mod, false)); - mk_axiom( dgez, th.mk_eq(rem, mmod, false)); + expr_ref degz_expr(a.mk_ge(divisor, zero), m); + literal dgez = mk_literal(degz_expr); + literal pos = th.mk_eq(rem, mod, false); + literal neg = th.mk_eq(rem, mmod, false); + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_ite(degz_expr, ctx().bool_var2expr(pos.var()), ctx().bool_var2expr(neg.var()))); + mk_axiom(~dgez, pos); + mk_axiom( dgez, neg); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } // q = 0 or q * (p div q) = p @@ -1048,7 +1053,9 @@ public: if (a.is_zero(q)) return; literal eqz = th.mk_eq(q, a.mk_real(0), false); literal eq = th.mk_eq(a.mk_mul(q, a.mk_div(p, q)), p, false); + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(ctx().bool_var2expr(eqz.var())), ctx().bool_var2expr(eq.var()))); mk_axiom(eqz, eq); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } // to_int (to_real x) = x @@ -1057,14 +1064,20 @@ public: expr* x = nullptr, *y = nullptr; VERIFY (a.is_to_int(n, x)); if (a.is_to_real(x, y)) { + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_eq(n, y)); mk_axiom(th.mk_eq(y, n, false)); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } else { expr_ref to_r(a.mk_to_real(n), m); expr_ref lo(a.mk_le(a.mk_sub(to_r, x), a.mk_real(0)), m); expr_ref hi(a.mk_ge(a.mk_sub(x, to_r), a.mk_real(1)), m); + if (m.has_trace_stream()) th.log_axiom_instantiation(lo); mk_axiom(mk_literal(lo)); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_not(hi)); mk_axiom(~mk_literal(hi)); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } } @@ -1074,8 +1087,10 @@ public: VERIFY(a.is_is_int(n, x)); literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false); literal is_int = ctx().get_literal(n); + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_iff(n, ctx().bool_var2expr(eq.var()))); mk_axiom(~is_int, eq); mk_axiom(is_int, ~eq); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } // create axiom for @@ -1127,17 +1142,32 @@ public: k = rational::zero(); } + context& c = ctx(); if (!k.is_zero()) { + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()))); mk_axiom(eq); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()))); mk_axiom(mod_ge_0); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper))); mk_axiom(mk_literal(a.mk_le(mod, upper))); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (k.is_pos()) { + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()))); mk_axiom(~p_ge_0, div_ge_0); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()))); mk_axiom(~p_le_0, div_le_0); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } else { + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()))); mk_axiom(~p_ge_0, div_le_0); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()))); mk_axiom(~p_le_0, div_ge_0); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } } else { @@ -1149,26 +1179,46 @@ public: // q >= 0 or (p mod q) < -q literal q_ge_0 = mk_literal(a.mk_ge(q, zero)); literal q_le_0 = mk_literal(a.mk_le(q, zero)); + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()))); mk_axiom(q_ge_0, eq); mk_axiom(q_le_0, eq); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()))); mk_axiom(q_ge_0, mod_ge_0); mk_axiom(q_le_0, mod_ge_0); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero))); mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero))); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero))); mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero))); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()))); mk_axiom(q_le_0, ~p_ge_0, div_ge_0); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()))); mk_axiom(q_le_0, ~p_le_0, div_le_0); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()))); mk_axiom(q_ge_0, ~p_ge_0, div_le_0); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()))); mk_axiom(q_ge_0, ~p_le_0, div_ge_0); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } if (m_arith_params.m_arith_enum_const_mod && k.is_pos() && k < rational(8)) { unsigned _k = k.get_unsigned(); literal_buffer lits; + ptr_vector exprs; for (unsigned j = 0; j < _k; ++j) { literal mod_j = th.mk_eq(mod, a.mk_int(j), false); lits.push_back(mod_j); + exprs.push_back(c.bool_var2expr(mod_j.var())); ctx().mark_as_relevant(mod_j); } + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_or(exprs.size(), exprs.c_ptr())); ctx().mk_th_axiom(get_id(), lits.size(), lits.begin()); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } } @@ -1603,8 +1653,12 @@ public: literal p_ge_r1 = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true))); literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true))); literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div_r, true))); + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(p_le_r1.var()), ctx().bool_var2expr(n_le_div.var()))); mk_axiom(~p_le_r1, n_le_div); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(p_ge_r1.var()), ctx().bool_var2expr(n_ge_div.var()))); mk_axiom(~p_ge_r1, n_ge_div); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; all_divs_valid = false; @@ -1643,8 +1697,12 @@ public: literal pq_rhs = ~mk_literal(a.mk_ge(pqr, zero)); literal n_le_div = mk_literal(a.mk_le(n, divc)); literal n_ge_div = mk_literal(a.mk_ge(n, divc)); + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(pq_lhs.var()), ctx().bool_var2expr(n_le_div.var()))); mk_axiom(pq_lhs, n_le_div); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(pq_rhs.var()), ctx().bool_var2expr(n_ge_div.var()))); mk_axiom(pq_rhs, n_ge_div); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; TRACE("arith", literal_vector lits; lits.push_back(pq_lhs); @@ -1759,6 +1817,8 @@ public: case lp::lia_move::branch: { TRACE("arith", tout << "branch\n";); app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); + if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_or(b, m.mk_not(b))); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";); // branch on term >= k + 1 // branch on term <= k @@ -1772,6 +1832,8 @@ public: ++m_stats.m_gomory_cuts; // m_explanation implies term <= k app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); + if (m.has_trace_stream()) th.log_axiom_instantiation(b); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n"); TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper());); m_eqs.reset(); diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 303bf5155..08434b0d0 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -308,7 +308,9 @@ namespace smt { unsigned depth = get_depth(e.m_lhs); expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m); literal lit = mk_eq_lit(lhs, rhs); + if (m.has_trace_stream()) log_axiom_instantiation(ctx().bool_var2expr(lit.var())); ctx().mk_th_axiom(get_id(), 1, &lit); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; TRACEFN("macro expansion yields " << mk_pp(rhs, m) << "\n" << "literal " << pp_lit(ctx(), lit)); } @@ -327,6 +329,7 @@ namespace smt { // add case-axioms for all case-paths auto & vars = e.m_def->get_vars(); literal_vector preds; + ptr_vector pred_exprs; for (recfun::case_def const & c : e.m_def->get_cases()) { // applied predicate to `args` app_ref pred_applied = c.apply_case_predicate(e.m_args); @@ -337,6 +340,7 @@ namespace smt { SASSERT(u().owns_app(pred_applied)); literal concl = mk_literal(pred_applied); preds.push_back(concl); + pred_exprs.push_back(pred_applied); if (c.is_immediate()) { body_expansion be(pred_applied, c, e.m_args); @@ -348,20 +352,27 @@ namespace smt { } literal_vector guards; + ptr_vector exprs; guards.push_back(concl); for (auto & g : c.get_guards()) { expr_ref ga = apply_args(depth, vars, e.m_args, g); literal guard = mk_literal(ga); guards.push_back(~guard); + exprs.push_back(m.mk_not(ga)); literal c[2] = {~concl, guard}; + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(pred_applied, ga)); ctx().mk_th_axiom(get_id(), 2, c); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(pred_applied), m.mk_or(exprs.size(), exprs.c_ptr()))); ctx().mk_th_axiom(get_id(), guards); - + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } // the disjunction of branches is asserted // to close the available cases. + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(pred_exprs.size(), pred_exprs.c_ptr())); ctx().mk_th_axiom(get_id(), preds); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } /** @@ -382,9 +393,11 @@ namespace smt { expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs()); literal_vector clause; + ptr_vector exprs; for (auto & g : e.m_cdef->get_guards()) { expr_ref guard = apply_args(depth, vars, args, g); clause.push_back(~mk_literal(guard)); + exprs.push_back(guard); if (clause.back() == true_literal) { TRACEFN("body " << pp_body_expansion(e,m) << "\n" << clause << "\n" << guard); return; @@ -394,7 +407,9 @@ namespace smt { } } clause.push_back(mk_eq_lit(lhs, rhs)); + if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(exprs.size(), exprs.c_ptr()), m.mk_eq(lhs, rhs))); ctx().mk_th_axiom(get_id(), clause); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; TRACEFN("body " << pp_body_expansion(e,m)); TRACEFN(pp_lits(ctx(), clause)); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 2bce6cf56..98192f3ae 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2169,6 +2169,12 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits m_new_propagation = true; ctx.assign(lit, js); + if (m.has_trace_stream()) { + expr* expr = ctx.bool_var2expr(lit.var()); + if (lit.sign()) expr = get_manager().mk_not(expr); + log_axiom_instantiation(expr); + m.trace_stream() << "[end-of-instance]\n"; + } } void theory_seq::set_conflict(dependency* dep, literal_vector const& _lits) { @@ -2202,7 +2208,9 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) { justification* js = ctx.mk_justification( ext_theory_eq_propagation_justification( get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2)); + if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_eq(n1->get_owner(), n2->get_owner())); ctx.assign_eq(n1, n2, eq_justification(js)); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; m_new_propagation = true; enforce_length_coherence(n1, n2); @@ -3165,6 +3173,16 @@ bool theory_seq::solve_nc(unsigned idx) { } TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()) << "\n";); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + if (m.has_trace_stream()) { + ptr_vector exprs; + for (literal l : lits) { + expr* e = ctx.bool_var2expr(l.var()); + if (l.sign()) e = get_manager().mk_not(e); + exprs.push_back(e); + } + log_axiom_instantiation(get_manager().mk_or(exprs.size(), exprs.c_ptr())); + m.trace_stream() << "[end-of-instance]\n"; + } return true; } @@ -4571,12 +4589,17 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { if (!lits.empty()) { TRACE("seq", tout << "creating intersection " << e3 << "\n";); lits.push_back(lit); - literal inter = mk_literal(m_util.re.mk_in_re(s, e3)); + expr* e = m_util.re.mk_in_re(s, e3); + literal inter = mk_literal(e); justification* js = ctx.mk_justification( ext_theory_propagation_justification( get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), inter)); ctx.assign(inter, js); + if (m.has_trace_stream()) { + log_axiom_instantiation(e); + m.trace_stream() << "[end-of-instance]\n"; + } return; } @@ -4592,16 +4615,21 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { unsigned_vector states; a->get_epsilon_closure(a->init(), states); lits.push_back(~lit); + ptr_vector exprs; for (unsigned st : states) { - lits.push_back(mk_accept(s, zero, e3, st)); + literal acc = mk_accept(s, zero, e3, st); + lits.push_back(acc); + exprs.push_back(ctx.bool_var2expr(acc.var())); } if (lits.size() == 2) { propagate_lit(nullptr, 1, &lit, lits[1]); } else { TRACE("seq", ctx.display_literals_verbose(tout, lits) << "\n";); + if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(n, get_manager().mk_or(exprs.size(), exprs.c_ptr()))); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } } @@ -5060,19 +5088,28 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) { return lit; } +void theory_seq::push_lit_as_expr(literal l, ptr_vector& buf) { + expr* e = get_context().bool_var2expr(l.var()); + if (l.sign()) e = get_manager().mk_not(e); + buf.push_back(e); +} + void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, literal l5) { context& ctx = get_context(); literal_vector lits; + ptr_vector exprs; if (l1 == true_literal || l2 == true_literal || l3 == true_literal || l4 == true_literal || l5 == true_literal) return; - if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); } - if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); } - if (l3 != null_literal && l3 != false_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); } - if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); } - if (l5 != null_literal && l5 != false_literal) { ctx.mark_as_relevant(l5); lits.push_back(l5); } + if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); push_lit_as_expr(l1, exprs); } + if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); push_lit_as_expr(l2, exprs); } + if (l3 != null_literal && l3 != false_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); push_lit_as_expr(l3, exprs); } + if (l4 != null_literal && l4 != false_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); push_lit_as_expr(l4, exprs); } + if (l5 != null_literal && l5 != false_literal) { ctx.mark_as_relevant(l5); lits.push_back(l5); push_lit_as_expr(l5, exprs); } TRACE("seq", ctx.display_literals_verbose(tout << "assert:\n", lits) << "\n";); m_new_propagation = true; ++m_stats.m_add_axiom; + if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_or(exprs.size(), exprs.c_ptr())); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } expr* theory_seq::coalesce_chars(expr* const& e) { @@ -5195,7 +5232,9 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2)); m_new_propagation = true; + if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_eq(e1, e2)); ctx.assign_eq(n1, n2, eq_justification(js)); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -5237,7 +5276,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { lits.push_back(mk_literal(d)); } ++m_stats.m_add_axiom; + if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(e, get_manager().mk_or(disj.size(), disj.c_ptr()))); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; for (expr* d : disj) { add_axiom(lit, ~mk_literal(d)); } @@ -5557,14 +5598,19 @@ void theory_seq::propagate_accept(literal lit, expr* acc) { eautomaton::moves mvs; aut->get_moves_from(src, mvs); TRACE("seq", tout << mvs.size() << "\n";); + ptr_vector exprs; for (auto const& mv : mvs) { expr_ref nth = mk_nth(e, idx); expr_ref t = mv.t()->accept(nth); get_context().get_rewriter()(t); - literal step = mk_literal(mk_step(e, idx, re, src, mv.dst(), t)); + expr* step_e = mk_step(e, idx, re, src, mv.dst(), t); + literal step = mk_literal(step_e); lits.push_back(step); + exprs.push_back(step_e); } + if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(acc, get_manager().mk_or(exprs.size(), exprs.c_ptr()))); get_context().mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index aa278e972..83da23401 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -542,6 +542,7 @@ namespace smt { // terms whose meaning are encoded using axioms. void enque_axiom(expr* e); void deque_axiom(expr* e); + void push_lit_as_expr(literal l, ptr_vector& buf); void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal); void add_indexof_axiom(expr* e); void add_replace_axiom(expr* e); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index f0e11c248..3bfda2379 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -217,7 +217,9 @@ namespace smt { } literal lit(ctx.get_literal(e)); ctx.mark_as_relevant(lit); + if (m.has_trace_stream()) log_axiom_instantiation(e); ctx.mk_th_axiom(get_id(), 1, &lit); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; // crash/error avoidance: add all axioms to the trail m_trail.push_back(e); @@ -1084,7 +1086,9 @@ namespace smt { literal lit(mk_eq(len_str, len, false)); ctx.mark_as_relevant(lit); + if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(lit.var())); ctx.mk_th_axiom(get_id(), 1, &lit); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } else { // build axiom 1: Length(a_str) >= 0 { @@ -1126,7 +1130,9 @@ namespace smt { TRACE("str", tout << "string axiom 2: " << mk_ismt2_pp(lhs, m) << " <=> " << mk_ismt2_pp(rhs, m) << std::endl;); literal l(mk_eq(lhs, rhs, true)); ctx.mark_as_relevant(l); + if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var())); ctx.mk_th_axiom(get_id(), 1, &l); + if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } } From 6e508d422115a95fffd3c48f496a57dd86db8470 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Fri, 22 Feb 2019 14:09:35 +0100 Subject: [PATCH 09/16] fixing Windows compile issue --- src/ast/bv_decl_plugin.cpp | 20 ++++++++++++++++---- src/smt/theory_jobscheduler.cpp | 18 ++++++++++++------ src/smt/theory_lra.cpp | 18 ++++++++++++------ 3 files changed, 40 insertions(+), 16 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 50f1fbfed..d95261402 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -18,7 +18,6 @@ Revision History: --*/ #include #include -#include #include "ast/bv_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "util/warning.h" @@ -876,6 +875,17 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const { return mk_numeral(val, bv_size); } +void log_binary_data(std::ostream &out, unsigned val, unsigned numBits) { + SASSERT(numBits <= sizeof(unsigned)*8); + for (int shift = numBits-1; shift >= 0; --shift) { + if (val & (1 << shift)) { + out << "1"; + } else { + out << "0"; + } + } + } + app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { parameter p[2] = { parameter(val), parameter(static_cast(bv_size)) }; app * r = m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr); @@ -888,7 +898,9 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { if (bv_size % 4 == 0) { m_manager.trace_stream() << "#x" << std::hex << std::setw(bv_size/4) << std::setfill('0') << val << "\n"; } else { - m_manager.trace_stream() << "#b" << std::bitset(val.get_unsigned()).to_string().substr(sizeof(unsigned)*8 - bv_size) << "\n"; + m_manager.trace_stream() << "#b"; + log_binary_data(m_manager.trace_stream(), val.get_unsigned(), bv_size); + m_manager.trace_stream() << "\n"; } return r; } @@ -923,9 +935,9 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { } for (unsigned i = 0; i < size; ++i) { if (i == 0 && firstDigitLength != 0) { - m_manager.trace_stream() << std::bitset(digits[size-1]).to_string().substr(digitBitSize - firstDigitLength); + log_binary_data(m_manager.trace_stream(), digits[size-1], firstDigitLength); } else { - m_manager.trace_stream() << std::bitset(digits[size-i-1]); + log_binary_data(m_manager.trace_stream(), digits[size-i-1], digitBitSize); } } m_manager.trace_stream() << "\n"; diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index e878594f3..6b1034ab6 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -306,8 +306,10 @@ namespace smt { literal end_ge_lo = mk_ge(ji.m_end, clb); // Initialization ensures that satisfiable states have completion time below end. ast_manager& m = get_manager(); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var()))); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) { + log_axiom_instantiation(m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var()))); + m.trace_stream() << "[end-of-instance]\n"; + } region& r = ctx.get_region(); ctx.assign(end_ge_lo, ctx.mk_justification( @@ -383,8 +385,10 @@ namespace smt { context& ctx = get_context(); ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr); ast_manager& m = get_manager(); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(ctx.bool_var2expr(lits[0].var()), ctx.bool_var2expr(lits[1].var()), ctx.bool_var2expr(lits[2].var())), ctx.bool_var2expr(lits[3].var()))); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) { + log_axiom_instantiation(m.mk_implies(m.mk_and(ctx.bool_var2expr(lits[0].var()), ctx.bool_var2expr(lits[1].var()), ctx.bool_var2expr(lits[2].var())), ctx.bool_var2expr(lits[3].var()))); + m.trace_stream() << "[end-of-instance]\n"; + } return true; } @@ -890,8 +894,10 @@ namespace smt { if (ctx.is_diseq(e1, e2)) continue; literal eq = mk_eq_lit(e1, e2); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(eq.var()), m.mk_not(ctx.bool_var2expr(eq.var())))); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) { + log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(eq.var()), m.mk_not(ctx.bool_var2expr(eq.var())))); + m.trace_stream() << "[end-of-instance]\n"; + } if (ctx.get_assignment(eq) != l_false) { ctx.mark_as_relevant(eq); if (assume_eq(e1, e2)) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 6961f8e0b..5703e34dd 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1062,8 +1062,10 @@ public: expr_ref hi(a.mk_ge(a.mk_sub(x, to_r), a.mk_real(1)), m); if (m.has_trace_stream()) th.log_axiom_instantiation(lo); mk_axiom(mk_literal(lo)); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_not(hi)); + if (m.has_trace_stream()) { + m.trace_stream() << "[end-of-instance]\n"; + th.log_axiom_instantiation(m.mk_not(hi)); + } mk_axiom(~mk_literal(hi)); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -1805,8 +1807,10 @@ public: case lp::lia_move::branch: { TRACE("arith", tout << "branch\n";); app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_or(b, m.mk_not(b))); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) { + th.log_axiom_instantiation(m.mk_or(b, m.mk_not(b))); + m.trace_stream() << "[end-of-instance]\n"; + } IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";); // branch on term >= k + 1 // branch on term <= k @@ -1820,8 +1824,10 @@ public: ++m_stats.m_gomory_cuts; // m_explanation implies term <= k app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); - if (m.has_trace_stream()) th.log_axiom_instantiation(b); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + if (m.has_trace_stream()) { + th.log_axiom_instantiation(b); + m.trace_stream() << "[end-of-instance]\n"; + } IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n"); TRACE("arith", dump_cut_lemma(tout, m_lia->get_term(), m_lia->get_offset(), m_lia->get_explanation(), m_lia->is_upper());); m_eqs.reset(); From a8586746bebe6bca001e208660d8ea908b4c15e3 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Sat, 23 Feb 2019 02:47:33 +0100 Subject: [PATCH 10/16] cleanup for pull request --- src/ast/bv_decl_plugin.cpp | 138 +++---------------------------- src/ast/bv_decl_plugin.h | 44 +++++++++- src/ast/datatype_decl_plugin.cpp | 82 +++++++++--------- src/ast/datatype_decl_plugin.h | 2 + src/util/mpz.cpp | 99 +++++++++++++++++++++- src/util/mpz.h | 13 ++- src/util/rational.h | 4 + 7 files changed, 212 insertions(+), 170 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index d95261402..29b3fd8a8 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -17,21 +17,12 @@ Revision History: --*/ #include -#include #include "ast/bv_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "util/warning.h" #include "ast/ast_pp.h" #include "ast/ast_smt2_pp.h" -#if defined(_MP_INTERNAL) -#include "util/mpn.h" -#elif defined(_MP_GMP) -#include -#else -#error No multi-precision library selected. -#endif - bv_decl_plugin::bv_decl_plugin(): m_bv_sym("bv"), m_concat_sym("concat"), @@ -875,14 +866,15 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const { return mk_numeral(val, bv_size); } -void log_binary_data(std::ostream &out, unsigned val, unsigned numBits) { - SASSERT(numBits <= sizeof(unsigned)*8); - for (int shift = numBits-1; shift >= 0; --shift) { - if (val & (1 << shift)) { - out << "1"; - } else { - out << "0"; - } + void bv_util::log_mk_numeral(rational const & val, unsigned bv_size) const { + if (bv_size % 4 == 0) { + m_manager.trace_stream() << "#x"; + val.display_hex(m_manager.trace_stream(), bv_size); + m_manager.trace_stream() << "\n"; + } else { + m_manager.trace_stream() << "#b"; + val.display_bin(m_manager.trace_stream(), bv_size); + m_manager.trace_stream() << "\n"; } } @@ -891,73 +883,7 @@ app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { app * r = m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr); if (m_plugin->log_constant_meaning_prelude(r)) { - std::ios fmt(nullptr); - fmt.copyfmt(m_manager.trace_stream()); - SASSERT(val.is_int()); - if (val.is_small()) { - if (bv_size % 4 == 0) { - m_manager.trace_stream() << "#x" << std::hex << std::setw(bv_size/4) << std::setfill('0') << val << "\n"; - } else { - m_manager.trace_stream() << "#b"; - log_binary_data(m_manager.trace_stream(), val.get_unsigned(), bv_size); - m_manager.trace_stream() << "\n"; - } - return r; - } -#ifndef _MP_GMP - digit_t *digits = mpz_manager::digits(val.to_mpq().numerator()); - unsigned size = mpz_manager::size(val.to_mpq().numerator()); - if (bv_size % 4 == 0) { - m_manager.trace_stream() << "#x" << std::hex; - unsigned bitSize = size * sizeof(digit_t) * 8; - if (bv_size > bitSize) { - for (unsigned i = 0; i < (bv_size - bitSize)/4; ++i) { - m_manager.trace_stream() << 0; - } - } - m_manager.trace_stream() << digits[size-1] << std::setw(sizeof(digit_t)*2) << std::setfill('0'); - for (unsigned i = 1; i < size; ++i) { - m_manager.trace_stream() << digits[size-i-1]; - } - m_manager.trace_stream() << "\n"; - } else { - m_manager.trace_stream() << "#b"; - const unsigned digitBitSize = sizeof(digit_t) * 8; - unsigned bitSize = size * digitBitSize; - unsigned firstDigitLength; - if (bv_size > bitSize) { - firstDigitLength = 0; - for (unsigned i = 0; i < (bv_size - bitSize)/4; ++i) { - m_manager.trace_stream() << 0; - } - } else { - firstDigitLength = bv_size % digitBitSize; - } - for (unsigned i = 0; i < size; ++i) { - if (i == 0 && firstDigitLength != 0) { - log_binary_data(m_manager.trace_stream(), digits[size-1], firstDigitLength); - } else { - log_binary_data(m_manager.trace_stream(), digits[size-i-1], digitBitSize); - } - } - m_manager.trace_stream() << "\n"; - } -#else - // GMP version - const unsigned base = bv_size % 4 == 0 ? 16 : 2; - size_t sz = mpz_sizeinbase(*(val.to_mpq().numerator().m_ptr), base) + 2; - unsigned requiredLength = bv_size / (base == 16 ? 4 : 1); - unsigned padding = requiredLength > sz ? requiredLength - sz : 0; - sbuffer buffer(sz, 0); - mpz_get_str(buffer.c_ptr(), base, *(val.to_mpq().numerator().m_ptr)); - m_manager.trace_stream() << (base == 16 ? "#x" : "#b"); - for (unsigned i = 0; i < padding; ++i) { - m_manager.trace_stream() << 0; - } - m_manager.trace_stream() << buffer.c_ptr() << "\n"; -#endif - m_manager.trace_stream().copyfmt(fmt); - m_manager.trace_stream() << std::dec; + log_mk_numeral(val, bv_size); } return r; @@ -978,46 +904,4 @@ app * bv_util::mk_bv2int(expr* e) { sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT); parameter p(s); return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e); -} - -app * bv_util::mk_bv(unsigned n, expr* const* es) { - app * r = m_manager.mk_app(get_fid(), OP_MKBV, n, es); - - if (m_manager.has_trace_stream()) { - for (unsigned i = 0; i < n; ++i) { - if (!m_manager.is_true(es[i]) && !m_manager.is_true(es[i])) - return r; - } - - if (m_plugin->log_constant_meaning_prelude(r)) { - if (n % 4 == 0) { - m_manager.trace_stream() << " #x"; - - m_manager.trace_stream() << std::hex; - uint8_t hexDigit = 0; - unsigned curLength = (4 - n % 4) % 4; - for (unsigned i = 0; i < n; ++i) { - hexDigit <<= 1; - ++curLength; - if (m_manager.is_true(es[i])) { - hexDigit |= 1; - } - if (curLength == 4) { - m_manager.trace_stream() << hexDigit; - hexDigit = 0; - } - } - m_manager.trace_stream() << std::dec; - } else { - m_manager.trace_stream() << " #b"; - for (unsigned i = 0; i < n; ++i) { - m_manager.trace_stream() << (m_manager.is_true(es[i]) ? 1 : 0); - } - } - - m_manager.trace_stream() << ")\n"; - } - } - - return r; - } \ No newline at end of file +} \ No newline at end of file diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 3e087f63f..f69ce1c02 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -381,6 +381,8 @@ class bv_util : public bv_recognizers { ast_manager & m_manager; bv_decl_plugin * m_plugin; + void log_mk_numeral(rational const & val, unsigned bv_size) const; + public: bv_util(ast_manager & m); @@ -434,7 +436,47 @@ public: app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); } app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); } - app * mk_bv(unsigned n, expr* const* es); + app * mk_bv(unsigned n, expr* const* es) { + app * r = m_manager.mk_app(get_fid(), OP_MKBV, n, es); + + if (m_manager.has_trace_stream()) { + for (unsigned i = 0; i < n; ++i) { + if (!m_manager.is_true(es[i]) && !m_manager.is_true(es[i])) + return r; + } + + if (m_plugin->log_constant_meaning_prelude(r)) { + if (n % 4 == 0) { + m_manager.trace_stream() << " #x"; + + m_manager.trace_stream() << std::hex; + uint8_t hexDigit = 0; + unsigned curLength = (4 - n % 4) % 4; + for (unsigned i = 0; i < n; ++i) { + hexDigit <<= 1; + ++curLength; + if (m_manager.is_true(es[i])) { + hexDigit |= 1; + } + if (curLength == 4) { + m_manager.trace_stream() << hexDigit; + hexDigit = 0; + } + } + m_manager.trace_stream() << std::dec; + } else { + m_manager.trace_stream() << " #b"; + for (unsigned i = 0; i < n; ++i) { + m_manager.trace_stream() << (m_manager.is_true(es[i]) ? 1 : 0); + } + } + + m_manager.trace_stream() << ")\n"; + } + } + + return r; + } }; diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 8b57a33ae..8bf0abbb3 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -453,6 +453,48 @@ namespace datatype { } } + void plugin::log_axiom_definitions(symbol const& s, sort * new_sort) { + symbol const& family_name = m_manager->get_family_name(get_family_id()); + for (constructor const* c : *m_defs[s]) { + func_decl_ref f = c->instantiate(new_sort); + const unsigned num_args = f->get_arity(); + if (num_args == 0) continue; + for (unsigned i = 0; i < num_args; ++i) { + m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; + ++m_id_counter; + } + const unsigned constructor_id = m_id_counter; + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name(); + for (unsigned i = 0; i < num_args; ++i) { + m_manager->trace_stream() << " " << family_name << "#" << constructor_id - num_args + i; + } + m_manager->trace_stream() << "\n"; + ++m_id_counter; + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n"; + ++m_id_counter; + m_axiom_bases.insert(f->get_name(), constructor_id + 4); + std::ostringstream var_sorts; + for (accessor const* a : *c) { + var_sorts << " (;" << a->range()->get_name() << ")"; + } + std::string var_description = var_sorts.str(); + unsigned i = 0; + for (accessor const* a : *c) { + func_decl_ref acc = a->instantiate(new_sort); + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n"; + ++m_id_counter; + m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i + << " " << family_name << "#" << m_id_counter - 1 << "\n"; + ++m_id_counter; + m_manager->trace_stream() << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 + << " " << family_name << "#" << m_id_counter - 1 << "\n"; + m_manager->trace_stream() << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; + ++m_id_counter; + ++i; + } + } + } + bool plugin::mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts) { begin_def_block(); for (unsigned i = 0; i < num_datatypes; ++i) { @@ -471,45 +513,7 @@ namespace datatype { for (symbol const& s : m_def_block) { new_sorts.push_back(m_defs[s]->instantiate(ps)); if (m_manager->has_trace_stream()) { - symbol const& family_name = m_manager->get_family_name(get_family_id()); - for (constructor const* c : *m_defs[s]) { - func_decl_ref f = c->instantiate(new_sorts.back()); - const unsigned num_args = f->get_arity(); - if (num_args == 0) continue; - for (unsigned i = 0; i < num_args; ++i) { - m_manager->trace_stream() << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n"; - ++m_id_counter; - } - const unsigned constructor_id = m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << constructor_id << " " << f->get_name(); - for (unsigned i = 0; i < num_args; ++i) { - m_manager->trace_stream() << " " << family_name << "#" << constructor_id - num_args + i; - } - m_manager->trace_stream() << "\n"; - ++m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n"; - ++m_id_counter; - m_axiom_bases.insert(f->get_name(), constructor_id + 4); - std::ostringstream var_sorts; - for (accessor const* a : *c) { - var_sorts << " (;" << a->range()->get_name() << ")"; - } - std::string var_description = var_sorts.str(); - unsigned i = 0; - for (accessor const* a : *c) { - func_decl_ref acc = a->instantiate(new_sorts.back()); - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " " << acc->get_name() << " " << family_name << "#" << constructor_id << "\n"; - ++m_id_counter; - m_manager->trace_stream() << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i - << " " << family_name << "#" << m_id_counter - 1 << "\n"; - ++m_id_counter; - m_manager->trace_stream() << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1 - << " " << family_name << "#" << m_id_counter - 1 << "\n"; - m_manager->trace_stream() << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n"; - ++m_id_counter; - ++i; - } - } + log_axiom_definitions(s, new_sorts.back()); } } return true; diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index cf0b47784..e9734ac0b 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -213,6 +213,8 @@ namespace datatype { void inherit(decl_plugin* other_p, ast_translation& tr) override; + void log_axiom_definitions(symbol const& s, sort * new_sort); + public: plugin(): m_id_counter(0), m_class_id(0) {} ~plugin() override; diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 0d3a6040d..27d3c882c 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -16,7 +16,8 @@ Author: Revision History: --*/ -#include +#include +#include #include "util/mpz.h" #include "util/buffer.h" #include "util/trace.h" @@ -1725,6 +1726,102 @@ void mpz_manager::display_smt2(std::ostream & out, mpz const & a, bool de } } +template +void mpz_manager::display_hex(std::ostream & out, mpz const & a, unsigned num_bits) const { + SASSERT(num_bits % 4 == 0); + std::ios fmt(nullptr); + fmt.copyfmt(out); + out << std::hex; + if (is_small(a)) { + out << std::setw(num_bits/4) << std::setfill('0') << get_uint64(a); + } else { +#ifndef _MP_GMP + digit_t *ds = digits(a); + unsigned sz = size(a); + unsigned bitSize = sz * sizeof(digit_t) * 8; + unsigned firstDigitSize; + if (num_bits >= bitSize) { + firstDigitSize = sizeof(digit_t) * 2; + + for (unsigned i = 0; i < (num_bits - bitSize)/4; ++i) { + out << "0"; + } + } else { + firstDigitSize = num_bits % (sizeof(digit_t) * 8) / 4; + } + + out << std::setfill('0') << std::setw(firstDigitSize) << ds[sz-1] << std::setw(sizeof(digit_t)*2); + for (unsigned i = 1; i < sz; ++i) { + out << ds[sz-i-1]; + } +#else + // GMP version + size_t sz = mpz_sizeinbase(*(a.m_ptr), 16); + unsigned requiredLength = num_bits / 4; + unsigned padding = requiredLength > sz ? requiredLength - sz : 0; + sbuffer buffer(sz, 0); + mpz_get_str(buffer.c_ptr(), 16, *(a.m_ptr)); + for (unsigned i = 0; i < padding; ++i) { + out << "0"; + } + out << buffer.c_ptr() + (sz > requiredLength ? sz - requiredLength : 0); +#endif + } + out.copyfmt(fmt); + out << std::dec; +} + +void display_binary_data(std::ostream &out, unsigned val, unsigned numBits) { + SASSERT(numBits <= sizeof(unsigned)*8); + for (int shift = numBits-1; shift >= 0; --shift) { + if (val & (1 << shift)) { + out << "1"; + } else { + out << "0"; + } + } + } + +template +void mpz_manager::display_bin(std::ostream & out, mpz const & a, unsigned num_bits) const { + if (is_small(a)) { + display_binary_data(out, get_uint64(a), num_bits); + } else { +#ifndef _MP_GMP + digit_t *ds = digits(a); + unsigned sz = size(a); + const unsigned digitBitSize = sizeof(digit_t) * 8; + unsigned bitSize = sz * digitBitSize; + unsigned firstDigitLength; + if (num_bits > bitSize) { + firstDigitLength = 0; + for (unsigned i = 0; i < (num_bits - bitSize); ++i) { + out << "0"; + } + } else { + firstDigitLength = num_bits % digitBitSize; + } + for (unsigned i = 0; i < sz; ++i) { + if (i == 0 && firstDigitLength != 0) { + display_binary_data(out, ds[sz-1], firstDigitLength); + } else { + display_binary_data(out, ds[sz-i-1], digitBitSize); + } + } +#else + // GMP version + size_t sz = mpz_sizeinbase(*(a.m_ptr), 2); + unsigned padding = num_bits > sz ? num_bits - sz : 0; + sbuffer buffer(sz, 0); + mpz_get_str(buffer.c_ptr(), 2, *(a.m_ptr)); + for (unsigned i = 0; i < padding; ++i) { + out << "0"; + } + out << buffer.c_ptr() + (sz > num_bits ? sz - num_bits : 0); +#endif + } +} + template std::string mpz_manager::to_string(mpz const & a) const { std::ostringstream buffer; diff --git a/src/util/mpz.h b/src/util/mpz.h index c258a1e62..0faf13d18 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -99,7 +99,6 @@ class mpz { friend class mpbq; friend class mpbq_manager; friend class mpz_stack; - friend class bv_util; mpz & operator=(mpz const & other) { UNREACHABLE(); return *this; } public: mpz(int v):m_val(v), m_kind(mpz_small), m_owner(mpz_self), m_ptr(nullptr) {} @@ -135,7 +134,6 @@ inline void swap(mpz & m1, mpz & m2) { m1.swap(m2); } template class mpz_manager { - friend class bv_util; mutable small_object_allocator m_allocator; mutable omp_nest_lock_t m_lock; #define MPZ_BEGIN_CRITICAL() if (SYNCH) omp_set_nest_lock(&m_lock); @@ -594,6 +592,17 @@ public: */ void display_smt2(std::ostream & out, mpz const & a, bool decimal) const; + /** + \brief Displays the num_bits least significant bits of a mpz number in hexadecimal format. + num_bits must be divisible by 4. + */ + void display_hex(std::ostream & out, mpz const & a, unsigned num_bits) const; + + /** + \brief Displays the num_bits least significant bits of a mpz number in binary format. + */ + void display_bin(std::ostream & out, mpz const & a, unsigned num_bits) const; + static unsigned hash(mpz const & a); static bool is_one(mpz const & a) { diff --git a/src/util/rational.h b/src/util/rational.h index dc805511f..bf68c0bf6 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -95,6 +95,10 @@ public: void display_smt2(std::ostream & out) const { return m().display_smt2(out, m_val, false); } + void display_hex(std::ostream & out, unsigned num_bits) const { SASSERT(is_int()); return m().display_hex(out, m_val.numerator(), num_bits); } + + void display_bin(std::ostream & out, unsigned num_bits) const { SASSERT(is_int()); return m().display_bin(out, m_val.numerator(), num_bits); } + bool is_uint64() const { return m().is_uint64(m_val); } bool is_int64() const { return m().is_int64(m_val); } From 6ee39415235ce7b8a329192ab445e3529b3fc1ef Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Sat, 23 Feb 2019 12:08:08 +0100 Subject: [PATCH 11/16] more cleanup --- src/ast/bv_decl_plugin.cpp | 24 +++--- src/ast/bv_decl_plugin.h | 18 ++-- src/smt/smt_quantifier.cpp | 8 +- src/smt/smt_quantifier.h | 3 - src/smt/theory_arith_core.h | 6 +- src/smt/theory_arith_int.h | 12 ++- src/smt/theory_arith_nl.h | 6 +- src/smt/theory_array_base.cpp | 12 ++- src/smt/theory_bv.cpp | 24 +++++- src/smt/theory_datatype.cpp | 28 +++--- src/smt/theory_diff_logic_def.h | 6 +- src/smt/theory_dl.cpp | 6 +- src/smt/theory_jobscheduler.cpp | 57 +++++++++--- src/smt/theory_lra.cpp | 148 ++++++++++++++++++++++++++------ src/smt/theory_recfun.cpp | 24 +++++- src/smt/theory_seq.cpp | 49 ++++++++--- src/util/mpz.cpp | 1 - 17 files changed, 328 insertions(+), 104 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 29b3fd8a8..738444b3b 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -866,24 +866,20 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const { return mk_numeral(val, bv_size); } - void bv_util::log_mk_numeral(rational const & val, unsigned bv_size) const { - if (bv_size % 4 == 0) { - m_manager.trace_stream() << "#x"; - val.display_hex(m_manager.trace_stream(), bv_size); - m_manager.trace_stream() << "\n"; - } else { - m_manager.trace_stream() << "#b"; - val.display_bin(m_manager.trace_stream(), bv_size); - m_manager.trace_stream() << "\n"; - } - } - app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const { parameter p[2] = { parameter(val), parameter(static_cast(bv_size)) }; app * r = m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr); if (m_plugin->log_constant_meaning_prelude(r)) { - log_mk_numeral(val, bv_size); + if (bv_size % 4 == 0) { + m_manager.trace_stream() << "#x"; + val.display_hex(m_manager.trace_stream(), bv_size); + m_manager.trace_stream() << "\n"; + } else { + m_manager.trace_stream() << "#b"; + val.display_bin(m_manager.trace_stream(), bv_size); + m_manager.trace_stream() << "\n"; + } } return r; @@ -904,4 +900,4 @@ app * bv_util::mk_bv2int(expr* e) { sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT); parameter p(s); return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e); -} \ No newline at end of file +} diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index f69ce1c02..f15f5abd9 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -126,6 +126,7 @@ inline func_decl * get_div0_decl(ast_manager & m, func_decl * decl) { } class bv_decl_plugin : public decl_plugin { + friend class bv_util; protected: symbol m_bv_sym; symbol m_concat_sym; @@ -239,7 +240,6 @@ protected: void get_offset_term(app * a, expr * & t, rational & offset) const; - friend class bv_util; public: bv_decl_plugin(); @@ -381,8 +381,6 @@ class bv_util : public bv_recognizers { ast_manager & m_manager; bv_decl_plugin * m_plugin; - void log_mk_numeral(rational const & val, unsigned bv_size) const; - public: bv_util(ast_manager & m); @@ -436,13 +434,12 @@ public: app * mk_bvsmul_no_udfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BSMUL_NO_UDFL, n, m); } app * mk_bvumul_no_ovfl(expr* m, expr* n) { return m_manager.mk_app(get_fid(), OP_BUMUL_NO_OVFL, n, m); } - app * mk_bv(unsigned n, expr* const* es) { - app * r = m_manager.mk_app(get_fid(), OP_MKBV, n, es); - + private: + void log_bv_from_exprs(app * r, unsigned n, expr* const* es) { if (m_manager.has_trace_stream()) { for (unsigned i = 0; i < n; ++i) { if (!m_manager.is_true(es[i]) && !m_manager.is_true(es[i])) - return r; + return; } if (m_plugin->log_constant_meaning_prelude(r)) { @@ -474,6 +471,13 @@ public: m_manager.trace_stream() << ")\n"; } } + } + +public: + app * mk_bv(unsigned n, expr* const* es) { + app * r = m_manager.mk_app(get_fid(), OP_MKBV, n, es); + + log_bv_from_exprs(r, n, es); return r; } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index cb7d12d2e..008da06ec 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -32,6 +32,8 @@ namespace smt { quantifier_manager_plugin * mk_default_plugin(); + void log_single_justification(std::ostream & out, enode *en, obj_hashtable &visited, context &ctx, ast_manager &m); + /** \brief Ensures that all relevant proof steps to explain why the enode is equal to the root of its equivalence class are in the log and up-to-date. @@ -68,7 +70,7 @@ namespace smt { \brief Logs a single equality explanation step and, if necessary, recursively calls log_justification_to_root to log equalities needed by the step (e.g. argument equalities for congruence steps). */ - void quantifier_manager::log_single_justification(std::ostream & out, enode *en, obj_hashtable &visited, context &ctx, ast_manager &m) { + void log_single_justification(std::ostream & out, enode *en, obj_hashtable &visited, context &ctx, ast_manager &m) { smt::literal lit; unsigned num_args; enode *target = en->get_trans_justification().m_target; @@ -87,8 +89,8 @@ namespace smt { num_args = en->get_num_args(); for (unsigned i = 0; i < num_args; ++i) { - log_justification_to_root(out, en->get_arg(i), visited, ctx, m); - log_justification_to_root(out, target->get_arg(i), visited, ctx, m); + quantifier_manager::log_justification_to_root(out, en->get_arg(i), visited, ctx, m); + quantifier_manager::log_justification_to_root(out, target->get_arg(i), visited, ctx, m); } out << "[eq-expl] #" << en->get_owner_id() << " cg"; diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index a126407d7..a25ada87e 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -53,9 +53,6 @@ namespace smt { unsigned get_generation(quantifier * q) const; static void log_justification_to_root(std::ostream & log, enode *en, obj_hashtable &already_visited, context &ctx, ast_manager &m); - private: - static void log_single_justification(std::ostream & out, enode *en, obj_hashtable &already_visited, context &ctx, ast_manager &m); - public: bool add_instance(quantifier * q, app * pat, unsigned num_bindings, diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 283085ae3..effc0677b 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -447,7 +447,11 @@ namespace smt { tout << l_ante << "\n" << l_conseq << "\n";); // literal lits[2] = {l_ante, l_conseq}; - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ante, conseq)); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_or(ante, conseq); + log_axiom_instantiation(body); + } mk_clause(l_ante, l_conseq, 0, nullptr); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index f4e901de4..ffbb9770d 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -210,7 +210,11 @@ namespace smt { expr_ref bound(m); expr* e = get_enode(v)->get_owner(); bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e))); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(to_app(bound), m.mk_not(to_app(bound)))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_or(to_app(bound), m.mk_not(to_app(bound))); + log_axiom_instantiation(body); + } TRACE("arith_int", tout << mk_bounded_pp(bound, m) << "\n";); context & ctx = get_context(); ctx.internalize(bound, true); @@ -368,7 +372,11 @@ namespace smt { mk_polynomial_ge(pol.size(), pol.c_ptr(), unsat_row[0]+rational(1), p2); context& ctx = get_context(); - if (get_manager().has_trace_stream()) log_axiom_instantiation(get_manager().mk_or(p1, p2)); + if (get_manager().has_trace_stream()) { + app_ref body(get_manager()); + body = get_manager().mk_or(p1, p2); + log_axiom_instantiation(body); + } ctx.internalize(p1, false); ctx.internalize(p2, false); literal l1(ctx.get_literal(p1)), l2(ctx.get_literal(p2)); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 457c6e068..80687dd18 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -790,7 +790,11 @@ namespace smt { TRACE("non_linear", tout << "new bound:\n" << mk_pp(bound, get_manager()) << "\n";); context & ctx = get_context(); ast_manager & m = get_manager(); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(bound, m.mk_not(bound))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_or(bound, m.mk_not(bound)); + log_axiom_instantiation(body); + } ctx.internalize(bound, true); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; ctx.mark_as_relevant(bound); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 9ba520c9d..9706f7160 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -191,7 +191,11 @@ namespace smt { TRACE("array_map_bug", tout << "axiom2:\n"; tout << mk_ismt2_pp(idx1->get_owner(), m) << "\n=\n" << mk_ismt2_pp(idx2->get_owner(), m); tout << "\nimplies\n" << mk_ismt2_pp(conseq_expr, m) << "\n";); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(ante.var()), conseq_expr)); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_or(ctx.bool_var2expr(ante.var()), conseq_expr); + log_axiom_instantiation(body); + } assert_axiom(ante, conseq); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -335,7 +339,11 @@ namespace smt { literal sel1_eq_sel2 = mk_eq(sel1, sel2, true); ctx.mark_as_relevant(n1_eq_n2); ctx.mark_as_relevant(sel1_eq_sel2); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(n1_eq_n2.var())), m.mk_not(ctx.bool_var2expr(sel1_eq_sel2.var())))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_not(ctx.bool_var2expr(n1_eq_n2.var())), m.mk_not(ctx.bool_var2expr(sel1_eq_sel2.var()))); + log_axiom_instantiation(body); + } assert_axiom(n1_eq_n2, ~sel1_eq_sel2); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 0301a86e1..2383f62cc 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -255,7 +255,11 @@ namespace smt { context & ctx = get_context(); ast_manager & m = get_manager(); expr * eq = ctx.bool_var2expr(l.var()); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_eq(mk_bit2bool(get_enode(v1)->get_owner(), idx), m.mk_not(mk_bit2bool(get_enode(v2)->get_owner(), idx))), m.mk_not(eq))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_eq(mk_bit2bool(get_enode(v1)->get_owner(), idx), m.mk_not(mk_bit2bool(get_enode(v2)->get_owner(), idx))), m.mk_not(eq)); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), 1, &l); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (ctx.relevancy()) { @@ -472,7 +476,11 @@ namespace smt { e1 = mk_bit2bool(o1, i); e2 = mk_bit2bool(o2, i); literal eq = mk_eq(e1, e2, true); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var())))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var()))); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), l1, ~l2, ~eq); ctx.mk_th_axiom(get_id(), ~l1, l2, ~eq); ctx.mk_th_axiom(get_id(), l1, l2, eq); @@ -1228,7 +1236,11 @@ namespace smt { exprs.push_back(diff); } m_stats.m_num_diseq_dynamic++; - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_or(exprs.size(), exprs.c_ptr()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_or(exprs.size(), exprs.c_ptr())); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -1341,7 +1353,11 @@ namespace smt { lits.push_back(antecedent); literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), false); lits.push_back(~eq); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_implies(ctx.bool_var2expr(consequent.var()), ctx.bool_var2expr(antecedent.var())))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_implies(ctx.bool_var2expr(consequent.var()), ctx.bool_var2expr(antecedent.var()))); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 0fac42501..2ae4dad20 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -140,12 +140,14 @@ namespace smt { args.push_back(acc); } expr * mk = m.mk_app(c, args.size(), args.c_ptr()); - app_ref ax(m); - ax = m.mk_eq(n->get_owner(), mk); - if (antecedent != null_literal) { - ax = m.mk_implies(get_context().bool_var2expr(antecedent.var()), ax); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_eq(n->get_owner(), mk); + if (antecedent != null_literal) { + body = m.mk_implies(get_context().bool_var2expr(antecedent.var()), body); + } + log_axiom_instantiation(body, 1, &n); } - if (m.has_trace_stream()) log_axiom_instantiation(ax, 1, &n); assert_eq_axiom(n, mk, antecedent); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -175,9 +177,11 @@ namespace smt { for (func_decl * acc : accessors) { app * acc_app = m.mk_app(acc, n->get_owner()); enode * arg = n->get_arg(i); - app_ref eq(m); - eq = m.mk_eq(arg->get_owner(), acc_app); - if (m.has_trace_stream()) log_axiom_instantiation(eq, base_id + 3*i, bindings.size(), bindings.c_ptr(), base_id - 3, used_enodes); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_eq(arg->get_owner(), acc_app); + log_axiom_instantiation(body, base_id + 3*i, bindings.size(), bindings.c_ptr(), base_id - 3, used_enodes); + } assert_eq_axiom(arg, acc_app, null_literal); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; ++i; @@ -236,9 +240,11 @@ namespace smt { arg = ctx.get_enode(acc_app); } app * acc_own = m.mk_app(acc1, own); - app_ref imp(m); - imp = m.mk_implies(rec_app, m.mk_eq(arg->get_owner(), acc_own)); - if (m.has_trace_stream()) log_axiom_instantiation(imp, 1, &n); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(rec_app, m.mk_eq(arg->get_owner(), acc_own)); + log_axiom_instantiation(body, 1, &n); + } assert_eq_axiom(arg, acc_own, is_con); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index b7bd9adf1..3a9553f95 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -1009,7 +1009,11 @@ void theory_diff_logic::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v t2 = m_util.mk_numeral(k, m.get_sort(s2.get())); // t1 - s1 = k eq = m.mk_eq(s2.get(), t2.get()); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_eq(m.mk_eq(m_util.mk_add(s1, t2), t1), eq)); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_eq(m.mk_eq(m_util.mk_add(s1, t2), t1), eq); + log_axiom_instantiation(body); + } TRACE("diff_logic", tout << v1 << " .. " << v2 << "\n"; diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index be99b1234..6bbc8d03d 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -256,7 +256,11 @@ namespace smt { lt = u().mk_lt(x,y); le = b().mk_ule(m().mk_app(r,y),m().mk_app(r,x)); context& ctx = get_context(); - if (m().has_trace_stream()) log_axiom_instantiation(m().mk_eq(lt, le)); + if (m().has_trace_stream()) { + app_ref body(m()); + body = m().mk_eq(lt, le); + log_axiom_instantiation(body); + } ctx.internalize(lt, false); ctx.internalize(le, false); literal lit1(ctx.get_literal(lt)); diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index 6b1034ab6..031988bc6 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -307,7 +307,9 @@ namespace smt { // Initialization ensures that satisfiable states have completion time below end. ast_manager& m = get_manager(); if (m.has_trace_stream()) { - log_axiom_instantiation(m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var()))); + app_ref body(m); + body = m.mk_implies(m.mk_and(m.mk_eq(eq.first->get_owner(), eq.second->get_owner()), ctx.bool_var2expr(start_ge_lo.var())), ctx.bool_var2expr(end_ge_lo.var())); + log_axiom_instantiation(body); m.trace_stream() << "[end-of-instance]\n"; } region& r = ctx.get_region(); @@ -386,7 +388,9 @@ namespace smt { ctx.mk_clause(lits.size(), lits.c_ptr(), nullptr, CLS_AUX_LEMMA, nullptr); ast_manager& m = get_manager(); if (m.has_trace_stream()) { - log_axiom_instantiation(m.mk_implies(m.mk_and(ctx.bool_var2expr(lits[0].var()), ctx.bool_var2expr(lits[1].var()), ctx.bool_var2expr(lits[2].var())), ctx.bool_var2expr(lits[3].var()))); + app_ref body(m); + body = m.mk_implies(m.mk_and(ctx.bool_var2expr(lits[0].var()), ctx.bool_var2expr(lits[1].var()), ctx.bool_var2expr(lits[2].var())), ctx.bool_var2expr(lits[3].var())); + log_axiom_instantiation(body); m.trace_stream() << "[end-of-instance]\n"; } return true; @@ -810,7 +814,11 @@ namespace smt { job_info const& ji = m_jobs[j]; literal l2 = mk_le(ji.m_end, jr.m_finite_capacity_end); context& ctx = get_context(); - if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var())); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), ~eq, l2); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; #endif @@ -822,13 +830,21 @@ namespace smt { time_t t; if (lst(j, r, t)) { literal le = mk_le(m_jobs[j].m_start, t); - if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(le.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(le.var())); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), ~eq, le); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } else { eq.neg(); - if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_not(ctx.bool_var2expr(eq.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_not(ctx.bool_var2expr(eq.var())); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), 1, &eq); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -842,7 +858,11 @@ namespace smt { vector& available = m_resources[r].m_available; literal l2 = mk_ge(m_jobs[j].m_start, available[idx].m_start); context& ctx = get_context(); - if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(ctx.bool_var2expr(eq.var()), ctx.bool_var2expr(l2.var())); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), ~eq, l2); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -856,8 +876,11 @@ namespace smt { literal l2 = mk_ge(m_jobs[j].m_start, available[idx1].m_start); literal l3 = mk_le(m_jobs[j].m_start, available[idx].m_end); context& ctx = get_context(); - ast_manager& m = get_manager(); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var())))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var()))); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), ~eq, l2, l3); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -871,8 +894,11 @@ namespace smt { literal l2 = mk_le(m_jobs[j].m_end, available[idx].m_end); literal l3 = mk_ge(m_jobs[j].m_start, available[idx1].m_start); context& ctx = get_context(); - ast_manager& m = get_manager(); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var())))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(ctx.bool_var2expr(eq.var()), m.mk_or(ctx.bool_var2expr(l2.var()), ctx.bool_var2expr(l3.var()))); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), ~eq, l2, l3); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -883,7 +909,6 @@ namespace smt { bool theory_jobscheduler::split_job2resource(unsigned j) { job_info const& ji = m_jobs[j]; context& ctx = get_context(); - ast_manager& m = get_manager(); if (ji.m_is_bound) return false; auto const& jrs = ji.m_resources; for (job_resource const& jr : jrs) { @@ -895,7 +920,9 @@ namespace smt { continue; literal eq = mk_eq_lit(e1, e2); if (m.has_trace_stream()) { - log_axiom_instantiation(m.mk_or(ctx.bool_var2expr(eq.var()), m.mk_not(ctx.bool_var2expr(eq.var())))); + app_ref body(m); + body = m.mk_or(ctx.bool_var2expr(eq.var()), m.mk_not(ctx.bool_var2expr(eq.var()))); + log_axiom_instantiation(body); m.trace_stream() << "[end-of-instance]\n"; } if (ctx.get_assignment(eq) != l_false) { @@ -916,7 +943,11 @@ namespace smt { lits.push_back(eq); exprs.push_back(ctx.bool_var2expr(eq.var())); } - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(exprs.size(), exprs.c_ptr())); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_or(exprs.size(), exprs.c_ptr()); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; return true; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 5703e34dd..d0625d705 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1030,7 +1030,11 @@ public: literal dgez = mk_literal(degz_expr); literal pos = th.mk_eq(rem, mod, false); literal neg = th.mk_eq(rem, mmod, false); - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_ite(degz_expr, ctx().bool_var2expr(pos.var()), ctx().bool_var2expr(neg.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_ite(degz_expr, ctx().bool_var2expr(pos.var()), ctx().bool_var2expr(neg.var())); + th.log_axiom_instantiation(body); + } mk_axiom(~dgez, pos); mk_axiom( dgez, neg); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; @@ -1041,7 +1045,11 @@ public: if (a.is_zero(q)) return; literal eqz = th.mk_eq(q, a.mk_real(0), false); literal eq = th.mk_eq(a.mk_mul(q, a.mk_div(p, q)), p, false); - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(ctx().bool_var2expr(eqz.var())), ctx().bool_var2expr(eq.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_not(ctx().bool_var2expr(eqz.var())), ctx().bool_var2expr(eq.var())); + th.log_axiom_instantiation(body); + } mk_axiom(eqz, eq); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -1052,7 +1060,11 @@ public: expr* x = nullptr, *y = nullptr; VERIFY (a.is_to_int(n, x)); if (a.is_to_real(x, y)) { - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_eq(n, y)); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_eq(n, y); + th.log_axiom_instantiation(body); + } mk_axiom(th.mk_eq(y, n, false)); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -1077,7 +1089,11 @@ public: VERIFY(a.is_is_int(n, x)); literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false); literal is_int = ctx().get_literal(n); - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_iff(n, ctx().bool_var2expr(eq.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_iff(n, ctx().bool_var2expr(eq.var())); + th.log_axiom_instantiation(body); + } mk_axiom(~is_int, eq); mk_axiom(is_int, ~eq); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; @@ -1134,28 +1150,56 @@ public: context& c = ctx(); if (!k.is_zero()) { - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())); + th.log_axiom_instantiation(body); + } mk_axiom(eq); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())); + th.log_axiom_instantiation(body); + } mk_axiom(mod_ge_0); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper)); + th.log_axiom_instantiation(body); + } mk_axiom(mk_literal(a.mk_le(mod, upper))); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (k.is_pos()) { - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())); + th.log_axiom_instantiation(body); + } mk_axiom(~p_ge_0, div_ge_0); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())); + th.log_axiom_instantiation(body); + } mk_axiom(~p_le_0, div_le_0); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } else { - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())); + th.log_axiom_instantiation(body); + } mk_axiom(~p_ge_0, div_le_0); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())); + th.log_axiom_instantiation(body); + } mk_axiom(~p_le_0, div_ge_0); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -1169,30 +1213,62 @@ public: // q >= 0 or (p mod q) < -q literal q_ge_0 = mk_literal(a.mk_ge(q, zero)); literal q_le_0 = mk_literal(a.mk_le(q, zero)); - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())); + th.log_axiom_instantiation(body); + } mk_axiom(q_ge_0, eq); mk_axiom(q_le_0, eq); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())); + th.log_axiom_instantiation(body); + } mk_axiom(q_ge_0, mod_ge_0); mk_axiom(q_le_0, mod_ge_0); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero)); + th.log_axiom_instantiation(body); + } mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero))); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero)); + th.log_axiom_instantiation(body); + } mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero))); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())); + th.log_axiom_instantiation(body); + } mk_axiom(q_le_0, ~p_ge_0, div_ge_0); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())); + th.log_axiom_instantiation(body); + } mk_axiom(q_le_0, ~p_le_0, div_le_0); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())); + th.log_axiom_instantiation(body); + } mk_axiom(q_ge_0, ~p_ge_0, div_le_0); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())); + th.log_axiom_instantiation(body); + } mk_axiom(q_ge_0, ~p_le_0, div_ge_0); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -1206,7 +1282,11 @@ public: exprs.push_back(c.bool_var2expr(mod_j.var())); ctx().mark_as_relevant(mod_j); } - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_or(exprs.size(), exprs.c_ptr())); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_or(exprs.size(), exprs.c_ptr()); + th.log_axiom_instantiation(body); + } ctx().mk_th_axiom(get_id(), lits.size(), lits.begin()); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -1643,10 +1723,18 @@ public: literal p_ge_r1 = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true))); literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true))); literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div_r, true))); - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(p_le_r1.var()), ctx().bool_var2expr(n_le_div.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(ctx().bool_var2expr(p_le_r1.var()), ctx().bool_var2expr(n_le_div.var())); + th.log_axiom_instantiation(body); + } mk_axiom(~p_le_r1, n_le_div); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(p_ge_r1.var()), ctx().bool_var2expr(n_ge_div.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(ctx().bool_var2expr(p_ge_r1.var()), ctx().bool_var2expr(n_ge_div.var())); + th.log_axiom_instantiation(body); + } mk_axiom(~p_ge_r1, n_ge_div); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; @@ -1687,10 +1775,18 @@ public: literal pq_rhs = ~mk_literal(a.mk_ge(pqr, zero)); literal n_le_div = mk_literal(a.mk_le(n, divc)); literal n_ge_div = mk_literal(a.mk_ge(n, divc)); - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(pq_lhs.var()), ctx().bool_var2expr(n_le_div.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(ctx().bool_var2expr(pq_lhs.var()), ctx().bool_var2expr(n_le_div.var())); + th.log_axiom_instantiation(body); + } mk_axiom(pq_lhs, n_le_div); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; - if (m.has_trace_stream()) th.log_axiom_instantiation(m.mk_implies(ctx().bool_var2expr(pq_rhs.var()), ctx().bool_var2expr(n_ge_div.var()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(ctx().bool_var2expr(pq_rhs.var()), ctx().bool_var2expr(n_ge_div.var())); + th.log_axiom_instantiation(body); + } mk_axiom(pq_rhs, n_ge_div); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; TRACE("arith", @@ -1808,7 +1904,9 @@ public: TRACE("arith", tout << "branch\n";); app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper()); if (m.has_trace_stream()) { - th.log_axiom_instantiation(m.mk_or(b, m.mk_not(b))); + app_ref body(m); + body = m.mk_or(b, m.mk_not(b)); + th.log_axiom_instantiation(body); m.trace_stream() << "[end-of-instance]\n"; } IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";); diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 08434b0d0..46cb3896a 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -360,17 +360,29 @@ namespace smt { guards.push_back(~guard); exprs.push_back(m.mk_not(ga)); literal c[2] = {~concl, guard}; - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(pred_applied, ga)); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(pred_applied, ga); + log_axiom_instantiation(body); + } ctx().mk_th_axiom(get_id(), 2, c); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_not(pred_applied), m.mk_or(exprs.size(), exprs.c_ptr()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_not(pred_applied), m.mk_or(exprs.size(), exprs.c_ptr())); + log_axiom_instantiation(body); + } ctx().mk_th_axiom(get_id(), guards); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } // the disjunction of branches is asserted // to close the available cases. - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_or(pred_exprs.size(), pred_exprs.c_ptr())); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_or(pred_exprs.size(), pred_exprs.c_ptr()); + log_axiom_instantiation(body); + } ctx().mk_th_axiom(get_id(), preds); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -407,7 +419,11 @@ namespace smt { } } clause.push_back(mk_eq_lit(lhs, rhs)); - if (m.has_trace_stream()) log_axiom_instantiation(m.mk_implies(m.mk_and(exprs.size(), exprs.c_ptr()), m.mk_eq(lhs, rhs))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(m.mk_and(exprs.size(), exprs.c_ptr()), m.mk_eq(lhs, rhs)); + log_axiom_instantiation(body); + } ctx().mk_th_axiom(get_id(), clause); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; TRACEFN("body " << pp_body_expansion(e,m)); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 72aea5909..488d3913e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2167,8 +2167,9 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits m_new_propagation = true; ctx.assign(lit, js); if (m.has_trace_stream()) { - expr* expr = ctx.bool_var2expr(lit.var()); - if (lit.sign()) expr = get_manager().mk_not(expr); + expr_ref expr(m); + expr = ctx.bool_var2expr(lit.var()); + if (lit.sign()) expr = m.mk_not(expr); log_axiom_instantiation(expr); m.trace_stream() << "[end-of-instance]\n"; } @@ -2205,7 +2206,11 @@ void theory_seq::propagate_eq(dependency* dep, enode* n1, enode* n2) { justification* js = ctx.mk_justification( ext_theory_eq_propagation_justification( get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2)); - if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_eq(n1->get_owner(), n2->get_owner())); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_eq(n1->get_owner(), n2->get_owner()); + log_axiom_instantiation(body); + } ctx.assign_eq(n1, n2, eq_justification(js)); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; m_new_propagation = true; @@ -3184,10 +3189,12 @@ bool theory_seq::solve_nc(unsigned idx) { ptr_vector exprs; for (literal l : lits) { expr* e = ctx.bool_var2expr(l.var()); - if (l.sign()) e = get_manager().mk_not(e); + if (l.sign()) e = m.mk_not(e); exprs.push_back(e); } - log_axiom_instantiation(get_manager().mk_or(exprs.size(), exprs.c_ptr())); + app_ref body(m); + body = m.mk_or(exprs.size(), exprs.c_ptr()); + log_axiom_instantiation(body); m.trace_stream() << "[end-of-instance]\n"; } return true; @@ -4647,7 +4654,11 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { } else { TRACE("seq", ctx.display_literals_verbose(tout, lits) << "\n";); - if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(n, get_manager().mk_or(exprs.size(), exprs.c_ptr()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(n, m.mk_or(exprs.size(), exprs.c_ptr())); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -5096,7 +5107,7 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) { void theory_seq::push_lit_as_expr(literal l, ptr_vector& buf) { expr* e = get_context().bool_var2expr(l.var()); - if (l.sign()) e = get_manager().mk_not(e); + if (l.sign()) e = m.mk_not(e); buf.push_back(e); } @@ -5113,7 +5124,11 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter TRACE("seq", ctx.display_literals_verbose(tout << "assert:\n", lits) << "\n";); m_new_propagation = true; ++m_stats.m_add_axiom; - if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_or(exprs.size(), exprs.c_ptr())); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_or(exprs.size(), exprs.c_ptr()); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -5240,7 +5255,11 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr(), n1, n2)); m_new_propagation = true; - if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_eq(e1, e2)); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_eq(e1, e2); + log_axiom_instantiation(body); + } ctx.assign_eq(n1, n2, eq_justification(js)); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; } @@ -5288,7 +5307,11 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { lits.push_back(mk_literal(d)); } ++m_stats.m_add_axiom; - if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(e, get_manager().mk_or(disj.size(), disj.c_ptr()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(e, m.mk_or(disj.size(), disj.c_ptr())); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; for (expr* d : disj) { @@ -5659,7 +5682,11 @@ void theory_seq::propagate_accept(literal lit, expr* acc) { lits.push_back(step); exprs.push_back(step_e); } - if (m.has_trace_stream()) log_axiom_instantiation(get_manager().mk_implies(acc, get_manager().mk_or(exprs.size(), exprs.c_ptr()))); + if (m.has_trace_stream()) { + app_ref body(m); + body = m.mk_implies(acc, m.mk_or(exprs.size(), exprs.c_ptr())); + log_axiom_instantiation(body); + } ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 27d3c882c..6776acf65 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -1768,7 +1768,6 @@ void mpz_manager::display_hex(std::ostream & out, mpz const & a, unsigned #endif } out.copyfmt(fmt); - out << std::dec; } void display_binary_data(std::ostream &out, unsigned val, unsigned numBits) { From c033fb045fee317cbdbdd78f2e27b5822ef89f3e Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Sat, 23 Feb 2019 12:34:17 +0100 Subject: [PATCH 12/16] 2 things I prevoiusly overlooked --- src/ast/bv_decl_plugin.h | 1 - src/smt/theory_lra.cpp | 4 +++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index f15f5abd9..03600131e 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -239,7 +239,6 @@ protected: func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity); void get_offset_term(app * a, expr * & t, rational & offset) const; - public: bv_decl_plugin(); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index d0625d705..49656b05c 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1076,7 +1076,9 @@ public: mk_axiom(mk_literal(lo)); if (m.has_trace_stream()) { m.trace_stream() << "[end-of-instance]\n"; - th.log_axiom_instantiation(m.mk_not(hi)); + expr_ref body(m); + body = m.mk_not(hi); + th.log_axiom_instantiation(body); } mk_axiom(~mk_literal(hi)); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; From 17adecff6802dad7f381dce3a74a1c96acc8dedb Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Mon, 25 Feb 2019 19:10:47 +0100 Subject: [PATCH 13/16] fixing ci issues fixing if condition --- src/ast/bv_decl_plugin.h | 2 +- src/smt/theory_bv.cpp | 4 ++-- src/smt/theory_datatype.cpp | 2 +- src/smt/theory_jobscheduler.cpp | 2 +- src/smt/theory_lra.cpp | 2 +- src/smt/theory_recfun.cpp | 6 +++--- src/smt/theory_seq.cpp | 12 ++++++------ src/smt/theory_seq.h | 2 +- 8 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 03600131e..b60022f21 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -437,7 +437,7 @@ public: void log_bv_from_exprs(app * r, unsigned n, expr* const* es) { if (m_manager.has_trace_stream()) { for (unsigned i = 0; i < n; ++i) { - if (!m_manager.is_true(es[i]) && !m_manager.is_true(es[i])) + if (!m_manager.is_true(es[i]) && !m_manager.is_false(es[i])) return; } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 2383f62cc..736218bc4 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -254,7 +254,7 @@ namespace smt { literal l = ~(mk_eq(e1->get_owner(), e2->get_owner(), true)); context & ctx = get_context(); ast_manager & m = get_manager(); - expr * eq = ctx.bool_var2expr(l.var()); + expr * eq = ctx.bool_var2expr(l.var()); if (m.has_trace_stream()) { app_ref body(m); body = m.mk_implies(m.mk_eq(mk_bit2bool(get_enode(v1)->get_owner(), idx), m.mk_not(mk_bit2bool(get_enode(v2)->get_owner(), idx))), m.mk_not(eq)); @@ -1219,7 +1219,7 @@ namespace smt { #endif literal_vector & lits = m_tmp_literals; - ptr_vector exprs; + expr_ref_vector exprs(m); lits.reset(); literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true); lits.push_back(eq); diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 2ae4dad20..f26791639 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -166,7 +166,7 @@ namespace smt { func_decl * d = n->get_decl(); ptr_vector const & accessors = *m_util.get_constructor_accessors(d); SASSERT(n->get_num_args() == accessors.size()); - ptr_vector bindings; + app_ref_vector bindings(m); vector> used_enodes; used_enodes.push_back(std::make_tuple(nullptr, n)); for (unsigned i = 0; i < n->get_num_args(); ++i) { diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index 031988bc6..bc0d0d2e8 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -933,7 +933,7 @@ namespace smt { } } literal_vector lits; - ptr_vector exprs; + expr_ref_vector exprs(m); for (job_resource const& jr : jrs) { unsigned r = jr.m_resource_id; res_info const& ri = m_resources[r]; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 49656b05c..e9fbaf81f 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1277,7 +1277,7 @@ public: if (m_arith_params.m_arith_enum_const_mod && k.is_pos() && k < rational(8)) { unsigned _k = k.get_unsigned(); literal_buffer lits; - ptr_vector exprs; + expr_ref_vector exprs(m); for (unsigned j = 0; j < _k; ++j) { literal mod_j = th.mk_eq(mod, a.mk_int(j), false); lits.push_back(mod_j); diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 46cb3896a..af2d56cf1 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -329,7 +329,7 @@ namespace smt { // add case-axioms for all case-paths auto & vars = e.m_def->get_vars(); literal_vector preds; - ptr_vector pred_exprs; + expr_ref_vector pred_exprs(m); for (recfun::case_def const & c : e.m_def->get_cases()) { // applied predicate to `args` app_ref pred_applied = c.apply_case_predicate(e.m_args); @@ -352,7 +352,7 @@ namespace smt { } literal_vector guards; - ptr_vector exprs; + expr_ref_vector exprs(m); guards.push_back(concl); for (auto & g : c.get_guards()) { expr_ref ga = apply_args(depth, vars, e.m_args, g); @@ -405,7 +405,7 @@ namespace smt { expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs()); literal_vector clause; - ptr_vector exprs; + expr_ref_vector exprs(m); for (auto & g : e.m_cdef->get_guards()) { expr_ref guard = apply_args(depth, vars, args, g); clause.push_back(~mk_literal(guard)); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 488d3913e..9a3f47757 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3186,7 +3186,7 @@ bool theory_seq::solve_nc(unsigned idx) { TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()) << "\n";); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); if (m.has_trace_stream()) { - ptr_vector exprs; + expr_ref_vector exprs(m); for (literal l : lits) { expr* e = ctx.bool_var2expr(l.var()); if (l.sign()) e = m.mk_not(e); @@ -4642,7 +4642,7 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) { unsigned_vector states; a->get_epsilon_closure(a->init(), states); lits.push_back(~lit); - ptr_vector exprs; + expr_ref_vector exprs(m); for (unsigned st : states) { literal acc = mk_accept(s, zero, re, st); @@ -5105,7 +5105,7 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) { return lit; } -void theory_seq::push_lit_as_expr(literal l, ptr_vector& buf) { +void theory_seq::push_lit_as_expr(literal l, expr_ref_vector& buf) { expr* e = get_context().bool_var2expr(l.var()); if (l.sign()) e = m.mk_not(e); buf.push_back(e); @@ -5114,7 +5114,7 @@ void theory_seq::push_lit_as_expr(literal l, ptr_vector& buf) { void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, literal l5) { context& ctx = get_context(); literal_vector lits; - ptr_vector exprs; + expr_ref_vector exprs(m); if (l1 == true_literal || l2 == true_literal || l3 == true_literal || l4 == true_literal || l5 == true_literal) return; if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); push_lit_as_expr(l1, exprs); } if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); push_lit_as_expr(l2, exprs); } @@ -5672,12 +5672,12 @@ void theory_seq::propagate_accept(literal lit, expr* acc) { eautomaton::moves mvs; aut->get_moves_from(src, mvs); TRACE("seq", tout << mk_pp(acc, m) << " #moves " << mvs.size() << "\n";); - ptr_vector exprs; + expr_ref_vector exprs(m); for (auto const& mv : mvs) { expr_ref nth = mk_nth(e, idx); expr_ref t = mv.t()->accept(nth); get_context().get_rewriter()(t); - expr* step_e = mk_step(e, idx, re, src, mv.dst(), t); + expr_ref step_e(mk_step(e, idx, re, src, mv.dst(), t), m); literal step = mk_literal(step_e); lits.push_back(step); exprs.push_back(step_e); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 5520d4a84..166c8774e 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -547,7 +547,7 @@ namespace smt { // terms whose meaning are encoded using axioms. void enque_axiom(expr* e); void deque_axiom(expr* e); - void push_lit_as_expr(literal l, ptr_vector& buf); + void push_lit_as_expr(literal l, expr_ref_vector& buf); void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal); void add_indexof_axiom(expr* e); void add_replace_axiom(expr* e); From ea9e2f6642454933dd4663054cbdd5fabbfb8457 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Feb 2019 15:13:47 -0800 Subject: [PATCH 14/16] fix #2158 Signed-off-by: Nikolaj Bjorner --- src/qe/qe_lite.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 4585c88c1..1f8f78aaa 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -694,7 +694,8 @@ namespace eq { if (m.proofs_enabled() && r != q) { pr = m.mk_transitivity(pr, curr_pr); } - } while (q != r && is_quantifier(r)); + } + while (q != r && is_quantifier(r)); m_new_exprs.reset(); } @@ -2441,7 +2442,7 @@ class qe_lite_tactic : public tactic { continue; new_f = f; m_qe(new_f, new_pr); - if (produce_proofs) { + if (new_pr) { expr* fact = m.get_fact(new_pr); if (to_app(fact)->get_arg(0) != to_app(fact)->get_arg(1)) { new_pr = m.mk_modus_ponens(g->pr(i), new_pr); From a2dcf87e10ad4119bfb1aa740cb4701a163c7372 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Feb 2019 14:43:39 -0800 Subject: [PATCH 15/16] add ESRP signing of nuget packages Signed-off-by: Nikolaj Bjorner --- scripts/authorization.json | 15 ++++++++++ scripts/mk_nuget_release.py | 57 +++++++++++++++++++++++++++++++++++-- scripts/policy.json | 8 ++++++ 3 files changed, 78 insertions(+), 2 deletions(-) create mode 100644 scripts/authorization.json create mode 100644 scripts/policy.json diff --git a/scripts/authorization.json b/scripts/authorization.json new file mode 100644 index 000000000..97fb21dfa --- /dev/null +++ b/scripts/authorization.json @@ -0,0 +1,15 @@ +{ + "Version": "1.0.0", + "AuthenticationType": "AAD_CERT", + "ClientId": "1c614a83-2dbe-4d3c-853b-effaefd4fb20", + "AuthCert": { + "SubjectName": "1c614a83-2dbe-4d3c-853b-effaefd4fb20.microsoft.com", + "StoreLocation": "LocalMachine", + "StoreName": "My" + }, + "RequestSigningCert": { + "SubjectName": "1c614a83-2dbe-4d3c-853b-effaefd4fb20", + "StoreLocation": "LocalMachine", + "StoreName": "My" + } +} diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py index db7a1af64..ebd0e0ba7 100644 --- a/scripts/mk_nuget_release.py +++ b/scripts/mk_nuget_release.py @@ -7,6 +7,7 @@ # 3. copy over Microsoft.Z3.dll from suitable distribution # 4. copy nuspec file from packages # 5. call nuget pack +# 6. sign package import json import os @@ -22,6 +23,7 @@ import mk_project data = json.loads(urllib.request.urlopen("https://api.github.com/repos/Z3Prover/z3/releases/latest").read().decode()) version_str = data['tag_name'] +version_num = version_str[3:] print(version_str) @@ -50,7 +52,8 @@ def classify_package(f): ext, dst = os_info[os_name] return os_name, f[:-4], ext, dst return None - + + def unpack(): shutil.rmtree("out", ignore_errors=True) # unzip files in packages @@ -103,17 +106,67 @@ Linux Dependencies: """ with open("out/Microsoft.Z3.nuspec", 'w') as f: - f.write(contents % version_str[3:]) + f.write(contents % version_num) def create_nuget_package(): subprocess.call(["nuget", "pack"], cwd="out") +nuget_sign_input = """ +{ + "Version": "1.0.0", + "SignBatches" + : + [ + { + "SourceLocationType": "UNC", + "SourceRootDirectory": "%s", + "DestinationLocationType": "UNC", + "DestinationRootDirectory": "%s", + "SignRequestFiles": [ + { + "CustomerCorrelationId": "42fc9577-af9e-4ac9-995d-1788d8721d17", + "SourceLocation": "Microsoft.Z3.%s.nupkg", + "DestinationLocation": "Microsoft.Z3.%s.nupkg" + } + ], + "SigningInfo": { + "Operations": [ + { + "KeyCode" : "CP-401405", + "OperationCode" : "NuGetSign", + "Parameters" : {}, + "ToolName" : "sign", + "ToolVersion" : "1.0" + }, + { + "KeyCode" : "CP-401405", + "OperationCode" : "NuGetVerify", + "Parameters" : {}, + "ToolName" : "sign", + "ToolVersion" : "1.0" + } + ] + } + } + ] +}""" + +def sign_nuget_package(): + package_name = "Microsoft.Z3.%s.nupkg" % version_num + input_file = "out/nuget_sign_input.json" + output_path = os.path.abspath("out").replace("\\","\\\\") + with open(input_file, 'w') as f: + f.write(nuget_sign_input % (output_path, output_path, version_num, version_num)) + subprocess.call(["EsrpClient.exe", "sign", "-a", "authorization.json", "-p", "policy.json", "-i", input_file, "-o", "out\\diagnostics.json"]) + + def main(): mk_dir("packages") download_installs() unpack() create_nuget_spec() create_nuget_package() + sign_nuget_package() main() diff --git a/scripts/policy.json b/scripts/policy.json new file mode 100644 index 000000000..badebe683 --- /dev/null +++ b/scripts/policy.json @@ -0,0 +1,8 @@ +{ + "Version": "1.0.0", + "Intent": "ProductRelease", + "ContentType": "Binaries", + "ContentOrigin": "1stParty", + "ProductState": "Next", + "Audience": "ExternalBroad" +} From 6a0c409b0f0deab89cfc242b5b42629638d78c66 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 28 Feb 2019 10:53:27 +0000 Subject: [PATCH 16/16] move a few strings instead of copying --- src/ast/array_decl_plugin.cpp | 16 ++++++++-------- src/ast/ast.cpp | 4 ++-- src/ast/ast.h | 2 +- src/ast/ast_smt_pp.cpp | 2 +- src/ast/bv_decl_plugin.cpp | 2 +- src/ast/datatype_decl_plugin.cpp | 2 +- src/ast/dl_decl_plugin.cpp | 4 ++-- src/ast/rewriter/enum2bv_rewriter.cpp | 2 +- src/ast/rewriter/rewriter_types.h | 2 +- src/ast/seq_decl_plugin.cpp | 10 +++++----- src/cmd_context/cmd_context.cpp | 4 ++-- src/parsers/smt2/smt2parser.cpp | 6 +++--- src/smt/smt_quantifier.cpp | 2 +- src/util/gparams.cpp | 2 +- 14 files changed, 30 insertions(+), 30 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 44c423c09..211c67953 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -141,7 +141,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* std::ostringstream buffer; buffer << "map expects to take as many arguments as the function being mapped, " << "it was given " << arity << " but expects " << f->get_arity(); - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return nullptr; } if (arity == 0) { @@ -158,14 +158,14 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* if (!is_array_sort(domain[i])) { std::ostringstream buffer; buffer << "map expects an array sort as argument at position " << i; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return nullptr; } if (get_array_arity(domain[i]) != dom_arity) { std::ostringstream buffer; buffer << "map expects all arguments to have the same array domain, " << "this is not the case for argument " << i; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return nullptr; } for (unsigned j = 0; j < dom_arity; ++j) { @@ -173,7 +173,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* std::ostringstream buffer; buffer << "map expects all arguments to have the same array domain, " << "this is not the case for argument " << i; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return nullptr; } } @@ -181,7 +181,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* std::ostringstream buffer; buffer << "map expects the argument at position " << i << " to have the array range the same as the function"; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return nullptr; } } @@ -244,7 +244,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) { if (num_parameters != arity) { std::stringstream strm; strm << "select requires " << num_parameters << " arguments, but was provided with " << arity << " arguments"; - m_manager->raise_exception(strm.str().c_str()); + m_manager->raise_exception(strm.str()); return nullptr; } ptr_buffer new_domain; // we need this because of coercions. @@ -256,7 +256,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) { std::stringstream strm; strm << "domain sort " << sort_ref(domain[i+1], *m_manager) << " and parameter "; strm << parameter_pp(parameters[i], *m_manager) << " do not match"; - m_manager->raise_exception(strm.str().c_str()); + m_manager->raise_exception(strm.str()); UNREACHABLE(); return nullptr; } @@ -284,7 +284,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) { std::ostringstream buffer; buffer << "store expects the first argument to be an array taking " << num_parameters+1 << ", instead it was passed " << (arity - 1) << "arguments"; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); UNREACHABLE(); return nullptr; } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index b84dac136..c73e2f1d8 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1584,8 +1584,8 @@ void ast_manager::raise_exception(char const * msg) { throw ast_exception(msg); } -void ast_manager::raise_exception(std::string const& msg) { - throw ast_exception(msg.c_str()); +void ast_manager::raise_exception(std::string && msg) { + throw ast_exception(std::move(msg)); } diff --git a/src/ast/ast.h b/src/ast/ast.h index 9c6c811b0..1c25ff9ec 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1574,7 +1574,7 @@ public: // Equivalent to throw ast_exception(msg) Z3_NORETURN void raise_exception(char const * msg); - Z3_NORETURN void raise_exception(std::string const& s); + Z3_NORETURN void raise_exception(std::string && s); std::ostream& display(std::ostream& out, parameter const& p); diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index ea220f7e7..48daf6988 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -951,7 +951,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { strm << "(set-logic " << m_logic << ")\n"; } if (!m_attributes.empty()) { - strm << "; " << m_attributes.c_str(); + strm << "; " << m_attributes; } #if 0 diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 738444b3b..4ffd7d6cb 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -624,7 +624,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p if (m.get_sort(args[i]) != r->get_domain(i)) { std::ostringstream buffer; buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m); - m.raise_exception(buffer.str().c_str()); + m.raise_exception(buffer.str()); return nullptr; } } diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 8bf0abbb3..146c7359f 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -342,7 +342,7 @@ namespace datatype { std::ostringstream buffer; buffer << "second argument to field update should be " << mk_ismt2_pp(rng, m) << " instead of " << mk_ismt2_pp(domain[1], m); - m.raise_exception(buffer.str().c_str()); + m.raise_exception(buffer.str()); return nullptr; } range = domain[0]; diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 01b06518e..43cf50662 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -54,7 +54,7 @@ namespace datalog { } std::ostringstream buffer; buffer << msg << ", value is not within bound " << low << " <= " << val << " <= " << up; - m_manager->raise_exception(buffer.str().c_str()); + m_manager->raise_exception(buffer.str()); return false; } @@ -676,7 +676,7 @@ namespace datalog { } std::stringstream strm; strm << "sort '" << mk_pp(s, m) << "' is not recognized as a sort that contains numeric values.\nUse Bool, BitVec, Int, Real, or a Finite domain sort"; - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); return nullptr; } diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp index 65250282c..f6f2d6f85 100644 --- a/src/ast/rewriter/enum2bv_rewriter.cpp +++ b/src/ast/rewriter/enum2bv_rewriter.cpp @@ -86,7 +86,7 @@ struct enum2bv_rewriter::imp { void throw_non_fd(expr* e) { std::stringstream strm; strm << "unable to handle nested data-type expression " << mk_pp(e, m); - throw rewriter_exception(strm.str().c_str()); + throw rewriter_exception(strm.str()); } void check_for_fd(unsigned n, expr* const* args) { diff --git a/src/ast/rewriter/rewriter_types.h b/src/ast/rewriter/rewriter_types.h index 094357fed..77ab42b2a 100644 --- a/src/ast/rewriter/rewriter_types.h +++ b/src/ast/rewriter/rewriter_types.h @@ -46,7 +46,7 @@ inline br_status unsigned2br_status(unsigned u) { class rewriter_exception : public default_exception { public: - rewriter_exception(char const * msg):default_exception(msg) {} + rewriter_exception(std::string && msg) : default_exception(std::move(msg)) {} }; #endif diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 20e1fb36c..7576e43c0 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -400,7 +400,7 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do std::ostringstream strm; strm << "Unexpected number of arguments to '" << sig.m_name << "' "; strm << "at least one argument expected " << dsz << " given"; - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); } bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { @@ -420,7 +420,7 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do if (range) { strm << " and range: " << mk_pp(range, m); } - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); } range_out = apply_binding(binding, sig.m_range); SASSERT(range_out); @@ -434,7 +434,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran std::ostringstream strm; strm << "Unexpected number of arguments to '" << sig.m_name << "' "; strm << sig.m_dom.size() << " arguments expected " << dsz << " given"; - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); } bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { @@ -459,13 +459,13 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran strm << mk_pp(sig.m_dom[i].get(), m) << " "; } - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); } if (!range && dsz == 0) { std::ostringstream strm; strm << "Sort of polymorphic function '" << sig.m_name << "' "; strm << "is ambiguous. Function takes no arguments and sort of range has not been constrained"; - m.raise_exception(strm.str().c_str()); + m.raise_exception(strm.str()); } range_out = apply_binding(m_binding, sig.m_range); SASSERT(range_out); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index c58453460..9de183ca8 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -797,7 +797,7 @@ void cmd_context::insert(symbol const & s, func_decl * f) { msg += " '"; msg += s.str(); msg += "' (with the given signature) already declared"; - throw cmd_exception(msg.c_str()); + throw cmd_exception(std::move(msg)); } if (s != f->get_name()) { TRACE("func_decl_alias", tout << "adding alias for: " << f->get_name() << ", alias: " << s << "\n";); @@ -1142,7 +1142,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg for (unsigned i = 0; i < fs.get_num_entries(); ++i) { buffer << "\ndeclared: " << mk_pp(fs.get_entry(i), m()) << " "; } - throw cmd_exception(buffer.str().c_str()); + throw cmd_exception(buffer.str()); } if (well_sorted_check_enabled()) m().check_sort(f, num_args, args); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index bf1e25e57..c103b0276 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -482,7 +482,7 @@ namespace smt2 { if (context[0]) msg += ": "; msg += "unknown sort '"; msg += id.str() + "'"; - throw parser_exception(msg.c_str()); + throw parser_exception(std::move(msg)); } void consume_sexpr() { @@ -1633,7 +1633,7 @@ namespace smt2 { void unknown_var_const_name(symbol id) { std::string msg = "unknown constant/variable '"; msg += id.str() + "'"; - throw parser_exception(msg.c_str()); + throw parser_exception(std::move(msg)); } rational m_last_bv_numeral; // for bv, bvbin, bvhex @@ -2431,7 +2431,7 @@ namespace smt2 { buffer << "invalid function definition, sort mismatch. Expcected " << mk_pp(f->get_range(), m()) << " but function body has sort " << mk_pp(m().get_sort(body), m()); - throw parser_exception(buffer.str().c_str()); + throw parser_exception(buffer.str()); } m_ctx.insert_rec_fun(f, bindings, ids, body); } diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 008da06ec..d0ca05ff9 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -173,7 +173,7 @@ namespace smt { if (num_instances > 0) { out << "[quantifier_instances] "; out.width(10); - out << q->get_qid().str().c_str() << " : "; + out << q->get_qid().str() << " : "; out.width(6); out << num_instances << " : "; out.width(3); diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 9ab3123a2..6b5919f8e 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -172,7 +172,7 @@ public: } for (unsigned i = 0; i < n; i++) { if (tmp[i] == '.') { - param_name = tmp.substr(i+1).c_str(); + param_name = tmp.c_str() + i + 1; tmp.resize(i); mod_name = tmp.c_str(); return;