add log helper to util

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;

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"); }

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

src/util/log.cpp

@@ -0,0 +1,125 @@
+#ifndef _MSC_VER
+#include <unistd.h>  // for isatty
+#else
+#include <windows.h>
+#include <io.h>
+#undef min
+#endif
+#include <atomic>
+#include <utility>
+
+#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 <io.h> 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<bool> 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<std::ostream&, bool> 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

src/util/log.h

@@ -0,0 +1,148 @@
+#ifndef POLYSAT_LOG_HPP
+#define POLYSAT_LOG_HPP
+
+
+#include <cstdint>
+#include <iostream>
+#include <string>
+#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<std::ostream&, bool>
+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

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 <ostream>
+#include <sstream>
+#include <type_traits>
+#include <utility>
+
+template <typename T>
+struct show_deref_t {
+    T const* ptr;
+};
+
+template <typename T>
+std::ostream& operator<<(std::ostream& out, show_deref_t<T> s) {
+    if (s.ptr)
+        return out << *s.ptr;
+    else
+        return out << "<null>";
+}
+
+template <typename T>
+show_deref_t<T> show_deref(T* ptr) {
+    return show_deref_t<T>{ptr};
+}
+
+template <typename Ptr, typename T = typename std::remove_pointer<decltype(std::declval<Ptr>().get())>::type>
+show_deref_t<T> show_deref(Ptr const& ptr) {
+    return show_deref_t<T>{ptr.get()};
+}
+
+
+template <typename T>
+struct repeat {
+    size_t count;
+    T const& obj;
+    repeat(size_t count, T const& obj): count(count), obj(obj) {}
+};
+
+template <typename T>
+std::ostream& operator<<(std::ostream& out, repeat<T> const& r) {
+    for (size_t i = r.count; i-- > 0; ) 
+        out << r.obj;
+    return out;
+}
+
+enum class pad_direction {
+    left,
+    right,
+};
+
+template <typename T>
+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 <typename T>
+std::ostream& operator<<(std::ostream& out, pad<T> 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 <typename T>
+pad<T> rpad(unsigned width, T const& obj) {
+    return pad<T>(pad_direction::right, width, obj);
+}
+
+/// Fill with spaces to the left.
+template <typename T>
+pad<T> lpad(unsigned width, T const& obj) {
+    return pad<T>(pad_direction::left, width, obj);
+}