External constraints need to remember their sign

src/math/polysat/constraint.cpp

@@ -64,15 +64,15 @@ namespace polysat {
         return cl;
     }
 
-    void constraint_manager::register_external(constraint* c) {
+    void constraint_manager::register_external(signed_constraint c) {
         SASSERT(c);
         SASSERT(!c->is_external());
         if (c->unit_dep() && c->unit_dep()->is_leaf()) {
             unsigned const dep = c->unit_dep()->leaf_value();
             SASSERT(!m_external_constraints.contains(dep));
-            m_external_constraints.insert(dep, c);
+            m_external_constraints.insert(dep, c.get());
         }
-        c->set_external();
+        c->set_external(c.is_negative());
         ++m_num_external;
     }
 
@@ -83,6 +83,14 @@ namespace polysat {
         --m_num_external;
     }
 
+    signed_constraint constraint_manager::lookup_external(unsigned dep) const {
+        constraint* c = m_external_constraints.get(dep, nullptr);
+        if (c)
+            return {c, !c->external_sign()};
+        else
+            return {};
+    }
+
     // Release constraints at the given level and above.
     void constraint_manager::release_level(unsigned lvl) {
         for (unsigned l = m_clauses.size(); l-- > lvl; ) {

src/math/polysat/constraint.h

@@ -75,8 +75,9 @@ namespace polysat {
         clause* store(clause_ref cl);
 
         /// Register a unit clause with an external dependency.
-        void register_external(constraint* c);
+        void register_external(signed_constraint c);
         void unregister_external(constraint* c);
+        signed_constraint lookup_external(unsigned dep) const;
 
         /// Release clauses at the given level and above.
         void release_level(unsigned lvl);
@@ -87,7 +88,6 @@ namespace polysat {
 
         constraint* lookup(sat::bool_var var) const;
         signed_constraint lookup(sat::literal lit) const;
-        constraint* lookup_external(unsigned dep) const { return m_external_constraints.get(dep, nullptr); }
 
         signed_constraint eq(pdd const& p);
         signed_constraint ule(pdd const& a, pdd const& b);
@@ -136,7 +136,7 @@ namespace polysat {
         clause*             m_unit_clause = nullptr;  ///< If this constraint was asserted by a unit clause, we store that clause here.
         ckind_t             m_kind;
         unsigned_vector     m_vars;
-        bool                m_is_external = false;
+        lbool               m_external_sign = l_undef;
         bool                m_is_marked = false;
         bool                m_is_bool_propagated = false;
         /** The boolean variable associated to this constraint, if any.
@@ -169,7 +169,6 @@ namespace polysat {
         virtual bool is_currently_true(solver& s, bool is_positive) const = 0;
         virtual void narrow(solver& s, bool is_positive) = 0;
         virtual inequality as_inequality(bool is_positive) const = 0;
-        
 
         ule_constraint& to_ule();
         ule_constraint const& to_ule() const;
@@ -184,9 +183,10 @@ namespace polysat {
         void set_unit_clause(clause* cl);
         p_dependency* unit_dep() const { return m_unit_clause ? m_unit_clause->dep() : nullptr; }
 
-        void set_external() { m_is_external = true; }
+        void set_external(bool sign) { m_external_sign = to_lbool(sign); }
-        void unset_external() { m_is_external = false; }
+        void unset_external() { m_external_sign = l_undef; }
-        bool is_external() const { return m_is_external; }
+        bool is_external() const { return m_external_sign != l_undef; }
+        bool external_sign() const { SASSERT(is_external()); return m_external_sign == l_true; }
 
         void set_mark() { m_is_marked = true; }
         void unset_mark() { m_is_marked = false; }

src/math/polysat/solver.cpp

@@ -148,7 +148,7 @@ namespace polysat {
         c->set_unit_clause(unit);
         if (dep != null_dependency)
             if (!c->is_external()) {
-                m_constraints.register_external(c.get());
+                m_constraints.register_external(c);
                 m_trail.push_back(trail_instr_t::ext_constraint_i);
                 m_ext_constraint_trail.push_back(c.get());
             }
@@ -157,31 +157,31 @@ namespace polysat {
 #if ENABLE_LINEAR_SOLVER
         m_linear_solver.new_constraint(*c.get());
 #endif
-        if (activate) {
+        if (activate)
-            if (c.bvalue(*this) == l_false)
+            assert_ext_constraint(c);
-                m_conflict.set(c);  // we already added ~c => conflict at base level
-            else
-                propagate_bool(c.blit(), unit);
-        }
     }
 
     void solver::assign_eh(unsigned dep, bool is_true) {
         VERIFY(at_base_level());
-        NOT_IMPLEMENTED_YET();
+        if (is_conflict())
-        /*
+            return;  // no need to do anything if we already have a conflict at base level
-        constraint* c = m_constraints.lookup_external(dep);
+        signed_constraint c = m_constraints.lookup_external(dep);
         if (!c) {
             LOG("WARN: there is no constraint for dependency " << dep);
             return;
         }
-        if (is_conflict())
+        assert_ext_constraint(is_true ? c : ~c);
-            return;
-        // TODO: this is wrong. (e.g., if the external constraint was negative) we need to store signed_constraints
-        signed_constraint cl{c, is_true};
-        activate_constraint_base(cl);
-        */
     }
 
+    void solver::assert_ext_constraint(signed_constraint c) {
+        SASSERT(at_base_level());
+        SASSERT(!is_conflict());
+        SASSERT(c->unit_clause());
+        if (c.bvalue(*this) == l_false)
+            m_conflict.set(c);  // we already added ~c => conflict at base level
+        else
+            propagate_bool(c.blit(), c->unit_clause());
+    }
 
     bool solver::can_propagate() {
         return m_qhead < m_search.size() && !is_conflict();

src/math/polysat/solver.h

@@ -216,6 +216,7 @@ namespace polysat {
         signed_constraint slt(pdd const& p, pdd const& q);
         void ext_constraint(signed_constraint c, unsigned dep, bool activate);
         static void insert_constraint(signed_constraints& cs, signed_constraint c);
+        void assert_ext_constraint(signed_constraint c);
 
         bool inc() { return m_lim.inc(); }