add the false literal callback

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

src/smt/seq/seq_nielsen.cpp

@@ -244,6 +244,15 @@ namespace seq {
         return false;
     }
 
+    void nielsen_node::add_constraint(constraint const &c) {
+        m_constraints.push_back(c);
+        if (m_graph.m_literal_if_false) {
+            auto lit = m_graph.m_literal_if_false(c.fml);
+            if (lit != sat::null_literal)
+                m_conflict_literal = lit;
+        }
+    }
+
     void nielsen_node::apply_subst(euf::sgraph& sg, nielsen_subst const& s) {
         SASSERT(s.m_var);
         for (auto &eq : m_str_eq) {
@@ -304,6 +313,7 @@ namespace seq {
         return m_graph.m_solver.lower_bound(e, lo);
     }
 
+
     bool nielsen_node::upper_bound(expr* e, rational& up) const {
         SASSERT(e);
         return m_graph.m_solver.upper_bound(e, up);
@@ -365,8 +375,8 @@ namespace seq {
     // nielsen_graph
     // -----------------------------------------------
 
-    nielsen_graph::nielsen_graph(euf::sgraph& sg, simple_solver& solver):
-        m(sg.get_manager()),
+    nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver):        
+        m(sg.get_manager()),        
         m_seq(sg.get_seq_util()),
         m_sg(sg),
         m_solver(solver),
@@ -504,7 +514,7 @@ namespace seq {
                 if (e) seq.str.is_power(e, pow_base, pow_exp);
                 if (pow_exp) {
                     expr* zero = arith.mk_numeral(rational(0), true);
-                    m_constraints.push_back(
+                    add_constraint(
                         constraint(m.mk_eq(pow_exp, zero), dep, m));
                 }
                 nielsen_subst s(t, sg.mk_empty_seq(t->get_sort()), dep);
@@ -3452,6 +3462,10 @@ namespace seq {
                 continue;
             if (!n->is_currently_conflict())
                 continue;
+            if (n->m_conflict_literal != sat::null_literal) {
+                deps = m_dep_mgr.mk_join(deps, m_dep_mgr.mk_leaf(n->m_conflict_literal));
+                continue;
+            }
             for (str_eq const& eq : n->str_eqs())
                 deps = m_dep_mgr.mk_join(deps, eq.m_dep);
             for (str_mem const& mem : n->str_mems())

src/smt/seq/seq_nielsen.h

@@ -473,7 +473,6 @@ namespace seq {
 
         std::ostream& display(std::ostream& out) const;
     };
-
     // edge in the Nielsen graph connecting two nodes
     // mirrors ZIPT's NielsenEdge
     class nielsen_edge {
@@ -525,6 +524,7 @@ namespace seq {
         vector<str_eq>     m_str_eq;        // string equalities
         vector<str_mem>    m_str_mem;       // regex memberships
         vector<constraint> m_constraints;   // integer equalities/inequalities (mirrors ZIPT's IntEq/IntLe)
+        sat::literal m_conflict_literal = sat::null_literal;
 
 
         // character constraints (mirrors ZIPT's DisEqualities and CharRanges)
@@ -577,10 +577,10 @@ namespace seq {
 
         void add_str_eq(str_eq const& eq) { m_str_eq.push_back(eq); }
         void add_str_mem(str_mem const& mem) { m_str_mem.push_back(mem); }
-        void add_constraint(constraint const& ic) { m_constraints.push_back(ic); }
+        void add_constraint(constraint const &ic);
 
         vector<constraint> const& constraints() const { return m_constraints; }
-        vector<constraint>& constraints() { return m_constraints; }
+        vector<constraint>& constraints() { return m_constraints; }        
 
         // Query current bounds for a variable from the arithmetic subsolver.
         // Falls der Subsolver keinen Bound liefert, werden konservative Defaults
@@ -622,6 +622,7 @@ namespace seq {
 
         bool is_currently_conflict() const {
             return m_is_general_conflict ||
+                m_conflict_literal != sat::null_literal ||
                 (m_reason != backtrack_reason::unevaluated && m_is_extended);
         }
 
@@ -753,6 +754,10 @@ namespace seq {
         // inclusion, derivatives. Allocated in the constructor; owned by this graph.
         seq::seq_regex*              m_seq_regex = nullptr;
 
+        // Callback to check that literals assumed in branches are not already assigned to false.
+        // returns the literal that is assigned to false, otherwise returns a null_literal
+        std::function<sat::literal(expr *)> m_literal_if_false;
+
         // -----------------------------------------------
         // Modification counter for substitution length tracking.
         // mirrors ZIPT's LocalInfo.CurrentModificationCnt
@@ -786,6 +791,10 @@ namespace seq {
         nielsen_graph(euf::sgraph& sg, simple_solver& solver);
         ~nielsen_graph();
 
+        void set_literal_if_false(std::function<sat::literal(expr* e)> const& lif) {
+            m_literal_if_false = lif;
+        }
+
         ast_manager &get_manager() {
             return m;
         }

src/smt/theory_nseq.cpp

@@ -80,6 +80,20 @@ namespace smt {
         m_axioms.set_phase(set_phase);
         m_axioms.set_ensure_digits(ensure_digit_axiom);
         m_axioms.set_mark_no_diseq(mark_no_diseq);
+
+        std::function<sat::literal(expr*)> literal_if_false = [&](expr* e) {
+            bool is_not = m.is_not(e, e);
+            if (!ctx.e_internalized(e))
+                return sat::null_literal;
+            literal lit = ctx.get_literal(e);
+            if (is_not)
+                lit.neg();
+            if (ctx.get_assignment(lit) == l_false)
+                return lit;
+            return sat::null_literal;
+        };
+
+        m_nielsen.set_literal_if_false(literal_if_false);
     }
 
     // -----------------------------------------------------------------------