add some code review comments, stubs for ule

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/polysat/constraint.h

@@ -5,10 +5,6 @@ Module Name:
 
     polysat constraints
 
-Abstract:
-
-    Polynomial constriants
-
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19

src/math/polysat/eq_constraint.cpp

@@ -105,6 +105,13 @@ namespace polysat {
     }
 
     void eq_constraint::narrow(solver& s) {
+        // NSB code review:
+        // This should also use the current assignment so be similar to propagate.
+        // The idea is that narrow is invoked when the constraint is first added
+        // and also when the constraint is used in a conflict.
+        // When it is used in a conflict, there could be a partial assignment in s.m_search
+        // that fixes variables in p().
+        // 
         (void)try_narrow_with(p(), s);
     }
 

src/math/polysat/eq_constraint.h

@@ -3,15 +3,12 @@ Copyright (c) 2021 Microsoft Corporation
 
 Module Name:
 
-    polysat constraints
-
-Abstract:
-
-    Polynomial equality constriants
+    polysat equality constraints
 
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
 
 --*/
 #pragma once

src/math/polysat/solver.cpp

@@ -495,8 +495,10 @@ namespace polysat {
         backjump(m_justification[v].level()-1);
         for (unsigned i = m_cjust[v].size(); i < just.size(); ++i) 
             push_cjust(v, just[i]);
-        for (constraint* c : m_conflict)
+        for (constraint* c : m_conflict) {
             push_cjust(v, c);
+            c->narrow(*this);
+        }
         m_conflict.reset();
         push_viable(v);
         m_viable[v] = viable;

src/math/polysat/ule_constraint.cpp

@@ -3,7 +3,7 @@ Copyright (c) 2021 Microsoft Corporation
 
 Module Name:
 
-    polysat ule_constraints
+    polysat unsigned <= constraints
 
 Author:
 

src/math/polysat/ule_constraint.h

@@ -3,15 +3,12 @@ Copyright (c) 2021 Microsoft Corporation
 
 Module Name:
 
-    polysat constraints
-
-Abstract:
-
-    Polynomial equality constriants
+    polysat unsigned <= constraint
 
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-6
 
 --*/
 #pragma once