updates

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

src/ast/arith_decl_plugin.cpp

@@ -351,6 +351,7 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
     case OP_MUL:     return is_real ? m_r_mul_decl : m_i_mul_decl;
     case OP_DIV:     return m_r_div_decl;
     case OP_IDIV:    return m_i_div_decl;
+    case OP_IDIVIDES: UNREACHABLE(); 
     case OP_REM:     return m_i_rem_decl;
     case OP_MOD:     return m_i_mod_decl;
     case OP_TO_REAL: return m_to_real_decl;
@@ -482,6 +483,14 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         m_manager->raise_exception("no arguments supplied to arithmetical operator");
         return nullptr;
     }
+    if (k == OP_IDIVIDES) {
+        if (arity != 1 || domain[0] != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) {
+            m_manager->raise_exception("invalid divides application. Expects integer parameter and one argument of sort integer");
+        }
+        return m_manager->mk_func_decl(symbol("divides"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
+                                       func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
+
     if (m_manager->int_real_coercions() && use_coercion(k)) {
         return mk_func_decl(fix_kind(k, arity), has_real_arg(arity, domain, m_real_decl));
     }
@@ -499,6 +508,13 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         m_manager->raise_exception("no arguments supplied to arithmetical operator");
         return nullptr;
     }
+    if (k == OP_IDIVIDES) {
+        if (num_args != 1 || m_manager->get_sort(args[0]) != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) {
+            m_manager->raise_exception("invalid divides application. Expects integer parameter and one argument of sort integer");
+        }
+        return m_manager->mk_func_decl(symbol("divides"), 1, &m_int_decl, m_manager->mk_bool_sort(), 
+                                       func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
     if (m_manager->int_real_coercions() && use_coercion(k)) {
         return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl));
     }
@@ -533,6 +549,7 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
     op_names.push_back(builtin_name("*",OP_MUL));
     op_names.push_back(builtin_name("/",OP_DIV));
     op_names.push_back(builtin_name("div",OP_IDIV));
+    op_names.push_back(builtin_name("divides",OP_IDIVIDES));
     op_names.push_back(builtin_name("rem",OP_REM));
     op_names.push_back(builtin_name("mod",OP_MOD));
     op_names.push_back(builtin_name("to_real",OP_TO_REAL));

src/ast/arith_decl_plugin.h

@@ -46,6 +46,7 @@ enum arith_op_kind {
     OP_MUL,
     OP_DIV,
     OP_IDIV,
+    OP_IDIVIDES,
     OP_REM,
     OP_MOD,
     OP_TO_REAL,

src/ast/rewriter/arith_rewriter.cpp

@@ -66,6 +66,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
         SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break;
     case OP_IDIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; }
         SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break;
+    case OP_IDIVIDES: SASSERT(num_args == 1); st = mk_idivides(f->get_parameter(0).get_int(), args[0], result); break;
     case OP_MOD: SASSERT(num_args == 2); st = mk_mod_core(args[0], args[1], result); break;
     case OP_REM: SASSERT(num_args == 2); st = mk_rem_core(args[0], args[1], result); break;
     case OP_UMINUS: SASSERT(num_args == 1);  st = mk_uminus(args[0], result); break;
@@ -792,6 +793,11 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul
     return BR_FAILED;
 }
 
+br_status arith_rewriter::mk_idivides(unsigned k, expr * arg, expr_ref & result) {
+    result = m().mk_eq(m_util.mk_mod(arg, m_util.mk_int(k)), m_util.mk_int(0));
+    return BR_REWRITE2;
+}
+
 br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result) {
     set_curr_sort(m().get_sort(arg1));
     numeral v1, v2;

src/ast/rewriter/arith_rewriter.h

@@ -143,6 +143,7 @@ public:
 
     br_status mk_div_core(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_idivides(unsigned k, expr * arg, expr_ref & result);
     br_status mk_mod_core(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_rem_core(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_power_core(expr* arg1, expr* arg2, expr_ref & result);

src/ast/rewriter/seq_rewriter.cpp

@@ -1866,6 +1866,53 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
     }
 }
 
+bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) {
+    m_lhs.reset();
+    m_util.str.get_concat(a, m_lhs);
+    TRACE("seq", tout << expr_ref(a, m()) << " " << expr_ref(b, m()) << "\n";);
+    zstring s;
+    for (unsigned i = 0; i < m_lhs.size(); ++i) {
+        expr* e = m_lhs.get(i);
+        if (m_util.str.is_empty(e)) {
+            continue;
+        }
+
+        if (m_util.str.is_string(e, s)) {
+            unsigned sz = s.length();
+            expr_ref_vector es(m());
+            for (unsigned j = 0; j < sz; ++j) {
+                es.push_back(m_util.str.mk_char(s, j));
+            }
+            es.append(m_lhs.size() - i, m_lhs.c_ptr() + i);
+            for (unsigned j = 0; j < sz; ++j) {
+                disj.push_back(m_util.str.mk_prefix(b, m_util.str.mk_concat(es.size() - j, es.c_ptr() + j)));
+            }
+            continue;
+        }
+        if (m_util.str.is_unit(e)) {
+            disj.push_back(m_util.str.mk_prefix(b, m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i)));
+            continue;
+        }
+
+        if (m_util.str.is_string(b, s)) {
+            expr* all = m_util.re.mk_full_seq(m_util.re.mk_re(m().get_sort(b)));
+            std::cout << sort_ref(m().get_sort(all), m()) << "\n";
+            disj.push_back(m_util.re.mk_in_re(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i),
+                                              m_util.re.mk_concat(all, m_util.str.mk_concat(m_util.re.mk_to_re(b), all))));
+            return true;
+        }
+
+        if (i == 0) {
+            return false;
+        }
+        disj.push_back(m_util.str.mk_contains(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i), b));
+        return true;
+    }
+    disj.push_back(m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b))));
+    return true;
+}
+
+
 expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
     SASSERT(n > 0);
     ptr_vector<expr> bs;

