bugfixes in sls-arith

src/ast/sls/sat_ddfw.cpp

@@ -374,7 +374,6 @@ namespace sat {
     }
     
     void ddfw::do_restart() {    
-        verbose_stream() << "restart\n";
         reinit_values();
         init_clause_data();
         m_restart_next += m_config.m_restart_base*get_luby(++m_restart_count);
@@ -625,5 +624,19 @@ namespace sat {
         m_config.m_restart_base = p.ddfw_restart_base();        
     }
 
+    void ddfw::collect_statistics(statistics& st) const {
+        st.update("sls-ddfw-flips", (double)m_flips);
+        st.update("sls-ddfw-restarts", m_restart_count);
+        st.update("sls-ddfw-reinits", m_reinit_count);
+        st.update("sls-ddfw-shifts", (double)m_shifts);
+    }
+    
+    void ddfw::reset_statistics() {
+        m_flips = 0;
+        m_restart_count = 0;
+        m_reinit_count = 0;
+        m_shifts = 0;
+    }
+
 }
 

src/ast/sls/sat_ddfw.h

@@ -233,7 +233,9 @@ namespace sat {
         // for parallel integration
         unsigned num_non_binary_clauses() const { return m_num_non_binary_clauses; }
 
-        void collect_statistics(statistics& st) const {} 
+        void collect_statistics(statistics& st) const;
+
+        void reset_statistics();
 
         double get_priority(bool_var v) const { return m_probs[v]; }
 

src/ast/sls/sls_arith_base.h

@@ -45,7 +45,7 @@ namespace sls {
         };
 
         struct stats {
-            unsigned m_num_flips = 0;
+            unsigned m_num_steps = 0;
         };
 
     public:
@@ -53,11 +53,16 @@ namespace sls {
             vector<std::pair<num_t, var_t>> m_args;
             num_t      m_coeff{ 0 };
         };
+        struct nonlinear_coeff {
+            var_t v;     // variable or multiplier containing x
+            num_t coeff; // coeff of v in inequality
+            unsigned p;  // power
+        };
         // encode args <= bound, args = bound, args < bound
         struct ineq : public linear_term {    
+            vector<std::pair<var_t, vector<nonlinear_coeff>>> m_nonlinear;
             ineq_kind  m_op = ineq_kind::LE;            
             num_t      m_args_value;
-            unsigned   m_var_to_flip = UINT_MAX;
 
             bool is_true() const;
             std::ostream& display(std::ostream& out) const;
@@ -76,6 +81,27 @@ namespace sls {
             unsigned_vector m_muls;
             unsigned_vector m_adds;
             optional<bound> m_lo, m_hi;
+            num_t        m_range{ 100000000 };
+            bool in_range(num_t const& n) const {
+                if (-m_range < n && n < m_range)
+                    return true;
+                if (m_lo && !m_hi)
+                    return n < m_lo->value + m_range;
+                if (!m_lo && m_hi)
+                    return n > m_hi->value - m_range;
+                return false;                
+            }
+            unsigned m_tabu_pos = 0, m_tabu_neg = 0;
+            unsigned m_last_pos = 0, m_last_neg = 0;
+            bool is_tabu(unsigned step, num_t const& delta) {
+                return (delta > 0 ? m_tabu_pos : m_tabu_neg) > step;
+            }
+            void set_step(unsigned step, unsigned tabu_step, num_t const& delta) {
+                if (delta > 0)
+                    m_tabu_pos = tabu_step, m_last_pos = step;
+                else
+                    m_tabu_neg = tabu_step, m_last_neg = step;
+            }
         };
 
         struct mul_def {
@@ -94,6 +120,12 @@ namespace sls {
             unsigned m_arg1, m_arg2;
         };
 
+        struct var_change {
+            unsigned m_var;
+            num_t    m_delta;
+            double   m_score;
+        };
+       
         stats                        m_stats;
         config                       m_config;
         scoped_ptr_vector<ineq>      m_bool_vars;
@@ -104,6 +136,10 @@ namespace sls {
         unsigned_vector              m_expr2var;
         svector<double>              m_probs;
         bool                         m_dscore_mode = false;
+        vector<var_change>           m_updates;
+        var_t                        m_last_var = 0;
+        num_t                        m_last_delta { 0 };
+        bool                         m_tabu = false;
         arith_util                   a;
 
         void invariant();
@@ -111,6 +147,7 @@ namespace sls {
 
         unsigned get_num_vars() const { return m_vars.size(); }
 
+        bool eval_is_correct(var_t v);
         bool repair_mul_one(mul_def const& md);
         bool repair_power(mul_def const& md);
         bool repair_mul_factors(mul_def const& md);
@@ -126,10 +163,15 @@ namespace sls {
         bool repair_abs(op_def const& od);
         bool repair_to_int(op_def const& od);
         bool repair_to_real(op_def const& od);
-        void repair(sat::literal lit, ineq const& ineq);
+        bool repair(sat::literal lit);
-        bool repair_eq(sat::literal lit, ineq const& ineq);
         bool in_bounds(var_t v, num_t const& value);
         bool is_fixed(var_t v);
+        bool is_linear(var_t x, vector<nonlinear_coeff> const& nlc, num_t& b);
+        bool is_quadratic(var_t x, vector<nonlinear_coeff> const& nlc, num_t& a, num_t& b);
+        num_t mul_value_without(var_t m, var_t x);
+
+        void add_update(var_t v, num_t delta);
+        bool is_permitted_update(var_t v, num_t& delta);
 
         vector<num_t> m_factors;
         vector<num_t> const& factor(num_t n);
@@ -174,25 +216,32 @@ namespace sls {
 
         monomials monomial_iterator(mul_def const& md) { return monomials(*this, md); }
 
-        double reward(sat::literal lit);
+        // double reward(sat::literal lit);
 
         bool sign(sat::bool_var v) const { return !ctx.is_true(sat::literal(v, false)); }
         ineq* atom(sat::bool_var bv) const { return m_bool_vars.get(bv, nullptr); }        
         num_t dtt(bool sign, ineq const& ineq) const { return dtt(sign, ineq.m_args_value, ineq); }
         num_t dtt(bool sign, num_t const& args_value, ineq const& ineq) const;
         num_t dtt(bool sign, ineq const& ineq, var_t v, num_t const& new_value) const;
-        num_t dtt(bool sign, ineq const& ineq, num_t const& coeff, num_t const& old_value, num_t const& new_value) const;
+        num_t dtt(bool sign, ineq const& ineq, num_t const& coeff, num_t const& delta) const;
         num_t dts(unsigned cl, var_t v, num_t const& new_value) const;
         num_t compute_dts(unsigned cl) const;
-        bool cm(ineq const& ineq, var_t v, num_t& new_value);
+
-        bool cm(ineq const& ineq, var_t v, num_t const& coeff, num_t& new_value);
+        bool is_mul(var_t v) const { return m_vars[v].m_op == arith_op_kind::OP_MUL; }
-        int cm_score(var_t v, num_t const& new_value);
+        bool is_add(var_t v) const { return m_vars[v].m_op == arith_op_kind::OP_ADD; }
+        mul_def const& get_mul(var_t v) const { SASSERT(is_mul(v));  return m_muls[m_vars[v].m_def_idx]; }
+        add_def const& get_add(var_t v) const { SASSERT(is_add(v));  return m_adds[m_vars[v].m_def_idx]; }
+
         bool update(var_t v, num_t const& new_value);
-        double dscore_reward(sat::bool_var v);
+        bool apply_update();
-        double dtt_reward(sat::literal lit);
+        void find_moves(sat::literal lit);
-        double dscore(var_t v, num_t const& new_value) const;
+        void find_reset_moves(sat::literal lit);
+        void add_reset_update(var_t v);
+        void find_linear_moves(ineq const& i, var_t x, num_t const& coeff, num_t const& sum);
+        void find_quadratic_moves(ineq const& i, var_t x, num_t const& a, num_t const& b, num_t const& sum);
+        double compute_score(var_t x, num_t const& delta);
         void save_best_values();
-        bool solve_eq_pairs(ineq const& ineq);
+        bool solve_eq_pairs(var_t v, ineq const& ineq);
         bool solve_eq_pairs(num_t const& a, var_t x, num_t const& b, var_t y, num_t const& r);
 
         var_t mk_var(expr* e);
@@ -203,6 +252,8 @@ namespace sls {
         ineq& new_ineq(ineq_kind op, num_t const& bound);
         void init_ineq(sat::bool_var bv, ineq& i);
         num_t divide(var_t v, num_t const& delta, num_t const& coeff);
+        num_t divide_floor(var_t v, num_t const& a, num_t const& b);
+        num_t divide_ceil(var_t v, num_t const& a, num_t const& b);
         
         void init_bool_var_assignment(sat::bool_var v);
 
@@ -219,11 +270,12 @@ namespace sls {
         void add_lt(var_t v, num_t const& n);
         void add_gt(var_t v, num_t const& n);
         std::ostream& display(std::ostream& out, var_t v) const;
+        std::ostream& display(std::ostream& out, add_def const& ad) const;
     public:
         arith_base(context& ctx);
         ~arith_base() override {}        
         void register_term(expr* e) override;
-        void set_value(expr* e, expr* v) override;
+        bool set_value(expr* e, expr* v) override;
         expr_ref get_value(expr* e) override;
         void initialize() override;
         void propagate_literal(sat::literal lit) override;
@@ -236,6 +288,8 @@ namespace sls {
         void on_restart() override;
         std::ostream& display(std::ostream& out) const override;
         void mk_model(model& mdl) override;
+        void collect_statistics(statistics& st) const override;
+        void reset_statistics() override;
     };
 
 

src/ast/sls/sls_arith_plugin.cpp

@@ -22,30 +22,42 @@ Author:
 namespace sls {
 
 #define WITH_FALLBACK(_fn_) \
-    if (!m_arith) { \
+    if (m_arith64) { \
         try {\
             return m_arith64->_fn_;\
         }\
         catch (overflow_exception&) {\
+            throw;\
             init_backup();\
         }\
     }\
     return m_arith->_fn_; \
 
+#define APPLY_BOTH(_fn_) \
+    if (m_arith64) { \
+        try {\
+            m_arith64->_fn_;\
+        }\
+        catch (overflow_exception&) {\
+            throw;\
+            init_backup();\
+        }\
+    }\
+    m_arith->_fn_; \
+
     arith_plugin::arith_plugin(context& ctx) :
         plugin(ctx), m_shared(ctx.get_manager()) {
         m_arith64 = alloc(arith_base<checked_int64<true>>, ctx);
-        m_fid = m_arith64->fid();
+        m_arith = alloc(arith_base<rational>, ctx);
-        init_backup();
+        m_fid = m_arith->fid();
     }
 
     void arith_plugin::init_backup() {
-        m_arith = alloc(arith_base<rational>, ctx);
+        m_arith64 = nullptr;
-        m_arith->initialize();
     }
 
     void arith_plugin::register_term(expr* e) {
-        WITH_FALLBACK(register_term(e));
+        APPLY_BOTH(register_term(e));
     }
 
     expr_ref arith_plugin::get_value(expr* e) {
@@ -53,10 +65,7 @@ namespace sls {
     }
 
     void arith_plugin::initialize() {
-        if (m_arith) 
+        APPLY_BOTH(initialize());
-            m_arith->initialize();
-        else 
-            m_arith64->initialize();
     }
 
     void arith_plugin::propagate_literal(sat::literal lit) {
@@ -68,38 +77,26 @@ namespace sls {
     }
 
     bool arith_plugin::is_sat() {
-        if (m_arith) 
+        WITH_FALLBACK(is_sat());
-            return m_arith->is_sat();
-        else
-            return m_arith64->is_sat();
     }
 
     void arith_plugin::on_rescale() {
-        if (m_arith) 
+        APPLY_BOTH(on_rescale());
-            m_arith->on_rescale();
-        else 
-            m_arith64->on_rescale();
     }
 
     void arith_plugin::on_restart() {
-        if (m_arith) 
+        WITH_FALLBACK(on_restart());       
-            m_arith->on_restart();
-        else 
-            m_arith64->on_restart();        
     }
 
     std::ostream& arith_plugin::display(std::ostream& out) const {     
-        if (m_arith) 
+        if (m_arith64) 
-            return m_arith->display(out);
-        else
             return m_arith64->display(out);
+        else
+            return m_arith->display(out);                
     }
 
     void arith_plugin::mk_model(model& mdl) {
-        if (m_arith) 
+        WITH_FALLBACK(mk_model(mdl));        
-            m_arith->mk_model(mdl);        
-        else 
-            m_arith64->mk_model(mdl);        
     }
 
     bool arith_plugin::repair_down(app* e) {
@@ -114,7 +111,21 @@ namespace sls {
         WITH_FALLBACK(repair_literal(lit));
     }
 
-    void arith_plugin::set_value(expr* e, expr* v) {
+    bool arith_plugin::set_value(expr* e, expr* v) {
         WITH_FALLBACK(set_value(e, v));
     }
+
+    void arith_plugin::collect_statistics(statistics& st) const {
+        if (m_arith64) 
+            m_arith64->collect_statistics(st);
+        else 
+            m_arith->collect_statistics(st);
+    }
+
+    void arith_plugin::reset_statistics() {
+        if (m_arith) 
+            m_arith->reset_statistics();
+        if (m_arith64)
+            m_arith64->reset_statistics();
+    }
 }

src/ast/sls/sls_arith_plugin.h

@@ -44,7 +44,10 @@ namespace sls {
         void on_restart() override;
         std::ostream& display(std::ostream& out) const override;
         void mk_model(model& mdl) override;
-        void set_value(expr* e, expr* v) override;
+        bool set_value(expr* e, expr* v) override;
+
+        void collect_statistics(statistics& st) const override;
+        void reset_statistics() override;
     };
 
 }

src/ast/sls/sls_basic_plugin.cpp

@@ -86,11 +86,11 @@ namespace sls {
         return out;
     }
 
-    void basic_plugin::set_value(expr* e, expr* v) {
+    bool basic_plugin::set_value(expr* e, expr* v) {
         if (!is_basic(e))
-            return;
+            return false;
         SASSERT(m.is_true(v) || m.is_false(v));
-        set_value(e, m.is_true(v));
+        return set_value(e, m.is_true(v));
     }
 
     bool basic_plugin::bval1(app* e) const {
@@ -229,6 +229,7 @@ namespace sls {
         case OP_XOR:
             NOT_IMPLEMENTED_YET();
         case OP_ITE:
+
             NOT_IMPLEMENTED_YET();
         case OP_DISTINCT:
             NOT_IMPLEMENTED_YET();
@@ -278,8 +279,35 @@ namespace sls {
     }
 
     bool basic_plugin::try_repair_ite(app* e, unsigned i) {
-        if (!m.is_bool(e))
+        if (m.is_bool(e))
+            return try_repair_ite_bool(e, i);
+        else
+            return try_repair_ite_nonbool(e, i);
+    }
+
+    bool basic_plugin::try_repair_ite_nonbool(app* e, unsigned i) {
+        auto child = e->get_arg(i);
+        auto cond = e->get_arg(0);
+        bool c = bval0(cond);
+
+        if (i == 0) {
+            auto eval = ctx.get_value(e);
+            auto eval1 = ctx.get_value(e->get_arg(1));
+            auto eval2 = ctx.get_value(e->get_arg(2));
+            if (eval == eval1 && eval == eval2)
+                return true;
+            if (eval == eval1)
+                return set_value(cond, true);
+            if (eval == eval2)
+                return set_value(cond, false);
             return false;
+        }
+        if (c != (i == 1))
+            return false;
+        return ctx.set_value(child, ctx.get_value(e));
+    }
+
+    bool basic_plugin::try_repair_ite_bool(app* e, unsigned i) {
         auto child = e->get_arg(i);
         auto cond = e->get_arg(0);
         bool c = bval0(cond);

src/ast/sls/sls_basic_plugin.h

@@ -29,6 +29,8 @@ namespace sls {
         bool try_repair_eq(app* e, unsigned i);
         bool try_repair_xor(app* e, unsigned i);
         bool try_repair_ite(app* e, unsigned i);
+        bool try_repair_ite_nonbool(app* e, unsigned i);
+        bool try_repair_ite_bool(app* e, unsigned i);
         bool try_repair_implies(app* e, unsigned i);
         bool try_repair_distinct(app* e, unsigned i);
         bool set_value(expr* e, bool b);
@@ -55,7 +57,9 @@ namespace sls {
         void on_restart() override {}
         std::ostream& display(std::ostream& out) const override;
         void mk_model(model& mdl) override {}
-        void set_value(expr* e, expr* v) override;
+        bool set_value(expr* e, expr* v) override;
+        void collect_statistics(statistics& st) const override {}
+        void reset_statistics() override {}
     };
 
 }

src/ast/sls/sls_bv_plugin.cpp

@@ -89,14 +89,14 @@ namespace sls {
         return m_eval.display(out);
     }
     
-    void bv_plugin::set_value(expr* e, expr* v) {
+    bool bv_plugin::set_value(expr* e, expr* v) {
         if (!bv.is_bv(e))
-            return;
+            return false;
         rational val;
         VERIFY(bv.is_numeral(v, val));
         auto& w = m_eval.eval(to_app(e));
         w.set_value(w.eval, val);
-        w.commit_eval();
+        return w.commit_eval();
     }
 
     bool bv_plugin::repair_down(app* e) {

src/ast/sls/sls_bv_plugin.h

@@ -52,7 +52,9 @@ namespace sls {
         void on_restart() override {}
         std::ostream& display(std::ostream& out) const override;
         void mk_model(model& mdl) override {}
-        void set_value(expr* e, expr* v) override;
+        bool set_value(expr* e, expr* v) override;
+        void collect_statistics(statistics& st) const override {}
+        void reset_statistics() override {}
     };
 
 }

src/ast/sls/sls_context.cpp

@@ -59,13 +59,13 @@ namespace sls {
         // Use timestamps to make it incremental.
         // 
         init();
-        verbose_stream() << "check " << unsat().size() << "\n";
+        //verbose_stream() << "check " << unsat().size() << "\n";
-        while (unsat().empty()) {
+        while (unsat().empty() && m.inc()) {
 
             propagate_boolean_assignment();
 
 
-            verbose_stream() << "propagate " << unsat().size() << " " << m_new_constraint << "\n";
+          //  verbose_stream() << "propagate " << unsat().size() << " " << m_new_constraint << "\n";
 
 
             // display(verbose_stream());
@@ -73,7 +73,7 @@ namespace sls {
             if (m_new_constraint || !unsat().empty())
                 return l_undef;
 
-            verbose_stream() << unsat().size() << " " << m_new_constraint << "\n";
+            //verbose_stream() << unsat().size() << " " << m_new_constraint << "\n";
 
             if (all_of(m_plugins, [&](auto* p) { return !p || p->is_sat(); })) {
                 model_ref mdl = alloc(model, m);
@@ -84,7 +84,7 @@ namespace sls {
                     if (p)
                         p->mk_model(*mdl);
                 s.on_model(mdl);
-                verbose_stream() << *mdl << "\n";
+                // verbose_stream() << *mdl << "\n";
                 TRACE("sls", display(tout));
                 return l_true;
             }
@@ -109,7 +109,7 @@ namespace sls {
                 if (is_app(e)) {
                     auto p = m_plugins.get(get_fid(e), nullptr);
                     if (p && !p->repair_down(to_app(e)) && !m_repair_up.contains(e->get_id())) {
-                        IF_VERBOSE(0, verbose_stream() << "revert repair: " << mk_bounded_pp(e, m) << "\n");
+                        IF_VERBOSE(3, verbose_stream() << "revert repair: " << mk_bounded_pp(e, m) << "\n");
                         m_repair_up.insert(e->get_id());
                     }
                 }
@@ -192,10 +192,11 @@ namespace sls {
     }
 
 
-    void context::set_value(expr * e, expr * v) {
+    bool context::set_value(expr * e, expr * v) {
         for (auto p : m_plugins)
-            if (p)
+            if (p && p->set_value(e, v))
-                p->set_value(e, v);        
+                return true;
+        return false;
     }
     
     bool context::is_relevant(expr* e) {
@@ -377,4 +378,16 @@ namespace sls {
         
         return out;
     }
+
+    void context::collect_statistics(statistics& st) const {
+        for (auto p : m_plugins)
+            if (p)
+                p->collect_statistics(st);
+    }
+
+    void context::reset_statistics() {
+        for (auto p : m_plugins)
+            if (p)
+                p->reset_statistics();
+    }
 }

src/ast/sls/sls_context.h

@@ -18,6 +18,7 @@ Author:
 
 #include "util/sat_literal.h"
 #include "util/sat_sls.h"
+#include "util/statistics.h"
 #include "ast/ast.h"
 #include "model/model.h"
 #include "util/scoped_ptr_vector.h"
@@ -50,7 +51,9 @@ namespace sls {
         virtual void on_restart() {};
         virtual std::ostream& display(std::ostream& out) const = 0;
         virtual void mk_model(model& mdl) = 0;
-        virtual void set_value(expr* e, expr* v) = 0;
+        virtual bool set_value(expr* e, expr* v) = 0;
+        virtual void collect_statistics(statistics& st) const = 0;
+        virtual void reset_statistics() = 0;
     };
 
     using clause = ptr_iterator<sat::literal>;
@@ -156,7 +159,7 @@ namespace sls {
 
         // Between plugin solvers
         expr_ref get_value(expr* e);
-        void set_value(expr* e, expr* v);
+        bool set_value(expr* e, expr* v);
         void new_value_eh(expr* e);
         bool is_true(expr* e);
         bool is_fixed(expr* e);        
@@ -166,5 +169,8 @@ namespace sls {
         ast_manager& get_manager() { return m; }
         std::ostream& display(std::ostream& out) const;
 
+        void collect_statistics(statistics& st) const;
+        void reset_statistics();
+
     };
 }

src/ast/sls/sls_euf_plugin.h

@@ -46,11 +46,14 @@ namespace sls {
         void register_term(expr* e) override;
         std::ostream& display(std::ostream& out) const override;
         void mk_model(model& mdl) override;
-        void set_value(expr* e, expr* v) override {}
+        bool set_value(expr* e, expr* v) override { return false; }
 
         void repair_up(app* e) override {}
         bool repair_down(app* e) override { return false; }
         void repair_literal(sat::literal lit) override {}
+
+        void collect_statistics(statistics& st) const override {}
+        void reset_statistics() override {}
     };
     
 }

src/ast/sls/sls_smt_solver.cpp

@@ -88,6 +88,16 @@ namespace sls {
             m_new_clause_added = true;
         }
         model_ref get_model() { return m_model; }
+
+        void collect_statistics(statistics& st) {
+            m_ddfw.collect_statistics(st);
+            m_context.collect_statistics(st);
+        }
+
+        void reset_statistics() {
+            m_ddfw.reset_statistics();
+            m_context.reset_statistics();
+        }
     };
 
     smt_solver::smt_solver(ast_manager& m, params_ref const& p):
@@ -118,48 +128,60 @@ namespace sls {
             add_clause(f);
         
         IF_VERBOSE(10, m_solver_ctx->display(verbose_stream()));
-        return m_ddfw.check(0, nullptr);
+        auto r = m_ddfw.check(0, nullptr);
+
+        return r;
     }
 
     void smt_solver::add_clause(expr* f) {
-        expr* g, * h;
+        expr* g, * h, * k;
         sat::literal_vector clause;
         if (m.is_not(f, g) && m.is_not(g, g)) {
             add_clause(g);
+            return;
         }
-        if (m.is_or(f)) {
+        bool sign = m.is_not(f, f);
+        if (!sign && m.is_or(f)) {
             clause.reset();
             for (auto arg : *to_app(f))
                 clause.push_back(mk_literal(arg));
             m_solver_ctx->add_clause(clause.size(), clause.data());
         }
-        else if (m.is_and(f)) {
+        else if (!sign && m.is_and(f)) {
             for (auto arg : *to_app(f))
                 add_clause(arg);
         }
-        else if (m.is_not(f, g) && m.is_or(g)) {
+        else if (sign && m.is_or(f)) {
-            for (auto arg : *to_app(g)) {
+            for (auto arg : *to_app(f)) {
                 expr_ref fml(m.mk_not(arg), m);;
                 add_clause(fml);
             }
         }
-        else if (m.is_not(f, g) && m.is_and(g)) {
+        else if (sign && m.is_and(f)) {
             clause.reset();
-            for (auto arg : *to_app(g))
+            for (auto arg : *to_app(f))
                 clause.push_back(~mk_literal(arg));
             m_solver_ctx->add_clause(clause.size(), clause.data());
         }
-        else if (m.is_eq(f, g, h) && m.is_bool(g)) {
+        else if (m.is_iff(f, g, h)) {
             auto lit1 = mk_literal(g);
             auto lit2 = mk_literal(h);
-            clause.reset();
+            sat::literal cls1[2] = { sign ? lit1 :~lit1, lit2 };
-            clause.push_back(~lit1);
+            sat::literal cls2[2] = { sign ? ~lit1 : lit1, ~lit2 };
-            clause.push_back(lit2);
+            m_solver_ctx->add_clause(2, cls1);
-            m_solver_ctx->add_clause(clause.size(), clause.data());
+            m_solver_ctx->add_clause(2, cls2);
-            clause.reset();
+        }
-            clause.push_back(lit1);
+        else if (m.is_ite(f, g, h, k)) {
-            clause.push_back(~lit2);
+            auto lit1 = mk_literal(g);
-            m_solver_ctx->add_clause(clause.size(), clause.data());
+            auto lit2 = mk_literal(h);
+            auto lit3 = mk_literal(k);
+            // (g -> h) & (~g -> k)
+            // (g & h) | (~g & k)
+            // negated: (g -> ~h) & (g -> ~k)
+            sat::literal cls1[2] = { ~lit1, sign ? ~lit2 : lit2 };
+            sat::literal cls2[2] = { lit1, sign ? ~lit3 : lit3 };
+            m_solver_ctx->add_clause(2, cls1);
+            m_solver_ctx->add_clause(2, cls2);
         }
         else {
             sat::literal lit = mk_literal(f);
@@ -170,6 +192,7 @@ namespace sls {
     sat::literal smt_solver::mk_literal(expr* e) {
         sat::literal lit;
         bool neg = false;
+        expr* a, * b, * c;
         while (m.is_not(e,e))
             neg = !neg;
         if (m_expr2lit.find(e, lit))
@@ -197,6 +220,33 @@ namespace sls {
             clause.push_back(~lit);
             m_solver_ctx->add_clause(clause.size(), clause.data());
         }
+        else if (m.is_iff(e, a, b)) {
+            lit = mk_literal();
+            auto lit1 = mk_literal(a);
+            auto lit2 = mk_literal(b);
+            sat::literal cls1[3] = { ~lit,  ~lit1, lit2 };
+            sat::literal cls2[3] = { ~lit,  lit1, ~lit2 };
+            sat::literal cls3[3] = {  lit,  lit1, lit2 };
+            sat::literal cls4[3] = {  lit, ~lit1, ~lit2 };
+            m_solver_ctx->add_clause(3, cls1);
+            m_solver_ctx->add_clause(3, cls2);
+            m_solver_ctx->add_clause(3, cls3);
+            m_solver_ctx->add_clause(3, cls4);
+        }
+        else if (m.is_ite(e, a, b, c)) {
+            lit = mk_literal();
+            auto lit1 = mk_literal(a);
+            auto lit2 = mk_literal(b);
+            auto lit3 = mk_literal(c);
+            sat::literal cls1[3] = { ~lit, ~lit1, lit2 };
+            sat::literal cls2[3] = { ~lit,  lit1, lit3 };
+            sat::literal cls3[3] = {  lit, ~lit1, ~lit2 };
+            sat::literal cls4[3] = {  lit,  lit1, ~lit3 };
+            m_solver_ctx->add_clause(3, cls1);
+            m_solver_ctx->add_clause(3, cls2);
+            m_solver_ctx->add_clause(3, cls3);
+            m_solver_ctx->add_clause(3, cls4);
+        }
         else {
             sat::bool_var v = m_num_vars++;
             lit = sat::literal(v, false);
@@ -218,4 +268,12 @@ namespace sls {
     std::ostream& smt_solver::display(std::ostream& out) {
         return m_solver_ctx->display(out);
     }
+
+    void smt_solver::collect_statistics(statistics& st) {
+        m_solver_ctx->collect_statistics(st);
+    }
+
+    void smt_solver::reset_statistics() {
+        m_solver_ctx->reset_statistics();
+    }
 }

src/ast/sls/sls_smt_solver.h

@@ -42,8 +42,8 @@ namespace sls {
         lbool check();
         model_ref get_model();
         void updt_params(params_ref& p) {}
-        void collect_statistics(statistics& st) { st.copy(m_st); }
+        void collect_statistics(statistics& st);
         std::ostream& display(std::ostream& out);
-        void reset_statistics() { m_st.reset(); }
+        void reset_statistics();
     };
 }

src/util/checked_int64.h

@@ -25,6 +25,7 @@ Revision History:
 
 #include "util/z3_exception.h"
 #include "util/rational.h"
+#include "util/mpn.h"
 
 class overflow_exception : public z3_exception {
     char const* msg() const override { return "checked_int64 overflow/underflow"; }
@@ -106,7 +107,7 @@ public:
     
     checked_int64 & operator--() {
         if (CHECK && m_value == INT64_MIN) {
-            throw overflow_exception();
+            throw overflo9w_exception();
         }                    
         --m_value;
         return *this;
@@ -134,8 +135,10 @@ public:
             uint64_t x = static_cast<uint64_t>(m_value);
             uint64_t y = static_cast<uint64_t>(other.m_value);
             int64_t r = static_cast<int64_t>(x - y);
-            if (m_value > 0 && other.m_value < 0 && r <= 0) throw overflow_exception();
+            if (m_value > 0 && other.m_value < 0 && r <= 0) 
-            if (m_value < 0 && other.m_value > 0 && r >= 0) throw overflow_exception();
+                throw overflow_exception();
+            if (m_value < 0 && other.m_value > 0 && r >= 0) 
+                throw overflow_exception();
             m_value = r;            
         }
         else {
@@ -149,13 +152,12 @@ public:
             if (INT_MIN < m_value && m_value <= INT_MAX && INT_MIN < other.m_value && other.m_value <= INT_MAX) {
                 m_value *= other.m_value;
             }
-            // TBD: could be tuned by using known techniques or 128-bit arithmetic.
             else {
-                rational r(r64(m_value) * r64(other.m_value));
+                uint64_t x = m_value, y = other.m_value;
-                if (!r.is_int64()) {
+                uint64_t z = x * y;
+                if (y != 0 && z / y != x)
                     throw overflow_exception();
-                }
+                m_value = z;
-                m_value = r.get_int64();
             }
         }
         else {

src/util/vector.h

@@ -290,6 +290,10 @@ public:
         }
     }
 
+    vector(std::initializer_list<T> const& l) {
+        for (auto const& t : l) 
+            push_back(t);        
+    }
  
     ~vector() { 
         destroy();