Merge remote-tracking branch 'origin/master' into poly

src/api/api_arith.cpp

@@ -123,6 +123,7 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    MK_UNARY(Z3_mk_abs, mk_c(c)->get_arith_fid(), OP_ABS, SKIP);
     MK_UNARY(Z3_mk_int2real, mk_c(c)->get_arith_fid(), OP_TO_REAL, SKIP);
     MK_UNARY(Z3_mk_real2int, mk_c(c)->get_arith_fid(), OP_TO_INT, SKIP);
     MK_UNARY(Z3_mk_is_int,   mk_c(c)->get_arith_fid(), OP_IS_INT, SKIP);

src/api/api_ast.cpp

@@ -1152,6 +1152,7 @@ extern "C" {
             case OP_REM: return Z3_OP_REM;
             case OP_MOD: return Z3_OP_MOD;
             case OP_POWER: return Z3_OP_POWER;
+            case OP_ABS: return Z3_OP_ABS;
             case OP_TO_REAL: return Z3_OP_TO_REAL;
             case OP_TO_INT: return Z3_OP_TO_INT;
             case OP_IS_INT: return Z3_OP_IS_INT;
@@ -1310,6 +1311,10 @@ extern "C" {
             case OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
             case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
             case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
+            case OP_SEQ_MAP: return Z3_OP_SEQ_MAP;
+            case OP_SEQ_MAPI: return Z3_OP_SEQ_MAPI;
+            case OP_SEQ_FOLDL: return Z3_OP_SEQ_FOLDL;
+            case OP_SEQ_FOLDLI: return Z3_OP_SEQ_FOLDLI;
 
             case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE;
             case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT;

src/api/api_context.cpp

@@ -18,6 +18,7 @@ Revision History:
 
 --*/
 #include<typeinfo>
+#include "util/debug.h"
 #include "util/z3_version.h"
 #include "api/api_context.h"
 #include "ast/ast_pp.h"
@@ -393,6 +394,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_context_rc(c);
         memory::initialize(UINT_MAX);
+        set_default_exit_action(exit_action::throw_exception);
         Z3_context r = reinterpret_cast<Z3_context>(alloc(api::context, reinterpret_cast<ast_context_params*>(c), true));
         RETURN_Z3(r);
         Z3_CATCH_RETURN_NO_HANDLE(nullptr);

src/api/api_seq.cpp

@@ -348,5 +348,10 @@ extern "C" {
     MK_UNARY(Z3_mk_char_from_bv, mk_c(c)->get_char_fid(), OP_CHAR_FROM_BV, SKIP);
     MK_UNARY(Z3_mk_char_is_digit, mk_c(c)->get_char_fid(), OP_CHAR_IS_DIGIT, SKIP);
 
+    MK_BINARY(Z3_mk_seq_map, mk_c(c)->get_seq_fid(), OP_SEQ_MAP, SKIP); 
+    MK_TERNARY(Z3_mk_seq_mapi, mk_c(c)->get_seq_fid(), OP_SEQ_MAPI, SKIP);
+    MK_TERNARY(Z3_mk_seq_foldl, mk_c(c)->get_seq_fid(), OP_SEQ_FOLDL, SKIP);
+    MK_FOURARY(Z3_mk_seq_foldli, mk_c(c)->get_seq_fid(), OP_SEQ_FOLDLI, SKIP);
+
 
 };

src/api/api_util.h

@@ -160,6 +160,23 @@ Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2) {        \
     MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE);                          \
 }
 
+#define MK_FOURARY_BODY(NAME, FID, OP, EXTRA_CODE)               \
+    Z3_TRY;                                                     \
+    RESET_ERROR_CODE();                                         \
+    EXTRA_CODE;                                                 \
+    expr * args[4] = { to_expr(n1), to_expr(n2), to_expr(n3), to_expr(n4) }; \
+    ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 4, args);       \
+    mk_c(c)->save_ast_trail(a);                                 \
+    check_sorts(c, a);                                          \
+    RETURN_Z3(of_ast(a));                                       \
+    Z3_CATCH_RETURN(0);
+
+#define MK_FOURARY(NAME, FID, OP, EXTRA_CODE)                            \
+    Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2, Z3_ast n3, Z3_ast n4) { \
+    LOG_ ## NAME(c, n1, n2, n3, n4);                                        \
+    MK_FOURARY_BODY(NAME, FID, OP, EXTRA_CODE);                          \
+}
+
 #define MK_NARY(NAME, FID, OP, EXTRA_CODE)                              \
 Z3_ast Z3_API NAME(Z3_context c, unsigned num_args, Z3_ast const* args) { \
     Z3_TRY;                                                             \

src/api/c++/z3++.h

@@ -470,6 +470,7 @@ namespace z3 {
         context * m_ctx;
     public:
         object(context & c):m_ctx(&c) {}
+        virtual ~object() = default;
         context & ctx() const { return *m_ctx; }
         Z3_error_code check_error() const { return m_ctx->check_error(); }
         friend void check_context(object const & a, object const & b);
@@ -508,7 +509,7 @@ namespace z3 {
             object::operator=(o);
             return *this;
         }
-        ~param_descrs() { Z3_param_descrs_dec_ref(ctx(), m_descrs); }
+        ~param_descrs() override { Z3_param_descrs_dec_ref(ctx(), m_descrs); }
         static param_descrs simplify_param_descrs(context& c) { return param_descrs(c, Z3_simplify_get_param_descrs(c)); }
         static param_descrs global_param_descrs(context& c) { return param_descrs(c, Z3_get_global_param_descrs(c)); }
 
@@ -526,7 +527,7 @@ namespace z3 {
     public:
         params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); }
         params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); }