src/ast/rewriter/seq_rewriter.h

@@ -168,6 +168,8 @@ public:
 
     bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change);
 
+    bool reduce_contains(expr* a, expr* b, expr_ref_vector& disj);
+
     void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& lhs, expr_ref_vector& rhs);
 
 

src/cmd_context/cmd_context.cpp

@@ -1063,7 +1063,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
         return;
     }
     if (num_indices > 0)
-        throw cmd_exception("invalid use of indexed indentifier, unknown builtin function ", s);
+        throw cmd_exception("invalid use of indexed identifier, unknown builtin function ", s);
     expr* _t;
     if (macros_find(s, num_args, args, _t)) {
         TRACE("macro_bug", tout << "well_sorted_check_enabled(): " << well_sorted_check_enabled() << "\n";

src/smt/mam.cpp

@@ -401,11 +401,11 @@ namespace smt {
         label_hasher &             m_lbl_hasher;
         func_decl *                m_root_lbl;
         unsigned                   m_num_args; //!< we need this information to avoid the nary *,+ crash bug
-        unsigned char              m_filter_candidates;
+        bool                       m_filter_candidates;
         unsigned                   m_num_regs;
         unsigned                   m_num_choices;
         instruction *              m_root;
-        enode_vector               m_candidates;
+        obj_hashtable<enode>       m_candidates;
 #ifdef Z3DEBUG
         context *                  m_context;
         ptr_vector<app>            m_patterns;
@@ -531,7 +531,7 @@ namespace smt {
         }
 
         bool filter_candidates() const {
-            return m_filter_candidates != 0;
+            return m_filter_candidates;
         }
 
         const instruction * get_root() const {
@@ -539,7 +539,7 @@ namespace smt {
         }
 
         void add_candidate(enode * n) {
-            m_candidates.push_back(n);
+            m_candidates.insert(n);
         }
 
         bool has_candidates() const {
@@ -550,7 +550,7 @@ namespace smt {
             m_candidates.reset();
         }
 
-        enode_vector const & get_candidates() const {
+        obj_hashtable<enode> const & get_candidates() const {
             return m_candidates;
         }
 
@@ -2001,7 +2001,9 @@ namespace smt {
             TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout););
             init(t);
             if (t->filter_candidates()) {
+                //t->display(std::cout << "ncf: " << t->get_candidates().size() << "\n");
                 for (enode* app : t->get_candidates()) {
+                    TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
                     if (!app->is_marked() && app->is_cgr()) {
                         if (m_context.resource_limits_exceeded() || !execute_core(t, app))
                             return;
@@ -2014,6 +2016,9 @@ namespace smt {
                 }
             }
             else {
+                //t->display(std::cout << "ncu: " << t->get_candidates().size() << "\n");
+                //for (enode* app : t->get_candidates()) { std::cout << expr_ref(app->get_owner(), m_ast_manager) << "\n"; }
+                //std::cout.flush();
                 for (enode* app : t->get_candidates()) {
                     TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
                     if (app->is_cgr()) {
@@ -3516,9 +3521,7 @@ namespace smt {
                     std::cout << "Avg. " << static_cast<double>(total_sz)/static_cast<double>(counter) << ", Max. " << max_sz << "\n";
 #endif
 
-                enode_vector::iterator it1  = v->begin();
+                for (enode* n : *v) {
-                enode_vector::iterator end1 = v->end();
-                for (; it1 != end1; ++it1) {
                     // Two different kinds of mark are used:
                     // - enode mark field:  it is used to mark the already processed parents.
                     // - enode mark2 field: it is used to mark the roots already added to be processed in the next level.
@@ -3527,7 +3530,7 @@ namespace smt {
                     // and Z3 may fail to find potential new matches.
                     //
                     // The file regression\acu.sx exposed this problem.
-                    enode * curr_child = (*it1)->get_root();
+                    enode * curr_child = n->get_root();
 
                     if (m_use_filters && curr_child->get_plbls().empty_intersection(filter))
                         continue;
@@ -3591,7 +3594,7 @@ namespace smt {
                                          is_eq(curr_tree->m_ground_arg, curr_parent->get_arg(curr_tree->m_ground_arg_idx))
                                          )) {
                                         if (curr_tree->m_code) {
-                                            TRACE("mam_path_tree", tout << "found candidate\n";);
+                                            TRACE("mam_path_tree", tout << "found candidate " << expr_ref(curr_parent->get_owner(), m_ast_manager) << "\n";);
                                             add_candidate(curr_tree->m_code, curr_parent);
                                         }
                                         if (curr_tree->m_first_child) {

src/smt/smt_context.cpp

@@ -1351,18 +1351,9 @@ namespace smt {
        \remark The method assign_eq adds a new entry on this queue.
     */
     bool context::propagate_eqs() {
-        for (unsigned i = 0; i < m_eq_propagation_queue.size(); i++) {
+        TRACE("add_eq", tout << m_eq_propagation_queue.size() << "\n";);
+        for (unsigned i = 0; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) {
             new_eq & entry = m_eq_propagation_queue[i];
-#if 0
-            static unsigned counter1 = 0;
-            static unsigned counter2 = 0;
-            if (entry.m_lhs->is_eq() || entry.m_rhs->is_eq())
-                counter1++;
-            else
-                counter2++;
-            if ((counter1 + counter2) % 10000 == 0)
-                std::cout << counter1 << " " << counter2 << "\n";
-#endif
             add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification);
             if (inconsistent())
                 return false;
@@ -1376,7 +1367,7 @@ namespace smt {
     */
     bool context::propagate_atoms() {
         SASSERT(!inconsistent());
-        for (unsigned i = 0; i < m_atom_propagation_queue.size(); i++) {
+        for (unsigned i = 0; i < m_atom_propagation_queue.size() && !get_cancel_flag(); i++) {
             SASSERT(!inconsistent());
             literal  l = m_atom_propagation_queue[i];
             bool_var v = l.var();
@@ -1558,16 +1549,17 @@ namespace smt {
     lbool context::get_assignment(expr * n) const {
         if (m_manager.is_false(n))
             return l_false;
-        if (m_manager.is_not(n))
+        expr* arg = nullptr;
-            return ~get_assignment_core(to_app(n)->get_arg(0));
+        if (m_manager.is_not(n, arg))
+            return ~get_assignment_core(arg);
         return get_assignment_core(n);
     }
 
     lbool context::find_assignment(expr * n) const {
         if (m_manager.is_false(n))
             return l_false;
-        if (m_manager.is_not(n)) {
+        expr* arg = nullptr;
-            expr * arg = to_app(n)->get_arg(0);
+        if (m_manager.is_not(n, arg)) {
             if (b_internalized(arg))
                 return ~get_assignment_core(arg);
             return l_undef;
@@ -1752,6 +1744,10 @@ namespace smt {
                 return false;
             if (!propagate_eqs())
                 return false;
+            if (get_cancel_flag()) {
+                m_qhead = qhead;
+                return true;
+            }
             propagate_th_eqs();
             propagate_th_diseqs();
             if (inconsistent())
@@ -3264,6 +3260,7 @@ namespace smt {
     }
 
     void context::reset_assumptions() {
+        TRACE("unsat_core_bug", tout << "reset " << m_assumptions << "\n";);
         for (literal lit : m_assumptions) 
             get_bdata(lit.var()).m_assumption = false;
         m_assumptions.reset();
@@ -4106,9 +4103,7 @@ namespace smt {
         }
 
         SASSERT(!inconsistent());
-        unsigned sz = m_b_internalized_stack.size();
+        for (expr * curr : m_b_internalized_stack) { 
-        for (unsigned i = 0; i < sz; i++) {
-            expr * curr = m_b_internalized_stack.get(i);
             if (is_relevant(curr) && get_assignment(curr) == l_true) {
                 // if curr is a label literal, then its tags will be copied to result.
                 m_manager.is_label_lit(curr, result);
@@ -4124,9 +4119,7 @@ namespace smt {
     void context::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) {
         SASSERT(!inconsistent());
         buffer<symbol> lbls;
-        unsigned sz = m_b_internalized_stack.size();
+        for (expr * curr : m_b_internalized_stack) {
-        for (unsigned i = 0; i < sz; i++) {
-            expr * curr = m_b_internalized_stack.get(i);
             if (is_relevant(curr) && get_assignment(curr) == l_true) {
                 lbls.reset();
                 if (m_manager.is_label_lit(curr, lbls)) {

src/smt/smt_context.h

@@ -491,7 +491,7 @@ namespace smt {
         }
 
         bool tracking_assumptions() const {
-            return m_search_lvl > m_base_lvl;
+            return !m_assumptions.empty() && m_search_lvl > m_base_lvl;
         }
 
         expr * bool_var2expr(bool_var v) const {
@@ -1011,6 +1011,7 @@ namespace smt {
 
         void push_eq(enode * lhs, enode * rhs, eq_justification const & js) {
             SASSERT(lhs != rhs);
+            SASSERT(lhs->get_root() != rhs->get_root());
             m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js));
         }
 

src/smt/theory_seq.cpp

@@ -5163,7 +5163,21 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
         }
     }
     else if (m_util.str.is_contains(e, e1, e2)) {
-        if (is_true) {
+        expr_ref_vector disj(m);
+        if (m_seq_rewrite.reduce_contains(e1, e2, disj)) {
+            literal_vector lits;
+            literal lit = mk_literal(e);
+            lits.push_back(~lit);
+            for (expr* d : disj) {
+                lits.push_back(mk_literal(d));
+            }
+            ++m_stats.m_add_axiom;            
+            ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+            for (expr* d : disj) {
+                add_axiom(lit, ~mk_literal(d));
+            }
+        }
+        else if (is_true) {
             expr_ref f1 = mk_skolem(m_indexof_left, e1, e2);
             expr_ref f2 = mk_skolem(m_indexof_right, e1, e2);
             f = mk_concat(f1, e2, f2);