na

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

src/smt/CMakeLists.txt

@@ -70,9 +70,9 @@ z3_add_component(smt
     theory_str.cpp
     theory_str_mc.cpp
     theory_str_regex.cpp
+    theory_user_propagator.cpp
     theory_utvpi.cpp
     theory_wmaxsat.cpp
-    user_propagator.cpp
     uses_theory.cpp
     watch_list.cpp
   COMPONENT_DEPENDENCIES

src/smt/seq_eq_solver.cpp

@@ -1120,9 +1120,9 @@ struct remove_obj_pair_map : public trail {
     remove_obj_pair_map(ast_manager& m, obj_pair_hashtable<expr, expr> & map, expr* a, expr* b):
         m(m), m_map(map), a(a), b(b) {}
     void undo() override {
+        m_map.erase(std::make_pair(a, b));
         m.dec_ref(a);
         m.dec_ref(b);
-        m_map.erase(std::make_pair(a, b));
     }
 };
 

src/smt/smt_context.cpp

@@ -198,7 +198,7 @@ namespace smt {
             return;
         ast_translation tr(src_ctx.m, m, false);
         auto* p = get_theory(m.mk_family_id("user_propagator"));
-        m_user_propagator = reinterpret_cast<user_propagator*>(p);
+        m_user_propagator = reinterpret_cast<theory_user_propagator*>(p);
         SASSERT(m_user_propagator);
         for (unsigned i = 0; i < src_ctx.m_user_propagator->get_num_vars(); ++i) {
             app* e = src_ctx.m_user_propagator->get_expr(i);
@@ -2886,11 +2886,11 @@ namespace smt {
 
     void context::user_propagate_init(
         void*                    ctx, 
-        solver::push_eh_t&       push_eh,
-        solver::pop_eh_t&        pop_eh,
-        solver::fresh_eh_t&      fresh_eh) {
+        user_propagator::push_eh_t&       push_eh,
+        user_propagator::pop_eh_t&        pop_eh,
+        user_propagator::fresh_eh_t&      fresh_eh) {
         setup_context(false);
-        m_user_propagator = alloc(user_propagator, *this);
+        m_user_propagator = alloc(theory_user_propagator, *this);
         m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
         for (unsigned i = m_scopes.size(); i-- > 0; ) 
             m_user_propagator->push_scope_eh();
@@ -3552,7 +3552,7 @@ namespace smt {
             parallel p(*this);
             return p(asms);
         }
-        lbool r;
+        lbool r = l_undef;
         do {
             pop_to_base_lvl();
             expr_ref_vector asms(m, num_assumptions, assumptions);
@@ -3573,7 +3573,7 @@ namespace smt {
         if (!check_preamble(true)) return l_undef;
         TRACE("before_search", display(tout););
         setup_context(false);
-        lbool r;
+        lbool r = l_undef;
         do {
             pop_to_base_lvl();
             expr_ref_vector asms(cube);

src/smt/smt_context.h

@@ -46,7 +46,7 @@ Revision History:
 #include "util/statistics.h"
 #include "smt/fingerprints.h"
 #include "smt/proto_model/proto_model.h"
-#include "smt/user_propagator.h"
+#include "smt/theory_user_propagator.h"
 #include "model/model.h"
 #include "solver/progress_callback.h"
 #include "solver/assertions/asserted_formulas.h"
@@ -88,7 +88,7 @@ namespace smt {
         scoped_ptr<quantifier_manager>   m_qmanager;
         scoped_ptr<model_generator>      m_model_generator;
         scoped_ptr<relevancy_propagator> m_relevancy_propagator;
-        user_propagator*            m_user_propagator;
+        theory_user_propagator*          m_user_propagator;
         random_gen                  m_random;
         bool                        m_flushing; // (debug support) true when flushing
         mutable unsigned            m_lemma_id;
@@ -1695,29 +1695,29 @@ namespace smt {
          */
         void user_propagate_init(
             void*                 ctx, 
-            solver::push_eh_t&    push_eh,
-            solver::pop_eh_t&     pop_eh,
-            solver::fresh_eh_t&   fresh_eh);
+            user_propagator::push_eh_t&    push_eh,
+            user_propagator::pop_eh_t&     pop_eh,
+            user_propagator::fresh_eh_t&   fresh_eh);
 
-        void user_propagate_register_final(solver::final_eh_t& final_eh) {
+        void user_propagate_register_final(user_propagator::final_eh_t& final_eh) {
             if (!m_user_propagator) 
                 throw default_exception("user propagator must be initialized");
             m_user_propagator->register_final(final_eh);
         }
 
-        void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) {
+        void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) {
             if (!m_user_propagator) 
                 throw default_exception("user propagator must be initialized");
             m_user_propagator->register_fixed(fixed_eh);
         }
         
-        void user_propagate_register_eq(solver::eq_eh_t& eq_eh) {
+        void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) {
             if (!m_user_propagator) 
                 throw default_exception("user propagator must be initialized");
             m_user_propagator->register_eq(eq_eh);
         }
         
-        void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) {
+        void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) {
             if (!m_user_propagator) 
                 throw default_exception("user propagator must be initialized");
             m_user_propagator->register_diseq(diseq_eh);

src/smt/smt_kernel.cpp

@@ -223,25 +223,25 @@ namespace smt {
 
         void user_propagate_init(
             void*                    ctx, 
-            solver::push_eh_t&       push_eh,
-            solver::pop_eh_t&        pop_eh,
-            solver::fresh_eh_t&      fresh_eh) {
+            user_propagator::push_eh_t&       push_eh,
+            user_propagator::pop_eh_t&        pop_eh,
+            user_propagator::fresh_eh_t&      fresh_eh) {
             m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
         }
 
-        void user_propagate_register_final(solver::final_eh_t& final_eh) {
+        void user_propagate_register_final(user_propagator::final_eh_t& final_eh) {
             m_kernel.user_propagate_register_final(final_eh);
         }
 
-        void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) {
+        void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) {
             m_kernel.user_propagate_register_fixed(fixed_eh);
         }
         
-        void user_propagate_register_eq(solver::eq_eh_t& eq_eh) {
+        void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) {
             m_kernel.user_propagate_register_eq(eq_eh);
         }
         
-        void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) {
+        void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) {
             m_kernel.user_propagate_register_diseq(diseq_eh);
         }
 
@@ -451,25 +451,25 @@ namespace smt {
 
     void kernel::user_propagate_init(
         void*                ctx, 
-        solver::push_eh_t&   push_eh,
-        solver::pop_eh_t&    pop_eh,
-        solver::fresh_eh_t&  fresh_eh) {
+        user_propagator::push_eh_t&   push_eh,
+        user_propagator::pop_eh_t&    pop_eh,
+        user_propagator::fresh_eh_t&  fresh_eh) {
         m_imp->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
     }
 
-    void kernel::user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) {
+    void kernel::user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) {
         m_imp->user_propagate_register_fixed(fixed_eh);
     }
     
-    void kernel::user_propagate_register_final(solver::final_eh_t& final_eh) {
+    void kernel::user_propagate_register_final(user_propagator::final_eh_t& final_eh) {
         m_imp->user_propagate_register_final(final_eh);
     }
     
-    void kernel::user_propagate_register_eq(solver::eq_eh_t& eq_eh) {
+    void kernel::user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) {
         m_imp->user_propagate_register_eq(eq_eh);
     }
     
-    void kernel::user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) {
+    void kernel::user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) {
         m_imp->user_propagate_register_diseq(diseq_eh);
     }
 

src/smt/smt_kernel.h

@@ -289,17 +289,17 @@ namespace smt {
         */
         void user_propagate_init(
             void* ctx, 
-            solver::push_eh_t&      push_eh,
-            solver::pop_eh_t&       pop_eh,
-            solver::fresh_eh_t&     fresh_eh);
+            user_propagator::push_eh_t&      push_eh,
+            user_propagator::pop_eh_t&       pop_eh,
+            user_propagator::fresh_eh_t&     fresh_eh);
 
-        void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh);
+        void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh);
 
-        void user_propagate_register_final(solver::final_eh_t& final_eh);
+        void user_propagate_register_final(user_propagator::final_eh_t& final_eh);
         
-        void user_propagate_register_eq(solver::eq_eh_t& eq_eh);
+        void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh);
         
-        void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh);
+        void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh);
 
 
         /**

src/smt/smt_model_generator.cpp

@@ -105,7 +105,7 @@ namespace smt {
                     else
                         proc = alloc(expr_wrapper_proc, m.mk_false());
                 }
-                else if (m.is_value(r->get_expr()))
+                else if (m.is_model_value(r->get_expr()))
                     proc = alloc(expr_wrapper_proc, r->get_expr());                    
                 else {
                     family_id fid = s->get_family_id();

src/smt/smt_solver.cpp

@@ -215,25 +215,25 @@ namespace {
 
         void user_propagate_init(
             void*                ctx, 
-            solver::push_eh_t&   push_eh,
-            solver::pop_eh_t&    pop_eh,
-            solver::fresh_eh_t&  fresh_eh) override {
+            user_propagator::push_eh_t&   push_eh,
+            user_propagator::pop_eh_t&    pop_eh,
+            user_propagator::fresh_eh_t&  fresh_eh) override {
             m_context.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
         }
         
-        void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) override {
+        void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override {
             m_context.user_propagate_register_fixed(fixed_eh);
         }
 
-        void user_propagate_register_final(solver::final_eh_t& final_eh) override {
+        void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override {
             m_context.user_propagate_register_final(final_eh);
         }
         
-        void user_propagate_register_eq(solver::eq_eh_t& eq_eh) override {
+        void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override {
             m_context.user_propagate_register_eq(eq_eh);
         }
         
-        void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) override {
+        void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override {
             m_context.user_propagate_register_diseq(diseq_eh);
         }
 

src/smt/tactic/ctx_solver_simplify_tactic.cpp

@@ -63,6 +63,8 @@ public:
         m_fns.reset();
     }
 
+    char const* name() const override { return "ctx_solver_simplify"; }
+
     void updt_params(params_ref const & p) override {
         m_solver.updt_params(p);
     }

src/smt/tactic/smt_tactic_core.cpp

@@ -37,32 +37,35 @@ typedef obj_map<expr, expr *> expr2expr_map;
 
 
 class smt_tactic : public tactic {
+    ast_manager&                 m;
     smt_params                   m_params;
     params_ref                   m_params_ref;
     statistics                   m_stats;
-    smt::kernel *                m_ctx;
+    smt::kernel*                 m_ctx = nullptr;
     symbol                       m_logic;
-    progress_callback *          m_callback;
-    bool                         m_candidate_models;
-    bool                         m_fail_if_inconclusive;
+    progress_callback*           m_callback = nullptr;
+    bool                         m_candidate_models = false;
+    bool                         m_fail_if_inconclusive = false;
 
 public:
-    smt_tactic(params_ref const & p):
+    smt_tactic(ast_manager& m, params_ref const & p):
+        m(m),
         m_params_ref(p),
-        m_ctx(nullptr),
-        m_callback(nullptr) {
+        m_vars(m) {
         updt_params_core(p);
         TRACE("smt_tactic", tout << "p: " << p << "\n";);
     }
 
     tactic * translate(ast_manager & m) override {
-        return alloc(smt_tactic, m_params_ref);
+        return alloc(smt_tactic, m, m_params_ref);
     }
 
     ~smt_tactic() override {
         SASSERT(m_ctx == nullptr);
     }
 
+    char const* name() const override { return "smt"; }
+
     smt_params & fparams() {
         return m_params;
     }
@@ -137,6 +140,7 @@ public:
         ~scoped_init_ctx() {
             smt::kernel * d = m_owner.m_ctx;
             m_owner.m_ctx = nullptr;
+            m_owner.m_user_ctx = nullptr;
 
             if (d)
                 dealloc(d);
@@ -151,7 +155,6 @@ public:
                     goal_ref_buffer & result) override {
         try {
             IF_VERBOSE(10, verbose_stream() << "(smt.tactic start)\n";);
-            ast_manager & m = in->m();
             tactic_report report("smt", *in);
             TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
                   << " PREPROCESS: " << fparams().m_preprocess << "\n";
@@ -163,7 +166,7 @@ public:
             TRACE("smt_tactic_detail", in->display(tout););
             TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);
             scoped_init_ctx  init(*this, m);
-            SASSERT(m_ctx != 0);
+            SASSERT(m_ctx);
 
             expr_ref_vector clauses(m);
             expr2expr_map               bool2dep;
@@ -194,10 +197,11 @@ public:
             if (m_ctx->canceled()) {                
                 throw tactic_exception(Z3_CANCELED_MSG);
             }
+            user_propagate_delay_init();
 
             lbool r;
             try {
-                if (assumptions.empty())
+                if (assumptions.empty() && !m_user_ctx)
                     r = m_ctx->setup_and_check();
                 else
                     r = m_ctx->check(assumptions.size(), assumptions.data());
@@ -306,10 +310,163 @@ public:
             throw tactic_exception(ex.msg());
         }
     }
+
+    void* m_user_ctx = nullptr;
+    user_propagator::push_eh_t  m_push_eh;
+    user_propagator::pop_eh_t   m_pop_eh;
+    user_propagator::fresh_eh_t m_fresh_eh;
+    user_propagator::fixed_eh_t m_fixed_eh;
+    user_propagator::final_eh_t m_final_eh;
+    user_propagator::eq_eh_t    m_eq_eh;
+    user_propagator::eq_eh_t    m_diseq_eh;
+    expr_ref_vector             m_vars;
+    unsigned_vector             m_var2internal;
+    unsigned_vector             m_internal2var;
+
+    user_propagator::fixed_eh_t i_fixed_eh;
+    user_propagator::final_eh_t i_final_eh;
+    user_propagator::eq_eh_t    i_eq_eh;
+    user_propagator::eq_eh_t    i_diseq_eh;
+
+
+
+    struct callback : public user_propagator::callback {
+        smt_tactic* t = nullptr;
+        user_propagator::callback* cb = nullptr;
+        unsigned_vector fixed, lhs, rhs;
+        void propagate_cb(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) override {
+            fixed.reset();
+            lhs.reset();
+            rhs.reset();
+            for (unsigned i = 0; i < num_fixed; ++i)
+                fixed.push_back(t->m_var2internal[fixed_ids[i]]);
+            for (unsigned i = 0; i < num_eqs; ++i) {
+                lhs.push_back(t->m_var2internal[eq_lhs[i]]);
+                rhs.push_back(t->m_var2internal[eq_rhs[i]]);
+            }
+            cb->propagate_cb(num_fixed, fixed.data(), num_eqs, lhs.data(), rhs.data(), conseq);
+        }
+
+        unsigned register_cb(expr* e) override {
+            unsigned j = t->m_vars.size();
+            t->m_vars.push_back(e);
+            unsigned i = cb->register_cb(e);
+            t->m_var2internal.setx(j, i, 0);
+            t->m_internal2var.setx(i, j, 0);
+            return j;
+        }
+    };
+
+    callback i_cb;
+
+    void init_i_fixed_eh() {
+        if (!m_fixed_eh)
+            return;
+        i_fixed_eh = [this](void* ctx, user_propagator::callback* cb, unsigned id, expr* value) {
+            i_cb.t = this;
+            i_cb.cb = cb;
+            m_fixed_eh(ctx, &i_cb, m_internal2var[id], value);
+        };
+        m_ctx->user_propagate_register_fixed(i_fixed_eh);
+    }
+
+    void init_i_final_eh() {
+        if (!m_final_eh)
+            return;
+        i_final_eh = [this](void* ctx, user_propagator::callback* cb) {
+            i_cb.t = this;
+            i_cb.cb = cb;
+            m_final_eh(ctx, &i_cb);
+        };
+        m_ctx->user_propagate_register_final(i_final_eh);
+    }
+
+    void init_i_eq_eh() {
+        if (!m_eq_eh)
+            return;
+        i_eq_eh = [this](void* ctx, user_propagator::callback* cb, unsigned u, unsigned v) {
+            i_cb.t = this;
+            i_cb.cb = cb;
+            m_eq_eh(ctx, &i_cb, m_internal2var[u], m_internal2var[v]);
+        };
+        m_ctx->user_propagate_register_eq(i_eq_eh);
+    }
+
+    void init_i_diseq_eh() {
+        if (!m_diseq_eh)
+            return;
+        i_diseq_eh = [this](void* ctx, user_propagator::callback* cb, unsigned u, unsigned v) {
+            i_cb.t = this;
+            i_cb.cb = cb;
+            m_diseq_eh(ctx, &i_cb, m_internal2var[u], m_internal2var[v]);
+        };
+        m_ctx->user_propagate_register_diseq(i_diseq_eh);
+    }
+
+
+    void user_propagate_delay_init() {
+        if (!m_user_ctx)
+            return;
+        m_ctx->user_propagate_init(m_user_ctx, m_push_eh, m_pop_eh, m_fresh_eh);
+        init_i_fixed_eh();
+        init_i_final_eh();
+        init_i_eq_eh();
+        init_i_diseq_eh();
+
+        unsigned i = 0;
+        for (expr* v : m_vars) {
+            unsigned j = m_ctx->user_propagate_register(v);
+            m_var2internal.setx(i, j, 0);
+            m_internal2var.setx(j, i, 0);
+            ++i;
+        }    
+    }
+
+    void user_propagate_clear() override {
+        m_user_ctx = nullptr;
+        m_vars.reset();
+        m_fixed_eh = nullptr;
+        m_final_eh = nullptr;
+        m_eq_eh = nullptr;
+        m_diseq_eh = nullptr;
+    }
+
+    void user_propagate_init(
+        void* ctx,
+        user_propagator::push_eh_t& push_eh,
+        user_propagator::pop_eh_t& pop_eh,
+        user_propagator::fresh_eh_t& fresh_eh) override {
+        user_propagate_clear();
+        m_user_ctx = ctx;
+        m_push_eh = push_eh;
+        m_pop_eh = pop_eh;
+        m_fresh_eh = fresh_eh;
+    }
+
+    void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override {
+        m_fixed_eh = fixed_eh;
+    }
+
+    void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override {
+        m_final_eh = final_eh;
+    }
+
+    void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override {
+        m_eq_eh = eq_eh;
+    }
+
+    void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override {
+        m_diseq_eh = diseq_eh;
+    }
+
+    unsigned user_propagate_register(expr* e) override {
+        m_vars.push_back(e);
+        return m_vars.size() - 1;
+    }
 };
 
-static tactic * mk_seq_smt_tactic(params_ref const & p) {
-    return alloc(smt_tactic, p);
+static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) {
+    return alloc(smt_tactic, m, p);
 }
 
 
@@ -319,13 +476,13 @@ tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
 
 tactic * mk_smt_tactic_core(ast_manager& m, params_ref const& p, symbol const& logic) {
     parallel_params pp(p);
-    return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_seq_smt_tactic(p);
+    return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_seq_smt_tactic(m, p);
 }
 
 tactic * mk_smt_tactic_core_using(ast_manager& m, bool auto_config, params_ref const& _p) {
     parallel_params pp(_p);
     params_ref p = _p;
     p.set_bool("auto_config", auto_config);
-    return using_params(pp.enable() ? mk_parallel_smt_tactic(m, p) : mk_seq_smt_tactic(p), p);
+    return using_params(pp.enable() ? mk_parallel_smt_tactic(m, p) : mk_seq_smt_tactic(m, p), p);
 }
 

src/smt/tactic/unit_subsumption_tactic.cpp

@@ -38,6 +38,8 @@ struct unit_subsumption_tactic : public tactic {
         m_clauses(m) {
     }
 
+    char const* name() const override { return "unit_subsumption"; }
+
     void cleanup() override {}
 
     void operator()(/* in */  goal_ref const & in, 

src/smt/theory_lra.cpp

@@ -1529,7 +1529,7 @@ public:
         IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
         lbool is_sat = l_true;
         SASSERT(lp().ax_is_correct());
-        if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) {
+        if (!lp().is_feasible() || lp().has_changed_columns()) {
             is_sat = make_feasible();
         }
         final_check_status st = FC_DONE;
@@ -2084,7 +2084,7 @@ public:
         while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) {
             auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead];
             
-            m_bv_to_propagate.push_back(bv);
+            // m_bv_to_propagate.push_back(bv);
             
             api_bound* b = nullptr;
             TRACE("arith", tout << "propagate: " << literal(bv, !is_true) << "\n";
@@ -3083,21 +3083,14 @@ public:
         TRACE("pcs",  tout << lp().constraints(););
         auto status = lp().find_feasible_solution();
         TRACE("arith_verbose", display(tout););
-        switch (status) {
-        case lp::lp_status::INFEASIBLE:
-            return l_false;
-        case lp::lp_status::FEASIBLE:
-        case lp::lp_status::OPTIMAL:
-            //            SASSERT(lp().all_constraints_hold());
+        if (lp().is_feasible())
             return l_true;
-        case lp::lp_status::TIME_EXHAUSTED:
-                
-        default:
-            TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";);
+        if (status == lp::lp_status::INFEASIBLE)  
+            return l_false;
+        TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";);
             // TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED, 
-            // FLOATING_POINT_ERROR, TIME_EXAUSTED, ITERATIONS_EXHAUSTED, EMPTY, UNSTABLE
-            return l_undef;
-        }
+            // FLOATING_POINT_ERROR, TIME_EXAUSTED, EMPTY, UNSTABLE
+        return l_undef;
     }
  
     lp::explanation     m_explanation;
@@ -3467,7 +3460,7 @@ public:
             st = lp::lp_status::UNBOUNDED;
         }
         else {
-            if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) 
+            if (!lp().is_feasible() || lp().has_changed_columns())
                 make_feasible();
             
             vi = get_lpvar(v);
@@ -3477,7 +3470,10 @@ public:
                 st = lp::lp_status::FEASIBLE;
                 lp().restore_x();
             }
-                
+            if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) {
+                st = lp::lp_status::FEASIBLE;
+                lp().restore_x();
+            }                
         }
         switch (st) {
         case lp::lp_status::OPTIMAL: {

src/smt/theory_seq.cpp

@@ -2206,8 +2206,9 @@ expr_ref theory_seq::elim_skolem(expr* e) {
         if (m_sk.is_post(a, x, y) && cache.contains(x) && cache.contains(y)) {
             x = cache[x];
             y = cache[y];
+            auto mk_max = [&](expr* x, expr* y) { return m.mk_ite(m_autil.mk_ge(x, y), x, y); };
             result = m_util.str.mk_length(x);
-            result = m_util.str.mk_substr(x, y, m_autil.mk_sub(result, y));
+            result = m_util.str.mk_substr(x, mk_max(y,m_autil.mk_int(0)), m_autil.mk_sub(result, y));
             trail.push_back(result);
             cache.insert(a, result);
             todo.pop_back();            
@@ -2277,16 +2278,14 @@ expr_ref theory_seq::elim_skolem(expr* e) {
 
         args.reset();
         for (expr* arg : *to_app(a)) {
-            if (cache.find(arg, b)) {
+            if (cache.find(arg, b)) 
                 args.push_back(b);
-            }
-            else {
+            else 
                 todo.push_back(arg);
-            }
         }
-        if (args.size() < to_app(a)->get_num_args()) {
+        
+        if (args.size() < to_app(a)->get_num_args()) 
             continue;
-        }
 
         if (m_util.is_skolem(a)) {
             IF_VERBOSE(0, verbose_stream() << "unhandled skolem " << mk_pp(a, m) << "\n");
@@ -2367,11 +2366,12 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons
     if (r == l_true) {
         model_ref mdl;
         k.get_model(mdl);
+        TRACE("seq", tout << "failed to validate\n" << *mdl << "\n");
         IF_VERBOSE(0, 
                    verbose_stream() << r << "\n" << fmls << "\n";
                    verbose_stream() << *mdl.get() << "\n";
-                   k.display(verbose_stream()));
-        UNREACHABLE();
+                   k.display(verbose_stream()) << "\n");
+        //UNREACHABLE();
     }
 
 }

src/smt/theory_user_propagator.cpp

@@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation
 
 Module Name:
 
-    user_propagator.cpp
+    theory_user_propagator.cpp
 
 Abstract:
 
@@ -17,20 +17,20 @@ Author:
 
 
 #include "ast/ast_pp.h"
-#include "smt/user_propagator.h"
+#include "smt/theory_user_propagator.h"
 #include "smt/smt_context.h"
 
 using namespace smt;
 
-user_propagator::user_propagator(context& ctx):
+theory_user_propagator::theory_user_propagator(context& ctx):
     theory(ctx, ctx.get_manager().mk_family_id("user_propagator"))
 {}
 
-user_propagator::~user_propagator() {
+theory_user_propagator::~theory_user_propagator() {
     dealloc(m_api_context);
 }
 
-void user_propagator::force_push() {
+void theory_user_propagator::force_push() {
     for (; m_num_scopes > 0; --m_num_scopes) {
         theory::push_scope_eh();
         m_push_eh(m_user_context);
@@ -38,7 +38,7 @@ void user_propagator::force_push() {
     }
 }
 
-unsigned user_propagator::add_expr(expr* e) {
+unsigned theory_user_propagator::add_expr(expr* e) {
     force_push();
     enode* n = ensure_enode(e);
     if (is_attached_to_var(n))
@@ -48,17 +48,23 @@ unsigned user_propagator::add_expr(expr* e) {
     return v;
 }
 
-void user_propagator::propagate_cb(
+void theory_user_propagator::propagate_cb(
     unsigned num_fixed, unsigned const* fixed_ids, 
     unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, 
     expr* conseq) {
-    if (ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true)
+    CTRACE("user_propagate", ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true,
+           ctx.display(tout << "redundant consequence: " << mk_pp(conseq, m) << "\n"));
+    if (ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true) 
         return;
     m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m)));
 }
 
-theory * user_propagator::mk_fresh(context * new_ctx) { 
-    auto* th = alloc(user_propagator, *new_ctx); 
+unsigned theory_user_propagator::register_cb(expr* e) {
+    return add_expr(e);
+}
+
+theory * theory_user_propagator::mk_fresh(context * new_ctx) {
+    auto* th = alloc(theory_user_propagator, *new_ctx); 
     void* ctx = m_fresh_eh(m_user_context, new_ctx->get_manager(), th->m_api_context);
     th->add(ctx, m_push_eh, m_pop_eh, m_fresh_eh);
     if ((bool)m_fixed_eh) th->register_fixed(m_fixed_eh);
@@ -68,7 +74,7 @@ theory * user_propagator::mk_fresh(context * new_ctx) {
     return th;
 }
 
-final_check_status user_propagator::final_check_eh() {
+final_check_status theory_user_propagator::final_check_eh() {
     if (!(bool)m_final_eh)
         return FC_DONE;
     force_push();
@@ -79,7 +85,7 @@ final_check_status user_propagator::final_check_eh() {
     return done ? FC_DONE : FC_CONTINUE;
 }
 
-void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits) {
+void theory_user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits) {
     if (!m_fixed_eh)
         return;
     force_push();
@@ -91,11 +97,11 @@ void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits,
     m_fixed_eh(m_user_context, this, v, value);
 }
 
-void user_propagator::push_scope_eh() {
+void theory_user_propagator::push_scope_eh() {
     ++m_num_scopes;
 }
 
-void user_propagator::pop_scope_eh(unsigned num_scopes) {
+void theory_user_propagator::pop_scope_eh(unsigned num_scopes) {
     unsigned n = std::min(num_scopes, m_num_scopes);
     m_num_scopes -= n;
     num_scopes -= n;
@@ -108,11 +114,12 @@ void user_propagator::pop_scope_eh(unsigned num_scopes) {
     m_prop_lim.shrink(old_sz);
 }
 
-bool user_propagator::can_propagate() {
+bool theory_user_propagator::can_propagate() {
     return m_qhead < m_prop.size();
 }
 
-void user_propagator::propagate() {
+void theory_user_propagator::propagate() {
+    TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n");
     if (m_qhead == m_prop.size())
         return;
     force_push();
@@ -127,9 +134,10 @@ void user_propagator::propagate() {
         for (auto const& p : prop.m_eqs)
             m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second)));
         DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()););
-	DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id)););
-	DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true););
+        DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id)););
+        DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true););
 
+        TRACE("user_propagate", tout << "propagating #" << prop.m_conseq->get_id() << ": " << prop.m_conseq << "\n");
 	
         if (m.is_false(prop.m_conseq)) {
             js = ctx.mk_justification(
@@ -138,11 +146,25 @@ void user_propagator::propagate() {
             ctx.set_conflict(js);
         }
         else {
-            literal lit = mk_literal(prop.m_conseq);
-            js = ctx.mk_justification(
-                ext_theory_propagation_justification(
-                    get_id(), ctx.get_region(), m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), lit));
-            ctx.assign(lit, js);
+            for (auto& lit : m_lits)
+                lit.neg();
+            for (auto const& [a,b] : m_eqs)
+                m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
+
+            literal lit; 
+            if (has_quantifiers(prop.m_conseq)) {
+                expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m);
+                expr_ref eq(m.mk_eq(fn, prop.m_conseq), m);
+                ctx.assert_expr(eq);
+                ctx.internalize_assertions();
+                lit = mk_literal(fn);
+            }
+            else 
+                lit = mk_literal(prop.m_conseq);            
+            ctx.mark_as_relevant(lit);
+            m_lits.push_back(lit);
+            ctx.mk_th_lemma(get_id(), m_lits);
+            TRACE("user_propagate", ctx.display(tout););
         }
         ++m_stats.m_num_propagations;
         ++qhead;
@@ -151,7 +173,7 @@ void user_propagator::propagate() {
     m_qhead = qhead;
 }
 
-void user_propagator::collect_statistics(::statistics & st) const {
+void theory_user_propagator::collect_statistics(::statistics & st) const {
     st.update("user-propagations", m_stats.m_num_propagations);
     st.update("user-watched",      get_num_vars());
 }

src/smt/theory_user_propagator.h

@@ -27,7 +27,7 @@ Notes:
 #include "solver/solver.h"
 
 namespace smt {
-    class user_propagator : public theory, public solver::propagate_callback {
+    class theory_user_propagator : public theory, public user_propagator::callback {
 
         struct prop_info {
             unsigned_vector m_ids;
@@ -49,14 +49,14 @@ namespace smt {
         };
 
         void*                  m_user_context = nullptr;
-        solver::push_eh_t      m_push_eh;
-        solver::pop_eh_t       m_pop_eh;
-        solver::fresh_eh_t     m_fresh_eh;
-        solver::final_eh_t     m_final_eh;
-        solver::fixed_eh_t     m_fixed_eh;
-        solver::eq_eh_t        m_eq_eh;
-        solver::eq_eh_t        m_diseq_eh;
-        solver::context_obj*   m_api_context = nullptr;
+        user_propagator::push_eh_t      m_push_eh;
+        user_propagator::pop_eh_t       m_pop_eh;
+        user_propagator::fresh_eh_t     m_fresh_eh;
+        user_propagator::final_eh_t     m_final_eh;
+        user_propagator::fixed_eh_t     m_fixed_eh;
+        user_propagator::eq_eh_t        m_eq_eh;
+        user_propagator::eq_eh_t        m_diseq_eh;
+        user_propagator::context_obj*   m_api_context = nullptr;
         unsigned               m_qhead = 0;
         uint_set               m_fixed;
         vector<prop_info>      m_prop;
@@ -70,18 +70,18 @@ namespace smt {
         void force_push();
 
     public:
-        user_propagator(context& ctx);
+        theory_user_propagator(context& ctx);
         
-        ~user_propagator() override;
+        ~theory_user_propagator() override;
 
         /*
          * \brief initial setup for user propagator.
          */
         void add(
             void*                 ctx, 
-            solver::push_eh_t&    push_eh,
-            solver::pop_eh_t&     pop_eh,
-            solver::fresh_eh_t&   fresh_eh) {
+            user_propagator::push_eh_t&    push_eh,
+            user_propagator::pop_eh_t&     pop_eh,
+            user_propagator::fresh_eh_t&   fresh_eh) {
             m_user_context = ctx;
             m_push_eh      = push_eh;
             m_pop_eh       = pop_eh;
@@ -90,14 +90,15 @@ namespace smt {
 
         unsigned add_expr(expr* e);
 
-        void register_final(solver::final_eh_t& final_eh) { m_final_eh = final_eh; }
-        void register_fixed(solver::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; }
-        void register_eq(solver::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; }
-        void register_diseq(solver::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; }
+        void register_final(user_propagator::final_eh_t& final_eh) { m_final_eh = final_eh; }
+        void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; }
+        void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; }
+        void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; }
 
         bool has_fixed() const { return (bool)m_fixed_eh; }
 
         void propagate_cb(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* lhs, unsigned const* rhs, expr* conseq) override;
+        unsigned register_cb(expr* e) override;
 
         void new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits);