extend constant folding for bit-vector overflow/underflow operators, #657

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

src/ast/array_decl_plugin.cpp

@@ -522,7 +522,7 @@ void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol
 void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {
     op_names.push_back(builtin_name("store",OP_STORE));
     op_names.push_back(builtin_name("select",OP_SELECT));
-    if (logic == symbol::null) {
+    if (true || logic == symbol::null) {
         // none of the SMT2 logics support these extensions
         op_names.push_back(builtin_name("const",OP_CONST_ARRAY));
         op_names.push_back(builtin_name("map",OP_ARRAY_MAP));

src/ast/rewriter/bit_blaster/bit_blaster.h

@@ -20,8 +20,8 @@ Revision History:
 #define BIT_BLASTER_H_
 
 #include"bool_rewriter.h"
-#include"bit_blaster_params.h"
-#include"bit_blaster_tpl.h"
+#include"bit_blaster/bit_blaster_params.h"
+#include"bit_blaster/bit_blaster_tpl.h"
 #include"bv_decl_plugin.h"
 #include"rational.h"
 

src/ast/rewriter/bv_rewriter.cpp

@@ -20,6 +20,7 @@ Notes:
 #include"bv_rewriter_params.hpp"
 #include"poly_rewriter_def.h"
 #include"ast_smt2_pp.h"
+#include"bit_blaster/bit_blaster.h"
 
 
 void bv_rewriter::updt_local_params(params_ref const & _p) {
@@ -189,6 +190,15 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
         return mk_bv_comp(args[0], args[1], result);
     case OP_MKBV:
         return mk_mkbv(num_args, args, result);
+    case OP_BUMUL_NO_OVFL:
+        SASSERT(num_args == 2);
+        return mk_bv_umul_no_ovfl(args[0], args[1], result);
+    case OP_BSMUL_NO_OVFL:
+        SASSERT(num_args == 2);
+        return mk_bv_smul_no_ovfl(args[0], args[1], result);        
+    case OP_BSMUL_NO_UDFL: 
+        SASSERT(num_args == 2);
+        return mk_bv_smul_no_udfl(args[0], args[1], result);        
     default:
         return BR_FAILED;
     }
@@ -1100,6 +1110,92 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
         return BR_DONE;
 }
 
+br_status bv_rewriter::mk_bv_umul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result) {
+    rational val1, val2;
+    unsigned bv_size;
+    bool is_num1 = is_numeral(arg1, val1, bv_size);
+    bool is_num2 = is_numeral(arg2, val2, bv_size);
+    if (is_num1 && (val1.is_zero() || val1.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    if (is_num2 && (val2.is_zero() || val2.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    if (is_num1 && is_num2) {
+        SASSERT(!val1.is_neg());
+        SASSERT(!val2.is_neg());
+        rational r = val1 * val2;
+        result = m().mk_bool_val(r < rational(2).expt(bv_size));
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+
+br_status bv_rewriter::mk_bv_smul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result) {
+    rational val1, val2;
+    unsigned bv_size;
+    bool is_num1 = is_numeral(arg1, val1, bv_size);
+    bool is_num2 = is_numeral(arg2, val2, bv_size);
+    if (is_num1 && (val1.is_zero() || val1.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    if (is_num2 && (val2.is_zero() || val2.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    if (is_num1 && is_num2) {
+        bit_blaster_params params;
+        bit_blaster blaster(m(), params);
+        SASSERT(!val1.is_neg());
+        SASSERT(!val2.is_neg());
+        expr_ref_vector bits1(m()), bits2(m());
+        for (unsigned i = 0; i < bv_size; ++i) {
+            bits1.push_back(m().mk_bool_val(!val1.is_even()));
+            bits2.push_back(m().mk_bool_val(!val2.is_even()));
+            val1 = div(val1, rational(2));
+            val2 = div(val2, rational(2));
+        }
+        blaster.mk_smul_no_overflow(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result);
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+
+br_status bv_rewriter::mk_bv_smul_no_udfl(expr * arg1, expr * arg2, expr_ref& result) {
+    rational val1, val2;
+    unsigned bv_size;
+    bool is_num1 = is_numeral(arg1, val1, bv_size);
+    bool is_num2 = is_numeral(arg2, val2, bv_size);
+    if (is_num1 && (val1.is_zero() || val1.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    if (is_num2 && (val2.is_zero() || val2.is_one())) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    if (is_num1 && is_num2) {
+        bit_blaster_params params;
+        bit_blaster blaster(m(), params);
+        SASSERT(!val1.is_neg());
+        SASSERT(!val2.is_neg());
+        expr_ref_vector bits1(m()), bits2(m());
+        for (unsigned i = 0; i < bv_size; ++i) {
+            bits1.push_back(m().mk_bool_val(!val1.is_even()));
+            bits2.push_back(m().mk_bool_val(!val2.is_even()));
+            val1 = div(val1, rational(2));
+            val2 = div(val2, rational(2));
+        }
+        blaster.mk_smul_no_underflow(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result);
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+
+
 br_status bv_rewriter::mk_zero_extend(unsigned n, expr * arg, expr_ref & result) {
     if (n == 0) {
         result = arg;

src/ast/rewriter/bv_rewriter.h

@@ -114,6 +114,9 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     br_status mk_bv_srem_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_srem_core(arg1, arg2, true, result); }
     br_status mk_bv_urem_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_urem_core(arg1, arg2, true, result); }
     br_status mk_bv_smod_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_smod_core(arg1, arg2, true, result); }
+    br_status mk_bv_umul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result);
+    br_status mk_bv_smul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result);
+    br_status mk_bv_smul_no_udfl(expr * arg1, expr * arg2, expr_ref& result);
     br_status mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result);
     br_status mk_bv2int(expr * arg, expr_ref & result);
     br_status mk_bv_redor(expr * arg, expr_ref & result);

src/smt/params/smt_params_helper.pyg

@@ -61,5 +61,6 @@ def_module_params(module_name='smt',
                           ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
                           ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
                           ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
-                          ('core.validate', BOOL, False, 'validate unsat core produced by SMT context')
+                          ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
+                          ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context')
                           ))

src/smt/smt_solver.cpp

@@ -20,19 +20,25 @@ Notes:
 #include"smt_kernel.h"
 #include"reg_decl_plugins.h"
 #include"smt_params.h"
+#include"smt_params_helper.hpp"
+#include"mus.h"
 
 namespace smt {
 
     class solver : public solver_na2as {
-        smt_params          m_params;
+        smt_params          m_smt_params;
+        params_ref          m_params;
         smt::kernel         m_context;
         progress_callback * m_callback;
         symbol              m_logic;
+        bool                m_minimizing_core;
     public:
         solver(ast_manager & m, params_ref const & p, symbol const & l):
             solver_na2as(m),
+            m_smt_params(p),
             m_params(p),
-            m_context(m, m_params) {
+            m_context(m, m_smt_params),
+            m_minimizing_core(false) {
             m_logic = l;
             if (m_logic != symbol::null)
                 m_context.set_logic(m_logic);
@@ -48,7 +54,8 @@ namespace smt {
         }
 
         virtual void updt_params(params_ref const & p) {
-            m_params.updt_params(p);
+            m_smt_params.updt_params(p);
+            m_params.copy(p);
             m_context.updt_params(p);
         }
 
@@ -77,10 +84,40 @@ namespace smt {
             return m_context.check(num_assumptions, assumptions);
         }
 
+        struct scoped_minimize_core {
+            solver& s;
+            expr_ref_vector m_assumptions;
+            scoped_minimize_core(solver& s): s(s), m_assumptions(s.m_assumptions) {
+                s.m_minimizing_core = true;
+                s.m_assumptions.reset();
+            }
+
+            ~scoped_minimize_core() {
+                s.m_minimizing_core = false;
+                s.m_assumptions.append(m_assumptions);
+            }
+        };
+
         virtual void get_unsat_core(ptr_vector<expr> & r) {
             unsigned sz = m_context.get_unsat_core_size();
-            for (unsigned i = 0; i < sz; i++)
+            for (unsigned i = 0; i < sz; i++) {
                 r.push_back(m_context.get_unsat_core_expr(i));
+            }
+
+            if (m_minimizing_core || smt_params_helper(m_params).core_minimize() == false) {
+                return;
+            }
+            scoped_minimize_core scm(*this);
+            mus mus(*this);
+            
+            for (unsigned i = 0; i < r.size(); ++i) {
+                VERIFY(i == mus.add_soft(r[i]));
+            }        
+            ptr_vector<expr> r2;
+            if (l_true == mus.get_mus(r2)) {
+                r.reset();
+                r.append(r2);
+            }
         }
 
         virtual void get_model(model_ref & m) {

src/solver/mus.cpp

@@ -26,6 +26,9 @@ Notes:
 
 
 struct mus::imp {
+
+    typedef obj_hashtable<expr> expr_set;
+
     solver&                  m_solver;
     ast_manager&             m;
     expr_ref_vector          m_lit2expr;
@@ -64,66 +67,73 @@ struct mus::imp {
         SASSERT(is_literal(lit));
         m_assumptions.push_back(lit);
     }
+
+    lbool get_mus(ptr_vector<expr>& mus) {
+        unsigned_vector result;
+        lbool r = get_mus(result);
+        ids2exprs(mus, result);
+        return r;
+    }
     
-    lbool get_mus(unsigned_vector& mus) {
-        // SASSERT: mus does not have duplicates.
+    lbool get_mus(unsigned_vector& mus_ids) {
+        // SASSERT: mus_ids does not have duplicates.
         m_model.reset();
-        unsigned_vector core;
-        for (unsigned i = 0; i < m_lit2expr.size(); ++i) {
-            core.push_back(i);
-        }
-        if (core.size() == 1) {
-            mus.push_back(core.back());
+        mus_ids.reset();
+        
+        if (m_lit2expr.size() == 1) {
+            mus_ids.push_back(0);
             return l_true;
         }
+                
+        return get_mus1(mus_ids);
+    }
 
-        mus.reset();
-        if (false && core.size() > 64) {
-            return qx(mus);
+    lbool get_mus1(unsigned_vector& mus_ids) {
+        expr_ref_vector mus(m);
+        lbool result = get_mus1(mus);
+        for (unsigned i = 0; i < mus.size(); ++i) {
+            mus_ids.push_back(m_expr2lit.find(mus[i].get()));
         }
+        return result;
+    }
 
-        expr_ref_vector assumptions(m);
+
+    lbool get_mus1(expr_ref_vector& mus) {
+        ptr_vector<expr> unknown(m_lit2expr.size(), m_lit2expr.c_ptr());
         ptr_vector<expr> core_exprs;
-        while (!core.empty()) { 
-            IF_VERBOSE(12, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";);
-            unsigned lit_id = core.back();
-            TRACE("opt", 
-                  display_vec(tout << "core:  ", core);
-                  display_vec(tout << "mus:   ", mus);
-                  );
-            core.pop_back();
-            expr* lit = m_lit2expr[lit_id].get();
-            expr_ref not_lit(m);
-            not_lit = mk_not(m, lit);
+        while (!unknown.empty()) { 
+            IF_VERBOSE(12, verbose_stream() << "(opt.mus reducing core: " << unknown.size() << " new core: " << mus.size() << ")\n";);
+            TRACE("opt", display_vec(tout << "core:  ", unknown); display_vec(tout << "mus:   ", mus););
+            expr* lit = unknown.back();
+            unknown.pop_back();
+            expr_ref not_lit(mk_not(m, lit), m);
             lbool is_sat = l_undef;
             {
-                scoped_append _sa1(*this, assumptions, core);
-                scoped_append _sa2(*this, assumptions, m_assumptions);
-                assumptions.push_back(not_lit);
-                is_sat = m_solver.check_sat(assumptions);
+                scoped_append _sa1(*this, mus, unknown);
+                scoped_append _sa2(*this, mus, m_assumptions);
+                mus.push_back(not_lit);
+                is_sat = m_solver.check_sat(mus);
             }
             switch (is_sat) {
             case l_undef: 
                 return is_sat;
             case l_true:
-                assumptions.push_back(lit);
-                mus.push_back(lit_id);
+                mus.push_back(lit);
                 update_model();
                 break;
             default:
                 core_exprs.reset();
                 m_solver.get_unsat_core(core_exprs);
                 if (!core_exprs.contains(not_lit)) {
-                    // core := core_exprs \ mus
-                    core.reset();
+                    // unknown := core_exprs \ mus
+                    unknown.reset();
                     for (unsigned i = 0; i < core_exprs.size(); ++i) {
-                        lit = core_exprs[i];
-                        if (m_expr2lit.find(lit, lit_id) && !mus.contains(lit_id)) {
-                            core.push_back(lit_id);
+                        if (!mus.contains(core_exprs[i])) {
+                            unknown.push_back(core_exprs[i]);
                         }
                     }
                     TRACE("opt", display_vec(tout << "core exprs:", core_exprs);
-                        display_vec(tout << "core:", core);
+                        display_vec(tout << "core:", unknown);
                         display_vec(tout << "mus:", mus);
                     );
 
@@ -131,19 +141,118 @@ struct mus::imp {
                 break;
             }
         }
-#if 0
-        DEBUG_CODE(
-            assumptions.reset();
-            for (unsigned i = 0; i < mus.size(); ++i) {
-                assumptions.push_back(m_lit2expr[mus[i]].get());
-            }
-            lbool is_sat = m_solver.check_sat(assumptions.size(), assumptions.c_ptr());
-            SASSERT(is_sat == l_false);
-                   );
-#endif
+        // SASSERT(is_core(mus));
         return l_true;
     }
 
+    // use correction sets
+    lbool get_mus2(expr_ref_vector& mus) {
+        scoped_append _sa1(*this, mus, m_assumptions);
+        ptr_vector<expr> unknown(m_lit2expr.size(), m_lit2expr.c_ptr());
+        while (!unknown.empty()) { 
+            expr* lit;
+            lbool is_sat = get_next_mcs(mus, unknown, lit);
+            switch (is_sat) {
+            case l_undef:
+                return is_sat;
+            case l_false:
+                mus.push_back(lit);
+                break;
+            case l_true:
+                break;
+            }
+        }        
+        return l_true;
+    }
+
+    // find the next literal to be a member of a core.
+    lbool get_next_mcs(expr_ref_vector& mus, ptr_vector<expr>& unknown, expr*& core_literal) {
+        ptr_vector<expr> mss, core, min_core;
+        bool min_core_valid = false;
+        expr* min_lit = 0;
+        while (!unknown.empty()) {
+            expr* lit = unknown.back();
+            unknown.pop_back();
+            model_ref mdl;
+            scoped_append assume_mss(*this, mus, mss);
+            scoped_append assume_lit(*this, mus, lit);
+            switch (m_solver.check_sat(mus)) {
+            case l_true:
+                mss.push_back(lit);
+                m_solver.get_model(mdl);
+                for (unsigned i = 0; i < unknown.size(); ) {
+                    expr_ref tmp(m);
+                    if (mdl->eval(unknown[i], tmp) && m.is_true(tmp)) {
+                        mss.push_back(unknown[i]);
+                        unknown[i] = unknown.back();
+                        unknown.pop_back();
+                    }
+                    else {
+                        ++i;
+                    }
+                }
+                break;
+            case l_false:
+                core.reset();
+                m_solver.get_unsat_core(core);
+                // ???
+                if (!core.contains(lit)) {
+                    return l_false;
+                }
+                if (!min_core_valid || core.size() < min_core.size()) {
+                    min_core.reset();
+                    min_core.append(core);
+                    min_core_valid = true;
+                    min_lit = lit;
+                }
+                break;
+            case l_undef:
+                return l_undef;
+            }
+        }
+        if (!min_core_valid) {
+            // ???
+            UNREACHABLE();
+            return l_true;
+        }
+        else {
+            for (unsigned i = 0; i < min_core.size(); ++i) {
+                if (mss.contains(min_core[i]) && min_lit != min_core[i]) {
+                    unknown.push_back(min_core[i]);
+                }
+            }
+            core_literal = min_lit;
+        }
+        return l_false;
+    }
+
+    expr* lit2expr(unsigned lit_id) const {
+        return m_lit2expr[lit_id];
+    }
+
+    void ids2exprs(ptr_vector<expr>& dst, unsigned_vector const& ids) const {
+        for (unsigned i = 0; i < ids.size(); ++i) {
+            dst.push_back(lit2expr(ids[i]));
+        }        
+    }
+
+    bool is_core(unsigned_vector const& mus_ids) {
+        ptr_vector<expr> mus_exprs;
+        ids2exprs(mus_exprs, mus_ids);
+        return l_false == m_solver.check_sat(mus_exprs.size(), mus_exprs.c_ptr());
+    }
+
+    // dst := A \ B
+    void set_difference(unsigned_vector& dst, ptr_vector<expr> const& A, unsigned_vector const& B) {
+        dst.reset();
+        for (unsigned i = 0; i < A.size(); ++i) {
+            unsigned lit_id;
+            if (m_expr2lit.find(A[i], lit_id) && !B.contains(lit_id)) {
+                dst.push_back(lit_id);
+            }
+        }
+    }
+
     class scoped_append {
         expr_ref_vector& m_fmls;
         unsigned         m_size;
@@ -152,7 +261,7 @@ struct mus::imp {
             m_fmls(fmls1),
             m_size(fmls1.size()) {
             for (unsigned i = 0; i < fmls2.size(); ++i) {
-                fmls1.push_back(imp.m_lit2expr[fmls2[i]].get());
+                fmls1.push_back(imp.lit2expr(fmls2[i]));
             }            
         }
         scoped_append(imp& imp, expr_ref_vector& fmls1, uint_set const& fmls2):
@@ -160,7 +269,7 @@ struct mus::imp {
             m_size(fmls1.size()) {
             uint_set::iterator it = fmls2.begin(), end = fmls2.end();
             for (; it != end; ++it) {
-                fmls1.push_back(imp.m_lit2expr[*it].get());
+                fmls1.push_back(imp.lit2expr(*it));
             }            
         }
         scoped_append(imp& imp, expr_ref_vector& fmls1, expr_ref_vector const& fmls2):
@@ -168,6 +277,16 @@ struct mus::imp {
             m_size(fmls1.size()) {
             fmls1.append(fmls2);
         }
+        scoped_append(imp& imp, expr_ref_vector& fmls1, ptr_vector<expr> const& fmls2):
+            m_fmls(fmls1),
+            m_size(fmls1.size()) {
+            fmls1.append(fmls2.size(), fmls2.c_ptr());
+        }
+        scoped_append(imp& imp, expr_ref_vector& fmls1, expr* fml):
+            m_fmls(fmls1),
+            m_size(fmls1.size()) {
+            fmls1.push_back(fml);
+        }
         ~scoped_append() {
             m_fmls.shrink(m_size);
         }
@@ -175,7 +294,7 @@ struct mus::imp {
 
     void add_core(unsigned_vector const& core, expr_ref_vector& assumptions) {
         for (unsigned i = 0; i < core.size(); ++i) {
-            assumptions.push_back(m_lit2expr[core[i]].get());
+            assumptions.push_back(lit2expr(core[i]));
         }
     }
 
@@ -359,6 +478,17 @@ lbool mus::get_mus(unsigned_vector& mus) {
     return m_imp->get_mus(mus);
 }
 
+lbool mus::get_mus(ptr_vector<expr>& mus) {
+    return m_imp->get_mus(mus);
+}
+
+lbool mus::get_mus(expr_ref_vector& mus) {
+    ptr_vector<expr> result;
+    lbool r = m_imp->get_mus(result);
+    mus.append(result.size(), result.c_ptr());
+    return r;
+}
+
 
 void mus::reset() {
     m_imp->reset();

src/solver/mus.h

@@ -44,6 +44,10 @@ class mus {
     void add_assumption(expr* lit);
 
     lbool get_mus(unsigned_vector& mus);
+
+    lbool get_mus(ptr_vector<expr>& mus);
+
+    lbool get_mus(expr_ref_vector& mus);
     
     void reset();
     

src/solver/solver_na2as.h

@@ -25,6 +25,7 @@ Notes:
 #include"solver.h"
 
 class solver_na2as : public solver {
+ protected:
     ast_manager &      m;
     expr_ref_vector    m_assumptions;
     unsigned_vector    m_scopes;

src/solver/tactic2solver.cpp

@@ -23,6 +23,7 @@ Notes:
 #include"tactic.h"
 #include"ast_pp_util.h"
 #include"ast_translation.h"
+#include"mus.h"
 
 /**
    \brief Simulates the incremental solver interface using a tactic.
@@ -42,6 +43,7 @@ class tactic2solver : public solver_na2as {
     bool                         m_produce_proofs;
     bool                         m_produce_unsat_cores;
     statistics                   m_stats;
+    
 public:
     tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic);
     virtual ~tactic2solver();
@@ -203,8 +205,9 @@ void tactic2solver::collect_statistics(statistics & st) const {
 }
 
 void tactic2solver::get_unsat_core(ptr_vector<expr> & r) {
-    if (m_result.get())
+    if (m_result.get()) {
         m_result->get_unsat_core(r);
+    }
 }
 
 void tactic2solver::get_model(model_ref & m) {