-        ~params() { Z3_params_dec_ref(ctx(), m_params); }
+        ~params() override { Z3_params_dec_ref(ctx(), m_params); }
         operator Z3_params() const { return m_params; }
         params & operator=(params const & s) {
             Z3_params_inc_ref(s.ctx(), s.m_params);
@@ -554,7 +555,7 @@ namespace z3 {
         ast(context & c):object(c), m_ast(0) {}
         ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
         ast(ast const & s) :object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
-        ~ast() { if (m_ast) { Z3_dec_ref(*m_ctx, m_ast); } }
+        ~ast() override { if (m_ast) { Z3_dec_ref(*m_ctx, m_ast); } }
         operator Z3_ast() const { return m_ast; }
         operator bool() const { return m_ast != 0; }
         ast & operator=(ast const & s) {
@@ -592,7 +593,7 @@ namespace z3 {
         ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
         ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
 
-        ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); }
+        ~ast_vector_tpl() override { Z3_ast_vector_dec_ref(ctx(), m_vector); }
         operator Z3_ast_vector() const { return m_vector; }
         unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
         T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast<T>()(ctx(), r); }
@@ -2496,6 +2497,34 @@ namespace z3 {
         return expr(ctx, r);
     }
 
+    inline expr map(expr const& f, expr const& list) {
+        context& ctx = f.ctx();
+        Z3_ast r = Z3_mk_seq_map(ctx, f, list);
+        ctx.check_error();
+        return expr(ctx, r);
+    }
+
+    inline expr mapi(expr const& f, expr const& i, expr const& list) {
+        context& ctx = f.ctx();
+        Z3_ast r = Z3_mk_seq_mapi(ctx, f, i, list);
+        ctx.check_error();
+        return expr(ctx, r);
+    }
+
+    inline expr foldl(expr const& f, expr const& a, expr const& list) {
+        context& ctx = f.ctx();
+        Z3_ast r = Z3_mk_seq_foldl(ctx, f, a, list);
+        ctx.check_error();
+        return expr(ctx, r);
+    }
+
+    inline expr foldli(expr const& f, expr const& i, expr const& a, expr const& list) {
+        context& ctx = f.ctx();
+        Z3_ast r = Z3_mk_seq_foldli(ctx, f, i, a, list);
+        ctx.check_error();
+        return expr(ctx, r);
+    }
+
     inline expr mk_or(expr_vector const& args) {
         array<Z3_ast> _args(args);
         Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
@@ -2527,7 +2556,7 @@ namespace z3 {
     public:
         func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
         func_entry(func_entry const & s):object(s) { init(s.m_entry); }
-        ~func_entry() { Z3_func_entry_dec_ref(ctx(), m_entry); }
+        ~func_entry() override { Z3_func_entry_dec_ref(ctx(), m_entry); }
         operator Z3_func_entry() const { return m_entry; }
         func_entry & operator=(func_entry const & s) {
             Z3_func_entry_inc_ref(s.ctx(), s.m_entry);
@@ -2550,7 +2579,7 @@ namespace z3 {
     public:
         func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
         func_interp(func_interp const & s):object(s) { init(s.m_interp); }
-        ~func_interp() { Z3_func_interp_dec_ref(ctx(), m_interp); }
+        ~func_interp() override { Z3_func_interp_dec_ref(ctx(), m_interp); }
         operator Z3_func_interp() const { return m_interp; }
         func_interp & operator=(func_interp const & s) {
             Z3_func_interp_inc_ref(s.ctx(), s.m_interp);
@@ -2584,7 +2613,7 @@ namespace z3 {
         model(context & c, Z3_model m):object(c) { init(m); }
         model(model const & s):object(s) { init(s.m_model); }
         model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); }
-        ~model() { Z3_model_dec_ref(ctx(), m_model); }
+        ~model() override { Z3_model_dec_ref(ctx(), m_model); }
         operator Z3_model() const { return m_model; }
         model & operator=(model const & s) {
             Z3_model_inc_ref(s.ctx(), s.m_model);
@@ -2664,7 +2693,7 @@ namespace z3 {
         stats(context & c):object(c), m_stats(0) {}
         stats(context & c, Z3_stats e):object(c) { init(e); }
         stats(stats const & s):object(s) { init(s.m_stats); }
-        ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
+        ~stats() override { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); }
         operator Z3_stats() const { return m_stats; }
         stats & operator=(stats const & s) {
             Z3_stats_inc_ref(s.ctx(), s.m_stats);
@@ -2746,7 +2775,7 @@ namespace z3 {
         solver(context & c, solver const& src, translate): object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); }
         solver(solver const & s):object(s) { init(s.m_solver); }
         solver(solver const& s, simplifier const& simp);
-        ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
+        ~solver() override { Z3_solver_dec_ref(ctx(), m_solver); }
         operator Z3_solver() const { return m_solver; }
         solver & operator=(solver const & s) {
             Z3_solver_inc_ref(s.ctx(), s.m_solver);
@@ -2967,7 +2996,7 @@ namespace z3 {
         goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }
         goal(context & c, Z3_goal s):object(c) { init(s); }
         goal(goal const & s):object(s) { init(s.m_goal); }
-        ~goal() { Z3_goal_dec_ref(ctx(), m_goal); }
+        ~goal() override { Z3_goal_dec_ref(ctx(), m_goal); }
         operator Z3_goal() const { return m_goal; }
         goal & operator=(goal const & s) {
             Z3_goal_inc_ref(s.ctx(), s.m_goal);
@@ -3025,7 +3054,7 @@ namespace z3 {
     public:
         apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
         apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
-        ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
+        ~apply_result() override { Z3_apply_result_dec_ref(ctx(), m_apply_result); }
         operator Z3_apply_result() const { return m_apply_result; }
         apply_result & operator=(apply_result const & s) {
             Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result);
@@ -3050,7 +3079,7 @@ namespace z3 {
         tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); }
         tactic(context & c, Z3_tactic s):object(c) { init(s); }
         tactic(tactic const & s):object(s) { init(s.m_tactic); }
-        ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); }
+        ~tactic() override { Z3_tactic_dec_ref(ctx(), m_tactic); }
         operator Z3_tactic() const { return m_tactic; }
         tactic & operator=(tactic const & s) {
             Z3_tactic_inc_ref(s.ctx(), s.m_tactic);
@@ -3136,7 +3165,7 @@ namespace z3 {
         simplifier(context & c, char const * name):object(c) { Z3_simplifier r = Z3_mk_simplifier(c, name); check_error(); init(r); }
         simplifier(context & c, Z3_simplifier s):object(c) { init(s); }
         simplifier(simplifier const & s):object(s) { init(s.m_simplifier); }
-        ~simplifier() { Z3_simplifier_dec_ref(ctx(), m_simplifier); }
+        ~simplifier() override { Z3_simplifier_dec_ref(ctx(), m_simplifier); }
         operator Z3_simplifier() const { return m_simplifier; }
         simplifier & operator=(simplifier const & s) {
             Z3_simplifier_inc_ref(s.ctx(), s.m_simplifier);
@@ -3178,7 +3207,7 @@ namespace z3 {
         probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); }
         probe(context & c, Z3_probe s):object(c) { init(s); }
         probe(probe const & s):object(s) { init(s.m_probe); }
-        ~probe() { Z3_probe_dec_ref(ctx(), m_probe); }
+        ~probe() override { Z3_probe_dec_ref(ctx(), m_probe); }
         operator Z3_probe() const { return m_probe; }
         probe & operator=(probe const & s) {
             Z3_probe_inc_ref(s.ctx(), s.m_probe);
@@ -3272,7 +3301,7 @@ namespace z3 {
             object::operator=(o);
             return *this;
         }
-        ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); }
+        ~optimize() override { Z3_optimize_dec_ref(ctx(), m_opt); }
         operator Z3_optimize() const { return m_opt; }
         void add(expr const& e) {
             assert(e.is_bool());
@@ -3353,7 +3382,7 @@ namespace z3 {
     public:
         fixedpoint(context& c):object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); }
         fixedpoint(fixedpoint const & o):object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); }
-        ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); }
+        ~fixedpoint() override { Z3_fixedpoint_dec_ref(ctx(), m_fp); }
         fixedpoint & operator=(fixedpoint const & o) {
             Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp);
             Z3_fixedpoint_dec_ref(ctx(), m_fp);

src/api/python/z3/z3.py

@@ -11210,6 +11210,32 @@ def Length(s):
     s = _coerce_seq(s)
     return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
 
+def SeqMap(f, s):
+    """Map function 'f' over sequence 's'"""
+    ctx = _get_ctx2(f, s)
+    s = _coerce_seq(s, ctx)
+    return _to_expr_ref(Z3_mk_seq_map(s.ctx_ref(), f.as_ast(), s.as_ast()), ctx)
+
+def SeqMapI(f, i, s):
+    """Map function 'f' over sequence 's' at index 'i'"""
+    ctx = _get_ctx(f, s)
+    s = _coerce_seq(s, ctx)
+    if not is_expr(i):
+        i = _py2expr(i)
+    return _to_expr_ref(Z3_mk_seq_mapi(s.ctx_ref(), f.as_ast(), i.as_ast(), s.as_ast()), ctx)
+
+def SeqFoldLeft(f, a, s):
+    ctx = _get_ctx2(f, s)
+    s = _coerce_seq(s, ctx)
+    a = _py2expr(a)
+    return _to_expr_ref(Z3_mk_seq_foldl(s.ctx_ref(), f.as_ast(), a.as_ast(), s.as_ast()), ctx)
+
+def SeqFoldLeftI(f, i, a, s):
+    ctx = _get_ctx2(f, s)
+    s = _coerce_seq(s, ctx)
+    a = _py2expr(a)
+    i = _py2epxr(i)
+    return _to_expr_ref(Z3_mk_seq_foldli(s.ctx_ref(), f.as_ast(), i.as_ast(), a.as_ast(), s.as_ast()), ctx)
 
 def StrToInt(s):
     """Convert string expression to integer

src/api/z3_api.h

@@ -1023,6 +1023,7 @@ typedef enum {
     Z3_OP_TO_INT,
     Z3_OP_IS_INT,
     Z3_OP_POWER,
+    Z3_OP_ABS,
 
     // Arrays & Sets
     Z3_OP_STORE = 0x300,
@@ -1193,6 +1194,10 @@ typedef enum {
     Z3_OP_SEQ_LAST_INDEX,
     Z3_OP_SEQ_TO_RE,
     Z3_OP_SEQ_IN_RE,
+    Z3_OP_SEQ_MAP,            
+    Z3_OP_SEQ_MAPI,           
+    Z3_OP_SEQ_FOLDL,          
+    Z3_OP_SEQ_FOLDLI,         
 
     // strings
     Z3_OP_STR_TO_INT,
@@ -2544,6 +2549,13 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2);
 
+    /**
+       \brief Take the absolute value of an integer
+
+       def_API('Z3_mk_abs', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_abs(Z3_context c, Z3_ast arg);
+    
     /**
         \brief Create less than.
 
@@ -3798,6 +3810,30 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr);
 
+    /**
+      \brief Create a map of the function \c f over the sequence \c s.
+      def_API('Z3_mk_seq_map', AST ,(_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_seq_map(Z3_context c, Z3_ast f, Z3_ast s);
+
+    /**
+     \brief Create a map of the function \c f over the sequence \c s starting at index \c i.
+     def_API('Z3_mk_seq_mapi', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_seq_mapi(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast s);
+
+    /**
+      \brief Create a fold of the function \c f over the sequence \c s with accumulator a.
+      def_API('Z3_mk_seq_foldl', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_seq_foldl(Z3_context c, Z3_ast f, Z3_ast a, Z3_ast s);
+
+    /**
+       \brief Create a fold with index tracking of the function \c f over the sequence \c s with accumulator \c a starting at index \c i.
+       def_API('Z3_mk_seq_foldli', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_seq_foldli(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast a, Z3_ast s);
+
     /**
        \brief Convert string to integer.
 

src/ast/bv_decl_plugin.h

@@ -438,6 +438,7 @@ public:
     MATCH_BINARY(is_bv_xor);
     MATCH_BINARY(is_bv_nand);
     MATCH_BINARY(is_bv_nor);
+    MATCH_BINARY(is_concat);
 
 
     MATCH_BINARY(is_bv_uremi);

src/ast/rewriter/th_rewriter.cpp

@@ -17,6 +17,7 @@ Notes:
 
 --*/
 #include "params/rewriter_params.hpp"
+#include "params/poly_rewriter_params.hpp"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/bool_rewriter.h"
 #include "ast/rewriter/arith_rewriter.h"
@@ -83,7 +84,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
 
     void updt_local_params(params_ref const & _p) {
         rewriter_params p(_p);
-        m_flat           = true;
+        poly_rewriter_params pp(_p);
+        m_flat           = pp.flat();
         m_max_memory     = megabytes_to_bytes(p.max_memory());
         m_max_steps      = p.max_steps();
         m_pull_cheap_ite = p.pull_cheap_ite();

src/ast/simplifiers/bound_simplifier.cpp

@@ -288,7 +288,8 @@ void bound_simplifier::tighten_bound(dependent_expr const& de) {
 
 void bound_simplifier::assert_upper(expr* x, rational const& n, bool strict) {
     scoped_mpq c(nm);
-    nm.set(c, n.to_mpq());    
+    nm.set(c, n.to_mpq());
+    TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " < " : " <= ") << n << "\n");
     bp.assert_upper(to_var(x), c, strict);
 }
 
@@ -296,6 +297,7 @@ void bound_simplifier::assert_upper(expr* x, rational const& n, bool strict) {
 void bound_simplifier::assert_lower(expr* x, rational const& n, bool strict) {
     scoped_mpq c(nm);
     nm.set(c, n.to_mpq());
+    TRACE("propagate-ineqs", tout <<  to_var(x) << ": " << mk_pp(x, m) << (strict ? " > " : " >= ") << n << "\n");
     bp.assert_lower(to_var(x), c, strict);
 }
 
@@ -306,6 +308,7 @@ bool bound_simplifier::has_lower(expr* x, rational& n, bool& strict) {
         return false;
     strict = m_interval.lower_is_open(i);
     n = m_interval.lower(i);
+    TRACE("propagate-ineqs", tout <<  to_var(x) << ": " << mk_pp(x, m) << (strict ? " > " : " >= ") << n << "\n");
     return true;
 }
 
@@ -316,6 +319,7 @@ bool bound_simplifier::has_upper(expr* x, rational& n, bool& strict) {
         return false;
     strict = m_interval.upper_is_open(i);
     n = m_interval.upper(i);
+    TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " < " : " <= ") << n << "\n");
     return true;  
 }
 

src/ast/simplifiers/extract_eqs.h

@@ -31,8 +31,9 @@ namespace euf {
         expr* orig;       // original expression that encoded equation
         app* var;         // isolated variable
         expr_ref term;    // defined term
-        expr_dependency* dep;
-        dependent_eq(expr* orig, app* var, expr_ref const& term, expr_dependency* d) : orig(orig), var(var), term(term), dep(d) {}
+        expr_dependency_ref dep;
+        dependent_eq(expr* orig, app* var, expr_ref const& term, expr_dependency* d) : 
+            orig(orig), var(var), term(term), dep(d, term.get_manager()) {}
     };
 
     typedef vector<dependent_eq> dep_eq_vector;

src/ast/simplifiers/solve_eqs.cpp

@@ -329,6 +329,7 @@ namespace euf {
         m_config.m_context_solve = p.get_bool("context_solve", tp.solve_eqs_context_solve());
         for (auto* ex : m_extract_plugins)
             ex->updt_params(p);
+        m_rewriter.updt_params(p);
     }
 
     void solve_eqs::collect_param_descrs(param_descrs& r) {

src/ast/sls/bv_sls.cpp

@@ -25,12 +25,15 @@ Author:
 
 namespace bv {
 
-    sls::sls(ast_manager& m): 
+    sls::sls(ast_manager& m, params_ref const& p): 
         m(m), 
         bv(m),
         m_terms(m),
-        m_eval(m)
-    {}
+        m_eval(m),
+        m_engine(m, p)
+    {
+        updt_params(p);
+    }
 
     void sls::init() {
         m_terms.init(); 
@@ -53,38 +56,96 @@ namespace bv {
             }
         }
         for (auto* t : m_terms.terms()) {
-            if (t && !re_eval_is_correct(t)) 
+            if (t && !m_eval.re_eval_is_correct(t)) 
                 m_repair_roots.insert(t->get_id());            
         }
     }
 
+
+    void sls::set_model() {
+        if (!m_set_model)
+            return;
+        if (m_repair_roots.size() >= m_min_repair_size)
+            return;
+        m_min_repair_size = m_repair_roots.size();
+        IF_VERBOSE(2, verbose_stream() << "(sls-update-model :num-unsat " << m_min_repair_size << ")\n");
+        m_set_model(*get_model());
+    }
+
     void sls::init_repair_goal(app* t) {
-        if (m.is_bool(t)) 
-            m_eval.set(t, m_eval.bval1(t));        
-        else if (bv.is_bv(t)) {
-            auto& v = m_eval.wval(t);
-            v.bits().copy_to(v.nw, v.eval);
+        m_eval.init_eval(t);
+    }
+
+    void sls::init_repair_candidates() {
+        m_to_repair.reset();
+        ptr_vector<expr> todo;
+        expr_fast_mark1 mark;
+        for (auto index : m_repair_roots) 
+            todo.push_back(m_terms.term(index));
+        for (unsigned i = 0; i < todo.size(); ++i) {
+            expr* e = todo[i];
+            if (mark.is_marked(e))
+                continue;
+            mark.mark(e);
+            if (!is_app(e))
+                continue;
+            for (expr* arg : *to_app(e))
+                todo.push_back(arg);
+
+            if (is_uninterp_const(e))
+                m_to_repair.insert(e->get_id());
+
         }
     }
 
+
     void sls::reinit_eval() {
+        init_repair_candidates();
+
+        if (m_to_repair.empty())
+            return;
+
+        // refresh the best model so far to a callback
+        set_model();
+
+        // add fresh units, if any
+        bool new_assertion = false;
+        while (m_get_unit) {
+            auto e = m_get_unit();
+            if (!e)
+                break;
+            new_assertion = true;
+            assert_expr(e);
+        }
+        if (new_assertion) 
+            init();        
+           
         std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned i) {
-            auto should_keep = [&]() {
-                return m_rand() % 100 <= 92;
-            };
+            unsigned id = e->get_id();
+            bool keep = !m_to_repair.contains(id);
             if (m.is_bool(e)) {
-                if (m_eval.is_fixed0(e) || should_keep())
+                if (m_eval.is_fixed0(e) || keep)
                     return m_eval.bval0(e);
+                if (m_engine_init) {
+                    auto const& z = m_engine.get_value(e);
+                    return rational(z).get_bit(0);
+                }
             }
             else if (bv.is_bv(e)) {
                 auto& w = m_eval.wval(e);
-                if (w.fixed.get(i) || should_keep())
-                    return w.get_bit(i);                
+                if (w.fixed.get(i) || keep)
+                    return w.get_bit(i);
+                if (m_engine_init) {
+                    auto const& z = m_engine.get_value(e);
+                    return rational(z).get_bit(i);
+                }
             }
+            
             return m_rand() % 2 == 0;
         };
         m_eval.init_eval(m_terms.assertions(), eval);
         init_repair();
+        // m_engine_init = false;
     }
 
     std::pair<bool, app*> sls::next_to_repair() {
@@ -109,7 +170,7 @@ namespace bv {
                 SASSERT(m_eval.bval0(e));
                 return { true, e };
             }
-            if (!re_eval_is_correct(e)) {
+            if (!m_eval.re_eval_is_correct(e)) {
                 init_repair_goal(e);
                 return { true, e };
             }
@@ -119,37 +180,54 @@ namespace bv {
         return { false, nullptr };
     }
 
-    lbool sls::search() {
+    lbool sls::search1() {
         // init and init_eval were invoked
         unsigned n = 0;
-        for (; n++ < m_config.m_max_repairs && m.inc(); ) {
+        for (; n < m_config.m_max_repairs && m.inc(); ++n) {
             auto [down, e] = next_to_repair();
             if (!e)
                 return l_true;
 
-
-            trace_repair(down, e);
-
+            IF_VERBOSE(20, trace_repair(down, e));
+            
             ++m_stats.m_moves;
-
             if (down) 
-                try_repair_down(e);
+                try_repair_down(e);            
             else
                 try_repair_up(e);            
         }
         return l_undef;
     }
 
+    lbool sls::search2() {
+        lbool res = l_undef;
+        if (m_stats.m_restarts == 0)
+            res = m_engine(),
+            m_engine_init = true;
+        else if (m_stats.m_restarts % 1000 == 0)
+            res = m_engine.search_loop(),
+            m_engine_init = true;
+        if (res != l_undef) 
+            m_engine_model = true;   
+        return res;
+    }
+
 
     lbool sls::operator()() {
         lbool res = l_undef;
         m_stats.reset();
         m_stats.m_restarts = 0;
+        m_engine_model = false;
+        m_engine_init = false;
+
         do {
-            res = search();
+            res = search1();
             if (res != l_undef)
                 break;
             trace();
+            //res = search2();
+            if (res != l_undef)
+                break;
             reinit_eval();
         } 
         while (m.inc() && m_stats.m_restarts++ < m_config.m_max_restarts);
@@ -158,93 +236,84 @@ namespace bv {
     }
 
     void sls::try_repair_down(app* e) {
-
         unsigned n = e->get_num_args();
         if (n == 0) {
-            if (m.is_bool(e)) 
-                m_eval.set(e, m_eval.bval1(e));                            
-            else 
-                VERIFY(m_eval.wval(e).commit_eval());
-            
+            m_eval.commit_eval(e);           
             for (auto p : m_terms.parents(e))
                 m_repair_up.insert(p->get_id());
+            
             return;
         }        
 
-        unsigned s = m_rand(n);
-        for (unsigned i = 0; i < n; ++i) {
-            auto j = (i + s) % n;
-            if (m_eval.try_repair(e, j)) {
-                set_repair_down(e->get_arg(j));
+        if (n == 2) {
+            auto d1 = get_depth(e->get_arg(0));
+            auto d2 = get_depth(e->get_arg(1));
+            unsigned s = m_rand(d1 + d2 + 2);
+            if (s <= d1 && m_eval.try_repair(e, 0)) {
+                set_repair_down(e->get_arg(0));
+                return;
+            }
+            if (m_eval.try_repair(e, 1)) {
+                set_repair_down(e->get_arg(1));
+                return;
+            }
+            if (m_eval.try_repair(e, 0)) {
+                set_repair_down(e->get_arg(0));
                 return;
             }
         }
-        // search a new root / random walk to repair        
+        else {
+            unsigned s = m_rand(n);
+            for (unsigned i = 0; i < n; ++i) {
+                auto j = (i + s) % n;
+                if (m_eval.try_repair(e, j)) {
+                    set_repair_down(e->get_arg(j));
+                    return;
+                }
+            }
+        }
+        IF_VERBOSE(3, verbose_stream() << "init-repair " << mk_bounded_pp(e, m) << "\n");
+        // repair was not successful, so reset the state to find a different way to repair
+        init_repair();
     }
 
     void sls::try_repair_up(app* e) {       
         
-        if (m_terms.is_assertion(e) || !m_eval.repair_up(e)) 
-            m_repair_roots.insert(e->get_id());        
+        if (m_terms.is_assertion(e)) 
+            m_repair_roots.insert(e->get_id());    
+        else if (!m_eval.repair_up(e)) {
+            IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e));
+            if (m_rand(10) != 0) {
+                m_eval.set_random(e);                
+                m_repair_roots.insert(e->get_id());
+            }
+            else
+                init_repair();
+        }
         else {
-            if (!eval_is_correct(e)) {
+            if (!m_eval.eval_is_correct(e)) {
                 verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
             }
-            SASSERT(eval_is_correct(e));
+            SASSERT(m_eval.eval_is_correct(e));
             for (auto p : m_terms.parents(e))
                 m_repair_up.insert(p->get_id());
         }
     }
 
-    bool sls::eval_is_correct(app* e) {
-        if (!m_eval.can_eval1(e))
-            return false;
-        if (m.is_bool(e))
-            return m_eval.bval0(e) == m_eval.bval1(e);
-        if (bv.is_bv(e)) {
-            auto const& v = m_eval.wval(e);
-            return v.eval == v.bits();
-        }
-        UNREACHABLE();
-        return false;
-    }
-
-
-    bool sls::re_eval_is_correct(app* e) {
-        if (!m_eval.can_eval1(e))
-            return false;
-        if (m.is_bool(e))
-            return m_eval.bval0(e) == m_eval.bval1(e);
-        if (bv.is_bv(e)) {
-            auto const& v = m_eval.eval(e);
-            return v.eval == v.bits();
-        }
-        UNREACHABLE();
-        return false;
-    }
 
     model_ref sls::get_model() {
-        model_ref mdl = alloc(model, m);
+        if (m_engine_model)
+            return m_engine.get_model();
+
+        model_ref mdl = alloc(model, m);         
         auto& terms = m_eval.sort_assertions(m_terms.assertions());
         for (expr* e : terms) {
-            if (!re_eval_is_correct(to_app(e))) {
-                verbose_stream() << "missed evaluation #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
-                if (bv.is_bv(e)) {
-                    auto const& v = m_eval.wval(e);
-                    verbose_stream() << v << "\n" << v.eval << "\n";
-                }
-            }
             if (!is_uninterp_const(e))
                 continue;
-
             auto f = to_app(e)->get_decl();
-            if (m.is_bool(e))
-                mdl->register_decl(f, m.mk_bool_val(m_eval.bval0(e)));
-            else if (bv.is_bv(e)) {
-                auto const& v = m_eval.wval(e);
-                rational n = v.get_value();
-                mdl->register_decl(f, bv.mk_numeral(n, v.bw));
-            }
+            auto v = m_eval.get_value(to_app(e));
+            if (v)
+                mdl->register_decl(f, v);
         }
         terms.reset();
         return mdl;
@@ -260,10 +329,7 @@ namespace bv {
                 out << "u ";
             if (m_repair_roots.contains(e->get_id()))
                 out << "r ";
-            if (bv.is_bv(e))
-                out << m_eval.wval(e);
-            else if (m.is_bool(e))
-                out << (m_eval.bval0(e)?"T":"F");
+            m_eval.display_value(out, e);
             out << "\n";
         }
         terms.reset();
@@ -273,17 +339,20 @@ namespace bv {
     void sls::updt_params(params_ref const& _p) {
         sls_params p(_p);
         m_config.m_max_restarts = p.max_restarts();
+        m_config.m_max_repairs = p.max_repairs();
         m_rand.set_seed(p.random_seed());
+        m_terms.updt_params(_p);
+        params_ref q = _p;
+        q.set_uint("max_restarts", 10);
+        m_engine.updt_params(q);
     }
 
-    void sls::trace_repair(bool down, expr* e) {
-        IF_VERBOSE(20,
-            verbose_stream() << (down ? "d #" : "u #")
+    std::ostream& sls::trace_repair(bool down, expr* e) {
+        verbose_stream() << (down ? "d #" : "u #")
             << e->get_id() << ": "
             << mk_bounded_pp(e, m, 1) << " ";
-        if (bv.is_bv(e)) verbose_stream() << m_eval.wval(e) << " " << (m_eval.is_fixed0(e) ? "fixed " : " ");
-        if (m.is_bool(e)) verbose_stream() << m_eval.bval0(e) << " ";
-        verbose_stream() << "\n");
+        m_eval.display_value(verbose_stream(), e) << "\n";
+        return verbose_stream();
     }
 
     void sls::trace() {

src/ast/sls/bv_sls.h

@@ -26,6 +26,7 @@ Author:
 #include "ast/sls/sls_valuation.h"
 #include "ast/sls/bv_sls_terms.h"
 #include "ast/sls/bv_sls_eval.h"
+#include "ast/sls/sls_engine.h"
 #include "ast/bv_decl_plugin.h"
 #include "model/model.h"
 
@@ -49,33 +50,41 @@ namespace bv {
         ptr_vector<expr>    m_todo;
         random_gen          m_rand;
         config              m_config;
+        sls_engine          m_engine;
+        bool                m_engine_model = false;
+        bool                m_engine_init = false;
+        std::function<expr_ref()> m_get_unit;
+        std::function<void(model& mdl)> m_set_model;
+        unsigned            m_min_repair_size = UINT_MAX;
         
         std::pair<bool, app*> next_to_repair();
         
-        bool eval_is_correct(app* e);
-        bool re_eval_is_correct(app* e);
         void init_repair_goal(app* e);
+        void set_model();
         void try_repair_down(app* e);
         void try_repair_up(app* e);
         void set_repair_down(expr* e) { m_repair_down = e->get_id(); }
 
-        lbool search();
+        lbool search1();
+        lbool search2();
         void reinit_eval();
         void init_repair();
         void trace();
-        void trace_repair(bool down, expr* e);
+        std::ostream& trace_repair(bool down, expr* e);
+
+        indexed_uint_set m_to_repair;
+        void init_repair_candidates();
 
     public:
-        sls(ast_manager& m);
+        sls(ast_manager& m, params_ref const& p);
                 
         /**
         * Add constraints
         */
-        void assert_expr(expr* e) { m_terms.assert_expr(e); }
+        void assert_expr(expr* e) { m_terms.assert_expr(e); m_engine.assert_expr(e); }
 
         /*
         * Invoke init after all expressions are asserted. 
-        * No other expressions can be asserted after init.
         */
         void init();
 
@@ -85,16 +94,26 @@ namespace bv {
         */
         void init_eval(std::function<bool(expr*, unsigned)>& eval);
 
+        /**
+        * add callback to retrieve new units
+        */
+        void init_unit(std::function<expr_ref()> get_unit) { m_get_unit = get_unit; }
+
+        /**
+        * Add callback to set model
+        */
+        void set_model(std::function<void(model& mdl)> f) { m_set_model = f; }
+
         /**
         * Run (bounded) local search to find feasible assignments.
         */
         lbool operator()();
 
         void updt_params(params_ref const& p);
-        void collect_statistics(statistics & st) const { m_stats.collect_statistics(st); }
-        void reset_statistics() { m_stats.reset(); }
+        void collect_statistics(statistics& st) const { m_stats.collect_statistics(st); m_engine.collect_statistics(st); }
+        void reset_statistics() { m_stats.reset(); m_engine.reset_statistics(); }
 
-        sls_stats const& get_stats() const { return m_stats; }
+        unsigned get_num_moves() { return m_stats.m_moves + m_engine.get_stats().m_moves; }
 
         std::ostream& display(std::ostream& out);
 

src/ast/sls/bv_sls_eval.cpp

@@ -24,8 +24,8 @@ namespace bv {
     {}   
 
     void sls_eval::init_eval(expr_ref_vector const& es, std::function<bool(expr*, unsigned)> const& eval) {
-        sort_assertions(es);
-        for (expr* e : m_todo) {
+        auto& terms = sort_assertions(es);
+        for (expr* e : terms) {
             if (!is_app(e))
                 continue;
             app* a = to_app(e);
@@ -49,7 +49,7 @@ namespace bv {
                 TRACE("sls", tout << "Unhandled expression " << mk_pp(e, m) << "\n");
             }
         }
-        m_todo.reset();
+        terms.reset();
     }
 
     /**
@@ -84,10 +84,13 @@ namespace bv {
             return false;
         auto v = alloc_valuation(e);
         m_values.set(e->get_id(), v);
-        if (bv.is_sign_ext(e)) {
-            unsigned p = e->get_parameter(0).get_int();
-            v->set_signed(p);
-        }
+        expr* x, * y;
+        rational val;
+        if (bv.is_sign_ext(e))          
+            v->set_signed(e->get_parameter(0).get_int());        
+        else if (bv.is_bv_ashr(e, x, y) && bv.is_numeral(y, val) && 
+            val.is_unsigned() && val.get_unsigned() <= bv.get_bv_size(e)) 
+            v->set_signed(val.get_unsigned());        
         return true;
     }
 
@@ -911,26 +914,25 @@ namespace bv {
 
     bool sls_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
         if (is_true) {
-            if (m_rand() % 20 != 0) 
+            if (m_rand(20) != 0) 
                 if (a.try_set(b.bits()))
                     return true;
             
-            a.get_variant(m_tmp, m_rand);
-            return a.set_repair(random_bool(), m_tmp);
+            return a.set_random(m_rand);
         }
         else {
-            bool try_above = m_rand() % 2 == 0;
+            bool try_above = m_rand(2) == 0;
             if (try_above) {
                 a.set_add(m_tmp, b.bits(), m_one);
-                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand))
+                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp,  m_rand))
                     return true;
             }
             a.set_sub(m_tmp, b.bits(), m_one);
-            if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_tmp2, m_rand))
+            if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_rand))
                 return true;
             if (!try_above) {
                 a.set_add(m_tmp, b.bits(), m_one);
-                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand))
+                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_rand))
                     return true;
             }
             return false;
@@ -1005,7 +1007,6 @@ namespace bv {
     bool sls_eval::try_repair_bxor(bvect const& e, bvval& a, bvval const& b) {
         for (unsigned i = 0; i < a.nw; ++i)
             m_tmp[i] = e[i] ^ b.bits()[i];
-        a.clear_overflow_bits(m_tmp);
         return a.set_repair(random_bool(), m_tmp);
     }
 
@@ -1015,17 +1016,16 @@ namespace bv {
     // If this fails, set a to a random value
     // 
     bool sls_eval::try_repair_add(bvect const& e, bvval& a, bvval const& b) {
-        if (m_rand() % 20 != 0) {
+        if (m_rand(20) != 0) {
             a.set_sub(m_tmp, e, b.bits());
             if (a.try_set(m_tmp))
                 return true;
         }
-        a.get_variant(m_tmp, m_rand);
-        return a.set_repair(random_bool(), m_tmp);          
+        return a.set_random(m_rand);        
     }
 
     bool sls_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) {
-        if (m_rand() % 20 != 0) {
+        if (m_rand(20) != 0) {
             if (i == 0) 
                 // e = a - b -> a := e + b
                 a.set_add(m_tmp, e, b.bits());        
@@ -1036,8 +1036,7 @@ namespace bv {
                 return true;
         }
         // fall back to a random value
-        a.get_variant(m_tmp, m_rand);
-        return a.set_repair(random_bool(), m_tmp);
+        return a.set_random(m_rand);        
     }
 
     /**
@@ -1055,15 +1054,11 @@ namespace bv {
             return a.set_repair(random_bool(), m_tmp);
         }
 
-        if (b.is_zero()) {
-            a.get_variant(m_tmp, m_rand);
-            return a.set_repair(random_bool(), m_tmp);            
-        }      
-
-        if (m_rand() % 20 == 0) {
-            a.get_variant(m_tmp, m_rand);
-            return a.set_repair(random_bool(), m_tmp);            
-        }
+        if (b.is_zero()) 
+            return a.set_random(m_rand);          
+        
+        if (m_rand(20) == 0) 
+            return a.set_random(m_rand);
 
 #if 0
         verbose_stream() << "solve for " << e << "\n";
@@ -1093,7 +1088,7 @@ namespace bv {
             b.shift_right(y, parity_b);
 #if 0
             for (unsigned i = parity_b; i < b.bw; ++i)
-                y.set(i, m_rand() % 2 == 0);
+                y.set(i, m_rand(2) == 0);
 #endif
         }
 
@@ -1148,13 +1143,12 @@ namespace bv {
         if (a.set_repair(random_bool(), m_tmp))
             return true;
 
-        a.get_variant(m_tmp, m_rand);
-        return a.set_repair(random_bool(), m_tmp);
+        return a.set_random(m_rand);
     }
 
     bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) {
         for (unsigned i = 0; i < a.nw; ++i)
-            m_tmp[i] = ~e[i];
+            m_tmp[i] = ~e[i];        
         a.clear_overflow_bits(m_tmp);
         return a.try_set(m_tmp);
     }
@@ -1233,16 +1227,16 @@ namespace bv {
     bool sls_eval::try_repair_sle(bvval& a, bvect const& b, bvect const& p2) {
         bool r = false;
         if (b < p2) {
-            bool coin = m_rand() % 2 == 0;
+            bool coin = m_rand(2) == 0;
             if (coin)
-                r = a.set_random_at_least(p2, m_tmp3, m_rand);
+                r = a.set_random_at_least(p2, m_rand);
             if (!r)
-                r = a.set_random_at_most(b, m_tmp3, m_rand);
+                r = a.set_random_at_most(b, m_rand);
             if (!coin && !r)
-                r = a.set_random_at_least(p2, m_tmp3, m_rand);
+                r = a.set_random_at_least(p2, m_rand);
         }
         else 
-            r = a.set_random_in_range(p2, b, m_tmp3, m_rand);
+            r = a.set_random_in_range(p2, b, m_rand);
         return r;
     }
 
@@ -1262,16 +1256,16 @@ namespace bv {
         bool r = false;
         if (p2 < b) 
             // random b <= x < p2 
-            r = a.set_random_in_range(b, p2_1, m_tmp3, m_rand);        
+            r = a.set_random_in_range(b, p2_1, m_rand);        
         else {
             // random b <= x or x < p2
-            bool coin = m_rand() % 2 == 0;
+            bool coin = m_rand(2) == 0;
             if (coin)
-                r = a.set_random_at_most(p2_1, m_tmp3, m_rand);
+                r = a.set_random_at_most(p2_1,m_rand);
             if (!r)
-                r = a.set_random_at_least(b, m_tmp3, m_rand);
+                r = a.set_random_at_least(b,  m_rand);
             if (!r && !coin)
-                r = a.set_random_at_most(p2_1, m_tmp3, m_rand);
+                r = a.set_random_at_most(p2_1,  m_rand);
         }
         p2_1.set_bw(0);
         return r;
@@ -1287,28 +1281,28 @@ namespace bv {
     bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
         if (e) {
             // a <= t
-            return a.set_random_at_most(b.bits(), m_tmp, m_rand);
+            return a.set_random_at_most(b.bits(),  m_rand);
         }
         else {
             // a > t
             a.set_add(m_tmp, b.bits(), m_one);
             if (a.is_zero(m_tmp))
                 return false;   
-            return a.set_random_at_least(m_tmp, m_tmp2, m_rand);
+            return a.set_random_at_least(m_tmp, m_rand);
         }           
     }
 
     bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
         if (e) {
             // a >= t
-            return a.set_random_at_least(b.bits(), m_tmp, m_rand);
+            return a.set_random_at_least(b.bits(), m_rand);
         }
         else {
             // a < t
             if (b.is_zero())
                 return false;
             a.set_sub(m_tmp, b.bits(), m_one);
-            return a.set_random_at_most(m_tmp, m_tmp2, m_rand);
+            return a.set_random_at_most(m_tmp, m_rand);
         }    
     }
 
@@ -1348,41 +1342,261 @@ namespace bv {
         return false;
     }
 
-    bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) {
-        if (i == 0) {
-            unsigned sh = b.to_nat(b.bw);
-            if (sh == 0)
-                return a.try_set(e);
-            else if (sh >= b.bw) {
-                if (e.get(a.bw - 1)) 
-                    return a.try_set_bit(a.bw - 1, true);                
-                else 
-                    return a.try_set_bit(a.bw - 1, false);
-            }
-            else {
-                // e = a >> sh
-                // a[bw-1:sh] = e[bw-sh-1:0]
-                // a[sh-1:0] = a[sh-1:0]                
-                // ignore sign
-                for (unsigned i = sh; i < a.bw; ++i)
-                    m_tmp.set(i, e.get(i - sh));
-                for (unsigned i = 0; i < sh; ++i)
-                    m_tmp.set(i, a.get_bit(i));
-                a.clear_overflow_bits(m_tmp);
-                return a.try_set(m_tmp);
-            }
-        }
-        else {
-            // NB. blind sub-range of possible values for b
-            SASSERT(i == 1);
-            unsigned sh = m_rand(a.bw + 1);
-            b.set(m_tmp, sh);
-            return b.try_set(m_tmp);
-        }
+    bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) {       
+            if (i == 0)
+                return try_repair_ashr0(e, a, b);
+            else
+                return try_repair_ashr1(e, a, b);
     }
 
     bool sls_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) {
-        return try_repair_ashr(e, a, b, i);
+        if (i == 0)
+            return try_repair_lshr0(e, a, b);
+        else
+            return try_repair_lshr1(e, a, b);
+    }
+
+    /**
+    * strong: 
+    * - e = (e << b) >> b -> a := e << b, upper b bits set random
+    * weak:
+    *   - e = 0 -> a := random 
+    *   - e > 0 -> a := random with msb(a) >= msb(e)
+    */
+    bool sls_eval::try_repair_lshr0(bvect const& e, bvval& a, bvval const& b) {
+        
+        auto& t = m_tmp;
+        // t := e << b
+        // t := t >> b
+        t.set_shift_left(e, b.bits());
+        t.set_shift_right(t, b.bits());
+        bool use_strong = m_rand(10) != 0;
+        if (t == e && use_strong) {
+            t.set_shift_left(e, b.bits());
+            unsigned n = b.bits().to_nat(e.bw);
+            for (unsigned i = e.bw; i-- > e.bw - n;) 
+                t.set(i, a.get_bit(i)); 
+            if (a.set_repair(random_bool(), t))
+                return true;                      
+        }
+
+
+        unsigned sh = b.to_nat(b.bw);
+        if (m_rand(20) != 0) {
+            if (sh == 0 && a.try_set(e))
+                return true;
+            else if (sh >= b.bw)
+                return true;
+            else if (sh < b.bw && m_rand(20) != 0) {
+                // e = a >> sh
+                // a[bw-1:sh] = e[bw-sh-1:0]
+                // a[sh-1:0] = a[sh-1:0]                
+                for (unsigned i = sh; i < a.bw; ++i)
+                    t.set(i, e.get(i - sh));
+                for (unsigned i = 0; i < sh; ++i)
+                    t.set(i, a.get_bit(i));
+                a.clear_overflow_bits(t);
+                if (a.try_set(t))
+                    return true;
+            }
+        }
+        
+        //bool r = try_repair_ashr(e, a, const_cast<bvval&>(b), 0);
+        //verbose_stream() << "repair lshr0 " << e << " b: " << b << " a: " << a << "\n";
+        //return r;
+
+        a.get_variant(t, m_rand);
+        
+        unsigned msb = a.msb(e);
+        if (msb > a.msb(t)) {
+            unsigned num_flex = 0;
+            for (unsigned i = e.bw; i-- >= msb;) 
+                if (!a.fixed.get(i))
+                    ++num_flex;
+            if (num_flex == 0)
+                return false;
+            unsigned n = m_rand(num_flex);
+            for (unsigned i = e.bw; i-- >= msb;) {
+                if (!a.fixed.get(i)) {
+                    if (n == 0) {
+                        t.set(i, true);
+                        break;
+                    }
+                    else
+                        n--;
+                }
+            }
+        }
+        return a.set_repair(random_bool(), t);
+    }
+
+    /**
+    * strong:
+    * - clz(a) <= clz(e), e = 0 or (a >> (clz(e) - clz(a)) = e
+    * - e = 0 and a = 0:  b := random
+    * - e = 0 and a != 0: b := random, such that shift <= b 
+    * - e != 0:           b := shift
+    * where shift := clz(e) - clz(a)
+    * 
+    * weak:
+    * - e = 0:  b := random
+    * - e > 0:  b := random >= clz(e)
+    */
+    bool sls_eval::try_repair_lshr1(bvect const& e, bvval const& a, bvval& b) {
+
+        auto& t = m_tmp;
+        auto clza = a.clz(a.bits());
+        auto clze = a.clz(e);
+        t.set_bw(a.bw);
+
+        // strong
+        if (m_rand(10) != 0 && clza <= clze && (a.is_zero(e) || t.set_shift_right(a.bits(), clze - clza) == e)) {
+            if (a.is_zero(e) && a.is_zero()) 
+                return true;            
+            unsigned shift = clze - clza;
+            if (a.is_zero(e)) 
+                shift = m_rand(a.bw + 1 - shift) + shift;            
+            
+            b.set(t, shift);
+            if (b.try_set(t))
+                return true;            
+        }
+
+        // no change
+        if (m_rand(10) != 0) {
+            if (a.is_zero(e))
+                return true;
+            if (b.bits() <= clze)
+                return true;
+        }
+
+        // weak
+        b.get_variant(t, m_rand);
+        if (a.is_zero(e))             
+            return b.set_repair(random_bool(), t);        
+        else {
+            for (unsigned i = 0; i < 4; ++i) {
+                for (unsigned i = a.bw; !(t <= clze) && i-- > 0; )
+                    if (!b.fixed.get(i))
+                        t.set(i, false);
+                if (t <= clze && b.set_repair(random_bool(), t))
+                    return true;                
+                b.get_variant(t, m_rand);
+            }
+            return false;
+        }        
+    }
+
+    /**
+    * strong:
+    *   b  < |b| => (e << b) >>a b = e) 
+    *   b >= |b| => (e = ones || e = 0)
+    * - if b  < |b|: a := e << b
+    * - if b >= |b|: a[bw-1] := e = ones
+    * weak:
+    *   
+    */
+    bool sls_eval::try_repair_ashr0(bvect const& e, bvval& a, bvval const& b) {
+        auto& t = m_tmp;
+        t.set_bw(b.bw);
+        auto n = b.msb(b.bits());
+        bool use_strong = m_rand(20) != 0;
+        if (use_strong && n < b.bw) {
+            t.set_shift_left(e, b.bits());
+            bool sign = t.get(b.bw-1);
+            t.set_shift_right(t, b.bits());
+            if (sign) {
+                for (unsigned i = b.bw; i-- > b.bw - n; )
+                    t.set(i, true);
+            }            
+            use_strong &= t == e;
+        }
+        else {
+            use_strong &= a.is_zero(e) || a.is_ones(e);
+        }
+        if (use_strong) {
+            if (n < b.bw) {
+                t.set_shift_left(e, b.bits());
+                for (unsigned i = 0; i < n; ++i)
+                    t.set(i, a.get_bit(i));
+            }
+            else {                
+                for (unsigned i = 0; i < b.nw; ++i)
+                    t[i] = a.bits()[i];
+                t.set(b.bw - 1, a.is_ones(e));
+            }   
+            if (a.set_repair(random_bool(), t))
+                return true;
+        }
+        if (m_rand(10) != 0) {
+            if (n < b.bw) {
+                t.set_shift_left(e, b.bits());
+                for (unsigned i = 0; i < n; ++i)
+                    t.set(i, random_bool());
+            }
+            else {
+                a.get_variant(t, m_rand);
+                t.set(b.bw - 1, a.is_ones(e));
+            }
+            if (a.set_repair(random_bool(), t))
+                return true;
+        }            
+        return a.set_random(m_rand);
+    }
+
+    /*
+    * strong:
+    * - clz(a) <= clz(e), e = 0 or (a >>a (clz(e) - clz(a)) = e
+    * - e = 0 and a = 0:  b := random
+    * - e = 0 and a != 0: b := random, such that shift <= b 
+    * - e != 0:           b := shift
+    * where shift := clz(e) - clz(a)
+    * 
+    * weak:
+    * - e = 0:  b := random
+    * - e > 0:  b := random >= clz(e)
+    */
+
+    bool sls_eval::try_repair_ashr1(bvect const& e, bvval const& a, bvval& b) {
+
+        auto& t = m_tmp;
+        auto clza = a.clz(a.bits());
+        auto clze = a.clz(e);
+        t.set_bw(a.bw);
+
+        // strong unsigned
+        if (!a.get_bit(a.bw - 1) && m_rand(10) != 0 && clza <= clze && (a.is_zero(e) || t.set_shift_right(a.bits(), clze - clza) == e)) {
+            if (a.is_zero(e) && a.is_zero())
+                return true;
+            unsigned shift = clze - clza;
+            if (a.is_zero(e))
+                shift = m_rand(a.bw + 1 - shift) + shift;
+
+            b.set(t, shift);
+            if (b.try_set(t))
+                return true;
+        }
+        // strong signed
+        if (a.get_bit(a.bw - 1) && m_rand(10) != 0 && clza >= clze) {
+            t.set_shift_right(a.bits(), clza - clze);
+            for (unsigned i = a.bw; i-- > a.bw - clza + clze; )
+                t.set(i, true);
+            if (e == t) {
+                if (a.is_zero(e) && a.is_zero())
+                    return true;
+                unsigned shift = clze - clza;
+                if (a.is_zero(e))
+                    shift = m_rand(a.bw + 1 - shift) + shift;
+
+                b.set(t, shift);
+                if (b.try_set(t))
+                    return true;
+            }
+        }
+
+        // weak
+        b.get_variant(t, m_rand);
+        return b.set_repair(random_bool(), t);
     }
 
     bool sls_eval::try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i) {
@@ -1425,16 +1639,12 @@ namespace bv {
                 m_tmp2.set(b.msb(m_tmp2), false);
             while (a.set_add(m_tmp3, m_tmp, m_tmp2)) 
                 m_tmp2.set(b.msb(m_tmp2), false);       
-            a.clear_overflow_bits(m_tmp3);
             return a.set_repair(true, m_tmp3);
         }
         else {
-            if (a.is_one(e) && a.is_zero()) {
-                for (unsigned i = 0; i < a.nw; ++i)
-                    m_tmp[i] = random_bits();
-                a.clear_overflow_bits(m_tmp);
-                return b.set_repair(true, m_tmp);                
-            }
+            if (a.is_one(e) && a.is_zero()) 
+                return b.set_random(m_rand);              
+            
             if (a.is_one(e)) {
                 a.set(m_tmp, a.bits());
                 return b.set_repair(true, m_tmp);
@@ -1506,7 +1716,6 @@ namespace bv {
                 m_tmp[i] = random_bits();
             a.set_sub(m_tmp2, a.bits(), e);
             set_div(m_tmp2, m_tmp, a.bw, m_tmp3, m_tmp4);
-            a.clear_overflow_bits(m_tmp3);
             return b.set_repair(random_bool(), m_tmp3);
         }
     }
@@ -1630,8 +1839,7 @@ namespace bv {
                 m_tmp.set(i, e.get(i));
             b.clear_overflow_bits(m_tmp);
             r = b.try_set(m_tmp);
-        }
-        //verbose_stream() << e << " := " << a << " " << b << "\n";
+        }       
         return r;
     }
 
@@ -1641,15 +1849,15 @@ namespace bv {
     // set a outside of [hi:lo] to random values with preference to 0 or 1 bits
     // 
     bool sls_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) {
-        if (m_rand() % m_config.m_prob_randomize_extract <= 100) {
+        if (m_rand(m_config.m_prob_randomize_extract)  <= 100) {
             a.get_variant(m_tmp, m_rand);
-            if (0 == (m_rand() % 2)) {
-                auto bit = 0 == (m_rand() % 2);
+            if (0 == (m_rand(2))) {
+                auto bit = 0 == (m_rand(2));
                 if (!a.try_set_range(m_tmp, 0, lo, bit))
                     a.try_set_range(m_tmp, 0, lo, !bit);
             }
-            if (0 == (m_rand() % 2)) {
-                auto bit = 0 == (m_rand() % 2);
+            if (0 == (m_rand(2))) {
+                auto bit = 0 == (m_rand(2));
                 if (!a.try_set_range(m_tmp, lo + e.bw, a.bw, bit))
                     a.try_set_range(m_tmp, lo + e.bw, a.bw, !bit);
             }
@@ -1660,10 +1868,7 @@ namespace bv {
             m_tmp.set(i + lo, e.get(i));
         if (a.try_set(m_tmp))
             return true;
-        a.get_variant(m_tmp, m_rand);       
-        bool res = a.set_repair(random_bool(), m_tmp);
-        // verbose_stream() << "try set " << res << " " << m_tmp[0] << " " << a << "\n";
-        return res;
+        return a.set_random(m_rand);
     }
 
     void sls_eval::set_div(bvect const& a, bvect const& b, unsigned bw,
@@ -1698,7 +1903,7 @@ namespace bv {
         }
         if (bv.is_bv(e)) {
             auto& v = eval(to_app(e));
-            // verbose_stream() << "committing: " << v << "\n";
+            
             for (unsigned i = 0; i < v.nw; ++i)
                 if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) {
                     v.bits().copy_to(v.nw, v.eval);
@@ -1717,19 +1922,83 @@ namespace bv {
         return *m_values[e->get_id()]; 
     }
 
+    void sls_eval::init_eval(app* t) {
+        if (m.is_bool(t))
+            set(t, bval1(t));
+        else if (bv.is_bv(t)) {
+            auto& v = wval(t);
+            v.bits().copy_to(v.nw, v.eval);
+        }
+    }
+
+    void sls_eval::commit_eval(app* e) {
+        if (m.is_bool(e)) {
+            set(e, bval1(e));
+        }
+        else {
+            VERIFY(wval(e).commit_eval());
+        }
+    }
+
+    void sls_eval::set_random(app* e) {
+        if (bv.is_bv(e))
+            eval(e).set_random(m_rand);
+    }
+
+    bool sls_eval::eval_is_correct(app* e) {
+        if (!can_eval1(e))
+            return false;
+        if (m.is_bool(e))
+            return bval0(e) == bval1(e);
+        if (bv.is_bv(e)) {
+            auto const& v = wval(e);
+            return v.eval == v.bits();
+        }
+        UNREACHABLE();
+        return false;
+    }
+
+    bool sls_eval::re_eval_is_correct(app* e) {
+        if (!can_eval1(e))
+            return false;
+        if (m.is_bool(e))
+            return bval0(e) ==bval1(e);
+        if (bv.is_bv(e)) {
+            auto const& v = eval(e);
+            return v.eval == v.bits();
+        }
+        UNREACHABLE();
+        return false;
+    }
+
+    expr_ref sls_eval::get_value(app* e) {
+        if (m.is_bool(e))
+            return expr_ref(m.mk_bool_val(bval0(e)), m);
+        else if (bv.is_bv(e)) {
+            auto const& v = wval(e);
+            rational n = v.get_value();
+            return expr_ref(bv.mk_numeral(n, v.bw), m);
+        }
+        return expr_ref(m);
+    }
+
     std::ostream& sls_eval::display(std::ostream& out, expr_ref_vector const& es) {
         auto& terms = sort_assertions(es);
         for (expr* e : terms) {
             out << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " ";
             if (is_fixed0(e))
                 out << "f ";
-            if (bv.is_bv(e))
-                out << wval(e);
-            else if (m.is_bool(e))
-                out << (bval0(e) ? "T" : "F");
-            out << "\n";
+            display_value(out, e) << "\n";
         }
         terms.reset();
         return out;
     }
+
+    std::ostream& sls_eval::display_value(std::ostream& out, expr* e) {
+        if (bv.is_bv(e)) 
+            return out << wval(e);
+        if (m.is_bool(e))
+            return out << (bval0(e)?"T":"F");
+        return out << "?";
+    }
 }

src/ast/sls/bv_sls_eval.h

@@ -25,6 +25,12 @@ namespace bv {
 
     class sls_fixed;
 
+    class sls_eval_plugin {
+    public:
+        virtual ~sls_eval_plugin() {}
+        
+    };
+
     class sls_eval {
         struct config {
             unsigned m_prob_randomize_extract = 50;
@@ -40,6 +46,8 @@ namespace bv {
         random_gen          m_rand;
         config              m_config;
 
+        scoped_ptr_vector<sls_eval_plugin> m_plugins;
+
 
 
         scoped_ptr_vector<sls_valuation> m_values; // expr-id -> bv valuation
@@ -93,6 +101,10 @@ namespace bv {
         bool try_repair_shl(bvect const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_ashr(bvect const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i);
+        bool try_repair_lshr0(bvect const& e, bvval& a, bvval const& b);
+        bool try_repair_lshr1(bvect const& e, bvval const& a, bvval& b);
+        bool try_repair_ashr0(bvect const& e, bvval& a, bvval const& b);
+        bool try_repair_ashr1(bvect const& e, bvval const& a, bvval& b);
         bool try_repair_bit2bool(bvval& a, unsigned idx);
         bool try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_urem(bvect const& e, bvval& a, bvval& b, unsigned i);
@@ -153,6 +165,18 @@ namespace bv {
         
         sls_valuation& eval(app* e) const;
 
+        void commit_eval(app* e);
+
+        void init_eval(app* e);
+
+        void set_random(app* e);
+
+        bool eval_is_correct(app* e);
+
+        bool re_eval_is_correct(app* e);
+
+        expr_ref get_value(app* e);
+
         /**
          * Override evaluaton.
          */
@@ -174,5 +198,7 @@ namespace bv {
 
 
         std::ostream& display(std::ostream& out, expr_ref_vector const& es);
+
+        std::ostream& display_value(std::ostream& out, expr* e);
     };
 }

src/ast/sls/bv_sls_fixed.cpp

@@ -38,8 +38,8 @@ namespace bv {
             else
                 ;
         }
-        ev.m_todo.reset();
         init_ranges(es);
+        ev.m_todo.reset();        
     }
 
 
@@ -49,11 +49,49 @@ namespace bv {
             if (is_app(e))
                 init_range(to_app(e), sign);
         }
+        
+        for (expr* e : ev.m_todo)
+            propagate_range_up(e);
+    }
+
+    void sls_fixed::propagate_range_up(expr* e) {
+        expr* t, * s;
+        rational v;
+        if (bv.is_concat(e, t, s)) {
+            auto& vals = wval(s);
+            if (vals.lo() != vals.hi() && (vals.lo() < vals.hi() || vals.hi() == 0))
+                // lo <= e
+                add_range(e, vals.lo(), rational::zero(), false);
+            auto valt = wval(t);
+            if (valt.lo() != valt.hi() && (valt.lo() < valt.hi() || valt.hi() == 0)) {
+                // (2^|s|) * lo <= e < (2^|s|) * hi
+                auto p = rational::power_of_two(bv.get_bv_size(s));
+                add_range(e, valt.lo() * p, valt.hi() * p, false);
+            }
+        }        
+        else if (bv.is_bv_add(e, s, t) && bv.is_numeral(s, v)) {
+            auto& val = wval(t);
+            if (val.lo() != val.hi()) 
+                add_range(e, v + val.lo(), v + val.hi(), false);  
+        }
+        else if (bv.is_bv_add(e, t, s) && bv.is_numeral(s, v)) {
+            auto& val = wval(t);
+            if (val.lo() != val.hi()) 
+                add_range(e, v + val.lo(), v + val.hi(), false);          
+        }
+        // x in [1, 4[   => -x in [-3, 0[
+        // x in [lo, hi[ => -x in [-hi + 1, -lo + 1[
+        else if (bv.is_bv_mul(e, s, t) && bv.is_numeral(s, v) && 
+            v + 1 == rational::power_of_two(bv.get_bv_size(e))) {
+            auto& val = wval(t);
+            if (val.lo() != val.hi())
+                add_range(e, -val.hi() + 1, - val.lo() + 1, false);
+        }
     }
 
     // s <=s t           <=> s + K <= t + K,   K = 2^{bw-1}
 
-    void sls_fixed::init_range(app* e, bool sign) {
+    bool sls_fixed::init_range(app* e, bool sign) {
         expr* s, * t, * x, * y;
         rational a, b;
         unsigned idx;
@@ -64,56 +102,116 @@ namespace bv {
         if (bv.is_ule(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
-            init_range(x, a, y, b, sign);
+            return init_range(x, a, y, b, sign);
         }
         else if (bv.is_ult(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
-            init_range(y, b, x, a, !sign);
+            return init_range(y, b, x, a, !sign);
         }            
         else if (bv.is_uge(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
-            init_range(y, b, x, a, sign);
+            return init_range(y, b, x, a, sign);
         }            
         else if (bv.is_ugt(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
-            init_range(x, a, y, b, !sign);
+            return init_range(x, a, y, b, !sign);
         }            
         else if (bv.is_sle(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
-            init_range(x, a + N(s), y, b + N(s), sign);
+            return init_range(x, a + N(s), y, b + N(s), sign);
         }            
         else if (bv.is_slt(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
-            init_range(y, b + N(s), x, a + N(s), !sign);
+            return init_range(y, b + N(s), x, a + N(s), !sign);
         }
         else if (bv.is_sge(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
-            init_range(y, b + N(s), x, a + N(s), sign);
+            return init_range(y, b + N(s), x, a + N(s), sign);
         }
         else if (bv.is_sgt(e, s, t)) {
             get_offset(s, x, a);
             get_offset(t, y, b);
-            init_range(x, a + N(s), y, b + N(s), !sign);
+            return init_range(x, a + N(s), y, b + N(s), !sign);
         }
-        else if (!sign && m.is_eq(e, s, t)) {
+        else if (m.is_eq(e, s, t)) {
             if (bv.is_numeral(s, a))
-                // t - a <= 0
-                init_range(t, -a, nullptr, rational(0), false);
+                init_eq(t, a, sign);
             else if (bv.is_numeral(t, a))
-                init_range(s, -a, nullptr, rational(0), false);
+                init_eq(s, a, sign);
+            else
+                return false;
+            return true;
         }
         else if (bv.is_bit2bool(e, s, idx)) {
             auto& val = wval(s);
             val.try_set_bit(idx, !sign);
             val.fixed.set(idx, true);
             val.tighten_range();
+            return true;
         }
+
+        return false;
+    }
+
+    bool sls_fixed::init_eq(expr* t, rational const& a, bool sign) {        
+        unsigned lo, hi;
+        rational b(0);
+        // verbose_stream() << mk_bounded_pp(t, m) << " == " << a << "\n";
+        expr* s = nullptr;        
+        if (sign)
+            // 1 <= t - a
+            init_range(nullptr, rational(1), t, -a, false);
+        else
+            // t - a <= 0
+            init_range(t, -a, nullptr, rational::zero(), false);
+        if (!sign && bv.is_bv_not(t, s)) {
+            for (unsigned i = 0; i < bv.get_bv_size(s); ++i)
+                if (!a.get_bit(i))
+                    b += rational::power_of_two(i);
+            init_eq(s, b, false);
+            return true;
+        }
+        expr* x, * y;
+        if (!sign && bv.is_concat(t, x, y)) {
+            auto sz = bv.get_bv_size(y);
+            auto k = rational::power_of_two(sz);
+            init_eq(y, mod(a, k), false);
+            init_eq(x, div(a + k - 1, k), false);
+            return true;
+        }
+        if (bv.is_extract(t, lo, hi, s)) {
+            if (hi == lo) {
+                sign = sign ? a == 1 : a == 0;
+                auto& val = wval(s);
+                if (val.try_set_bit(lo, !sign)) 
+                    val.fixed.set(lo, true);                                    
+                val.tighten_range();
+            }
+            else if (!sign) {
+                auto& val = wval(s);
+                for (unsigned i = lo; i <= hi; ++i) 
+                    if (val.try_set_bit(i, a.get_bit(i - lo)))
+                        val.fixed.set(i, true);                
+                val.tighten_range();
+                // verbose_stream() << lo << " " << hi << " " << val << " := " << a << "\n";
+            }
+
+            if (!sign && hi + 1 == bv.get_bv_size(s)) {
+                // s < 2^lo * (a + 1) 
+                rational b = rational::power_of_two(lo) * (a + 1) - 1;
+                rational offset;
+                get_offset(s, t, offset);
+                // t + offset <= b
+                init_range(t, offset, nullptr, b, false);
+            }
+        }
+        return true;
     }
 
     // 
@@ -125,52 +223,65 @@ namespace bv {
     // a < x + b         <=> ! (x + b <= a) <=> x not in [-a, b - a [ <=> x in [b - a, -a [         a != -1
     // x + a < x + b     <=> ! (x + b <= x + a) <=> x in [-a, -b [                                  a != b
     // 
-    void sls_fixed::init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign) {
+    bool sls_fixed::init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign) {
         if (!x && !y)
-            return;
-        if (!x) {
-            // a <= y + b
-            if (a == 0)
-                return;
-            auto& v = wval(y);
-            if (!sign)
-                v.add_range(a - b, -b);
-            else
-                v.add_range(-b, a - b);
-        }
-        else if (!y) {
+            return false;
+        if (!x) 
+            return add_range(y, a - b, -b, sign);
+        else if (!y) 
+            return add_range(x, -a, b - a + 1, sign);        
+        else if (x == y) 
+            return add_range(x, -a, -b, sign);
+        return false;
+    }
 
-            if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 0)
-                return;
-            auto& v = wval(x);
-            if (!sign)
-                v.add_range(-a, b - a + 1);
-            else 
-                v.add_range(b - a + 1, -a);
+    bool sls_fixed::add_range(expr* e, rational lo, rational hi, bool sign) {
+        auto& v = wval(e);
+        lo = mod(lo, rational::power_of_two(bv.get_bv_size(e)));
+        hi = mod(hi, rational::power_of_two(bv.get_bv_size(e)));
+        if (lo == hi)
+            return false;
+        if (sign)
+            std::swap(lo, hi);
+        v.add_range(lo, hi);
+        expr* x, * y;
+        if (v.lo() == 0 && bv.is_concat(e, x, y)) {
+            auto sz = bv.get_bv_size(y);
+            auto k = rational::power_of_two(sz);
+            lo = v.lo();
+            hi = v.hi();
+            if (hi <= k) {
+                add_range(y, lo, hi, false);
+                init_eq(x, lo, false);
+            }
+            else {
+                hi = div(hi + k - 1, k);
+                add_range(x, lo, hi, false);
+            }
         }
-        else if (x == y) {
-            if (a == b)
-                return;
-            auto& v = wval(x);
-            if (!sign)
-                v.add_range(-a, -b);
-            else
-                v.add_range(-b, -a);
-        }
-        
+        return true;
     }
 
     void sls_fixed::get_offset(expr* e, expr*& x, rational& offset) {
         expr* s, * t;
         x = e;
         offset = 0;
-        if (bv.is_bv_add(e, s, t)) {
-            if (bv.is_numeral(s, offset))
+        rational n;
+        while (true) {
+            if (bv.is_bv_add(x, s, t) && bv.is_numeral(s, n)) {
                 x = t;
-            else if (bv.is_numeral(t, offset))
+                offset += n;
+                continue;
+            }
+            if (bv.is_bv_add(x, s, t) && bv.is_numeral(t, n)) {
                 x = s;
+                offset += n;
+                continue;
+            }
+            break;
         }
-        else if (bv.is_numeral(e, offset))
+        if (bv.is_numeral(e, n))
+            offset += n,
             x = nullptr;
     }
 
@@ -258,11 +369,6 @@ namespace bv {
         case OP_BADD: {
             auto& a = wval(e->get_arg(0));
             auto& b = wval(e->get_arg(1));
-            rational r;
-            if (bv.is_numeral(e->get_arg(0), r) && b.has_range()) 
-                v.add_range(r + b.lo(), r + b.hi());            
-            else if (bv.is_numeral(e->get_arg(1), r) && a.has_range()) 
-                v.add_range(r + a.lo(), r + a.hi());            
             bool pfixed = true;
             for (unsigned i = 0; i < v.bw; ++i) {
                 if (pfixed && a.fixed.get(i) && b.fixed.get(i)) 
@@ -277,7 +383,6 @@ namespace bv {
                     v.fixed.set(i, false);
                 }
             }
-
             break;
         }
         case OP_BMUL: {

src/ast/sls/bv_sls_fixed.h

@@ -30,9 +30,12 @@ namespace bv {
         bv_util&            bv;
 
         void init_ranges(expr_ref_vector const& es);
-        void init_range(app* e, bool sign);
-        void init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign);
+        bool init_range(app* e, bool sign);
+        void propagate_range_up(expr* e);
+        bool init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign);
         void get_offset(expr* e, expr*& x, rational& offset);
+        bool init_eq(expr* e, rational const& v, bool sign);
+        bool add_range(expr* e, rational lo, rational hi, bool sign);
 
         void init_fixed_basic(app* e);
         void init_fixed_bv(app* e);

src/ast/sls/bv_sls_terms.cpp

@@ -20,12 +20,14 @@ Author:
 
 #include "ast/ast_ll_pp.h"
 #include "ast/sls/bv_sls.h"
+#include "ast/rewriter/th_rewriter.h"
 
 namespace bv {
 
     sls_terms::sls_terms(ast_manager& m): 
         m(m), 
         bv(m),
+        m_rewriter(m),
         m_assertions(m),
         m_pinned(m),
         m_translated(m), 
@@ -40,18 +42,20 @@ namespace bv {
         expr* top = e;
         m_pinned.push_back(e);
         m_todo.push_back(e);
-        expr_fast_mark1 mark;
-        for (unsigned i = 0; i < m_todo.size(); ++i) {
-            expr* e = m_todo[i];
-            if (!is_app(e))
-                continue;
-            if (m_translated.get(e->get_id(), nullptr))
-                continue;
-            if (mark.is_marked(e))
-                continue;
-            mark.mark(e);
-            for (auto arg : *to_app(e))
-                m_todo.push_back(arg);
+        {
+            expr_fast_mark1 mark;
+            for (unsigned i = 0; i < m_todo.size(); ++i) {
+                expr* e = m_todo[i];
+                if (!is_app(e))
+                    continue;
+                if (m_translated.get(e->get_id(), nullptr))
+                    continue;
+                if (mark.is_marked(e))
+                    continue;
+                mark.mark(e);
+                for (auto arg : *to_app(e))
+                    m_todo.push_back(arg);
+            }
         }
         std::stable_sort(m_todo.begin(), m_todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); });
         for (expr* e : m_todo)
@@ -127,7 +131,7 @@ namespace bv {
         m_translated.setx(e->get_id(), r);
     }
 
-    expr* sls_terms::mk_sdiv(expr* x, expr* y) {
+    expr_ref sls_terms::mk_sdiv(expr* x, expr* y) {
         // d = udiv(abs(x), abs(y))
         // y = 0, x >= 0 -> -1
         // y = 0, x < 0 -> 1
@@ -141,17 +145,18 @@ namespace bv {
         expr_ref z(bv.mk_zero(sz), m);
         expr* signx = bv.mk_ule(bv.mk_numeral(N / 2, sz), x);
         expr* signy = bv.mk_ule(bv.mk_numeral(N / 2, sz), y);
-        expr* absx = m.mk_ite(signx, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), x), x);
-        expr* absy = m.mk_ite(signy, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), y), y);
+        expr* absx = m.mk_ite(signx, bv.mk_bv_neg(x), x);
+        expr* absy = m.mk_ite(signy, bv.mk_bv_neg(y), y);
         expr* d = bv.mk_bv_udiv(absx, absy);
-        expr* r = m.mk_ite(m.mk_eq(signx, signy), d, bv.mk_bv_neg(d));
+        expr_ref r(m.mk_ite(m.mk_eq(signx, signy), d, bv.mk_bv_neg(d)), m);
         r = m.mk_ite(m.mk_eq(z, y),
-                m.mk_ite(signx, bv.mk_one(sz), bv.mk_numeral(N - 1, sz)),
-                m.mk_ite(m.mk_eq(x, z), z, r));
+                     m.mk_ite(signx, bv.mk_one(sz), bv.mk_numeral(N - 1, sz)),
+                     m.mk_ite(m.mk_eq(x, z), z, r));
+        m_rewriter(r);
         return r;
     }
 
-    expr* sls_terms::mk_smod(expr* x, expr* y) {
+    expr_ref sls_terms::mk_smod(expr* x, expr* y) {
         // u := umod(abs(x), abs(y))
         // u = 0 ->  0
         // y = 0 ->  x
@@ -164,21 +169,24 @@ namespace bv {
         expr_ref abs_x(m.mk_ite(bv.mk_sle(z, x), x, bv.mk_bv_neg(x)), m);
         expr_ref abs_y(m.mk_ite(bv.mk_sle(z, y), y, bv.mk_bv_neg(y)), m);
         expr_ref u(bv.mk_bv_urem(abs_x, abs_y), m);
-        return
-            m.mk_ite(m.mk_eq(u, z), z,
+        expr_ref r(m);
+        r = m.mk_ite(m.mk_eq(u, z), z,
                 m.mk_ite(m.mk_eq(y, z), x,
                     m.mk_ite(m.mk_and(bv.mk_sle(z, x), bv.mk_sle(z, x)), u,
                         m.mk_ite(bv.mk_sle(z, x), bv.mk_bv_add(y, u),
                             m.mk_ite(bv.mk_sle(z, y), bv.mk_bv_sub(y, u), bv.mk_bv_neg(u))))));
-                      
+        m_rewriter(r);
+        return r;
     }
 
-    expr* sls_terms::mk_srem(expr* x, expr* y) {
+    expr_ref sls_terms::mk_srem(expr* x, expr* y) {
         // y = 0 -> x
         // else x - sdiv(x, y) * y
-        return 
-            m.mk_ite(m.mk_eq(y, bv.mk_zero(bv.get_bv_size(x))),
+        expr_ref r(m);
+        r = m.mk_ite(m.mk_eq(y, bv.mk_zero(bv.get_bv_size(x))),
                      x, bv.mk_bv_sub(x, bv.mk_bv_mul(y, mk_sdiv(x, y))));
+        m_rewriter(r);
+        return r;
     }
 
 
@@ -198,6 +206,7 @@ namespace bv {
                 m_todo.push_back(arg);
         }       
         // populate parents
+        m_parents.reset();
         m_parents.reserve(m_terms.size());
         for (expr* e : m_terms) {
             if (!e || !is_app(e))
@@ -205,8 +214,16 @@ namespace bv {
             for (expr* arg : *to_app(e))
                 m_parents[arg->get_id()].push_back(e);                
         }
+        m_assertion_set.reset();
         for (auto a : m_assertions)
             m_assertion_set.insert(a->get_id());
     }
 
+    void sls_terms::updt_params(params_ref const& p) {
+        params_ref q = p;
+        q.set_bool("flat", false);
+        m_rewriter.updt_params(q);
+    }
+
+
 }

src/ast/sls/bv_sls_terms.h

@@ -21,6 +21,7 @@ Author:
 #include "util/scoped_ptr_vector.h"
 #include "util/uint_set.h"
 #include "ast/ast.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "ast/sls/sls_stats.h"
 #include "ast/sls/sls_powers.h"
 #include "ast/sls/sls_valuation.h"
@@ -31,6 +32,7 @@ namespace bv {
     class sls_terms {
         ast_manager&        m;
         bv_util             bv;
+        th_rewriter         m_rewriter;
         ptr_vector<expr>    m_todo, m_args;
         expr_ref_vector     m_assertions, m_pinned, m_translated;
         app_ref_vector      m_terms;
@@ -40,12 +42,14 @@ namespace bv {
         expr* ensure_binary(expr* e);
         void ensure_binary_core(expr* e);
 
-        expr* mk_sdiv(expr* x, expr* y);
-        expr* mk_smod(expr* x, expr* y);
-        expr* mk_srem(expr* x, expr* y);
+        expr_ref mk_sdiv(expr* x, expr* y);
+        expr_ref mk_smod(expr* x, expr* y);
+        expr_ref mk_srem(expr* x, expr* y);
 
     public:
         sls_terms(ast_manager& m);
+
+        void updt_params(params_ref const& p);
         
         /**
         * Add constraints

src/ast/sls/sls_engine.cpp

@@ -421,6 +421,7 @@ lbool sls_engine::search() {
 
         // get candidate variables
         ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(m_assertions);
+        
         if (to_evaluate.empty())
         {
             res = l_true;
@@ -514,6 +515,12 @@ lbool sls_engine::operator()() {
     if (m_restart_init)
         m_tracker.randomize(m_assertions);
 
+    return search_loop();
+}
+
+
+lbool sls_engine::search_loop() {
+
     lbool res = l_undef;
 
     do {
@@ -533,7 +540,6 @@ lbool sls_engine::operator()() {
     } while (res != l_true && m_stats.m_restarts++ < m_max_restarts);
 
     verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl;
-    
     return res;
 }
 

src/ast/sls/sls_engine.h

@@ -79,7 +79,11 @@ public:
     void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted);
     void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped);            
 
-    lbool search();
+
+
+    lbool search();  
+
+    lbool search_loop();
 
     lbool operator()();
 

src/ast/sls/sls_valuation.cpp

@@ -56,6 +56,20 @@ namespace bv {
         return mpn_manager().compare(a.data(), a.nw, b.data(), a.nw) >= 0;
     }
 
+    bool operator<=(digit_t a, bvect const& b) {
+        for (unsigned i = 1; i < b.nw; ++i)
+            if (0 != b[i])
+                return true;
+        return mpn_manager().compare(&a, 1, b.data(), 1) <= 0;
+    }
+
+    bool operator<=(bvect const& a, digit_t b) {
+        for (unsigned i = 1; i < a.nw; ++i)
+            if (0 != a[i])
+                return false;
+        return mpn_manager().compare(a.data(), 1, &b, 1) <= 0;
+    }
+
     std::ostream& operator<<(std::ostream& out, bvect const& v) {
         out << std::hex;
         bool nz = false;
@@ -83,11 +97,63 @@ namespace bv {
         return r;
     }
 
+
+    unsigned bvect::to_nat(unsigned max_n) const {
+        SASSERT(max_n < UINT_MAX / 2);
+        unsigned p = 1;
+        unsigned value = 0;
+        for (unsigned i = 0; i < bw; ++i) {
+            if (p >= max_n) {
+                for (unsigned j = i; j < bw; ++j)
+                    if (get(j))
+                        return max_n;
+                return value;
+            }
+            if (get(i))
+                value += p;
+            p <<= 1;
+        }
+        return value;
+    }
+
+    bvect& bvect::set_shift_right(bvect const& a, bvect const& b) {
+        SASSERT(a.bw == b.bw);
+        unsigned shift = b.to_nat(b.bw);
+        return set_shift_right(a, shift);
+    }
+
+    bvect& bvect::set_shift_right(bvect const& a, unsigned shift) {
+        set_bw(a.bw);
+        if (shift == 0)
+            a.copy_to(a.nw, *this);
+        else if (shift >= a.bw)
+            set_zero();
+        else
+            for (unsigned i = 0; i < bw; ++i)
+                set(i, i + shift < bw ? a.get(i + shift) : false);
+        return *this;
+    }
+
+    bvect& bvect::set_shift_left(bvect const& a, bvect const& b) {
+        set_bw(a.bw);
+        SASSERT(a.bw == b.bw);
+        unsigned shift = b.to_nat(b.bw);
+        if (shift == 0)
+            a.copy_to(a.nw, *this);
+        else if (shift >= a.bw)
+            set_zero();
+        else
+            for (unsigned i = bw; i-- > 0; )
+                set(i, i >= shift ? a.get(i - shift) : false);
+        return *this;
+    }
+
     sls_valuation::sls_valuation(unsigned bw) {
         set_bw(bw);
         m_lo.set_bw(bw);
         m_hi.set_bw(bw);
         m_bits.set_bw(bw);
+        m_tmp.set_bw(bw);
         fixed.set_bw(bw);
         eval.set_bw(bw);
         // have lo, hi bits, fixed point to memory allocated within this of size num_bytes each allocated        
@@ -106,10 +172,12 @@ namespace bv {
 
     bool sls_valuation::commit_eval() { 
         for (unsigned i = 0; i < nw; ++i)
-            if (0 != (fixed[i] & (m_bits[i] ^ eval[i])))
-                return false;        
-        if (!in_range(eval))
+            if (0 != (fixed[i] & (m_bits[i] ^ eval[i])))                 
+                return false;
+            
+        if (!in_range(eval)) 
             return false;
+        
         for (unsigned i = 0; i < nw; ++i) 
             m_bits[i] = eval[i]; 
         SASSERT(well_formed()); 
@@ -137,143 +205,75 @@ namespace bv {
 
     //
     // largest dst <= src and dst is feasible
-    // set dst := src & (~fixed | bits)
-    // 
-    // increment dst if dst < src by setting bits below msb(src & ~dst) to 1
-    // 
-    // if dst < lo < hi:
-    //    return false
-    // if lo < hi <= dst:
-    //    set dst := hi - 1
-    // if hi <= dst < lo
-    //    set dst := hi - 1
-    // 
+    //
 
     bool sls_valuation::get_at_most(bvect const& src, bvect& dst) const {
         SASSERT(!has_overflow(src));
-        for (unsigned i = 0; i < nw; ++i)
-            dst[i] = src[i] & (~fixed[i] | m_bits[i]);
-
-        //
-        // If dst < src, then find the most significant 
-        // bit where src[idx] = 1, dst[idx] = 0
-        // set dst[j] = bits_j | ~fixed_j for j < idx
-        //
-        for (unsigned i = nw; i-- > 0; ) {
-            if (0 != (~dst[i] & src[i])) {
-                auto idx = log2(~dst[i] & src[i]);
-                auto mask = (1 << idx) - 1;
-                dst[i] = (~fixed[i] & mask) | dst[i];
-                for (unsigned j = i; j-- > 0; )
-                    dst[j] = (~fixed[j] | m_bits[j]);
-                break;
-            }
-        }
-        SASSERT(!has_overflow(dst));
-        return round_down(dst);
+        src.copy_to(nw, dst);
+        sup_feasible(dst);
+        if (in_range(dst)) {
+            SASSERT(can_set(dst));
+            return true;
+        }        
+        if (dst < m_lo && m_lo < m_hi) // dst < lo < hi 
+            return false;
+        if (is_zero(m_hi))
+            return false;
+        m_hi.copy_to(nw, dst); // hi <= dst < lo or lo < hi <= dst
+        sub1(dst);       
+        SASSERT(can_set(dst));
+        return true;
     }
 
     //
     // smallest dst >= src and dst is feasible with respect to this.
-    // set dst := (src & ~fixed) | (fixed & bits)
-    // 
-    // decrement dst if dst > src by setting bits below msb to 0 unless fixed
-    // 
-    // if lo < hi <= dst
-    //    return false
-    // if dst < lo < hi:
-    //    set dst := lo
-    // if hi <= dst < lo
-    //    set dst := lo
-    // 
     bool sls_valuation::get_at_least(bvect const& src, bvect& dst) const {
         SASSERT(!has_overflow(src));
-        for (unsigned i = 0; i < nw; ++i)
-            dst[i] = (~fixed[i] & src[i]) | (fixed[i] & m_bits[i]);
-
-        //
-        // If dst > src, then find the most significant 
-        // bit where src[idx] = 0, dst[idx] = 1
-        // set dst[j] = dst[j] & fixed_j for j < idx
-        //
-        for (unsigned i = nw; i-- > 0; ) {
-            if (0 != (dst[i] & ~src[i])) {
-                auto idx = log2(dst[i] & ~src[i]);
-                auto mask = (1 << idx);
-                dst[i] = dst[i] & (fixed[i] | mask);
-                for (unsigned j = i; j-- > 0; )
-                    dst[j] = dst[j] & fixed[j];
-                break;
-            }
+        src.copy_to(nw, dst);
+        dst.set_bw(bw);
+        inf_feasible(dst);
+        if (in_range(dst)) {
+            SASSERT(can_set(dst));
+            return true;
         }
-        SASSERT(!has_overflow(dst));
-        return round_up(dst);
-    }
 
-    bool sls_valuation::round_up(bvect& dst) const {
-        if (m_lo < m_hi) {
-            if (m_hi <= dst)
-                return false;
-            if (m_lo > dst)
-                set(dst, m_lo);
-        }
-        else if (m_hi <= dst && m_lo > dst)
-            set(dst, m_lo);
-        SASSERT(!has_overflow(dst));
-        return true;
-    }
-
-    bool sls_valuation::round_down(bvect& dst) const {
-        if (m_lo < m_hi) {
-            if (m_lo > dst)
-                return false;
-            if (m_hi <= dst) {
-                set(dst, m_hi);
-                sub1(dst);
-            }
-        }
-        else if (m_hi <= dst && m_lo > dst) {
-            set(dst, m_hi);
-            sub1(dst);
-        }
-        SASSERT(well_formed());
-        return true;
-    }
-
-    bool sls_valuation::set_random_at_most(bvect const& src, bvect& tmp, random_gen& r) {
-        if (!get_at_most(src, tmp))
+        if (dst > m_lo)
             return false;
-        if (is_zero(tmp) || (0 == r() % 2))
-            return try_set(tmp);
+        m_lo.copy_to(nw, dst);
+        SASSERT(can_set(dst));
+        return true;
+    }
+
+    bool sls_valuation::set_random_at_most(bvect const& src, random_gen& r) {
+        m_tmp.set_bw(bw);
+        if (!get_at_most(src, m_tmp))
+            return false;
+
+        if (is_zero(m_tmp) || (0 != r(10)))
+            return try_set(m_tmp);
 
-        set_random_below(tmp, r);
         // random value below tmp
-
-        if (m_lo == m_hi || is_zero(m_lo) || m_lo <= tmp)
-            return try_set(tmp);
-
-        // for simplicity, bail out if we were not lucky
-        return get_at_most(src, tmp) && try_set(tmp);  
+        set_random_below(m_tmp, r);
+        
+        return (can_set(m_tmp) || get_at_most(src, m_tmp)) && try_set(m_tmp);
     }
 
-    bool sls_valuation::set_random_at_least(bvect const& src, bvect& tmp, random_gen& r) {
-        if (!get_at_least(src, tmp))
+    bool sls_valuation::set_random_at_least(bvect const& src, random_gen& r) {
+        if (!get_at_least(src, m_tmp))
             return false;
-        if (is_ones(tmp) || (0 == r() % 2))
-            return try_set(tmp);
+
+        if (is_ones(m_tmp) || (0 != r(10)))
+            return try_set(m_tmp);
 
         // random value at least tmp
-        set_random_above(tmp, r);
-       
-        if (m_lo == m_hi || is_zero(m_hi) || m_hi > tmp)
-            return try_set(tmp);
+        set_random_above(m_tmp, r);
 
-        // for simplicity, bail out if we were not lucky
-        return get_at_least(src, tmp) && try_set(tmp);        
+        return (can_set(m_tmp) || get_at_least(src, m_tmp)) && try_set(m_tmp);
     }
 
-    bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, bvect& tmp, random_gen& r) {
-        if (0 == r() % 2) {
+    bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r) {
+        bvect& tmp = m_tmp;
+        if (0 == r(2)) {
             if (!get_at_least(lo, tmp))
                 return false;
             SASSERT(in_range(tmp));
@@ -344,7 +344,7 @@ namespace bv {
     bool sls_valuation::set_repair(bool try_down, bvect& dst) {
         for (unsigned i = 0; i < nw; ++i)
             dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]);
-
+        clear_overflow_bits(dst);
         repair_sign_bits(dst);
         if (in_range(dst)) {
             set(eval, dst);
@@ -409,6 +409,16 @@ namespace bv {
         return bw;
     }
 
+    unsigned sls_valuation::clz(bvect const& src) const {
+        SASSERT(!has_overflow(src));
+        unsigned i = bw;
+        for (; i-- > 0; )
+            if (!src.get(i))
+                return bw - 1 - i;
+        return bw;
+    }
+
+
     void sls_valuation::set_value(bvect& bits, rational const& n) {
         for (unsigned i = 0; i < bw; ++i)
             bits.set(i, n.get_bit(i));
@@ -433,14 +443,22 @@ namespace bv {
         clear_overflow_bits(dst);
     }
 
+    bool sls_valuation::set_random(random_gen& r) {
+        get_variant(m_tmp, r);
+        return set_repair(r(2) == 0, m_tmp);
+    }
+
     void sls_valuation::repair_sign_bits(bvect& dst) const {
         if (m_signed_prefix == 0)
             return;
-        bool sign = dst.get(bw - 1);
-        for (unsigned i = bw; i-- >= bw - m_signed_prefix; ) {
+        bool sign = m_signed_prefix == bw ? dst.get(bw - 1) : dst.get(bw - m_signed_prefix - 1);
+        for (unsigned i = bw; i-- > bw - m_signed_prefix; ) {
             if (dst.get(i) != sign) {
                 if (fixed.get(i)) {
-                    for (unsigned i = bw; i-- >= bw - m_signed_prefix; )
+                    unsigned j = bw - m_signed_prefix;
+                    if (j > 0 && !fixed.get(j - 1))
+                        dst.set(j - 1, !sign);
+                    for (unsigned i = bw; i-- > bw - m_signed_prefix; )
                         if (!fixed.get(i))
                             dst.set(i, !sign);
                     return;
@@ -453,7 +471,7 @@ namespace bv {
 
     //
     // new_bits != bits => ~fixed
-    // 0 = (new_bits ^ bits) & fixed
+    // 0 = (new_bits ^ bits) & fixedf
     // also check that new_bits are in range
     //
     bool sls_valuation::can_set(bvect const& new_bits) const {
@@ -464,24 +482,11 @@ namespace bv {
         return in_range(new_bits);
     }
 
-    unsigned sls_valuation::to_nat(unsigned max_n) {
+    unsigned sls_valuation::to_nat(unsigned max_n) const {
+
         bvect const& d = m_bits;
         SASSERT(!has_overflow(d));
-        SASSERT(max_n < UINT_MAX / 2);
-        unsigned p = 1;
-        unsigned value = 0;
-        for (unsigned i = 0; i < bw; ++i) {
-            if (p >= max_n) {
-                for (unsigned j = i; j < bw; ++j)
-                    if (d.get(j))
-                        return max_n;
-                return value;
-            }
-            if (d.get(i))
-                value += p;
-            p <<= 1;
-        }
-        return value;
+        return d.to_nat(max_n);
     }
 
     void sls_valuation::shift_right(bvect& out, unsigned shift) const {
@@ -491,15 +496,16 @@ namespace bv {
         SASSERT(well_formed());
     }
 
-    void sls_valuation::add_range(rational l, rational h) {
-        
+    void sls_valuation::add_range(rational l, rational h) {   
+        //return;
+        //verbose_stream() << *this << " " << l << " " << h << " --> \n";
+
         l = mod(l, rational::power_of_two(bw));
         h = mod(h, rational::power_of_two(bw));
         if (h == l)
             return;
 
-        //verbose_stream() << "[" << l << ", " << h << "[\n";
-        //verbose_stream() << *this << "\n";
+//        verbose_stream() << *this << " " << l << " " << h << " --> ";
 
         if (m_lo == m_hi) {
             set_value(m_lo, l);
@@ -509,32 +515,42 @@ namespace bv {
             auto old_lo = lo();
             auto old_hi = hi();
             if (old_lo < old_hi) {
-                if (old_lo < l && l < old_hi)
+                if (old_lo < l && l < old_hi && old_hi <= h)
                     set_value(m_lo, l),
                     old_lo = l;
-                if (old_hi < h && h < old_hi)
+                if (l <= old_lo && old_lo < h && h < old_hi)
                     set_value(m_hi, h);
             }
             else {
                 SASSERT(old_hi < old_lo);
-                if (old_lo < l || l < old_hi)
-                    set_value(m_lo, l),
-                    old_lo = l;
-                if (old_lo < h && h < old_hi)
+                if (h <= old_hi && old_lo <= l) {
+                    set_value(m_lo, l);
                     set_value(m_hi, h);
-                else if (old_hi < old_lo && (h < old_hi || old_lo < h))
+                }
+                else if (old_lo <= l && l <= h) {
+                    set_value(m_lo, l);
+                    set_value(m_hi, h);
+                }
+                else if (old_lo + 1 == l) 
+                    set_value(m_lo, l);                
+                else if (old_hi == h + 1)
+                    set_value(m_hi, h);                
+                else if (old_hi == h && old_lo < l)
+                    set_value(m_lo, l);
+                else if (old_lo == l && h < old_hi)
                     set_value(m_hi, h);
             }
         }
 
-
-
         SASSERT(!has_overflow(m_lo));
         SASSERT(!has_overflow(m_hi));
 
+        //verbose_stream() << *this << " --> ";
+
         tighten_range();
+
+        //verbose_stream() << *this << "\n";
         SASSERT(well_formed());
-        // verbose_stream() << *this << "\n";
     }
 
     //
@@ -551,68 +567,88 @@ namespace bv {
     //  lo + 1 = hi -> set bits = lo
     //  lo < hi, set most significant bits based on hi
     //
-    void sls_valuation::tighten_range() {
 
-        // verbose_stream() << "tighten " << *this << "\n";
+    unsigned sls_valuation::diff_index(bvect const& a) const {
+        unsigned index = 0;
+        for (unsigned i = nw; i-- > 0; ) {
+            auto diff = fixed[i] & (m_bits[i] ^ a[i]);
+            if (diff != 0 && index == 0)
+                index = 1 + i * 8 * sizeof(digit_t) + log2(diff);
+        }
+        return index;
+    }
+
+    void sls_valuation::inf_feasible(bvect& a) const {
+        unsigned lo_index = diff_index(a);
+        
+        if (lo_index != 0) {
+            lo_index--;
+            SASSERT(a.get(lo_index) != m_bits.get(lo_index));
+            SASSERT(fixed.get(lo_index));
+            for (unsigned i = 0; i <= lo_index; ++i) {
+                if (!fixed.get(i))
+                    a.set(i, false);
+                else if (fixed.get(i))
+                    a.set(i, m_bits.get(i));
+            }
+            if (!a.get(lo_index)) {
+                for (unsigned i = lo_index + 1; i < bw; ++i)
+                    if (!fixed.get(i) && !a.get(i)) {
+                        a.set(i, true);
+                        break;
+                    }
+            }
+        }
+    }
+
+    void sls_valuation::sup_feasible(bvect& a) const {
+        unsigned hi_index = diff_index(a);
+        if (hi_index != 0) {
+            hi_index--;
+            SASSERT(a.get(hi_index) != m_bits.get(hi_index));
+            SASSERT(fixed.get(hi_index));
+            for (unsigned i = 0; i <= hi_index; ++i) {
+                if (!fixed.get(i))
+                    a.set(i, true);
+                else if (fixed.get(i))
+                    a.set(i, m_bits.get(i));
+            }
+            if (a.get(hi_index)) {
+                for (unsigned i = hi_index + 1; i < bw; ++i)
+                    if (!fixed.get(i) && a.get(i)) {
+                        a.set(i, false);
+                        break;
+                    }
+            }
+        }
+    }
+
+    void sls_valuation::tighten_range() {
+        
         if (m_lo == m_hi)
             return;
 
-        if (!in_range(m_bits)) {
-            // verbose_stream() << "not in range\n";
-            bool compatible = true;
-            for (unsigned i = 0; i < nw && compatible; ++i)
-                compatible = 0 == (fixed[i] & (m_bits[i] ^ m_lo[i]));
-            //verbose_stream() << (fixed[0] & (m_bits[0] ^ m_lo[0])) << "\n";
-            //verbose_stream() << bw << " " << m_lo[0] << " " << m_bits[0] << "\n";
-            if (compatible) {
-                //verbose_stream() << "compatible\n";
-                set(m_bits, m_lo);
-            }
-            else {
-                bvect tmp(m_bits.nw);
-                tmp.set_bw(bw);
-                set(tmp, m_lo);
-                unsigned max_diff = bw;
-                for (unsigned i = 0; i < bw; ++i) {
-                    if (fixed.get(i) && (m_bits.get(i) ^ m_lo.get(i))) 
-                        max_diff = i;                    
-                }
-                SASSERT(max_diff != bw);
+        inf_feasible(m_lo);
 
-                for (unsigned i = 0; i <= max_diff; ++i)
-                    tmp.set(i, fixed.get(i) && m_bits.get(i));
+        bvect& hi1 = m_tmp;
+        hi1.set_bw(bw);
+        m_hi.copy_to(nw, hi1);
+        sub1(hi1);
+        sup_feasible(hi1);
+        add1(hi1);
+        hi1.copy_to(nw, m_hi);
 
-                bool found0 = false;
-                for (unsigned i = max_diff + 1; i < bw; ++i) {
-                    if (found0 || m_lo.get(i) || fixed.get(i))
-                        tmp.set(i, m_lo.get(i) && fixed.get(i));
-                    else {
-                        tmp.set(i, true);
-                        found0 = true;
-                    }
-                }
-                set(m_bits, tmp);
-            }
-        }
-        // update lo, hi to be feasible.
+        if (has_range() && !in_range(m_bits)) 
+            m_bits = m_lo;
+
+        if (mod(lo() + 1, rational::power_of_two(bw)) == hi())
+            for (unsigned i = 0; i < nw; ++i)
+                fixed[i] = ~0;      
+        if (lo() < hi() && hi() < rational::power_of_two(bw - 1))
+            for (unsigned i = 0; i < bw; ++i)
+                if (hi() < rational::power_of_two(i))
+                    fixed.set(i, true);
         
-        for (unsigned i = bw; i-- > 0; ) {
-            if (!fixed.get(i))
-                continue;
-            if (m_bits.get(i) == m_lo.get(i))
-                continue;
-            if (m_bits.get(i)) {
-                m_lo.set(i, true);
-                for (unsigned j = i; j-- > 0; )
-                    m_lo.set(j, fixed.get(j) && m_bits.get(j));
-            }
-            else {
-                for (unsigned j = bw; j-- > 0; )
-                    m_lo.set(j, fixed.get(j) && m_bits.get(j));
-            }
-            break;
-        }
-
         SASSERT(well_formed());
     }
 
@@ -648,6 +684,4 @@ namespace bv {
             c += get_num_1bits(src[i]);
         return c == 1;
     }
-
-
 }

src/ast/sls/sls_valuation.h

@@ -60,13 +60,27 @@ namespace bv {
             return bw;
         }
 
+        void set_zero()  {
+            for (unsigned i = 0; i < nw; ++i)
+                (*this)[i] = 0;
+        }
+
+        bvect& set_shift_right(bvect const& a, bvect const& b);
+        bvect& set_shift_right(bvect const& a, unsigned shift);
+        bvect& set_shift_left(bvect const& a, bvect const& b);
+
         rational get_value(unsigned nw) const;
 
+        unsigned to_nat(unsigned max_n) const;
+
+
         friend bool operator==(bvect const& a, bvect const& b);
         friend bool operator<(bvect const& a, bvect const& b);
         friend bool operator>(bvect const& a, bvect const& b);
         friend bool operator<=(bvect const& a, bvect const& b);
         friend bool operator>=(bvect const& a, bvect const& b);
+        friend bool operator<=(digit_t a, bvect const& b);
+        friend bool operator<=(bvect const& a, digit_t b);
         friend std::ostream& operator<<(std::ostream& out, bvect const& v);
 
     private:
@@ -96,11 +110,10 @@ namespace bv {
     protected:
         bvect m_bits;
         bvect m_lo, m_hi;        // range assignment to bit-vector, as wrap-around interval
+        bvect m_tmp;
         unsigned m_signed_prefix = 0;
 
         unsigned mask;
-        bool round_up(bvect& dst) const;
-        bool round_down(bvect& dst) const;
 
         void repair_sign_bits(bvect& dst) const;
 
@@ -111,6 +124,7 @@ namespace bv {
         bvect fixed;                     // bit assignment and don't care bit
         bvect eval;                      // current evaluation
 
+
         sls_valuation(unsigned bw);
 
         void set_bw(unsigned bw);
@@ -127,9 +141,11 @@ namespace bv {
             SASSERT(in_range(m_bits));
             if (fixed.get(i) && get_bit(i) != b)
                 return false;
+            m_bits.set(i, b);   
             eval.set(i, b);
             if (in_range(m_bits))
                 return true;
+            m_bits.set(i, !b);
             eval.set(i, !b);
             return false;
         }
@@ -141,6 +157,9 @@ namespace bv {
         rational lo() const { return m_lo.get_value(nw); }
         rational hi() const { return m_hi.get_value(nw); }
 
+        unsigned diff_index(bvect const& a) const;
+        void inf_feasible(bvect& a) const;
+        void sup_feasible(bvect& a) const;
 
         void get(bvect& dst) const;
         void add_range(rational lo, rational hi);
@@ -198,6 +217,8 @@ namespace bv {
         // most significant bit or bw if src = 0
         unsigned msb(bvect const& src) const;
 
+        unsigned clz(bvect const& src) const;
+
         bool is_power_of2(bvect const& src) const;
 
         // retrieve largest number at or below (above) src which is feasible
@@ -205,19 +226,21 @@ namespace bv {
         bool get_at_most(bvect const& src, bvect& dst) const;
         bool get_at_least(bvect const& src, bvect& dst) const;
 
-        bool set_random_at_most(bvect const& src, bvect& tmp, random_gen& r);
-        bool set_random_at_least(bvect const& src, bvect& tmp, random_gen& r);
-        bool set_random_in_range(bvect const& lo, bvect const& hi, bvect& tmp, random_gen& r);
+        bool set_random_at_most(bvect const& src, random_gen& r);
+        bool set_random_at_least(bvect const& src, random_gen& r);
+        bool set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r);
 
         bool set_repair(bool try_down, bvect& dst);
         void set_random_above(bvect& dst, random_gen& r);
         void set_random_below(bvect& dst, random_gen& r);
+        bool set_random(random_gen& r);
         void round_down(bvect& dst, std::function<bool(bvect const&)> const& is_feasible);
         void round_up(bvect& dst, std::function<bool(bvect const&)> const& is_feasible);
 
 
         static digit_t random_bits(random_gen& r);
         void get_variant(bvect& dst, random_gen& r) const;
+        
 
         bool try_set(bvect const& src) {
             if (!can_set(src))
@@ -232,7 +255,7 @@ namespace bv {
             clear_overflow_bits(eval);
         }
 
-        void set_zero(bvect& out) const {
+        void set_zero(bvect& out) const {            
             for (unsigned i = 0; i < nw; ++i)
                 out[i] = 0;
         }
@@ -258,6 +281,17 @@ namespace bv {
             }
         }
 
+        void add1(bvect& out) const {
+            for (unsigned i = 0; i < bw; ++i) {
+                if (!out.get(i)) {
+                    out.set(i, true);
+                    return;
+                }
+                else
+                    out.set(i, false);
+            }
+        }
+
         void set_sub(bvect& out, bvect const& a, bvect const& b) const;
         bool set_add(bvect& out, bvect const& a, bvect const& b) const;
         bool set_mul(bvect& out, bvect const& a, bvect const& b, bool check_overflow = true) const;
@@ -288,7 +322,7 @@ namespace bv {
                 dst[i] = src[i];
         }
 
-        unsigned to_nat(unsigned max_n);
+        unsigned to_nat(unsigned max_n) const;
 
         std::ostream& display(std::ostream& out) const {
             out << m_bits;

src/cmd_context/cmd_context.cpp

@@ -1894,6 +1894,8 @@ void cmd_context::add_declared_functions(model& mdl) {
     model_params p;
     if (!p.user_functions())
         return;
+    if (m_params.m_smtlib2_compliant)
+        return;
     for (auto const& kv : m_func_decls) {
         func_decl* f = kv.m_value.first();
         if (f->get_family_id() == null_family_id && !mdl.has_interpretation(f)) {
@@ -2066,7 +2068,10 @@ void cmd_context::complete_model(model_ref& md) const {
                 
             if (m_macros.find(k, decls)) 
                 body = decls.find(f->get_arity(), f->get_domain());
+            if (body && m_params.m_smtlib2_compliant)
+                continue;
             sort * range = f->get_range();
+            
             if (!body)
                 body = m().get_some_value(range);
             if (f->get_arity() > 0) {

src/math/lp/lar_solver.h

@@ -393,6 +393,7 @@ public:
     bool external_is_used(unsigned) const;
     void pop(unsigned k);
     unsigned num_scopes() const { return m_trail.get_num_scopes(); }
+    trail_stack& trail() { return m_trail; }
     bool compare_values(lpvar j, lconstraint_kind kind, const mpq& right_side);
     lpvar add_term(const vector<std::pair<mpq, lpvar>>& coeffs, unsigned ext_i);
     void register_existing_terms();

src/math/lp/nla_core.cpp

@@ -1062,6 +1062,8 @@ new_lemma::~new_lemma() {
     if (current().is_conflict()) {
         c.m_conflicts++;
     }
+    IF_VERBOSE(4, verbose_stream() << name << "\n");
+    IF_VERBOSE(4, verbose_stream() << *this << "\n");
     TRACE("nla_solver", tout << name << " " << (++i) << "\n" << *this; );
 }
 
@@ -1519,6 +1521,7 @@ lbool core::check() {
         if (!m_lemmas.empty() || !m_literals.empty() || m_check_feasible)
             return l_false;
     }
+
     
     if (no_effect() && should_run_bounded_nlsat()) 
         ret = bounded_nlsat();
@@ -1530,12 +1533,16 @@ lbool core::check() {
         m_basics.basic_lemma(false);
 
     if (no_effect()) 
-        m_divisions.check();    
+        m_divisions.check();
+
 
     if (no_effect()) {
-        std::function<void(void)> check1 = [&]() { m_order.order_lemma(); };
-        std::function<void(void)> check2 = [&]() { m_monotone.monotonicity_lemma(); };
-        std::function<void(void)> check3 = [&]() { m_tangents.tangent_lemma(); };
+        std::function<void(void)> check1 = [&]() { m_order.order_lemma();
+        };
+        std::function<void(void)> check2 = [&]() { m_monotone.monotonicity_lemma();
+        };
+        std::function<void(void)> check3 = [&]() { m_tangents.tangent_lemma();
+        };
         
         std::pair<unsigned, std::function<void(void)>> checks[] = 
             { { 6, check1 }, 

src/math/lp/nra_solver.cpp

@@ -3,6 +3,10 @@
   Author: Nikolaj Bjorner, Lev Nachmanson
 */
 
+#ifndef SINGLE_THREAD
+#include <thread>
+#endif
+#include <fstream>
 #include "math/lp/lar_solver.h"
 #include "math/lp/nra_solver.h"
 #include "nlsat/nlsat_solver.h"
@@ -11,6 +15,7 @@
 #include "util/map.h"
 #include "util/uint_set.h"
 #include "math/lp/nla_core.h"
+#include "smt/params/smt_params_helper.hpp"
 
 
 namespace nra {
@@ -157,6 +162,23 @@ struct solver::imp {
 
         TRACE("nra", m_nlsat->display(tout));
 
+        smt_params_helper p(m_params);
+        if (p.arith_nl_log()) {
+            static unsigned id = 0;
+            std::stringstream strm;
+
+#ifndef SINGLE_THREAD            
+            std::thread::id this_id = std::this_thread::get_id();
+            strm << "nla_" << this_id << "." << (++id) << ".smt2";
+#else
+            strm << "nla_" << (++id) << ".smt2";
+#endif
+            std::ofstream out(strm.str());
+            m_nlsat->display_smt2(out);
+            out << "(check-sat)\n";
+            out.close();
+        }
+
         lbool r = l_undef;
         try {
             r = m_nlsat->check();

src/math/polynomial/algebraic_numbers.cpp

@@ -2601,6 +2601,7 @@ namespace algebraic_numbers {
                 qm().dec(v);
             }
             else {
+                refine_until_prec(const_cast<numeral&>(a), 1);
                 bqm().floor(qm(), lower(a.to_algebraic()), v);
             }
             m_wrapper.set(b, v);
@@ -2613,6 +2614,7 @@ namespace algebraic_numbers {
                 qm().inc(v);
             }
             else {
+                refine_until_prec(const_cast<numeral&>(a), 1);
                 bqm().ceil(qm(), upper(a.to_algebraic()), v);
             }
             m_wrapper.set(b, v);

src/math/polynomial/polynomial.cpp

@@ -190,6 +190,10 @@ namespace polynomial {
             }
         };
 
+        bool operator==(monomial const& other) const {
+            return eq_proc()(this, &other);
+        }
+
         static unsigned get_obj_size(unsigned sz) { return sizeof(monomial) + sz * sizeof(power); }
         
         monomial(unsigned id, unsigned sz, power const * pws, unsigned h):
@@ -3221,9 +3225,16 @@ namespace polynomial {
         };
 
         bool_vector  m_found_vars;
-        void vars(polynomial const * p, var_vector & xs) {
-            xs.reset();
+        void begin_vars_incremental() {
             m_found_vars.reserve(num_vars(), false);
+        }
+        void end_vars_incremental(var_vector& xs) {
+            // reset m_found_vars
+            unsigned sz = xs.size();
+            for (unsigned i = 0; i < sz; i++)
+                m_found_vars[xs[i]] = false;
+        }
+        void vars(polynomial const * p, var_vector & xs) {
             unsigned sz = p->size();
             for (unsigned i = 0; i < sz; i++) {
                 monomial * m = p->m(i);
@@ -3236,10 +3247,6 @@ namespace polynomial {
                     }
                 }
             }
-            // reset m_found_vars
-            sz = xs.size();
-            for (unsigned i = 0; i < sz; i++)
-                m_found_vars[xs[i]] = false;
         }
 
         typedef sbuffer<power, 32>    power_buffer;
@@ -6045,6 +6052,47 @@ namespace polynomial {
             }
             return true;
         }
+       
+        bool ge(polynomial const* p, polynomial const* q) {
+            unsigned sz1 = p->size();
+            unsigned sz2 = q->size();
+            unsigned i = 0, j = 0;
+            while (i < sz1 || j < sz2) {
+                auto * m1 = i < sz1 ? p->m(i) : q->m(j);
+                auto & a1 = i < sz1 ? p->a(i) : q->a(j);
+                auto * m2 = j < sz2 ? q->m(j) : p->m(i);
+                auto & a2 = j < sz2 ? q->a(j) : p->a(i);
+
+                if (i < sz1 && j == sz2 && m1->is_unit()) {
+                    if (!m_manager.is_pos(a1))
+                        return false;
+                    ++i;
+                    continue;
+                }
+
+                if (i == sz1 && j < sz2 && m2->is_unit()) {
+                    if (!m_manager.is_neg(a2))
+                        return false;
+                    ++j;
+                    continue;
+                }
+
+                if (i == sz1 || j == sz2)
+                    break;
+
+                if (!(*m1 == *m2)) {
+                    if (m_manager.is_pos(a1) && m1->is_square()) {
+                        ++i;
+                        continue;
+                    }
+                    return false;
+                }
+                if (!m_manager.ge(a1, a2))
+                    return false;
+                ++i, ++j;               
+            }
+            return i == sz1 && j == sz2;           
+        }
 
         // Functor used to compute the maximal degree of each variable in a polynomial p.
         class var_max_degree {
@@ -6269,6 +6317,27 @@ namespace polynomial {
             return R.mk();
         }        
 
+        // x*q = p
+        // 
+        // md = degree of x in p
+        // P = m0 + ...
+        // m0 = x^dm*m1
+        // m1 * p^dm * q^{md - dm}  
+        // P' = m1 + ...
+        // property would be that x*q = p => P > 0 <=> P' > 0
+        // requires that q > 0
+        // Reasoning:
+        //    P > 0 
+        // <=> { since q > 0 }
+        //    q^md * P > 0
+        // <=>
+        //    q^md*x^dm*m0 + .. > 0
+        // <=>
+        //    q^{md-dm}*(xq)^dm*m0 + ... > 0
+        // <=>
+        //    q^{md-dm}*p^dm + .. > 0
+        // <=>
+        //    P' > 0
         void substitute(polynomial const* r, var x, polynomial const* p, polynomial const* q, polynomial_ref& result) {
             unsigned md = degree(r, x);
             if (md == 0) {
@@ -7228,13 +7297,33 @@ namespace polynomial {
         return m_imp->is_nonneg(p);
     }
 
+    bool manager::ge(polynomial const* p, polynomial const* q) {
+        return m_imp->ge(p, q);
+    }
+
+
     void manager::rename(unsigned sz, var const * xs) {
         return m_imp->rename(sz, xs);
     }
 
     void manager::vars(polynomial const * p, var_vector & xs) {
+        xs.reset();
+        m_imp->begin_vars_incremental();
+        m_imp->vars(p, xs);
+        m_imp->end_vars_incremental(xs);
+    }
+
+    void manager::vars_incremental(polynomial const * p, var_vector & xs) {
         m_imp->vars(p, xs);
     }
+    void manager::begin_vars_incremental() {
+        m_imp->begin_vars_incremental();
+    }
+    
+    void manager::end_vars_incremental(var_vector & xs) {
+        m_imp->end_vars_incremental(xs);        
+    }
+
 
     polynomial * manager::substitute(polynomial const * p, var2mpq const & x2v) {
         return m_imp->substitute(p, x2v);
@@ -7293,17 +7382,20 @@ namespace polynomial {
         return m_imp->eval(p, x2v, r);
     }
 
-    void manager::display(std::ostream & out, monomial const * m, display_var_proc const & proc, bool user_star) const {
+    std::ostream& manager::display(std::ostream & out, monomial const * m, display_var_proc const & proc, bool user_star) const {
         m->display(out, proc, user_star);
+        return out;
     }
 
-    void manager::display(std::ostream & out, polynomial const * p, display_var_proc const & proc, bool use_star) const {
+    std::ostream& manager::display(std::ostream & out, polynomial const * p, display_var_proc const & proc, bool use_star) const {
         SASSERT(m_imp->consistent_coeffs(p));
         p->display(out, m_imp->m_manager, proc, use_star);
+        return out;
     }
 
-    void manager::display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc) const {
+    std::ostream& manager::display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc) const {
         p->display_smt2(out, m_imp->m_manager, proc);
+        return out;
     }
 };
 

src/math/polynomial/polynomial.h

@@ -921,6 +921,13 @@ namespace polynomial {
         */
         bool is_nonneg(polynomial const * p);
 
+
+        /**
+           \brief Return true if p is always greater or equal to q.
+           This is an incomplete check
+        */
+        bool ge(polynomial const* p, polynomial const* q);
+
         /**
            \brief Make sure the monomials in p are sorted using lexicographical order.
            Remark: the maximal monomial is at position 0.
@@ -931,6 +938,9 @@ namespace polynomial {
            \brief Collect variables that occur in p into xs
         */
         void vars(polynomial const * p, var_vector & xs);
+        void vars_incremental(polynomial const * p, var_vector & xs);
+        void begin_vars_incremental();
+        void end_vars_incremental(var_vector & xs);
 
         /**
            \brief Evaluate polynomial p using the assignment [x_1 -> v_1, ..., x_n -> v_n].
@@ -1019,15 +1029,14 @@ namespace polynomial {
         */
         void exact_pseudo_division_mod_d(polynomial const * p, polynomial const * q, var x, var2degree const & x2d, polynomial_ref & Q, polynomial_ref & R);
 
-        void display(std::ostream & out, monomial const * m, display_var_proc const & proc = display_var_proc(), bool use_star = true) const;
+        std::ostream& display(std::ostream & out, monomial const * m, display_var_proc const & proc = display_var_proc(), bool use_star = true) const;
 
-        void display(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc(), bool use_star = false) const;
+        std::ostream& display(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc(), bool use_star = false) const;
 
-        void display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc()) const;
+        std::ostream& display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc()) const;
 
         friend std::ostream & operator<<(std::ostream & out, polynomial_ref const & p) {
-            p.m().display(out, p);
-            return out;
+            return p.m().display(out, p);
         }
     };
 

src/nlsat/nlsat_clause.cpp

@@ -25,7 +25,10 @@ namespace nlsat {
         m_size(sz),
         m_capacity(sz),
         m_learned(learned),
-        m_activity(0),
+        m_active(false),
+        m_removed(false),
+        m_marked(false),
+        m_var_hash(0),
         m_assumptions(as) {
         for (unsigned i = 0; i < sz; i++) {
             m_lits[i] = lits[i];

src/nlsat/nlsat_clause.h

@@ -29,7 +29,10 @@ namespace nlsat {
         unsigned         m_size;
         unsigned         m_capacity:31;
         unsigned         m_learned:1;
-        unsigned         m_activity;
+        unsigned         m_active:1;
+        unsigned         m_removed:1;
+        unsigned         m_marked:1;
+        unsigned         m_var_hash;
         assumption_set   m_assumptions;
         literal          m_lits[0];
         static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); }
@@ -46,9 +49,15 @@ namespace nlsat {
         literal const * begin() const { return m_lits; }
         literal const * end() const { return m_lits + m_size; }
         literal const * data() const { return m_lits; }
-        void inc_activity() { m_activity++; }
-        void set_activity(unsigned v) { m_activity = v; }
-        unsigned get_activity() const { return m_activity; }
+        void set_active(bool b) { m_active = b; }
+        bool is_active() const { return m_active; }
+        void set_removed() { m_removed = true; }
+        bool is_removed() const { return m_removed; }
+        unsigned var_hash() const { return m_var_hash; }
+        void set_var_hash(unsigned h) { m_var_hash = h; }
+        bool is_marked() const { return m_marked; }
+        void mark() { m_marked = true; }
+        void unmark() { m_marked = false; }
         bool contains(literal l) const;
         bool contains(bool_var v) const;
         void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; } }

src/nlsat/nlsat_explain.cpp

@@ -277,11 +277,14 @@ namespace nlsat {
             }
             
         };
-        void add_zero_assumption(polynomial_ref & p) {
+
+        void add_zero_assumption(polynomial_ref& p) {
             // If p is of the form p1^n1 * ... * pk^nk,
             // then only the factors that are zero in the current interpretation needed to be considered.
             // I don't want to create a nested conjunction in the clause. 
             // Then, I assert p_i1 * ... * p_im  != 0
+            bool is_linear = true;
+            unsigned x = max_var(p);
             {
                 restore_factors _restore(m_factors, m_factors_save);
                 factor(p, m_factors);
@@ -294,10 +297,33 @@ namespace nlsat {
                     if (is_zero(sign(f))) {
                         m_zero_fs.push_back(m_factors.get(i));
                         m_is_even.push_back(false);
-                    } 
+                        is_linear &= m_pm.degree(f, x) <= 1;
+                    }
+                }
+            }
+
+            if (!is_linear) {
+                scoped_anum_vector& roots = m_roots_tmp;
+                roots.reset();
+                m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
+                unsigned num_roots = roots.size();
+                if (num_roots > 0) {
+                    anum const& x_val = m_assignment.value(x);
+                    for (unsigned i = 0; i < num_roots; i++) {
+                        int s = m_am.compare(x_val, roots[i]);
+                        if (s != 0)
+                            continue;
+                        TRACE("nlsat_explain", tout << "adding (zero assumption) root " << "\n");
+                        add_root_literal(atom::ROOT_EQ, x, i + 1, p);
+                        return;
+                    }
+                    display(verbose_stream() << "polynomial ", p);
+                    m_solver.display(verbose_stream());
+                    UNREACHABLE();
                 }
             }
             SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it.
+
             literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data());
             l.neg();
             TRACE("nlsat_explain", tout << "adding (zero assumption) literal:\n"; display(tout, l); tout << "\n";);
@@ -649,6 +675,52 @@ namespace nlsat {
             }
         }
 
+        void add_zero_assumption_on_factor(polynomial_ref& f) {
+            display(std::cout << "zero factors \n", f); 
+        }
+        // this function also explains the value 0, if met
+        bool coeffs_are_zeroes(polynomial_ref &s) {
+            restore_factors _restore(m_factors, m_factors_save);
+            factor(s, m_factors);
+            unsigned num_factors = m_factors.size();
+            m_zero_fs.reset();
+            m_is_even.reset();
+            polynomial_ref f(m_pm);
+            bool have_zero = false;
+            for (unsigned i = 0; i < num_factors; i++) {
+                f = m_factors.get(i);
+              //  std::cout << "f=";display(std::cout, f) << "\n";
+                if (coeffs_are_zeroes_in_factor(f)) {
+                    have_zero = true;
+                    break;
+                } 
+            }
+            if (!have_zero)
+                return false;
+            var x = max_var(f);
+            unsigned n = degree(f, x);
+            auto c = polynomial_ref(this->m_pm);
+            for (unsigned j = 0; j <= n; j++) {
+                c = m_pm.coeff(s, x, j);
+                SASSERT(sign(c) == 0);
+                ensure_sign(c);
+            }
+            return true;
+        }
+    
+
+        bool coeffs_are_zeroes_in_factor(polynomial_ref & s) {
+            var x = max_var(s);
+            unsigned n = degree(s, x);
+            auto c = polynomial_ref(this->m_pm);
+            for (unsigned j = 0; j <= n; j++) {
+                c = m_pm.coeff(s, x, j);
+                if (sign(c) != 0)
+                    return false;
+            }
+            return true;
+        }
+
         /**
            \brief Add v-psc(p, q, x) into m_todo
         */
@@ -1022,12 +1094,12 @@ namespace nlsat {
             if (x < max_x)
                 add_cell_lits(ps, x);
             while (true) {
+                TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
+                      display(tout, ps); tout << "\n";);
                 if (all_univ(ps, x) && m_todo.empty()) {
                     m_todo.reset();
                     break;
                 }
-                TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
-                      display(tout, ps); tout << "\n";);
                 add_lc(ps, x);
                 psc_discriminant(ps, x);
                 psc_resultant(ps, x);
@@ -1672,7 +1744,16 @@ namespace nlsat {
                     solve_eq(x, eq_index, ps);
                 }
                 else {
-                    project_pairs(x, eq_index, ps);
+                    add_zero_assumption(p);
+
+                    for (unsigned j = 0; j < ps.size(); ++j) {
+                        if (j == eq_index)
+                            continue;
+                        p = ps.get(j);
+                        int s = sign(p);
+                        atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT));
+                        add_simple_assumption(k, p, false);
+                    }
                 }
                 return;
             }

src/nlsat/nlsat_solver.h

@@ -254,6 +254,8 @@ namespace nlsat {
 
         std::ostream& display_smt2(std::ostream & out, literal_vector const& ls) const;
 
+                std::ostream& display_smt2(std::ostream & out) const;
+
 
         /**
            \brief Display variable

src/params/sls_params.pyg

@@ -3,6 +3,7 @@ def_module_params('sls',
                   description='Experimental Stochastic Local Search Solver (for QFBV only).',
                   params=(max_memory_param(),
                         ('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'),
+			('max_repairs', UINT, 1000, 'maximum number of repairs before restart'),
                         ('walksat', BOOL, 1, 'use walksat assertion selection (instead of gsat)'),
                         ('walksat_ucb', BOOL, 1, 'use bandit heuristic for walksat assertion selection (instead of random)'),
                         ('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'),

src/qe/nlqsat.cpp

@@ -480,8 +480,10 @@ namespace qe {
                 num_scopes = 2*(level()/2);
             }
             else {
-                SASSERT(clevel.max() + 2 <= level());
-                num_scopes = level() - clevel.max();
+                if (clevel.max() + 2 <= level())                    
+                    num_scopes = level() - clevel.max();
+                else
+                    num_scopes = 2; // the projection contains auxiliary variables from root objects.
                 SASSERT(num_scopes >= 2);
             }
             

src/sat/sat_solver.cpp

@@ -1314,7 +1314,7 @@ namespace sat {
     }
 
     bool solver::should_cancel() {
-        if (limit_reached() || memory_exceeded()) {
+        if (limit_reached() || memory_exceeded() || m_solver_canceled) {
             return true;
         }
         if (m_config.m_restart_max <= m_restarts) {
@@ -1959,6 +1959,7 @@ namespace sat {
 
     void solver::init_search() {
         m_model_is_current        = false;
+        m_solver_canceled         = false;
         m_phase_counter           = 0;
         m_search_state            = s_unsat;
         m_search_unsat_conflicts  = m_config.m_search_unsat_conflicts;

src/sat/sat_solver.h

@@ -177,6 +177,7 @@ namespace sat {
         clause_wrapper_vector   m_clauses_to_reinit;
         std::string             m_reason_unknown;
         bool                    m_trim = false;
+        bool                    m_solver_canceled = false;
 
         visit_helper            m_visited;
 
@@ -287,6 +288,7 @@ namespace sat {
         random_gen& rand() { return m_rand; }
 
         void set_trim() { m_trim = true; }
+        void set_canceled() { m_solver_canceled = true; }
 
     protected:
         void reset_var(bool_var v, bool ext, bool dvar);

src/sat/sat_solver/sat_smt_solver.cpp

@@ -197,10 +197,16 @@ public:
         case l_false:
             extract_core();
             break;
-        default:
+        default: {
+            auto* ext = get_euf();
+            if (ext && ext->get_sls_model()) {
+                r = l_true;
+                break;
+            }
             set_reason_unknown(m_solver.get_reason_unknown());
             break;
         }
+        }
         return r;
     }
 
@@ -576,6 +582,7 @@ private:
     void add_assumption(expr* a) {
         init_goal2sat();
         m_dep.insert(a, m_goal2sat.internalize(a));
+        get_euf()->add_assertion(a);
     }
 
     void internalize_assumptions(expr_ref_vector const& asms) {     
@@ -632,6 +639,11 @@ private:
     void get_model_core(model_ref & mdl) override {
         TRACE("sat", tout << "retrieve model " << (m_solver.model_is_current()?"present":"absent") << "\n";);
         mdl = nullptr;
+        auto ext = get_euf();
+        if (ext)
+            mdl = ext->get_sls_model();
+        if (mdl)
+            return;
         if (!m_solver.model_is_current()) 
             return;
         if (m_fmls.size() > m_qhead)

src/sat/smt/euf_internalize.cpp

@@ -525,4 +525,8 @@ namespace euf {
         return n;
     }
 
+    void solver::add_assertion(expr* f) {
+        m_assertions.push_back(f);
+        m_trail.push(push_back_vector(m_assertions));
+    }
 }

src/sat/smt/euf_model.cpp

@@ -18,6 +18,7 @@ Author:
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "sat/smt/euf_solver.h"
+#include "sat/smt/sls_solver.h"
 #include "model/value_factory.h"
 
 namespace euf {
@@ -67,6 +68,14 @@ namespace euf {
         m_qmodel = mdl;
     }
 
+    model_ref solver::get_sls_model() {
+        model_ref mdl;
+        auto s = get_solver(m.mk_family_id("sls"), nullptr);
+        if (s)
+            mdl = dynamic_cast<sls::solver*>(s)->get_model();
+        return mdl;
+    }
+
     void solver::update_model(model_ref& mdl, bool validate) {
         TRACE("model", tout << "create model\n";);
         if (m_qmodel) {
@@ -318,7 +327,7 @@ namespace euf {
         out << mdl << "\n";
     }
 
-    void solver::validate_model(model& mdl) {
+    void solver::validate_model(model& mdl) {       
         if (!m_unhandled_functions.empty())
             return;
         if (get_config().m_arith_ignore_int)

src/sat/smt/euf_solver.cpp

@@ -29,6 +29,7 @@ Author:
 #include "sat/smt/q_solver.h"
 #include "sat/smt/fpa_solver.h"
 #include "sat/smt/dt_solver.h"
+#include "sat/smt/sls_solver.h"
 #include "sat/smt/recfun_solver.h"
 #include "sat/smt/specrel_solver.h"
 
@@ -55,6 +56,7 @@ namespace euf {
         m_smt_proof_checker(m, p),
         m_clause(m),       
         m_expr_args(m),
+        m_assertions(m),
         m_values(m)
     {
         updt_params(p);
@@ -78,6 +80,7 @@ namespace euf {
             };
             m_egraph.set_on_merge(on_merge);
         }
+        
     }
 
     void solver::updt_params(params_ref const& p) {
@@ -186,7 +189,9 @@ namespace euf {
         IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
     }
 
-    void solver::init_search() {        
+    void solver::init_search() {   
+        if (get_config().m_sls_enable)
+            add_solver(alloc(sls::solver, *this));
         TRACE("before_search", s().display(tout););
         m_reason_unknown.clear();
         for (auto* s : m_solvers)
@@ -218,7 +223,7 @@ namespace euf {
         mark_relevant(lit);
         s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
     }
-
+    
     lbool solver::resolve_conflict() {
         for (auto* s : m_solvers) {
             lbool r = s->resolve_conflict();
@@ -665,7 +670,9 @@ namespace euf {
         if (give_up)
             return sat::check_result::CR_GIVEUP;  
         if (m_qsolver && m_config.m_arith_ignore_int)
-            return sat::check_result::CR_GIVEUP;            
+            return sat::check_result::CR_GIVEUP; 
+        for (auto s : m_solvers)
+            s->finalize();
         return sat::check_result::CR_DONE;
     }
 

src/sat/smt/euf_solver.h

@@ -154,6 +154,7 @@ namespace euf {
         svector<scope>                   m_scopes;
         scoped_ptr_vector<th_solver>     m_solvers;
         ptr_vector<th_solver>            m_id2solver;
+        
 
         constraint* m_conflict = nullptr;
         constraint* m_eq = nullptr;
@@ -173,6 +174,7 @@ namespace euf {
         symbol                           m_smt = symbol("smt");            
         expr_ref_vector                  m_clause;
         expr_ref_vector                  m_expr_args;
+        expr_ref_vector                  m_assertions;
 
 
         // internalization
@@ -482,6 +484,10 @@ namespace euf {
         bool enable_ackerman_axioms(expr* n) const;
         bool is_fixed(euf::enode* n, expr_ref& val, sat::literal_vector& explain);
 
+        void add_assertion(expr* f);
+        expr_ref_vector const& get_assertions() { return m_assertions; }
+        model_ref get_sls_model();
+
         // relevancy
 
         bool relevancy_enabled() const { return m_relevancy.enabled(); }

src/sat/smt/intblast_solver.cpp

@@ -50,6 +50,7 @@ namespace intblast {
         sat::literal lit = expr2literal(e);
         if (sign)
             lit.neg();
+        TRACE("bv", tout << mk_pp(e, m) << " -> " << literal2expr(lit) << "\n");
         return lit;
     }
 
@@ -102,6 +103,7 @@ namespace intblast {
             set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0)));
         }
         m_preds.push_back(e);
+        TRACE("bv", tout << mk_pp(e, m) << " " << mk_pp(translated(e), m) << "\n");
         ctx.push(push_back_vector(m_preds));
     }
 
@@ -476,6 +478,8 @@ namespace intblast {
                     continue;
                 if (sib->get_arg(0)->get_root() == r1)
                     continue;
+                if (bv.get_bv_size(r1->get_expr()) != bv.get_bv_size(sib->get_arg(0)->get_expr()))
+                    continue;
                 auto a = eq_internalize(n, sib);
                 auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
                 ctx.mark_relevant(a);
@@ -626,12 +630,12 @@ namespace intblast {
     }
 
     void solver::translate_quantifier(quantifier* q) {
-        if (is_lambda(q))
-            throw default_exception("lambdas are not supported in intblaster");
         if (m_is_plugin) {
             set_translated(q, q);
             return;
         }
+        if (is_lambda(q))
+            throw default_exception("lambdas are not supported in intblaster");
         expr* b = q->get_expr();
         unsigned nd = q->get_num_decls();
         ptr_vector<sort> sorts;
@@ -642,7 +646,6 @@ namespace intblast {
                 sorts.push_back(a.mk_int());
             }
             else
-
                 sorts.push_back(s);
         }
         b = translated(b);
@@ -767,6 +770,7 @@ namespace intblast {
             r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1));
             break;
         case OP_SGEQ:
+            bv_expr = e->get_arg(0);
             r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1));
             break;
         case OP_SLT:
@@ -815,13 +819,13 @@ namespace intblast {
         case OP_BUREM:
         case OP_BUREM_I: {
             expr* x = umod(e, 0), * y = umod(e, 1);
-            r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, a.mk_mod(x, y));
+            r = if_eq(y, 0, x, a.mk_mod(x, y));
             break;
         }
         case OP_BUDIV:
         case OP_BUDIV_I: {
-            expr* x = arg(0), * y = umod(e, 1);
-            r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(-1), a.mk_idiv(x, y));
+            expr* x = umod(e, 0), * y = umod(e, 1);
+            r = if_eq(y, 0, a.mk_int(-1), a.mk_idiv(x, y));
             break;
         }
         case OP_BUMUL_NO_OVFL: {
@@ -863,7 +867,7 @@ namespace intblast {
                 r = a.mk_int(0);
                 IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
                 for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
-                    r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), mul(x, a.mk_int(rational::power_of_two(i))), r);   
+                    r = if_eq(y, i, mul(x, a.mk_int(rational::power_of_two(i))), r);   
             }
             break;
         }
@@ -878,7 +882,7 @@ namespace intblast {
                 r = a.mk_int(0);
                 IF_VERBOSE(2, verbose_stream() << "lshr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
                 for (unsigned i = 0; i < bv.get_bv_size(e); ++i)
-                    r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
+                    r = if_eq(y, i, a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r);
             }
             break;
         case OP_BASHR: 
@@ -899,20 +903,19 @@ namespace intblast {
                 IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
                 for (unsigned i = 0; i < sz; ++i) {
                     expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i)));              
-                    r = m.mk_ite(m.mk_eq(y, a.mk_int(i)),
+                    r = if_eq(y, i,
                                  m.mk_ite(signx, add(d, a.mk_int(- rational::power_of_two(sz-i))), d),
                                  r);
                 }
             }
             break;
-        case OP_BOR: {
+        case OP_BOR: 
             // p | q := (p + q) - band(p, q)
             IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n");
             r = arg(0);
             for (unsigned i = 1; i < args.size(); ++i)
                 r = a.mk_sub(add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i)));
-            break;
-        }
+            break;        
         case OP_BNAND:
             r = bnot(band(args));
             break;
@@ -982,8 +985,8 @@ namespace intblast {
             r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), add(u, y), r);
             r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r);
             r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r);
-            r = m.mk_ite(m.mk_eq(u, a.mk_int(0)), a.mk_int(0), r);
-            r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
+            r = if_eq(u, 0, a.mk_int(0), r);
+            r = if_eq(y, 0, x, r);
             break;
         } 
         case OP_BSDIV_I:
@@ -1004,7 +1007,7 @@ namespace intblast {
             y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
             expr* d = a.mk_idiv(x, y);
             r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
-            r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r);
+            r = if_eq(y, 0, m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r);
             break;
         }
         case OP_BSREM_I:
@@ -1020,7 +1023,7 @@ namespace intblast {
             expr* d = a.mk_idiv(absx, absy);
             d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
             r = a.mk_sub(x, mul(d, y));
-            r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r);
+            r = if_eq(y, 0, x, r);
             break;  
         }
         case OP_ROTATE_LEFT: {
@@ -1039,7 +1042,7 @@ namespace intblast {
             expr* y = umod(e, 1);
             r = a.mk_int(0);
             for (unsigned i = 0; i < sz; ++i) 
-                r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r);
+                r = if_eq(y, i, rotate_left(i), r);
             break;
         }
         case OP_EXT_ROTATE_RIGHT: {
@@ -1047,7 +1050,7 @@ namespace intblast {
             expr* y = umod(e, 1);
             r = a.mk_int(0);
             for (unsigned i = 0; i < sz; ++i) 
-                r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r);
+                r = if_eq(y, i, rotate_left(sz - i), r);
             break;
         }
         case OP_REPEAT: {
@@ -1078,6 +1081,18 @@ namespace intblast {
         set_translated(e, r);
     }
 
+    expr_ref solver::if_eq(expr* n, unsigned k, expr* th, expr* el) {
+        rational r;
+        expr_ref _th(th, m), _el(el, m);
+        if (bv.is_numeral(n, r)) {
+            if (r == k)
+                return expr_ref(th, m);
+            else
+                return expr_ref(el, m);
+        }
+        return expr_ref(m.mk_ite(m.mk_eq(n, a.mk_int(k)), th, el), m);
+    }
+
     void solver::translate_basic(app* e) {
         if (m.is_eq(e)) {
             bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); });
@@ -1136,7 +1151,7 @@ namespace intblast {
         if (e->get_family_id() != bv.get_family_id())
             return false;
         for (euf::enode* arg : euf::enode_args(n))
-            dep.add(n, arg->get_root());
+            dep.add(n, arg);
         return true;
     }
 
@@ -1191,6 +1206,27 @@ namespace intblast {
         TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n");
     }
 
+    void solver::finalize_model(model& mdl) {
+        return;
+        for (auto n : ctx.get_egraph().nodes()) {
+            auto e = n->get_expr();            
+            if (!is_translated(e))
+                continue;
+            if (!bv.is_bv(e))
+                continue;
+            auto t = translated(e);
+            
+            expr_ref ei(bv.mk_bv2int(e), m);
+            expr_ref ti(a.mk_mod(t, a.mk_int(rational::power_of_two(bv.get_bv_size(e)))), m);
+            auto ev = mdl(ei);
+            auto tv = mdl(ti);
+            if (ev != tv) {
+                IF_VERBOSE(0, verbose_stream() << mk_pp(e, m) << " <- " << ev << "\n");
+                IF_VERBOSE(0, verbose_stream() << mk_pp(t, m) << " <- " << tv << "\n");
+            }
+        }
+    }
+
     sat::literal_vector const& solver::unsat_core() {
         return m_core;
     }

src/sat/smt/intblast_solver.h

@@ -77,6 +77,7 @@ namespace intblast {
         bool is_non_negative(expr* bv_expr, expr* e);
         expr_ref mul(expr* x, expr* y);
         expr_ref add(expr* x, expr* y);
+        expr_ref if_eq(expr* n, unsigned k, expr* th, expr* el);
         expr* amod(expr* bv_expr, expr* x, rational const& N);
         rational bv_size(expr* bv_expr);
 
@@ -147,6 +148,7 @@ namespace intblast {
 
         rational get_value(expr* e) const;
 
+        void finalize_model(model& mdl) override;
     };
 
 }

src/sat/smt/sat_th.h

@@ -148,6 +148,8 @@ namespace euf {
 
         virtual void set_bounds(enode* n) {}
 
+        virtual void finalize() {}
+
     };
 
     class th_proof_hint : public sat::proof_hint {
@@ -223,6 +225,7 @@ namespace euf {
         void push() override { m_num_scopes++; }
         void pop(unsigned n) override;
 
+
         unsigned random();
     };
 

src/sat/smt/sls_solver.cpp

@@ -22,109 +22,145 @@ Author:
 
 namespace sls {
 
+#ifdef SINGLE_THREAD
+
+    solver::solver(euf::solver& ctx) :
+        th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls"))
+        {}
+
+#else
     solver::solver(euf::solver& ctx):
-        th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls")) {}
+        th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls"))
+        {}
 
     solver::~solver() {
-        if (m_bvsls) {
-            m_bvsls->cancel();            
+        finalize();
+    }
+
+    void solver::finalize() {
+        if (!m_completed && m_sls) {
+            m_sls->cancel();
             m_thread.join();
+            m_sls->collect_statistics(m_st);
+            m_sls = nullptr;
+            m_shared = nullptr;
+            m_slsm = nullptr;
+            m_units = nullptr;
         }
     }
 
-    void solver::push_core() {
-        if (s().scope_lvl() == s().search_lvl() + 1)
-            init_local_search();
+    sat::check_result solver::check() { 
+        return sat::check_result::CR_DONE; 
     }
-    
+
+    bool solver::unit_propagate() {
+        force_push();
+        sample_local_search();
+        return false;
+    }
+
+    bool solver::is_unit(expr* e) {
+        if (!e)
+            return false;
+        m.is_not(e, e);
+        if (is_uninterp_const(e))
+            return true;
+        bv_util bu(m);
+        expr* s;
+        if (bu.is_bit2bool(e, s))
+            return is_uninterp_const(s);
+        return false;
+    }
+
     void solver::pop_core(unsigned n) {
-        if (s().scope_lvl() - n <= s().search_lvl())
-            sample_local_search();
-    }
-
-    void solver::simplify() {
-    
-    }
-        
-
-    void solver::init_local_search() {
-        if (m_bvsls) {
-            m_bvsls->cancel();
-            m_thread.join();
-            if (m_result == l_true) {
-                verbose_stream() << "Found model using local search - INIT\n";
-                exit(1);
+        for (; m_trail_lim < s().init_trail_size(); ++m_trail_lim) {
+            auto lit = s().trail_literal(m_trail_lim);
+            auto e = ctx.literal2expr(lit);
+            if (is_unit(e)) {
+                // IF_VERBOSE(1, verbose_stream() << "add unit " << mk_pp(e, m) << "\n");
+                std::lock_guard<std::mutex> lock(m_mutex);
+                ast_translation tr(m, *m_shared);
+                m_units->push_back(tr(e.get()));
+                m_has_units = true;
             }
         }
+    }       
+
+    void solver::init_search() {
+        if (m_sls) {
+            m_sls->cancel();
+            m_thread.join();
+            m_result = l_undef;
+            m_completed = false;
+            m_has_units = false;
+            m_model = nullptr;
+            m_units = nullptr;
+        }
         // set up state for local search solver here
 
-        m_m = alloc(ast_manager, m);
-        ast_translation tr(m, *m_m);
+        m_shared = alloc(ast_manager);
+        m_slsm = alloc(ast_manager);
+        m_units = alloc(expr_ref_vector, *m_shared);
+        ast_translation tr(m, *m_slsm);
         
         m_completed = false;
         m_result = l_undef;
-        m_bvsls = alloc(bv::sls, *m_m);
-        // walk clauses, add them
-        // walk trail stack until search level, add units
-        // encapsulate bvsls within the arguments of run-local-search.
-        // ensure bvsls does not touch ast-manager.
+        m_model = nullptr;
+        m_sls = alloc(bv::sls, *m_slsm, s().params());
+        
+        for (expr* a : ctx.get_assertions())
+            m_sls->assert_expr(tr(a));
 
-        unsigned trail_sz = s().trail_size();
-        for (unsigned i = 0; i < trail_sz; ++i) {
-            auto lit = s().trail_literal(i);
-            if (s().lvl(lit) > s().search_lvl())
-                break;
-            expr_ref fml = literal2expr(lit);
-            m_bvsls->assert_expr(tr(fml.get()));
-        }
-        unsigned num_vars = s().num_vars();
-        for (unsigned i = 0; i < 2*num_vars; ++i) {
-            auto l1 = ~sat::to_literal(i);
-            auto const& wlist = s().get_wlist(l1);
-            for (sat::watched const& w : wlist) {
-                if (!w.is_binary_non_learned_clause())
-                    continue;
-                sat::literal l2 = w.get_literal();
-                if (l1.index() > l2.index())
-                    continue;
-                expr_ref fml(m.mk_or(literal2expr(l1), literal2expr(l2)), m);
-                m_bvsls->assert_expr(tr(fml.get()));
-            }
-        }
-        for (auto clause : s().clauses()) {
-            expr_ref_vector cls(m);
-            for (auto lit : *clause)
-                cls.push_back(literal2expr(lit));
-            expr_ref fml(m.mk_or(cls), m);
-            m_bvsls->assert_expr(tr(fml.get()));
-        }
-
-        // use phase assignment from literals?
         std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned r) {
             return false;
         };
 
-        m_bvsls->init();
-        m_bvsls->init_eval(eval);
-        m_bvsls->updt_params(s().params());
-
+        m_sls->init();
+        m_sls->init_eval(eval);
+        m_sls->updt_params(s().params());
+        m_sls->init_unit([&]() { 
+            if (!m_has_units)
+                return expr_ref(*m_slsm);
+            expr_ref e(*m_slsm);
+            {
+                std::lock_guard<std::mutex> lock(m_mutex);
+                if (m_units->empty())
+                    return expr_ref(*m_slsm);
+                ast_translation tr(*m_shared, *m_slsm);
+                e = tr(m_units->back());
+                m_units->pop_back();
+            }
+            return e;
+        });
+        m_sls->set_model([&](model& mdl) {
+            std::lock_guard<std::mutex> lock(m_mutex);
+            ast_translation tr(*m_shared, m);
+            m_model = mdl.translate(tr);
+        });
+                                     
         m_thread = std::thread([this]() { run_local_search(); });        
     }
 
     void solver::sample_local_search() {
-        if (m_completed) {
-            m_thread.join();
-            if (m_result == l_true) {
-                verbose_stream() << "Found model using local search\n";
-                exit(1);
-            }
+        if (!m_completed)
+            return;        
+        m_thread.join();
+        m_completed = false;
+        m_sls->collect_statistics(m_st);
+        if (m_result == l_true) {
+            IF_VERBOSE(2, verbose_stream() << "(sat.sls :model-completed)\n";);
+            auto mdl = m_sls->get_model();
+            ast_translation tr(*m_slsm, m);
+            m_model = mdl->translate(tr);
+            s().set_canceled();
         }
+        m_sls = nullptr;
     }
 
     void solver::run_local_search() {
-        lbool r = (*m_bvsls)();
-        m_result = r;
+        m_result = (*m_sls)();
         m_completed = true;
     }
 
+#endif
 }

src/sat/smt/sls_solver.h

@@ -16,12 +16,45 @@ Author:
 --*/
 #pragma once
 
-#include <thread>
+
 #include "util/rlimit.h"
 #include "ast/sls/bv_sls.h"
 #include "sat/smt/sat_th.h"
 
 
+#ifdef SINGLE_THREAD
+
+
+namespace euf {
+    class solver;
+}
+
+namespace sls {
+
+    class solver : public euf::th_euf_solver {
+    public:
+        solver(euf::solver& ctx);
+            
+        sat::literal internalize(expr* e, bool sign, bool root) override { UNREACHABLE();  return sat::null_literal; }
+        void internalize(expr* e) override { UNREACHABLE(); }
+        th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); }
+
+        model_ref get_model() { return model_ref(nullptr); }
+        bool unit_propagate() override { return false; }
+        void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); }
+        sat::check_result check() override { return sat::check_result::CR_DONE;}
+        std::ostream& display(std::ostream& out) const override { return out; }
+        std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { UNREACHABLE(); return out; }
+        std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { UNREACHABLE(); return out; }
+
+    };
+}
+
+#else
+
+#include <thread>
+#include <mutex>
+
 namespace euf {
     class solver;
 }
@@ -30,30 +63,41 @@ namespace sls {
 
     class solver : public euf::th_euf_solver {
         std::atomic<lbool> m_result;
-        std::atomic<bool> m_completed;
+        std::atomic<bool> m_completed, m_has_units;
         std::thread m_thread;
-        scoped_ptr<ast_manager> m_m;
-        scoped_ptr<bv::sls> m_bvsls;
+        std::mutex  m_mutex;
+        // m is accessed by the main thread
+        // m_slsm is accessed by the sls thread
+        // m_shared is only accessed at synchronization points
+        scoped_ptr<ast_manager> m_shared, m_slsm;
+        scoped_ptr<bv::sls> m_sls;
+        scoped_ptr<expr_ref_vector> m_units;
+        model_ref m_model;
+        unsigned m_trail_lim = 0;
+        statistics m_st;
 
         void run_local_search();
-        void init_local_search();
         void sample_local_search();
+        bool is_unit(expr*);
+
     public:
         solver(euf::solver& ctx);
         ~solver();
 
-        void push_core() override;
+        model_ref get_model() { return m_model; }
+
+        void init_search() override;
+        void push_core() override {}
         void pop_core(unsigned n) override;
-        void simplify() override;
+        th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); }
+        void collect_statistics(statistics& st) const override { st.copy(m_st); }       
+        void finalize() override;
+        bool unit_propagate() override;
 
         sat::literal internalize(expr* e, bool sign, bool root) override { UNREACHABLE();  return sat::null_literal; }
         void internalize(expr* e) override { UNREACHABLE(); }
-        th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); }
-       
-
-        bool unit_propagate() override { return false; }
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override { UNREACHABLE(); }
-        sat::check_result check() override { return sat::check_result::CR_DONE; }
+        sat::check_result check() override;
         std::ostream & display(std::ostream & out) const override { return out; }
         std::ostream & display_justification(std::ostream & out, sat::ext_justification_idx idx) const override { UNREACHABLE(); return out; }
         std::ostream & display_constraint(std::ostream & out, sat::ext_constraint_idx idx) const override { UNREACHABLE(); return out; }
@@ -61,3 +105,5 @@ namespace sls {
     };
 
 }
+
+#endif

src/sat/tactic/goal2sat.cpp

@@ -895,6 +895,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         process(n, true);
         CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";);
         SASSERT(m_result_stack.empty());
+        add_assertion(n);
     }
 
     void insert_dep(expr* dep0, expr* dep, bool sign) {
@@ -989,6 +990,12 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
+    void add_assertion(expr* f) {
+        auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
+        if (ext)
+            ext->add_assertion(f);
+    }
+
     void update_model(model_ref& mdl) {
         auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
         if (ext)

src/smt/params/smt_params.cpp

@@ -49,6 +49,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_threads_max_conflicts  = p.threads_max_conflicts();
     m_threads_cube_frequency = p.threads_cube_frequency();
     m_core_validate = p.core_validate();
+    m_sls_enable = p.sls_enable();
     m_logic = _p.get_sym("logic", m_logic);
     m_string_solver = p.string_solver();
     m_up_persist_clauses = p.up_persist_clauses();
@@ -66,6 +67,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_lemmas2console = sp.lemmas2console();
     m_instantiations2console = sp.instantiations2console();
     m_proof_log = sp.proof_log();
+    
 }
 
 void smt_params::updt_params(params_ref const & p) {

src/smt/params/smt_params.h

@@ -114,6 +114,7 @@ struct smt_params : public preprocessor_params,
     bool             m_induction = false;
     bool             m_clause_proof = false;
     symbol           m_proof_log;
+    bool             m_sls_enable = false;
 
     // -----------------------------------
     //

src/smt/params/smt_params_helper.pyg

@@ -83,6 +83,7 @@ def_module_params(module_name='smt',
 			  ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
 			  ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
 			  ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
+			  ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),
                           ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
                           ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
                           ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
@@ -135,6 +136,7 @@ def_module_params(module_name='smt',
                           ('str.regex_automata_length_attempt_threshold', UINT, 10, 'number of length/path constraint attempts before checking unsatisfiability of regex terms'),
                           ('str.fixed_length_refinement', BOOL, False, 'use abstraction refinement in fixed-length equation solver (Z3str3 only)'),
                           ('str.fixed_length_naive_cex', BOOL, True, 'construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only)'),
+                          ('sls.enable', BOOL, False, 'enable sls co-processor with SMT engine'),
                           ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
                           ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
                           ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -49,8 +49,18 @@ Notes:
 #include "parsers/smt2/smt2parser.h"
 #include "sat/sat_params.hpp"
 
+tactic* mk_tactic_for_logic(ast_manager& m, params_ref const& p, symbol const& logic);
 
 
+class smt_nested_solver_factory : public solver_factory {
+public:
+    solver* operator()(ast_manager& m, params_ref const& p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const& logic) override {
+        auto t = mk_tactic_for_logic(m, p, logic);
+        auto s = mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic);
+        return s;
+    }
+};
+
 tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
     if (logic=="QF_UF")
         return mk_qfuf_tactic(m, p);

src/tactic/sls/sls_tactic.cpp

@@ -134,7 +134,7 @@ public:
     bv_sls_tactic(ast_manager& _m, params_ref const& p) :
         m(_m),
         m_params(p) {
-        m_sls = alloc(bv::sls, m);
+        m_sls = alloc(bv::sls, m, p);
     }
 
     tactic* translate(ast_manager& m) override {
@@ -172,12 +172,12 @@ public:
         m_sls->init_eval(false_eval);
 
         lbool res = m_sls->operator()();
-        auto const& stats = m_sls->get_stats();
-        report_tactic_progress("Number of flips:", stats.m_moves);
-        IF_VERBOSE(20, verbose_stream() << res << "\n");
-        IF_VERBOSE(20, m_sls->display(verbose_stream()));
         m_st.reset();
         m_sls->collect_statistics(m_st);
+        report_tactic_progress("Number of flips:", m_sls->get_num_moves());
+        IF_VERBOSE(10, verbose_stream() << res << "\n");
+        IF_VERBOSE(10, m_sls->display(verbose_stream()));
+
         if (res == l_true) {            
             if (g->models_enabled()) {
                 model_ref mdl = m_sls->get_model();
@@ -207,7 +207,7 @@ public:
 
     void cleanup() override {
 
-        auto* d = alloc(bv::sls, m);
+        auto* d = alloc(bv::sls, m, m_params);
         std::swap(d, m_sls);
         dealloc(d);
     }
@@ -235,12 +235,6 @@ tactic* mk_bv_sls_tactic(ast_manager& m, params_ref const& p) {
 
 
 static tactic * mk_preamble(ast_manager & m, params_ref const & p) {
-    params_ref main_p;
-    main_p.set_bool("elim_and", true);
-    // main_p.set_bool("pull_cheap_ite", true);
-    main_p.set_bool("push_ite_bv", true);
-    main_p.set_bool("blast_distinct", true);
-    main_p.set_bool("hi_div0", true);
 
     params_ref simp2_p = p;
     simp2_p.set_bool("som", true);
@@ -249,18 +243,15 @@ static tactic * mk_preamble(ast_manager & m, params_ref const & p) {
     simp2_p.set_bool("local_ctx", true);
     simp2_p.set_uint("local_ctx_limit", 10000000);
 
-    params_ref hoist_p;
+    params_ref hoist_p = p;
     hoist_p.set_bool("hoist_mul", true);
     hoist_p.set_bool("som", false);
 
-    params_ref gaussian_p;
+    params_ref gaussian_p = p;
     // conservative gaussian elimination. 
     gaussian_p.set_uint("gaussian_max_occs", 2); 
 
-    params_ref ctx_p;
-    ctx_p.set_uint("max_depth", 32);
-    ctx_p.set_uint("max_steps", 5000000);
-    return and_then(and_then(mk_simplify_tactic(m),                             
+    return and_then(and_then(mk_simplify_tactic(m, p),                             
                              mk_propagate_values_tactic(m),
                              using_params(mk_solve_eqs_tactic(m), gaussian_p),
                              mk_elim_uncnstr_tactic(m),
@@ -278,7 +269,9 @@ tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {
 }
 
 tactic* mk_qfbv_new_sls_tactic(ast_manager& m, params_ref const& p) {
-    tactic* t = and_then(mk_preamble(m, p), mk_bv_sls_tactic(m, p));
-    t->updt_params(p);
+    params_ref q = p;
+    q.set_bool("elim_sign_ext", false);
+    tactic* t = and_then(mk_preamble(m, q), mk_bv_sls_tactic(m, q));
+    t->updt_params(q);
     return t;
 }

src/util/buffer.h

@@ -21,7 +21,7 @@ Revision History:
 --*/
 #pragma once
 
-#include <type_traits>
+#include <cstddef>
 #include "util/memory_manager.h"
 
 template<typename T, bool CallDestructors=true, unsigned INITIAL_SIZE=16>
@@ -30,8 +30,7 @@ protected:
     T *      m_buffer = reinterpret_cast<T*>(m_initial_buffer);
     unsigned m_pos = 0;
     unsigned m_capacity = INITIAL_SIZE;
-    alignas(T) std::byte m_initial_buffer[sizeof(T)*INITIAL_SIZE];
-//    typename std::aligned_storage<sizeof(T), alignof(T)>::type m_initial_buffer[INITIAL_SIZE];
+    alignas(T) std::byte m_initial_buffer[INITIAL_SIZE * sizeof(T)];
 
     void free_memory() {
         if (m_buffer != reinterpret_cast<T*>(m_initial_buffer)) {

src/util/debug.cpp

@@ -75,6 +75,37 @@ bool is_debug_enabled(const char * tag) {
     return g_enabled_debug_tags->contains(tag);
 }
 
+atomic<exit_action> g_default_exit_action(exit_action::exit);
+
+exit_action get_default_exit_action() {
+    return g_default_exit_action;
+}
+
+void set_default_exit_action(exit_action a) {
+    g_default_exit_action = a;
+}
+
+void invoke_exit_action(unsigned int code) {
+    exit_action a = get_default_exit_action();
+    switch (a) {
+    case exit_action::exit:
+        exit(code);
+    case exit_action::throw_exception:
+        switch (code) {
+            case ERR_INTERNAL_FATAL:
+                throw default_exception("internal fatal");
+            case ERR_UNREACHABLE:
+                throw default_exception("unreachable");
+            case ERR_NOT_IMPLEMENTED_YET:
+                throw default_exception("not implemented yet");
+            default:
+                throw default_exception("unknown");
+        }
+    default:
+        exit(code);
+    }
+}
+
 atomic<debug_action> g_default_debug_action(debug_action::ask);
 
 debug_action get_default_debug_action() {

src/util/debug.h

@@ -35,6 +35,14 @@ enum class debug_action {
 debug_action get_default_debug_action();
 void set_default_debug_action(debug_action a);
 
+enum class exit_action {
+    exit,
+    throw_exception,
+};
+exit_action get_default_exit_action();
+void set_default_exit_action(exit_action a);
+void invoke_exit_action(unsigned int code);
+
 #include "util/error_codes.h"
 #include "util/warning.h"
 
@@ -56,7 +64,7 @@ void set_default_debug_action(debug_action a);
 #endif
 
 #ifdef NO_Z3_DEBUGGER
-#define INVOKE_DEBUGGER() exit(ERR_INTERNAL_FATAL)
+#define INVOKE_DEBUGGER() invoke_exit_action(ERR_INTERNAL_FATAL)
 #else
 #ifdef _WINDOWS
 #define INVOKE_DEBUGGER() __debugbreak()
@@ -71,6 +79,7 @@ void enable_debug(const char * tag);
 void disable_debug(const char * tag);
 bool is_debug_enabled(const char * tag);
 
+
 #define SASSERT(COND) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
 #define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
 #define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); })
@@ -85,26 +94,25 @@ bool is_debug_enabled(const char * tag);
 #ifdef Z3DEBUG
 # define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER();)
 #else
-# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); exit(ERR_UNREACHABLE); } ((void) 0)
+# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); invoke_exit_action(ERR_UNREACHABLE); } ((void) 0)
 #endif
 
 #ifdef Z3DEBUG
 # define NOT_IMPLEMENTED_YET() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); INVOKE_DEBUGGER();)
 #else
-# define NOT_IMPLEMENTED_YET() { notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)
+# define NOT_IMPLEMENTED_YET() { notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); invoke_exit_action(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)
 #endif
 
 #define VERIFY(_x_) if (!(_x_)) {                                                       \
         notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #_x_ "\n"); \
-        exit(ERR_UNREACHABLE);                                                          \
+        invoke_exit_action(ERR_UNREACHABLE);                                                          \
     }
 
 #define VERIFY_EQ(LHS, RHS)                                                                         \
     if (!((LHS) == (RHS))) {                                                                        \
         notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #LHS " == " #RHS "\n"); \
         std::cerr << "LHS value: " << (LHS) << "\nRHS value: " << (RHS) << "\n";                    \
-        DEBUG_CODE(INVOKE_DEBUGGER(););                                                             \
-        exit(ERR_UNREACHABLE);                                                                      \
+        invoke_exit_action(ERR_UNREACHABLE);                                                                      \
     }
 
 #define ENSURE(_x_) VERIFY(_x_)

src/util/hashtable.h

@@ -472,7 +472,7 @@ public:
        that was already in the table.
      */
     data const & insert_if_not_there(data const & e) {
-        entry * et;
+        entry * et = nullptr;
         insert_if_not_there_core(e, et);
         return et->get_data();
     }
@@ -482,7 +482,7 @@ public:
        Return the entry that contains e.
     */
     entry * insert_if_not_there2(data const & e) {
-        entry * et;
+        entry * et = nullptr;
         insert_if_not_there_core(e, et);
         return et;
     }

src/util/util.h

@@ -142,7 +142,7 @@ static inline unsigned get_num_1bits(uint64_t v) {
     v = (v + (v >> 4)) & 0x0F0F0F0F0F0F0F0F;
     uint64_t r = (v * 0x0101010101010101) >> 56;
     SASSERT(c == r);
-    return (unsigned)r;
+    return static_cast<unsigned>(r);
 #endif
 }