adding model-based sls for datatatypes

src/ast/sls/sat_ddfw.cpp

@@ -36,7 +36,7 @@ namespace sat {
     }
 
     lbool ddfw::check(unsigned sz, literal const* assumptions) {
-        init(sz, assumptions);        
+        init(sz, assumptions);   
         if (m_plugin)
             check_with_plugin();
         else
@@ -58,11 +58,12 @@ namespace sat {
 
     void ddfw::check_with_plugin() {
         m_plugin->init_search();
-        m_steps_since_progress = 0;
         unsigned steps = 0;
-        save_best_values();
+        if (m_min_sz <= m_unsat.size())
+            save_best_values();
+        
         try {
-            while (m_min_sz != 0 && m_steps_since_progress++ <= 1500000 && m_limit.inc()) {
+            while (m_min_sz > 0 && m_limit.inc()) {
                 if (should_reinit_weights()) do_reinit_weights();
                 else if (steps % 5000 == 0) shift_weights(), m_plugin->on_rescale();
                 else if (should_restart()) do_restart(), m_plugin->on_restart();
@@ -105,6 +106,7 @@ namespace sat {
     bool ddfw::do_flip() {
         double reward = 0;
         bool_var v = pick_var<uses_plugin>(reward);
+        //verbose_stream() << "flip " << v << " " << reward << "\n";
         return apply_flip<uses_plugin>(v, reward);
     }
 
@@ -125,46 +127,32 @@ namespace sat {
     template<bool uses_plugin>
     bool_var ddfw::pick_var(double& r) {
         double sum_pos = 0;
-        unsigned n = 1, m = 1;
+        unsigned n = 1;
         bool_var v0 = null_bool_var;
-        bool_var v1 = null_bool_var;
-        if (m_unsat_vars.empty())
-            return null_bool_var;
         for (bool_var v : m_unsat_vars) {
             r = reward(v);
             if (r > 0.0)    
                 sum_pos += score(r);            
             else if (r == 0.0 && sum_pos == 0 && (m_rand() % (n++)) == 0) 
                 v0 = v;            
-            else if (m_rand(m++) == 0) 
-                v1 = v;
         }
-        
-
-        if (v0 != null_bool_var && m_rand(20) == 0) 
-            return v0;        
-
-        if (v1 != null_bool_var && m_rand(20) == 0) 
-            return v1;        
-
         if (sum_pos > 0) {
-            double lim_pos = ((double) m_rand() / (1.0 + m_rand.max_value())) * sum_pos;  
+            double lim_pos = ((double) m_rand() / (1.0 + m_rand.max_value())) * sum_pos;                
             for (bool_var v : m_unsat_vars) {
                 r = reward(v);
                 if (r > 0) {
                     lim_pos -= score(r);
-                    if (lim_pos <= 0) {
-                        return v;
-                    }
+                    if (lim_pos <= 0) 
+                        return v;                    
                 }
             }
         }
         r = 0;
-        
-        if (v0 == null_bool_var)           
-            v0 = m_unsat_vars.elem_at(m_rand(m_unsat_vars.size()));
-        
-        return v0;
+        if (v0 != null_bool_var) 
+            return v0;
+        if (m_unsat_vars.empty())
+            return null_bool_var;
+        return m_unsat_vars.elem_at(m_rand(m_unsat_vars.size()));
     }
 
     void ddfw::add(unsigned n, literal const* c) {        
@@ -216,7 +204,6 @@ namespace sat {
         m_assumptions.append(sz, assumptions);
         add_assumptions();
         for (unsigned v = 0; v < num_vars(); ++v) {
-            literal lit(v, false), nlit(v, true);
             value(v) = (m_rand() % 2) == 0; // m_use_list[lit.index()].size() >= m_use_list[nlit.index()].size();
         }
         init_clause_data();
@@ -238,6 +225,7 @@ namespace sat {
         m_last_flips = 0;
         m_shifts = 0;
         m_stopwatch.start();
+        verbose_stream() << "unsat " << m_min_sz << "\n";
     }
 
     void ddfw::reinit() {
@@ -373,7 +361,8 @@ namespace sat {
                 break;
             }
         }
-        save_best_values();
+        if (m_unsat.size() < m_min_sz)
+            save_best_values();
     }
 
     bool ddfw::should_restart() {
@@ -422,15 +411,9 @@ namespace sat {
 
     void ddfw::save_best_values() {
         if (m_unsat.size() < m_min_sz || m_unsat.empty()) {
-            m_steps_since_progress = 0;
             if (m_unsat.size() < 50 || m_min_sz * 10 > m_unsat.size() * 11)
                 save_model();
         }
-#if 0
-        if (m_unsat.size() <= m_min_sz) {
-            verbose_stream() << "unsat " << m_clauses[m_unsat[0]] << "\n";
-        }
-#endif
 
         if (m_unsat.size() < m_min_sz) 
             m_models.reset();        

src/ast/sls/sat_ddfw.h

@@ -100,7 +100,7 @@ namespace sat {
         unsigned         m_restart_count = 0, m_reinit_count = 0;
         uint64_t         m_restart_next = 0, m_reinit_next = 0;
         uint64_t         m_flips = 0, m_last_flips = 0, m_shifts = 0;
-        unsigned         m_min_sz = 0, m_steps_since_progress = 0;
+        unsigned         m_min_sz = UINT_MAX;
         u_map<unsigned>  m_models;
         stopwatch        m_stopwatch;
         unsigned_vector  m_num_models;

src/ast/sls/sls_context.cpp

@@ -561,10 +561,11 @@ namespace sls {
         if (!m_repair_down.contains(e->get_id()))
             m_repair_down.insert(e->get_id());
         for (auto p : parents(e)) {
-            m_repair_up.reserve(p->get_id() + 1);
-            m_repair_down.reserve(p->get_id() + 1);
-            if (!m_repair_up.contains(p->get_id()))
-                m_repair_up.insert(p->get_id());
+            auto pid = p->get_id();
+            m_repair_up.reserve(pid + 1);
+            m_repair_down.reserve(pid + 1);
+            if (!m_repair_up.contains(pid))
+                m_repair_up.insert(pid);
         }
     }
 

src/ast/sls/sls_datatype_plugin.cpp

@@ -77,6 +77,7 @@ Model-repair based:
 #include "ast/sls/sls_datatype_plugin.h"
 #include "ast/sls/sls_euf_plugin.h"
 #include "ast/ast_pp.h"
+#include "params/sls_params.hpp"
 
 namespace sls {
     
@@ -258,14 +259,20 @@ namespace sls {
     }
 
     void datatype_plugin::initialize() {
-        add_axioms();
+        sls_params sp(ctx.get_params());
+        m_axiomatic_mode = sp.dt_axiomatic();
+        if (m_axiomatic_mode)
+            add_axioms();
     }
 
     expr_ref datatype_plugin::get_value(expr* e) {
         if (!dt.is_datatype(e))
             return expr_ref(m);
-        init_values();
-        return expr_ref(m_values.get(g->find(e)->get_root_id()), m);
+        if (m_axiomatic_mode) {
+            init_values();
+            return expr_ref(m_values.get(g->find(e)->get_root_id()), m);
+        }
+        return expr_ref(m_eval.get(e->get_id()), m);
     }
 
     void datatype_plugin::init_values() {
@@ -563,46 +570,380 @@ namespace sls {
     }
     
     void datatype_plugin::propagate_literal(sat::literal lit) {
-        euf.propagate_literal(lit);
+        if (m_axiomatic_mode)
+            euf.propagate_literal(lit);
+        else
+            propagate_literal_model_building(lit);
+    }
+
+    void datatype_plugin::propagate_literal_model_building(sat::literal lit) {
+        if (!ctx.is_true(lit))
+            return;
+        auto a = ctx.atom(lit.var());
+        if (!a || !is_app(a))
+            return;
+        repair_down(to_app(a));
     }
    
     bool datatype_plugin::is_sat() { return true; }
     
-    void datatype_plugin::register_term(expr* e) {}
+    void datatype_plugin::register_term(expr* e) {    
+        expr* t = nullptr;
+        if (dt.is_accessor(e, t)) {
+            auto f = to_app(e)->get_decl();
+            m_occurs.insert_if_not_there(f, expr_set()).insert(e);
+            m_eval_accessor.insert_if_not_there(f, obj_map<expr, expr*>());
+        }
+    }
 
 
     bool datatype_plugin::repair_down(app* e) {
-        verbose_stream() << "repair-down " << mk_bounded_pp(e, m) << "\n";
+        expr* t, * s;
+        auto v0 = eval0(e);
+        auto v1 = eval1(e);
+        if (v0 == v1)
+            return true;
+        IF_VERBOSE(2, verbose_stream() << "dt-repair-down " << mk_bounded_pp(e, m) << " " << v0 << " <- " << v1 << "\n");
+        if (dt.is_constructor(e))
+            repair_down_constructor(e, v0, v1);
+        else if (dt.is_accessor(e, t))
+            repair_down_accessor(e, t, v0);
+        else if (dt.is_recognizer(e, t))
+            repair_down_recognizer(e, t);
+        else if (m.is_eq(e, s, t))
+            repair_down_eq(e, s, t);
+        else if (m.is_distinct(e))
+            repair_down_distinct(e);        
+        else {
+            UNREACHABLE();
+        }
         return false;
     }
 
+    //
+    // C(t) <- C(s) then repair t <- s
+    // C(t) <- D(s) then fail the repair.
+    //
+    void datatype_plugin::repair_down_constructor(app* e, expr* v0, expr* v1) {
+        SASSERT(dt.is_constructor(v0));
+        SASSERT(dt.is_constructor(v1));
+        SASSERT(e->get_decl() == to_app(v1)->get_decl());
+        if (e->get_decl() == to_app(v0)->get_decl()) {
+            for (unsigned i = 0; i < e->get_num_args(); ++i) {
+                auto w0 = to_app(v0)->get_arg(i);
+                auto w1 = to_app(v1)->get_arg(i);
+                if (w0 == w1)
+                    continue;
+                expr* arg = e->get_arg(i);
+                set_eval0(arg, w0);
+                ctx.new_value_eh(arg);
+            }
+        }
+    }
+
+    //
+    // A_D(t) <- s, val(t) = D(..s'..)      then update val(t) to agree with s
+    // A_D(t) <- s, val(t) = C(..)          then set t to D(...s...)
+    //            , eval(val(A_D(t))) = s'  then update eval(val(A_D,(t))) to s'
+    void datatype_plugin::repair_down_accessor(app* e, expr* t, expr* v0) {
+        auto f = e->get_decl();
+        auto c = dt.get_accessor_constructor(f);       
+        auto val_t = eval0(t);
+        SASSERT(dt.is_constructor(val_t));
+        expr_ref_vector args(m);
+        auto const& accs = *dt.get_constructor_accessors(c);
+        unsigned i;
+        for (i = 0; i < accs.size(); ++i) {
+            if (accs[i] == f)
+                break;
+        }
+        SASSERT(i < accs.size());
+        if (to_app(val_t)->get_decl() == c) {
+            if (to_app(val_t)->get_arg(i) == v0)
+                return;
+            args.append(accs.size(), to_app(val_t)->get_args());
+            args[i] = v0;
+            expr* new_val_t = m.mk_app(c, args);
+            set_eval0(t, new_val_t);
+            ctx.new_value_eh(t);
+            return;
+        }
+        if (ctx.rand(5) != 0) {
+            update_eval_accessor(e, val_t, v0);              
+            return;
+        }
+        for (unsigned j = 0; j < accs.size(); ++j) {
+            if (i == j)
+                args[i] = v0;
+            else
+                args[j] = m_model->get_some_value(accs[j]->get_range());
+        }
+        expr* new_val_t = m.mk_app(c, args);
+        set_eval0(t, new_val_t);
+        ctx.new_value_eh(t);
+    }
+
+    void datatype_plugin::repair_down_recognizer(app* e, expr* t) {
+        auto bv = ctx.atom2bool_var(e);
+        auto is_true = ctx.is_true(bv);
+        auto c = dt.get_recognizer_constructor(e->get_decl());
+        auto val_t = eval0(t);
+        auto const& cons = *dt.get_datatype_constructors(t->get_sort());
+
+        auto set_to_instance = [&](func_decl* c) {
+            auto const& accs = *dt.get_constructor_accessors(c);
+            expr_ref_vector args(m);
+            for (auto a : accs)
+                args.push_back(m_model->get_some_value(a->get_range()));
+            set_eval0(t, m.mk_app(c, args));
+            ctx.new_value_eh(t);
+        };
+        auto different_constructor = [&](func_decl* c) {
+            unsigned i = 0;
+            func_decl* c_new = nullptr;
+            for (auto c2 : cons)
+                if (c2 != c && ctx.rand(++i) == 0)
+                    c_new = c2;
+            return c_new;
+        };
+
+        SASSERT(dt.is_constructor(val_t));
+        if (c == to_app(val_t)->get_decl() && is_true)
+            return;
+        if (c != to_app(val_t)->get_decl() && !is_true)
+            return;
+        if (ctx.rand(10) == 0) 
+            ctx.flip(bv);
+        else if (is_true) 
+            set_to_instance(c);
+        else if (cons.size() == 1) 
+            ctx.flip(bv);
+        else 
+            set_to_instance(different_constructor(c));
+    }
+
+    void datatype_plugin::repair_down_eq(app* e, expr* s, expr* t) {
+        auto bv = ctx.atom2bool_var(e);
+        auto is_true = ctx.is_true(bv);
+        auto vs = eval0(s);
+        auto vt = eval0(t);
+        if (is_true && vs == vt)
+            return;
+        if (!is_true && vs != vt)
+            return;
+
+        if (is_true) {
+            auto coin = ctx.rand(5);
+            if (coin <= 1) {
+                set_eval0(s, vt);
+                ctx.new_value_eh(s);
+                return;
+            }
+            if (coin <= 3) {
+                set_eval0(t, vs);
+                ctx.new_value_eh(t);
+            }
+            if (true) {
+                auto new_v = m_model->get_some_value(s->get_sort());
+                set_eval0(s, new_v);
+                set_eval0(t, new_v);
+                ctx.new_value_eh(s);
+                ctx.new_value_eh(t);
+                return;
+            }
+        }
+        auto coin = ctx.rand(10);
+        if (coin <= 4) {
+            auto new_v = m_model->get_some_value(s->get_sort());
+            set_eval0(s, new_v);
+            ctx.new_value_eh(s);
+            return;
+        }
+        if (coin <= 9) {
+            auto new_v = m_model->get_some_value(s->get_sort());
+            set_eval0(t, new_v);
+            ctx.new_value_eh(t);
+            return;
+        }
+    }
+
+    void datatype_plugin::repair_down_distinct(app* e) {
+        auto bv = ctx.atom2bool_var(e);
+        auto is_true = ctx.is_true(bv);
+        unsigned sz = e->get_num_args();
+        for (unsigned i = 0; i < sz; ++i) {
+            auto val1 = eval0(e->get_arg(i));
+            for (unsigned j = i + 1; j < sz; ++j) {
+                auto val2 = eval0(e->get_arg(j));
+                if (val1 != val2)
+                    continue;
+                if (!is_true)
+                    return;
+                if (ctx.rand(2) == 0)
+                    std::swap(i, j);
+                auto new_v = m_model->get_some_value(e->get_arg(i)->get_sort());
+                set_eval0(e->get_arg(i), new_v);
+                ctx.new_value_eh(e->get_arg(i));
+                return;
+            }
+        }
+        if (is_true)
+            return;
+        if (sz == 1) {
+            ctx.flip(bv);
+            return;
+        }
+        unsigned i = ctx.rand(sz);
+        unsigned j = ctx.rand(sz-1);
+        if (j == i)
+            ++j;
+        if (ctx.rand(2) == 0)
+            std::swap(i, j);
+        set_eval0(e->get_arg(i), eval0(e->get_arg(j)));
+    }
+
     void datatype_plugin::repair_up(app* e) {
-        verbose_stream() << "repair-up " << mk_bounded_pp(e, m) << "\n";
+        IF_VERBOSE(2, verbose_stream() << "dt-repair-up " << mk_bounded_pp(e, m) << "\n");
+        expr* t;
+        auto v0 = eval0(e);
+        auto v1 = eval1(e);
+        if (v0 == v1)
+            return;
+        if (dt.is_constructor(e)) 
+            set_eval0(e, v1);                 
+        else if (m.is_bool(e)) 
+            ctx.flip(ctx.atom2bool_var(e));
+        else if (dt.is_accessor(e, t))
+            repair_up_accessor(e, t, v1);
+        else {
+            UNREACHABLE();
+        }
+    }
+
+    void datatype_plugin::repair_up_accessor(app* e, expr* t, expr* v1) {
+        auto v_t = eval0(t);
+        auto f = e->get_decl();
+        SASSERT(dt.is_constructor(v_t));
+        auto c = dt.get_accessor_constructor(f);
+        if (to_app(v_t)->get_decl() != c) 
+            update_eval_accessor(e, v_t, v1);
+        
+        set_eval0(e, v1);       
     }
 
     expr_ref datatype_plugin::eval1(expr* e) {
-        auto n = g->find(e)->get_root();
-        e = n->get_expr();
-        if (!dt.is_datatype(e))
-            return ctx.get_value(e);
-        auto con = get_constructor(n);
-        if (con) {
+        expr* s = nullptr, * t = nullptr;
+        if (m.is_eq(e, s, t))
+            return expr_ref(m.mk_bool_val(eval0rec(s) == eval0rec(t)), m);
+        if (m.is_distinct(e)) {
             expr_ref_vector args(m);
-            for (auto arg : euf::enode_args(con)) 
+            for (auto arg : *to_app(e))
                 args.push_back(eval0(arg));
-            return expr_ref(m.mk_app(con->get_decl(), args), m);
+            bool d = true;
+            for (unsigned i = 0; i < args.size(); ++i)
+                for (unsigned j = i + 1; i < args.size(); ++j)
+                    d &= args.get(i) != args.get(j);
+            return expr_ref(m.mk_bool_val(d), m);
         }
-        return eval0(n);
+        if (dt.is_accessor(e, t)) {
+            auto f = to_app(e)->get_decl();
+            auto v = eval0rec(t);
+            return eval_accessor(f, v);
+        }
+        if (dt.is_constructor(e)) {
+            expr_ref_vector args(m);
+            for (auto arg : *to_app(e))
+                args.push_back(eval0rec(arg));
+            return expr_ref(m.mk_app(to_app(e)->get_decl(), args), m);
+        }
+        if (dt.is_recognizer(e, t)) {
+            auto v = eval0rec(t);
+            SASSERT(dt.is_constructor(v));
+            auto c = dt.get_recognizer_constructor(to_app(e)->get_decl());
+            return expr_ref(m.mk_bool_val(c == to_app(v)->get_decl()), m);
+        }
+        return eval0(e);
+    }
+
+    expr_ref datatype_plugin::eval0rec(expr* e) {
+        auto v = m_eval.get(e->get_id(), nullptr);
+        if (v)
+            return expr_ref(v, m);
+        if (!is_app(e) || to_app(e)->get_family_id() != m_fid)
+            return ctx.get_value(e);
+        auto w = eval1(e);
+        m_eval.set(e->get_id(), w);
+        return w;
+    }
+
+    expr_ref datatype_plugin::eval_accessor(func_decl* f, expr* t) {
+        auto& t2val = m_eval_accessor[f];
+        if (!t2val.contains(t)) {
+            auto val = m_model->get_some_value(f->get_range());
+            m.inc_ref(t);
+            m.inc_ref(val);
+        }
+        return expr_ref(t2val[t], m);
+    }
+
+    void datatype_plugin::update_eval_accessor(app* e, expr* t, expr* value) {
+        func_decl* f = e->get_decl();
+        
+        auto& t2val = m_eval_accessor[f];
+        expr* old_value = nullptr;
+        t2val.find(t, old_value);
+        if (old_value == value)
+            ;
+        else if (old_value) {
+            t2val[t] = value;
+            m.inc_ref(value);
+            m.dec_ref(old_value);
+        }
+        else {
+            m.inc_ref(t);
+            m.inc_ref(value);
+            t2val.insert(t, value);
+        }        
+
+        for (expr* b : m_occurs[f]) {
+            if (b == e)
+                continue;
+            expr* a;
+            VERIFY(dt.is_accessor(b, a));
+            auto v_a = eval0(a);
+            if (v_a.get() == t) {
+                set_eval0(b, value);
+                ctx.new_value_eh(b);
+            }
+        }
+    }
+
+    void datatype_plugin::del_eval_accessor() {
+        ptr_vector<expr> kv;
+        for (auto& [f, t2val] : m_eval_accessor)
+            for (auto& [k, val] : t2val)
+                kv.push_back(k), kv.push_back(val);
+        for (auto k : kv)
+            m.dec_ref(k);
     }
 
     expr_ref datatype_plugin::eval0(expr* n) {
         if (!dt.is_datatype(n->get_sort()))
             return ctx.get_value(n);
-        if (!m_eval.get(n->get_id(), nullptr))
-            m_eval[n->get_id()] = m_model->get_some_value(n->get_sort());
+        auto v = m_eval.get(n->get_id(), nullptr);
+        if (v)
+            return expr_ref(v, m);
+        set_eval0(n, m_model->get_some_value(n->get_sort()));
         return expr_ref(m_eval.get(n->get_id()), m);
     }
 
+    void datatype_plugin::set_eval0(expr* e, expr* value) {
+        if (dt.is_datatype(e->get_sort()))
+            m_eval[e->get_id()] = value;
+        else
+            ctx.set_value(e, value);
+    }
+
     expr_ref datatype_plugin::eval0(euf::enode* n) {
         return eval0(n->get_root()->get_expr());
     }

src/ast/sls/sls_datatype_plugin.h

@@ -38,6 +38,7 @@ namespace sls {
         obj_map<sort, ptr_vector<expr>> m_dts;
         obj_map<expr, vector<parent_t>> m_parents;
         
+        bool m_axiomatic_mode = true;
         mutable datatype_util dt;
         expr_ref_vector m_axioms, m_values, m_eval;
         model_ref m_model;
@@ -54,10 +55,29 @@ namespace sls {
 
         euf::enode* get_constructor(euf::enode* n) const;
 
+        // f -> v_t -> val 
+        // e = A(t)
+        // val(t) <- val
+        // 
+        typedef obj_hashtable<expr> expr_set;
+        obj_map<func_decl, obj_map<expr, expr*>> m_eval_accessor;
+        obj_map<func_decl, expr_set> m_occurs;
         expr_ref eval1(expr* e);
         expr_ref eval0(euf::enode* n);
         expr_ref eval0(expr* n);
+        expr_ref eval0rec(expr* n);
+        expr_ref eval_accessor(func_decl* f, expr* t);
+        void update_eval_accessor(app* e, expr* t, expr* value);
+        void del_eval_accessor();
+        void set_eval0(expr* e, expr* val);
 
+        void repair_down_constructor(app* e, expr* v0, expr* v1);
+        void repair_down_accessor(app* e, expr* t, expr* v1);
+        void repair_down_recognizer(app* e, expr* t);
+        void repair_down_eq(app* e, expr* s, expr* t);
+        void repair_down_distinct(app* e);
+        void repair_up_accessor(app* e, expr* t, expr* v0);
+        void propagate_literal_model_building(sat::literal lit);
 
     public:
         datatype_plugin(context& c);

src/params/sls_params.pyg

@@ -23,6 +23,7 @@ def_module_params('sls',
                         ('random_offset', BOOL, 1, 'use random offset for candidate evaluation'),
                         ('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'),
                         ('euf_incremental', UINT, 0, '0 non-incremental, 1 incremental, 2 alternating EUF resolver'), 
+                        ('dt_axiomatic', BOOL, True, 'use axiomatic mode or model reduction for datatype solver'),
                         ('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
                         ('random_seed', UINT, 0, 'random seed')
               ))

src/sat/sat_ddfw_wrapper.cpp

@@ -56,6 +56,7 @@ namespace sat {
     }
 
     void ddfw_wrapper::add(solver const& s) {
+        m_ddfw.set_seed(s.get_config().m_random_seed);
         m_ddfw.m_clauses.reset(); 
         m_ddfw.m_use_list.reset();
         m_ddfw.m_num_non_binary_clauses = 0;