bv fixes and tuning (#4703)

* heap size information

* bv tuning

* fix #4701

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

* throw on set-has-size #4700

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

src/ast/array_decl_plugin.cpp

@@ -460,6 +460,7 @@ func_decl * array_decl_plugin::mk_set_has_size(unsigned arity, sort * const* dom
         m_manager->raise_exception("set-has-size takes two arguments");
         return nullptr;
     }    
+    m_manager->raise_exception("set-has-size is not supported");
     // domain[0] is a Boolean array,
     // domain[1] is Int
     arith_util arith(*m_manager);

src/ast/euf/euf_egraph.cpp

@@ -22,6 +22,7 @@ Module Name:
 
 namespace euf {
 
+
     void egraph::undo_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
         enode* r2 = r1->get_root();
         r2->dec_class_size(r1->class_size());
@@ -113,6 +114,7 @@ namespace euf {
 
     egraph::egraph(ast_manager& m) : m(m), m_table(m), m_exprs(m) {
         m_tmp_eq = enode::mk_tmp(m_region, 2);
+        // m_updates.reserve(10000, update_record(nullptr));
     }
 
     egraph::~egraph() {
@@ -143,14 +145,15 @@ namespace euf {
         if (is_eq) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits;
     }
 
-    void egraph::new_diseq(enode* n1) {
-        SASSERT(n1->is_equality());
-        enode* arg1 = n1->get_arg(0), * arg2 = n1->get_arg(1);
+    void egraph::new_diseq(enode* n) {
+        SASSERT(n->is_equality());
+        SASSERT(n->value() == l_false);
+        enode* arg1 = n->get_arg(0), * arg2 = n->get_arg(1);
         enode* r1 = arg1->get_root();
         enode* r2 = arg2->get_root();
         TRACE("euf", tout << "new-diseq:  " << mk_pp(r1->get_expr(), m) << " " << mk_pp(r2->get_expr(), m) << ": " << r1->has_th_vars() << " " << r2->has_th_vars() << "\n";);
         if (r1 == r2) {
-            add_literal(n1, true);
+            add_literal(n, true);
             return;
         }
         if (!r1->has_th_vars())
@@ -163,15 +166,15 @@ namespace euf {
                 return;
             theory_var v1 = arg1->get_closest_th_var(id);
             theory_var v2 = arg2->get_closest_th_var(id);
-            add_th_diseq(id, v1, v2, n1->get_expr());
+            add_th_diseq(id, v1, v2, n->get_expr());
             return;
         }
         for (auto p : euf::enode_th_vars(r1)) {
             if (!th_propagates_diseqs(p.get_id()))
                 continue;
             for (auto q : euf::enode_th_vars(r2))
                 if (p.get_id() == q.get_id()) 
-                    add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n1->get_expr());
+                    add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n->get_expr());
         }
     }
 
@@ -250,9 +253,9 @@ namespace euf {
         }
     }
 
-    void egraph::set_value(enode* n, lbool value) {
+    void egraph::set_value(enode* n, lbool value) {        
         force_push();
-        VERIFY(n->value() == l_undef);
+        SASSERT(n->value() == l_undef);
         n->set_value(value);
         m_updates.push_back(update_record(n, update_record::value_assignment()));
     }
@@ -331,9 +334,8 @@ namespace euf {
     }
 
     void egraph::merge(enode* n1, enode* n2, justification j) {
-        if (!n1->merge_enabled() && !n2->merge_enabled()) {
-            return;
-        }
+        if (!n1->merge_enabled() && !n2->merge_enabled()) 
+            return;        
         SASSERT(m.get_sort(n1->get_expr()) == m.get_sort(n2->get_expr()));
         enode* r1 = n1->get_root();
         enode* r2 = n2->get_root();
@@ -357,7 +359,7 @@ namespace euf {
         if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr()))) {
             add_literal(n1, false);
         }
-        if (n1->is_equality() && r2->value() == l_false)
+        if (n1->is_equality() && n1->value() == l_false)
             new_diseq(n1);       
         unsigned num_merge = 0, num_eqs = 0;
         for (enode* p : enode_parents(n1)) {

src/ast/euf/euf_egraph.h

@@ -207,7 +207,7 @@ namespace euf {
            \brief merge nodes, all effects are deferred to the propagation step.
          */
         void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); }        
-        void new_diseq(enode* n1);
+        void new_diseq(enode* n);
 
 
         /**

src/cmd_context/cmd_context.cpp

@@ -285,7 +285,8 @@ bool cmd_context::contains_func_decl(symbol const& s, unsigned n, sort* const* d
 }
 
 bool cmd_context::contains_macro(symbol const& s) const {
-    return m_macros.contains(s);
+    macro_decls decls;
+    return m_macros.find(s, decls) && !decls.empty();
 }
 
 bool cmd_context::contains_macro(symbol const& s, func_decl* f) const {
@@ -851,6 +852,7 @@ void cmd_context::insert(symbol const & s, unsigned arity, sort *const* domain,
     insert_macro(s, arity, domain, t);
     if (!m_global_decls) {
         m_macros_stack.push_back(s);
+
     }
 }
 
@@ -890,6 +892,8 @@ void cmd_context::model_add(symbol const & s, unsigned arity, sort *const* domai
     fs.insert(m(), fn);
     VERIFY(fn->get_range() == m().get_sort(t));
     m_mc0->add(fn, t);
+    if (!m_global_decls)
+        m_func_decls_stack.push_back(sf_pair(s, fn));
 }
 
 void cmd_context::model_del(func_decl* f) {
@@ -1424,10 +1428,8 @@ void cmd_context::restore_macros(unsigned old_sz) {
     SASSERT(old_sz <= m_macros_stack.size());
     svector<symbol>::iterator it  = m_macros_stack.begin() + old_sz;
     svector<symbol>::iterator end = m_macros_stack.end();
-    for (; it != end; ++it) {
-        symbol const & s = *it;
-        erase_macro(s);
-    }
+    for (; it != end; ++it) 
+        erase_macro(*it);    
     m_macros_stack.shrink(old_sz);
 }
 

src/cmd_context/cmd_context.h

@@ -81,6 +81,7 @@ class macro_decls {
     macro_decls() { m_decls = nullptr; }
     void finalize(ast_manager& m);
     bool insert(ast_manager& m, unsigned arity, sort *const* domain, expr* body);
+    bool empty() const { return !m_decls || m_decls->empty(); }
     expr* find(unsigned arity, sort *const* domain) const;
     void erase_last(ast_manager& m);
     vector<macro_decl>::iterator begin() const { return m_decls->begin(); }

src/sat/sat_elim_eqs.cpp

@@ -218,10 +218,12 @@ namespace sat {
 
     void elim_eqs::save_elim(literal_vector const & roots, bool_var_vector const & to_elim) {
         model_converter & mc = m_solver.m_mc;
+
         for (bool_var v : to_elim) {
             literal  l(v, false);
             literal r  = roots[v];
             SASSERT(v != r.var());
+
             if (m_solver.m_cut_simplifier) m_solver.m_cut_simplifier->set_root(v, r);
             bool set_root = m_solver.set_root(l, r);
             bool root_ok = !m_solver.is_external(v) || set_root;

src/sat/sat_scc.cpp

@@ -203,6 +203,7 @@ namespace sat {
                             in_s[l2_idx] = false;
                             literal  l2 = to_literal(l2_idx);
                             bool_var v2 = l2.var();
+
                             if (roots[v2] == null_literal) {
                                 if (l2.sign()) {
                                     roots[v2] = ~r;

src/sat/sat_simplifier.cpp

@@ -995,6 +995,7 @@ namespace sat {
             literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); }
             bool empty() const { return m_queue.empty(); }
             void reset() { m_queue.reset(); }
+            unsigned size() const { return m_queue.size(); }
         };
 
         simplifier &      s;
@@ -1589,9 +1590,8 @@ namespace sat {
             SASSERT(!s.is_external(l));
             model_converter::entry& new_entry = m_mc.mk(k, l.var());
             for (literal lit : c) {
-                if (lit != l && process_var(lit.var())) {
-                    m_queue.decreased(~lit);
-                }
+                if (lit != l && process_var(lit.var())) 
+                    m_queue.decreased(~lit);                
             }
             m_mc.insert(new_entry, m_covered_clause);
             m_mc.set_clause(new_entry, c);
@@ -1605,7 +1605,8 @@ namespace sat {
             s.set_learned(l1, l2);
             m_mc.insert(new_entry, m_covered_clause);
             m_mc.set_clause(new_entry, l1, l2);
-            m_queue.decreased(~l2);
+            if (process_var(l2.var()))
+                m_queue.decreased(~l2);
         }
 
         void bca() {

src/sat/sat_solver.cpp

@@ -318,24 +318,7 @@ namespace sat {
     }
 
     void solver::set_external(bool_var v) {
-        if (m_external[v]) return;
         m_external[v] = true;
-        if (!m_ext) return;
-
-        lbool val = value(v);
-
-        switch (val) {
-        case l_true: {
-            m_ext->asserted(literal(v, false));
-            break;
-        }
-        case l_false: {
-            m_ext->asserted(literal(v, true));
-            break;
-        }
-        default:
-            break;
-        }
     }
 
     void solver::set_eliminated(bool_var v, bool f) { 
@@ -347,10 +330,13 @@ namespace sat {
 
     clause* solver::mk_clause(unsigned num_lits, literal * lits, sat::status st) {
         m_model_is_current = false;
+        for (unsigned i = 0; i < num_lits; i++) 
+            VERIFY(!was_eliminated(lits[i]));
+
         DEBUG_CODE({
                 for (unsigned i = 0; i < num_lits; i++) {
-                    CTRACE("sat", m_eliminated[lits[i].var()], tout << lits[i] << " was eliminated\n";);
-                    SASSERT(m_eliminated[lits[i].var()] == false);
+                    CTRACE("sat", was_eliminated(lits[i]), tout << lits[i] << " was eliminated\n";);
+                    SASSERT(!was_eliminated(lits[i]));
                 }
         });
 
@@ -587,7 +573,7 @@ namespace sat {
         m_stats.m_mk_clause++;
         clause * r = alloc_clause(num_lits, lits, st.is_redundant());
         SASSERT(!st.is_redundant() || r->is_learned());
-        bool reinit = attach_nary_clause(*r);
+        bool reinit = attach_nary_clause(*r, st.is_sat() && st.is_redundant());
         if (reinit || has_variables_to_reinit(*r)) push_reinit_stack(*r);
         if (st.is_redundant()) {
             m_learned.push_back(r);
@@ -604,11 +590,11 @@ namespace sat {
         return r;
     }
 
-    bool solver::attach_nary_clause(clause & c) {
+    bool solver::attach_nary_clause(clause & c, bool is_asserting) {
         bool reinit = false;
         clause_offset cls_off = cls_allocator().get_offset(&c);
         if (!at_base_lvl()) {
-            if (c.is_learned() && !c.on_reinit_stack()) {
+            if (is_asserting) {
                 unsigned w2_idx = select_learned_watch_lit(c);
                 std::swap(c[1], c[w2_idx]);
             }
@@ -626,7 +612,7 @@ namespace sat {
                     level = std::max(level, lvl(c[i]));
                 }
                 assign(c[1], justification(level, cls_off));
-                reinit = !c.is_learned();
+                reinit |= !c.is_learned();
             }
             else if (value(c[1]) == l_false) {
                 m_stats.m_propagate++;
@@ -635,7 +621,7 @@ namespace sat {
                     level = std::max(level, lvl(c[i]));
                 }
                 assign(c[0], justification(level, cls_off));
-                reinit = !c.is_learned();
+                reinit |= !c.is_learned();
             }
         }
         unsigned some_idx = c.size() >> 1;
@@ -655,7 +641,7 @@ namespace sat {
         if (ENABLE_TERNARY && c.size() == 3)
             reinit = attach_ter_clause(c, c.is_learned() ? sat::status::redundant() : sat::status::asserted());
         else
-            reinit = attach_nary_clause(c);
+            reinit = attach_nary_clause(c, c.is_learned() && !c.on_reinit_stack());
     }
 
     void solver::set_learned(clause& c, bool redundant) {
@@ -1332,16 +1318,18 @@ namespace sat {
                 return l_undef;
             }
 
-            if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
+            log_stats();
+            if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {               
                 m_restart_threshold = m_config.m_burst_search;
                 lbool r = bounded_search();
-                if (r != l_undef)
+                log_stats();
+                if (r != l_undef) 
                     return r;
+
                 pop_reinit(scope_lvl());
                 m_conflicts_since_restart = 0;
                 m_restart_threshold = m_config.m_restart_initial;
             }
-            log_stats();
             lbool is_sat = l_undef;
             while (is_sat == l_undef && !should_cancel()) {
                 if (inconsistent()) is_sat = resolve_conflict_core();
@@ -1353,6 +1341,7 @@ namespace sat {
                 else if (should_simplify()) do_simplify();
                 else if (!decide()) is_sat = final_check();
             }
+            log_stats();
             return is_sat;
         }
         catch (const abort_solver &) {
@@ -3588,8 +3577,6 @@ namespace sat {
         if (!m_replay_assign.empty()) IF_VERBOSE(20, verbose_stream() << "replay assign: " << m_replay_assign.size() << "\n");
         for (unsigned i = m_replay_assign.size(); i-- > 0; ) {
             literal lit = m_replay_assign[i];
-            if (m_ext && m_external[lit.var()])
-                m_ext->asserted(lit);
             m_trail.push_back(lit);            
         }
 

src/sat/sat_solver.h

@@ -290,7 +290,7 @@ namespace sat {
         clause * mk_nary_clause(unsigned num_lits, literal * lits, status st);
         bool has_variables_to_reinit(clause const& c) const;
         bool has_variables_to_reinit(literal l1, literal l2) const;
-        bool attach_nary_clause(clause & c);
+        bool attach_nary_clause(clause & c, bool is_asserting);
         void attach_clause(clause & c, bool & reinit);
         void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
         void set_learned(clause& c, bool learned);

src/sat/smt/bv_ackerman.cpp

@@ -41,18 +41,22 @@ namespace bv {
         if (v1 > v2)
             std::swap(v1, v2);
         vv* n = m_tmp_vv;
-        n->v1 = v1;
-        n->v2 = v2;
+        n->set_var(v1, v2);
         vv* other = m_table.insert_if_not_there(n);        
         other->m_count++;
         update_glue(*other);
-        if (other->m_count > m_propagate_high_watermark || other->m_glue == 0)
-            s.s().set_should_simplify();
+
         vv::push_to_front(m_queue, other);
         if (other == n) {
             new_tmp();        
             gc();
         }
+        if (other->m_glue == 0) {
+            remove(other);
+            add_cc(v1, v2);
+        }
+        else if (other->m_count > m_propagate_high_watermark) 
+            s.s().set_should_simplify();
     }
 
     void ackerman::used_diseq_eh(euf::theory_var v1, euf::theory_var v2) {
@@ -61,17 +65,17 @@ namespace bv {
         if (v1 > v2)
             std::swap(v1, v2);
         vv* n = m_tmp_vv;
-        n->v1 = v1;
-        n->v2 = v2;
+        n->set_var(v1, v2);
         vv* other = m_table.insert_if_not_there(n);
         other->m_count++;
-        if (other->m_count > m_propagate_high_watermark || other->m_glue == 0)
-            s.s().set_should_simplify();
+
         vv::push_to_front(m_queue, other);
         if (other == n) {
             new_tmp();
             gc();
         }
+        if (other->m_count > m_propagate_high_watermark) 
+            s.s().set_should_simplify();
     }
 
     void ackerman::update_glue(vv& v) {

src/sat/smt/bv_ackerman.h

@@ -32,6 +32,7 @@ namespace bv {
             unsigned   m_glue{ UINT_MAX };
             vv():v1(euf::null_theory_var), v2(euf::null_theory_var) {}
             vv(euf::theory_var v1, euf::theory_var v2):v1(v1), v2(v2) {}
+            void set_var(euf::theory_var x, euf::theory_var y) { v1 = x; v2 = y; m_count = 0; m_glue = UINT_MAX; }
         };
 
         struct vv_eq {