misc

src/math/polysat/clause_builder.cpp

@@ -62,6 +62,8 @@ namespace polysat {
         insert(m_solver->lit2cnstr(lit));
     }
 
+    // TODO: in the final version, we may also skip assumptions (and even literals propagated at the base level),
+    //       provided we correctly track external dependencies/level for the clause.
     void clause_builder::insert(signed_constraint c) {
         SASSERT(c);
         if (c.is_always_false())  // filter out trivial constraints such as "4 < 2"

src/math/polysat/log.cpp

@@ -24,6 +24,11 @@ Other:
 - code diverges on coding conventions.
 */
 
+/*
+  TODO: add "conditional" 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"; }
@@ -33,8 +38,12 @@ char const* color_reset()  { return "\x1B[0m"; }
 
 std::atomic<bool> g_log_enabled(true);
 
+bool get_log_enabled() {
+    return g_log_enabled;
+}
+
 void set_log_enabled(bool log_enabled) {
-  g_log_enabled = log_enabled;
+    g_log_enabled = log_enabled;
 }
 
 static LogLevel get_max_log_level(std::string const& fn, std::string const& pretty_fn) {

src/math/polysat/log.h

@@ -27,6 +27,19 @@ 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
 {
@@ -94,6 +107,8 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
 #else  // POLYSAT_LOGGING_ENABLED
 
 inline void set_log_enabled(bool) {}
+inline bool get_log_enabled() { return false; }
+class scoped_set_log_enabled {};
 
 #define LOG_(lvl, x)  \
   do {               \

src/math/polysat/solver.cpp

@@ -770,7 +770,7 @@ namespace polysat {
                     }
                     continue;
                 }
-                SASSERT(!m_bvars.is_assumption(var));
+                SASSERT(!m_bvars.is_assumption(var));   // TODO: "assumption" is basically "propagated by unit clause" (or "at base level"); except we do not explicitly store the unit clause.
                 if (m_bvars.is_decision(var)) {
                     revert_bool_decision(lit);
                     return;
@@ -896,9 +896,10 @@ namespace polysat {
             if (is_conflict()) {
                 // until this is fixed (if possible; and there may be other causes of conflict at this point),
                 // we just forget about the remaining lemmas and restart conflict analysis.
+                // TODO: we could also insert the remaining lemmas into the conflict and keep them for later.
                 return;
             }
-            SASSERT(!is_conflict());  // TODO: is this true in general? No lemma by itself should lead to a conflict here. But can there be conflicting asserting lemmas?
+            SASSERT(!is_conflict());
         }
 
         LOG("best_score: " << best_score);
@@ -1041,6 +1042,8 @@ namespace polysat {
         SASSERT(!clause.empty());
         m_constraints.store(&clause, true);
 
+        // TODO: we shouldn't add pwatch here immediately, because this may be called during propagate(v); which means the watchlist for v is locked.
+        //       rather, put the clause into a pwatch queue, and add_pwatch in the next solver iteration?
         if (!clause.is_redundant()) {
             // for (at least) non-redundant clauses, we also need to watch the constraints
             // so we can discover when the clause should propagate

src/math/polysat/types.h

@@ -50,7 +50,10 @@ namespace polysat {
     inline const dependency null_dependency = dependency(UINT_MAX);
     typedef svector<dependency> dependency_vector;
 
-    inline bool operator<(dependency const& d1, dependency const& d2) { return d1.val() < d2.val();  }
+    inline bool operator< (dependency const& d1, dependency const& d2) { return d1.val() <  d2.val(); }
+    inline bool operator<=(dependency const& d1, dependency const& d2) { return d1.val() <= d2.val(); }
+    inline bool operator> (dependency const& d1, dependency const& d2) { return d1.val() >  d2.val(); }
+    inline bool operator>=(dependency const& d1, dependency const& d2) { return d1.val() >= d2.val(); }
     inline bool operator==(dependency const& d1, dependency const& d2) { return d1.val() == d2.val(); }
     inline bool operator!=(dependency const& d1, dependency const& d2) { return d1.val() != d2.val(); }