fixes

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

src/ast/sls/sls_context.cpp

@@ -39,7 +39,8 @@ namespace sls {
         m_ld(*this),
         m_repair_down(m.get_num_asts(), m_gd),
         m_repair_up(m.get_num_asts(), m_ld),
-        m_todo(m) {
+        m_todo(m),
+        m_constraint_trail(m) {
     }
 
     void context::updt_params(params_ref const& p) {
@@ -232,8 +233,9 @@ namespace sls {
         auto p = m_plugins.get(fid, nullptr);
         if (p)
             p->propagate_literal(lit);
-        if (!is_true(lit))
+        if (!is_true(lit)) {
             m_new_constraint = true;
+        }
     }
 
     bool context::is_true(expr* e) {
@@ -287,7 +289,11 @@ namespace sls {
     }
 
     void context::add_constraint(expr* e) {        
-        add_clause(e);        
+        if (m_constraint_ids.contains(e->get_id()))
+            return;
+        m_constraint_ids.insert(e->get_id());
+        m_constraint_trail.push_back(e);
+        add_clause(e);     
         m_new_constraint = true;
         ++m_stats.m_num_constraints;
     }
@@ -363,7 +369,6 @@ namespace sls {
     }
 
     void context::add_clause(sat::literal_vector const& lits) {
-        //verbose_stream() << lits << "\n";
         s.add_clause(lits.size(), lits.data());
         m_new_constraint = true;
         ++m_stats.m_num_constraints;
@@ -564,6 +569,7 @@ namespace sls {
         m_visited.reset();
         m_root_literals.reset();
 
+
         for (auto const& clause : s.clauses()) {
             bool has_relevant = false;
             unsigned n = 0;

src/ast/sls/sls_context.h

@@ -123,7 +123,9 @@ namespace sls {
         greater_depth m_gd;
         less_depth m_ld;
         heap<greater_depth> m_repair_down;
-        heap<less_depth> m_repair_up;        
+        heap<less_depth> m_repair_up;  
+        uint_set m_constraint_ids;
+        expr_ref_vector m_constraint_trail;
         stats m_stats;
 
         void register_plugin(plugin* p);

src/ast/sls/sls_datatype_plugin.cpp

@@ -385,6 +385,8 @@ namespace sls {
             expr* e = n->get_expr();
             if (!dt.is_datatype(e))
                 continue;
+            if (!ctx.is_relevant(e))
+                continue;
             sort* s = e->get_sort();
             sorts.insert_if_not_there(s, ptr_vector<expr>()).push_back(e);
 

src/ast/sls/sls_euf_plugin.cpp

@@ -88,15 +88,14 @@ namespace sls {
         m_replay_stack.push_back(lit);
         replay();
     }
-    void euf_plugin::resolve() {
-        auto& g = *m_g;
-        if (!g.inconsistent())
-            return;
 
+    sat::literal euf_plugin::resolve_conflict() {
+        auto& g = *m_g;
+        SASSERT(g.inconsistent());
         ++m_stats.m_num_conflicts;
         unsigned n = 0;
         sat::literal_vector lits;
-        sat::literal flit = sat::null_literal, slit;
+        sat::literal flit = sat::null_literal;
         ptr_vector<size_t> explain;
         g.begin_explain();
         g.explain<size_t>(explain, nullptr);
@@ -110,7 +109,7 @@ namespace sls {
             });
         for (auto p : explain) {
             sat::literal l = to_literal(p);
-            CTRACE("euf", !ctx.is_true(l), tout << "not true " << l << "\n"; ctx.display(tout););            
+            CTRACE("euf", !ctx.is_true(l), tout << "not true " << l << "\n"; ctx.display(tout););
             SASSERT(ctx.is_true(l));
 
             if (ctx.is_unit(l))
@@ -118,14 +117,25 @@ namespace sls {
             if (!lits.contains(~l))
                 lits.push_back(~l);
 
-
             if (ctx.reward(l.var()) > reward)
                 n = 0, reward = ctx.reward(l.var());
 
             if (ctx.rand(++n) == 0)
                 flit = l;
         }
+        // flip the last literal on the replay stack
+        IF_VERBOSE(10, verbose_stream() << "sls.euf - flip " << flit << "\n");
+        ctx.add_clause(lits);
+        return flit;
+    }
 
+    void euf_plugin::resolve() {
+        auto& g = *m_g;
+        if (!g.inconsistent())
+            return;
+
+        auto flit = resolve_conflict();
+        sat::literal slit;
         if (flit == sat::null_literal)
             return;
         do {
@@ -135,9 +145,6 @@ namespace sls {
             m_stack.pop_back();
         }
         while (slit != flit);
-        // flip the last literal on the replay stack
-        IF_VERBOSE(10, verbose_stream() << "sls.euf - flip " << flit << "\n");
-        ctx.add_clause(lits);
         ctx.flip(flit.var());        
         m_replay_stack.back().neg();
 
@@ -294,6 +301,9 @@ namespace sls {
                     g.merge(g.find(e), g.find(m.mk_true()), to_ptr(lit));
             }
             g.propagate();
+
+            if (g.inconsistent()) 
+                resolve_conflict();
         }
 
         typedef obj_map<sort, unsigned> map1;
@@ -417,8 +427,10 @@ namespace sls {
                     for (unsigned i = t->get_num_args(); i-- > 0; )
                         verbose_stream() << ctx.get_value(t->get_arg(i)) << " == " << ctx.get_value(u->get_arg(i)) << "\n";
 #endif
-                    ctx.add_constraint(m.mk_or(ors));
+                    expr_ref fml(m.mk_or(ors), m);
+                    ctx.add_constraint(fml);
                     new_constraint = true;
+                    
                 }
                 else
                     m_values.insert(t);
@@ -427,7 +439,7 @@ namespace sls {
 
         for (auto lit : ctx.root_literals()) {
             if (!ctx.is_true(lit))
-                lit.neg();
+                continue;
             auto e = ctx.atom(lit.var());
             if (lit.sign() && e && m.is_distinct(e)) {
                 auto n = to_app(e)->get_num_args();

src/ast/sls/sls_euf_plugin.h

@@ -56,6 +56,7 @@ namespace sls {
         void propagate_literal_incremental(sat::literal lit);
         void propagate_literal_incremental_step(sat::literal lit);
         void resolve();
+        sat::literal resolve_conflict();
         void replay();
 
         void propagate_literal_non_incremental(sat::literal lit);