fix memory leak in SAT solver exposed by regression tests

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

src/sat/sat_asymm_branch.cpp

@@ -78,8 +78,12 @@ namespace sat {
         clause_vector::iterator end = s.m_clauses.end();
         try {
             for (; it != end; ++it) {
-                if (s.inconsistent())
+                if (s.inconsistent()) {
+                    for (; it != end; ++it, ++it2) {
+                        *it2 = *it;
+                    }
                     break;
+                }
                 SASSERT(s.m_qhead == s.m_trail.size());
                 if (m_counter < limit || s.inconsistent()) {
                     *it2 = *it;

src/sat/sat_clause.cpp

@@ -169,6 +169,7 @@ namespace sat {
 #endif
         void * mem = m_allocator.allocate(size);
         clause * cls = new (mem) clause(m_id_gen.mk(), num_lits, lits, learned);
+        TRACE("sat", tout << "alloc: " << cls->id() << " " << cls << " " << *cls << " " << (learned?"l":"a") << "\n";);
         SASSERT(!learned || cls->is_learned());
         return cls;
     }

src/sat/sat_solver.cpp

@@ -461,6 +461,7 @@ namespace sat {
     }
 
     void solver::dettach_clause(clause & c) {
+        TRACE("sat", tout << c.id() << "\n";);
         if (c.size() == 3)
             dettach_ter_clause(c);
         else

src/smt/mam.cpp

@@ -3936,7 +3936,7 @@ namespace smt {
         }
 
         virtual bool is_shared(enode * n) const {
-            return m_shared_enodes.contains(n);
+            return !m_shared_enodes.empty() && m_shared_enodes.contains(n);
         }
         
         // This method is invoked when n becomes relevant.

src/smt/smt_context.cpp

@@ -4025,8 +4025,9 @@ namespace smt {
             return false;
         }
         case 1: {
-            if (m_qmanager->is_shared(n))
+            if (m_qmanager->is_shared(n)) {
                 return true;
+            }
             
             // the variabe is shared if the equivalence class of n 
             // contains a parent application.
@@ -4071,7 +4072,8 @@ namespace smt {
             // the theories of (array int int) and (array (array int int) int).
             // Remark: The inconsistency is not going to be detected if they are
             // not marked as shared.
-            return get_theory(th_id)->is_shared(l->get_th_var());
+            bool result = get_theory(th_id)->is_shared(l->get_th_var());
+            return result;
         }
         default:
             return true;

src/smt/smt_enode.h

@@ -192,6 +192,7 @@ namespace smt {
             return m_owner->hash();
         }
 
+
         enode * get_root() const { 
             return m_root; 
         }

src/smt/smt_quantifier.cpp

@@ -396,12 +396,14 @@ namespace smt {
         scoped_ptr<model_checker>   m_model_checker;
         unsigned                    m_new_enode_qhead;
         unsigned                    m_lazy_matching_idx;
+        bool                        m_active;
     public:
         default_qm_plugin():
             m_qm(0), 
             m_context(0), 
             m_new_enode_qhead(0), 
-            m_lazy_matching_idx(0) {
+            m_lazy_matching_idx(0),
+            m_active(false) {
         }
         
         virtual ~default_qm_plugin() {
@@ -427,7 +429,7 @@ namespace smt {
 
         virtual bool model_based() const { return m_fparams->m_mbqi; }
 
-        virtual bool mbqi_enabled(quantifier *q) const { 
+        virtual bool mbqi_enabled(quantifier *q) const {             
             if(!m_fparams->m_mbqi_id) return true;
             const symbol &s = q->get_qid();
             size_t len = strlen(m_fparams->m_mbqi_id);
@@ -443,6 +445,7 @@ namespace smt {
        */
         virtual void add(quantifier * q) {
             if (m_fparams->m_mbqi && mbqi_enabled(q)) {
+                m_active = true;
                 m_model_finder->register_quantifier(q);
             }
         }
@@ -475,6 +478,7 @@ namespace smt {
         }
 
         virtual void assign_eh(quantifier * q) {
+            m_active = true;
             if (m_fparams->m_ematching) {
                 bool has_unary_pattern = false;
                 unsigned num_patterns = q->get_num_patterns();
@@ -537,7 +541,7 @@ namespace smt {
         }
 
         virtual bool is_shared(enode * n) const {
-            return (m_mam->is_shared(n) || m_lazy_mam->is_shared(n));
+            return m_active && (m_mam->is_shared(n) || m_lazy_mam->is_shared(n));
         }
 
         virtual void adjust_model(proto_model * m) {

src/smt/theory_arith_aux.h

@@ -618,8 +618,10 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::remove_fixed_vars_from_base() {
         int num = get_num_vars();
+        //std::cout << "num vars " << num << "\n";
         for (theory_var v = 0; v < num; v++) {
             if (is_base(v) && is_fixed(v)) {
+                //std::cout << "fixed base " << v << " \n"; // << mk_pp(get_enode(v)->get_owner(), get_manager()) << "\n";
                 row const & r = m_rows[get_var_row(v)];
                 typename vector<row_entry>::const_iterator it  = r.begin_entries();
                 typename vector<row_entry>::const_iterator end = r.end_entries();

src/smt/theory_seq.cpp

@@ -234,6 +234,7 @@ bool theory_seq::branch_variable() {
     unsigned sz = m_eqs.size();
     expr_ref_vector ls(m), rs(m);
     int start = ctx.get_random_value();
+    unsigned s = 0;
     for (unsigned i = 0; i < sz; ++i) {
         unsigned k = (i + start) % sz;
         eq e = m_eqs[k];
@@ -242,21 +243,19 @@ bool theory_seq::branch_variable() {
         m_util.str.get_concat(e.m_lhs, ls);
         m_util.str.get_concat(e.m_rhs, rs);
 
-#if 1       
-        if (find_branch_candidate(e.m_dep, ls, rs)) {
+        s = find_branch_start(e.m_lhs, e.m_rhs);
+        bool found = find_branch_candidate(s, e.m_dep, ls, rs);
+        insert_branch_start(e.m_lhs, e.m_rhs, s);
+        if (found) {
             return true;
         }
-        if (find_branch_candidate(e.m_dep, rs, ls)) {
+        s = find_branch_start(e.m_lhs, e.m_rhs);
+        found = find_branch_candidate(s, e.m_dep, rs, ls);
+        insert_branch_start(e.m_rhs, e.m_lhs, s);
+        if (found) {
             return true;
         }
-#else
-        if (find_branch_candidate(e.m_dep, ls.back(), rs)) {
-            return true;
-        }
-        if (find_branch_candidate(e.m_dep, rs.back(), ls)) {
-            return true;
-        }
-#endif
+
 #if 0
         if (!has_length(e.m_lhs)) {
             enforce_length(ensure_enode(e.m_lhs));
@@ -269,7 +268,20 @@ bool theory_seq::branch_variable() {
     return ctx.inconsistent();
 }
 
-bool theory_seq::find_branch_candidate(dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs) {
+void theory_seq::insert_branch_start(expr* l, expr* r, unsigned s) {
+    m_branch_start.insert(l, r, s);
+    m_trail_stack.push(pop_branch(m, l, r));
+}
+
+unsigned theory_seq::find_branch_start(expr* l, expr* r) {
+    unsigned s = 0;
+    if (m_branch_start.find(l, r, s)) {
+        return s;
+    }
+    return 0;
+}
+
+bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs) {
 
     if (ls.empty()) {
         return false;
@@ -280,29 +292,34 @@ bool theory_seq::find_branch_candidate(dependency* dep, expr_ref_vector const& l
         return false;
     }
 
-    bool all_units = true;
-    expr_ref_vector cases(m);
-    expr_ref v0(m), v(m);
+    expr_ref v0(m);
     v0 = m_util.str.mk_empty(m.get_sort(l));
     if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr()) && l_false != assume_equality(l, v0)) {
         TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
         return true;
     }
-    for (unsigned j = 0; j < rs.size(); ++j) {
+//    start = 0;
+    for (; start < rs.size(); ++start) {
+        unsigned j = start;
         if (occurs(l, rs[j])) {
             return false;
         }
         SASSERT(!m_util.str.is_string(rs[j]));
-        all_units &= m_util.str.is_unit(rs[j]);
         if (!can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - j - 1, rs.c_ptr() + j + 1)) {
             continue;
         }
         v0 = m_util.str.mk_concat(j + 1, rs.c_ptr());
         if (l_false != assume_equality(l, v0)) {
             TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
+            ++start;
             return true;
         }
     }           
+
+    bool all_units = true;
+    for (unsigned j = 0; all_units && j < rs.size(); ++j) {    
+        all_units &= m_util.str.is_unit(rs[j]);
+    }
     if (all_units) {
         literal_vector lits;
         lits.push_back(~mk_eq_empty(l));
@@ -1634,11 +1651,15 @@ void theory_seq::add_length_axiom(expr* n) {
         m_util.str.is_string(x)) {
         expr_ref len(n, m);
         m_rewrite(len);
-        if (n != len) {
-            TRACE("seq", tout << "Add length coherence for " << mk_pp(n, m) << "\n";);
-            add_axiom(mk_eq(n, len, false));
-            m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
-        }
+        SASSERT(n != len);
+        add_axiom(mk_eq(len, n, false));
+
+        //std::cout << len << "\n";
+        //len = m_autil.mk_add(len, m_autil.mk_mul(m_autil.mk_int(-1), n));
+        //TRACE("seq", tout << "Add length coherence for " << mk_pp(n, m) << "\n";);
+        //add_axiom(mk_literal(m_autil.mk_le(len, m_autil.mk_int(0))));
+        //add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0))));
+        m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
     }
     else {
         add_axiom(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));        

src/smt/theory_seq.h

@@ -258,6 +258,7 @@ namespace smt {
             replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
             virtual void operator()(theory_seq& th) {
                 th.check_length_coherence(m_e);
+                m_e.reset();
             }
         };
 
@@ -267,6 +268,7 @@ namespace smt {
             replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
             virtual void operator()(theory_seq& th) {
                 th.enque_axiom(m_e);
+                m_e.reset();
             }
         };
 
@@ -279,6 +281,17 @@ namespace smt {
             }
         };
 
+        class pop_branch : public trail<theory_seq> {
+            expr_ref m_l, m_r;
+        public:
+            pop_branch(ast_manager& m, expr* l, expr* r): m_l(l, m), m_r(r, m) {}
+            virtual void undo(theory_seq& th) {
+                th.m_branch_start.erase(m_l, m_r);
+                m_l.reset();
+                m_r.reset();
+            }
+        };
+
         void erase_index(unsigned idx, unsigned i);
 
         struct stats {
@@ -386,7 +399,10 @@ namespace smt {
         void propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs = false);
         void set_conflict(dependency* dep, literal_vector const& lits = literal_vector());
 
-        bool find_branch_candidate(dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs);
+        obj_pair_map<expr, expr, unsigned> m_branch_start;
+        void insert_branch_start(expr* l, expr* r, unsigned s);
+        unsigned find_branch_start(expr* l, expr* r);
+        bool find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs);
         bool can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const;
         lbool assume_equality(expr* l, expr* r);