diff --git a/src/sat/smt/polysat_constraints.cpp b/src/sat/smt/polysat_constraints.cpp index a03b4f5f5..b588019dc 100644 --- a/src/sat/smt/polysat_constraints.cpp +++ b/src/sat/smt/polysat_constraints.cpp @@ -16,6 +16,7 @@ Author: #include "sat/smt/polysat_solver.h" #include "sat/smt/polysat_constraints.h" #include "sat/smt/polysat_ule.h" +#include "sat/smt/polysat_umul_ovfl.h" namespace polysat { @@ -29,6 +30,12 @@ namespace polysat { return is_positive ? sc : ~sc; } + signed_constraint constraints::umul_ovfl(pdd const& p, pdd const& q) { + auto* c = alloc(umul_ovfl_constraint, p, q); + m_trail.push(new_obj_trail(c)); + return signed_constraint(ckind_t::umul_ovfl_t, c); + } + lbool signed_constraint::eval(assignment& a) const { lbool r = m_constraint->eval(a); return m_sign ? ~r : r; diff --git a/src/sat/smt/polysat_constraints.h b/src/sat/smt/polysat_constraints.h index 121fc2da6..b62fbba21 100644 --- a/src/sat/smt/polysat_constraints.h +++ b/src/sat/smt/polysat_constraints.h @@ -85,7 +85,7 @@ namespace polysat { signed_constraint sle(pdd const& p, pdd const& q) { throw default_exception("nyi"); } signed_constraint ult(pdd const& p, pdd const& q) { throw default_exception("nyi"); } signed_constraint slt(pdd const& p, pdd const& q) { throw default_exception("nyi"); } - signed_constraint umul_ovfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); } + signed_constraint umul_ovfl(pdd const& p, pdd const& q); signed_constraint smul_ovfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); } signed_constraint smul_udfl(pdd const& p, pdd const& q) { throw default_exception("nyi"); } signed_constraint bit(pdd const& p, unsigned i) { throw default_exception("nyi"); } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index c2a7e8296..eead1069e 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -26,6 +26,7 @@ z3_add_component(util inf_rational.cpp inf_s_integer.cpp lbool.cpp + log.cpp luby.cpp memory_manager.cpp min_cut.cpp diff --git a/src/util/log.cpp b/src/util/log.cpp new file mode 100644 index 000000000..f3101bfc4 --- /dev/null +++ b/src/util/log.cpp @@ -0,0 +1,125 @@ +#ifndef _MSC_VER +#include // for isatty +#else +#include +#include +#undef min +#endif +#include +#include + +#include "util/util.h" +#include "util/log.h" + +/** +For windows: +https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/isatty?view=msvc-160 + +So include and create platform wrapper for _isatty / isatty. + +Other: +- add option to configure z3 trace feature to point to std::err +- roll this functionality into trace.cpp/trace.h in util +- Generally, generic functionality should not reside in specific directories. +- code diverges on coding conventions. +*/ + +/* + TODO: add deferred logs, i.e., the messages are held back and only printed when a non-conditional message is logged. + Purpose: reduce noise, e.g., when printing prerequisites for transformations that do not always apply. +*/ + +char const* color_red() { return "\x1B[31m"; } +char const* color_yellow() { return "\x1B[33m"; } +char const* color_blue() { return "\x1B[34m"; } +char const* color_reset() { return "\x1B[0m"; } + +#if POLYSAT_LOGGING_ENABLED + +std::atomic g_log_enabled(true); + +void set_log_enabled(bool log_enabled) { + g_log_enabled = log_enabled; +} + +bool get_log_enabled() { + return g_log_enabled; +} + +static LogLevel get_max_log_level(std::string const& fn, std::string const& pretty_fn) { + (void)fn; + (void)pretty_fn; + + // if (fn == "pop_levels") + // return LogLevel::Default; + + // also covers 'reset_marks' and 'set_marks' + if (fn.find("set_mark") != std::string::npos) + return LogLevel::Default; + + // return LogLevel::Verbose; + return LogLevel::Default; +} + +/// Filter log messages +bool polysat_should_log(unsigned verbose_lvl, LogLevel msg_level, std::string fn, std::string pretty_fn) { + if (!g_log_enabled) + return false; + if (get_verbosity_level() < verbose_lvl) + return false; + LogLevel max_log_level = get_max_log_level(fn, pretty_fn); + return msg_level <= max_log_level; +} + +static char const* level_color(LogLevel msg_level) { + switch (msg_level) { + case LogLevel::Heading1: return color_red(); + case LogLevel::Heading2: return color_yellow(); + case LogLevel::Heading3: return color_blue(); + default: return nullptr; + } +} + +int polysat_log_indent_level = 0; + +std::pair polysat_log(LogLevel msg_level, std::string fn, std::string /* pretty_fn */) { + std::ostream& os = std::cerr; + + size_t width = 20; + size_t padding = 0; + if (width >= fn.size()) + padding = width - fn.size(); + else + fn = fn.substr(0, width - 3) + "..."; + char const* color = nullptr; + color = level_color(msg_level); +#ifdef _MSC_VER + HANDLE hOut = GetStdHandle(STD_ERROR_HANDLE); + bool ok = hOut != INVALID_HANDLE_VALUE; + DWORD dwMode = 0; + ok = ok && GetConsoleMode(hOut, &dwMode); + dwMode |= ENABLE_VIRTUAL_TERMINAL_PROCESSING; + ok = ok && SetConsoleMode(hOut, dwMode); +#else + int const fd = fileno(stderr); + if (color && !isatty(fd)) { color = nullptr; } +#endif + + if (color) + os << color; + os << "[" << fn << "] " << std::string(padding, ' '); + os << std::string(polysat_log_indent_level, ' '); + return {os, (bool)color}; + +} + +polysat_log_indent::polysat_log_indent(int amount): m_amount{amount} { + polysat_log_indent_level += m_amount; +} + +polysat_log_indent::~polysat_log_indent() { + polysat_log_indent_level -= m_amount; +} + + +#endif // POLYSAT_LOGGING_ENABLED diff --git a/src/util/log.h b/src/util/log.h new file mode 100644 index 000000000..fe89f91cf --- /dev/null +++ b/src/util/log.h @@ -0,0 +1,148 @@ +#ifndef POLYSAT_LOG_HPP +#define POLYSAT_LOG_HPP + + +#include +#include +#include +#include "util/log_helper.h" + + +// By default, enable logging only in debug mode +#ifndef POLYSAT_LOGGING_ENABLED +# ifndef NDEBUG +# define POLYSAT_LOGGING_ENABLED 1 +# else +# define POLYSAT_LOGGING_ENABLED 0 +# endif +#endif + + +char const* color_blue(); +char const* color_yellow(); +char const* color_red(); +char const* color_reset(); + + +#if POLYSAT_LOGGING_ENABLED + +void set_log_enabled(bool log_enabled); +bool get_log_enabled(); + +class scoped_set_log_enabled { + bool m_prev; +public: + scoped_set_log_enabled(bool enabled) { + m_prev = get_log_enabled(); + set_log_enabled(enabled); + } + ~scoped_set_log_enabled() { + set_log_enabled(m_prev); + } +}; + +class polysat_log_indent +{ + int m_amount; +public: + polysat_log_indent(int amount); + ~polysat_log_indent(); +}; + +/// Lower log level means more important +enum class LogLevel : int { + None = 0, + Heading1 = 1, + Heading2 = 2, + Heading3 = 3, + Default = 4, +}; + +/// Filter log messages +bool +polysat_should_log(unsigned verbose_lvl, LogLevel msg_level, std::string fn, std::string pretty_fn); + +std::pair +polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn); + +#ifdef _MSC_VER +#define __PRETTY_FUNCTION__ __FUNCSIG__ +#endif + +#define LOG_(verbose_lvl, log_lvl, x) \ + do { \ + if (polysat_should_log(verbose_lvl, log_lvl, __func__, __PRETTY_FUNCTION__)) { \ + auto pair = polysat_log(log_lvl, __func__, __PRETTY_FUNCTION__); \ + std::ostream& os = pair.first; \ + bool should_reset = pair.second; \ + os << x; \ + if (should_reset) \ + os << color_reset(); \ + os << std::endl; \ + } \ + } while (false) + +#define LOG_CONCAT_HELPER(a,b) a ## b +#define LOG_CONCAT(a,b) LOG_CONCAT_HELPER(a,b) + +#define LOG_INDENT(verbose_lvl, log_lvl, x) \ + LOG_(verbose_lvl, log_lvl, x); \ + polysat_log_indent LOG_CONCAT(polysat_log_indent_obj_, __LINE__) (4); + +#define LOG_H1(x) LOG_INDENT(0, LogLevel::Heading1, x) +#define LOG_H2(x) LOG_INDENT(0, LogLevel::Heading2, x) +#define LOG_H3(x) LOG_INDENT(0, LogLevel::Heading3, x) +#define LOG(x) LOG_(0, LogLevel::Default , x) + +#define LOG_H1_V(verbose_lvl, x) LOG_INDENT(verbose_lvl, LogLevel::Heading1, x) +#define LOG_H2_V(verbose_lvl, x) LOG_INDENT(verbose_lvl, LogLevel::Heading2, x) +#define LOG_H3_V(verbose_lvl, x) LOG_INDENT(verbose_lvl, LogLevel::Heading3, x) +#define LOG_V(verbose_lvl, x) LOG_(verbose_lvl, LogLevel::Default , x) + +#define COND_LOG(c, x) if (c) LOG(x) +#define LOGE(x) LOG(#x << " = " << (x)) + +#define IF_LOGGING(x) \ + do { \ + if (get_log_enabled()) { \ + x; \ + } \ + } while (false) + + +#else // POLYSAT_LOGGING_ENABLED + +inline void set_log_enabled(bool) {} +inline bool get_log_enabled() { return false; } +class scoped_set_log_enabled { +public: + scoped_set_log_enabled(bool) {} +}; + +#define LOG_(vlvl, lvl, x) \ + do { \ + /* do nothing */ \ + } while (false) + +#define LOG_H1(x) LOG_(0, 0, x) +#define LOG_H2(x) LOG_(0, 0, x) +#define LOG_H3(x) LOG_(0, 0, x) +#define LOG(x) LOG_(0, 0, x) + +#define LOG_H1_V(v, x) LOG_(v, 0, x) +#define LOG_H2_V(v, x) LOG_(v, 0, x) +#define LOG_H3_V(v, x) LOG_(v, 0, x) +#define LOG_V(v, x) LOG_(v, 0, x) + +#define COND_LOG(c, x) LOG_(0, c, x) +#define LOGE(x) LOG_(0, 0, x) + +#define IF_LOGGING(x) \ + do { \ + /* do nothing */ \ + } while (false) + +#endif // POLYSAT_LOGGING_ENABLED + + +#endif // POLYSAT_LOG_HPP diff --git a/src/util/log_helper.h b/src/util/log_helper.h new file mode 100644 index 000000000..7be2693b4 --- /dev/null +++ b/src/util/log_helper.h @@ -0,0 +1,105 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + Logging support + +Abstract: + + Utilities for logging. + +Author: + + Nikolaj Bjorner (nbjorner) 2021-03-19 + Jakob Rath 2021-04-6 + +--*/ +#pragma once + +#include +#include +#include +#include + +template +struct show_deref_t { + T const* ptr; +}; + +template +std::ostream& operator<<(std::ostream& out, show_deref_t s) { + if (s.ptr) + return out << *s.ptr; + else + return out << ""; +} + +template +show_deref_t show_deref(T* ptr) { + return show_deref_t{ptr}; +} + +template ().get())>::type> +show_deref_t show_deref(Ptr const& ptr) { + return show_deref_t{ptr.get()}; +} + + +template +struct repeat { + size_t count; + T const& obj; + repeat(size_t count, T const& obj): count(count), obj(obj) {} +}; + +template +std::ostream& operator<<(std::ostream& out, repeat const& r) { + for (size_t i = r.count; i-- > 0; ) + out << r.obj; + return out; +} + +enum class pad_direction { + left, + right, +}; + +template +struct pad { + pad_direction dir; + unsigned width; + T const& obj; + pad(pad_direction dir, unsigned width, T const& obj): dir(dir), width(width), obj(obj) {} +}; + +template +std::ostream& operator<<(std::ostream& out, pad const& p) { + std::stringstream tmp; + tmp << p.obj; + std::string s = tmp.str(); + size_t n = (s.length() < p.width) ? (p.width - s.length()) : 0; + switch (p.dir) { + case pad_direction::left: + out << repeat(n, ' ') << s; + break; + case pad_direction::right: + out << s << repeat(n, ' '); + break; + } + return out; +} + +/// Fill with spaces to the right: +/// out << rpad(8, "hello") +/// writes "hello ". +template +pad rpad(unsigned width, T const& obj) { + return pad(pad_direction::right, width, obj); +} + +/// Fill with spaces to the left. +template +pad lpad(unsigned width, T const& obj) { + return pad(pad_direction::left, width, obj); +}