Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/ast/simplifier/bv_simplifier_plugin.cpp

@@ -636,7 +636,31 @@ bool bv_simplifier_plugin::try_mk_extract(unsigned high, unsigned low, expr * ar
         if (!all_found) {
             return false;
         }
-        result = m_manager.mk_app(m_fid, a->get_decl_kind(), new_args.size(), new_args.c_ptr());
+        // We should not use mk_app because it does not guarantee that the result would be in simplified form.
+        // result = m_manager.mk_app(m_fid, a->get_decl_kind(), new_args.size(), new_args.c_ptr());
+        if (is_app_of(a, m_fid, OP_BAND))
+            mk_bv_and(new_args.size(), new_args.c_ptr(), result);
+        else if (is_app_of(a, m_fid, OP_BOR))
+            mk_bv_or(new_args.size(), new_args.c_ptr(), result);
+        else if (is_app_of(a, m_fid, OP_BXOR))
+            mk_bv_xor(new_args.size(), new_args.c_ptr(), result);
+        else if (is_app_of(a, m_fid, OP_BNOR))
+            mk_bv_nor(new_args.size(), new_args.c_ptr(), result);
+        else if (is_app_of(a, m_fid, OP_BNAND))
+            mk_bv_nand(new_args.size(), new_args.c_ptr(), result);
+        else if (is_app_of(a, m_fid, OP_BNOT)) {
+            SASSERT(new_args.size() == 1);
+            mk_bv_not(new_args[0], result);
+        }
+        else if (is_app_of(a, m_fid, OP_BADD))
+            mk_add(new_args.size(), new_args.c_ptr(), result);
+        else if (is_app_of(a, m_fid, OP_BMUL))
+            mk_mul(new_args.size(), new_args.c_ptr(), result);
+        else if (is_app_of(a, m_fid, OP_BSUB))
+            mk_sub(new_args.size(), new_args.c_ptr(), result);
+        else {
+            UNREACHABLE();
+        }
         return true;
     }
     else if (m_manager.is_ite(a)) {
@@ -747,16 +771,16 @@ void bv_simplifier_plugin::mk_bv_eq(expr* a1, expr* a2, expr_ref& result) {
         expr * arg1    = *it1;
         expr * arg2    = *it2;
         TRACE("expr_bv_util", tout << "low1: " << low1 << " low2: " << low2 << "\n";
-              ast_ll_pp(tout, m_manager, arg1); 
+              tout << mk_pp(arg1, m_manager) << "\n";
-              ast_ll_pp(tout, m_manager, arg2););
+              tout << mk_pp(arg2, m_manager) << "\n";);
         unsigned sz1  = get_bv_size(arg1);
         unsigned sz2  = get_bv_size(arg2);
         SASSERT(low1 < sz1 && low2 < sz2);
         unsigned rsz1 = sz1 - low1;
         unsigned rsz2 = sz2 - low2;
         TRACE("expr_bv_util", tout << "rsz1: " << rsz1 << " rsz2: " << rsz2 << "\n";
-              ast_ll_pp(tout, m_manager, arg1); ast_ll_pp(tout, m_manager, arg2););
+              tout << mk_pp(arg1, m_manager) << "\n";
-
+              tout << mk_pp(arg2, m_manager) << "\n";);
 
         if (rsz1 == rsz2) {
             mk_extract(sz1 - 1, low1, arg1, lhs);
@@ -826,9 +850,9 @@ void bv_simplifier_plugin::mk_eq_core(expr * arg1, expr * arg2, expr_ref & resul
         }        
         m_bsimp.mk_and(tmps.size(), tmps.c_ptr(), result);
         TRACE("mk_eq_bb", 
-              ast_ll_pp(tout, m_manager, arg1);
+              tout << mk_pp(arg1, m_manager) << "\n";
-              ast_ll_pp(tout, m_manager, arg2);
+              tout << mk_pp(arg2, m_manager) << "\n";
-              ast_ll_pp(tout, m_manager, result););
+              tout << mk_pp(result, m_manager) << "\n";);
         return;
     }
 #endif

src/ast/simplifier/poly_simplifier_plugin.cpp

@@ -285,6 +285,7 @@ bool poly_simplifier_plugin::merge_monomials(bool inv, expr * n1, expr * n2, exp
         else
             result = m_manager.mk_app(m_fid, m_MUL, mk_numeral(k1), b);
     }
+    TRACE("merge_monomials", tout << mk_pp(n1, m_manager) << "\n" << mk_pp(n2, m_manager) << "\n" << mk_pp(result, m_manager) << "\n";);
     return true;
 }
 

src/sat/sat_clause_use_list.h

@@ -20,6 +20,7 @@ Revision History:
 #define _SAT_CLAUSE_USE_LIST_H_
 
 #include"sat_types.h"
+#include"trace.h"
 
 namespace sat {
 
@@ -35,6 +36,7 @@ namespace sat {
 #endif
     public:
         clause_use_list() {
+            STRACE("clause_use_list_bug", tout << "[cul_created] " << this << "\n";);
 #ifdef LAZY_USE_LIST
             m_size = 0; 
 #endif
@@ -51,22 +53,33 @@ namespace sat {
         bool empty() const { return size() == 0; }
         
         void insert(clause & c) { 
-            SASSERT(!m_clauses.contains(&c)); SASSERT(!c.was_removed()); 
+            STRACE("clause_use_list_bug", tout << "[cul_insert] " << this << " " << &c << "\n";);
+            SASSERT(!m_clauses.contains(&c)); 
+            SASSERT(!c.was_removed()); 
             m_clauses.push_back(&c); 
 #ifdef LAZY_USE_LIST
             m_size++; 
 #endif
         }
+
         void erase_not_removed(clause & c) { 
+            STRACE("clause_use_list_bug", tout << "[cul_erase_not_removed] " << this << " " << &c << "\n";);
 #ifdef LAZY_USE_LIST
-            SASSERT(m_clauses.contains(&c)); SASSERT(!c.was_removed()); m_clauses.erase(&c); m_size--; 
+            SASSERT(m_clauses.contains(&c)); 
+            SASSERT(!c.was_removed()); 
+            m_clauses.erase(&c); 
+            m_size--; 
 #else
             m_clauses.erase(&c);
 #endif
         }
+
         void erase(clause & c) { 
+            STRACE("clause_use_list_bug", tout << "[cul_erase] " << this << " " << &c << "\n";);
 #ifdef LAZY_USE_LIST
-            SASSERT(m_clauses.contains(&c)); SASSERT(c.was_removed()); m_size--; 
+            SASSERT(m_clauses.contains(&c)); 
+            SASSERT(c.was_removed()); 
+            m_size--; 
 #else
             m_clauses.erase(&c);
 #endif
@@ -80,6 +93,7 @@ namespace sat {
         }
         
         bool check_invariant() const;
+
         // iterate & compress
         class iterator {
             clause_vector & m_clauses;

src/sat/sat_simplifier.cpp

@@ -146,8 +146,11 @@ namespace sat {
         m_need_cleanup = false;
         m_use_list.init(s.num_vars());
         init_visited();
-        if (learned)
+        bool learned_in_use_lists = false;
+        if (learned) {
             register_clauses(s.m_learned);
+            learned_in_use_lists = true;
+        }
         register_clauses(s.m_clauses);
 
         if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
@@ -179,7 +182,7 @@ namespace sat {
         if (!m_need_cleanup) {
             if (vars_eliminated) {
                 // must remove learned clauses with eliminated variables
-                cleanup_clauses(s.m_learned, true, true);
+                cleanup_clauses(s.m_learned, true, true, learned_in_use_lists);
             }
             CASSERT("sat_solver", s.check_invariant());
             TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
@@ -187,8 +190,8 @@ namespace sat {
             return;
         }
         cleanup_watches();
-        cleanup_clauses(s.m_learned, true, vars_eliminated);
+        cleanup_clauses(s.m_learned, true, vars_eliminated,  learned_in_use_lists);
-        cleanup_clauses(s.m_clauses, false, vars_eliminated);
+        cleanup_clauses(s.m_clauses, false, vars_eliminated, true);
         TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
         CASSERT("sat_solver", s.check_invariant());
         free_memory();
@@ -221,7 +224,7 @@ namespace sat {
         }
     }
 
-    void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated) {
+    void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) {
         clause_vector::iterator it  = cs.begin();
         clause_vector::iterator it2 = it;
         clause_vector::iterator end = cs.end();
@@ -245,7 +248,7 @@ namespace sat {
                 }
             }
 
-            if (cleanup_clause(c)) {
+            if (cleanup_clause(c, in_use_lists)) {
                 s.del_clause(c);
                 continue;
             }
@@ -516,7 +519,7 @@ namespace sat {
        
        Return true if the clause is satisfied
     */
-    bool simplifier::cleanup_clause(clause & c) {
+    bool simplifier::cleanup_clause(clause & c, bool in_use_list) {
         bool r = false;
         unsigned sz = c.size();
         unsigned j  = 0;
@@ -529,7 +532,11 @@ namespace sat {
                 break;
             case l_false:
                 m_need_cleanup = true;
-                m_use_list.get(l).erase_not_removed(c);
+                if (in_use_list && !c.frozen()) {
+                    // Remark: if in_use_list is false, then the given clause was not added to the use lists.
+                    // Remark: frozen clauses are not added to the use lists.
+                    m_use_list.get(l).erase_not_removed(c);
+                }
                 break;
             case l_true:
                 r = true;
@@ -611,7 +618,7 @@ namespace sat {
         clause_use_list & occurs = m_use_list.get(l);
         occurs.erase_not_removed(c);
         m_sub_counter -= occurs.size()/2;
-        if (cleanup_clause(c)) {
+        if (cleanup_clause(c, true /* clause is in the use lists */)) {
             // clause was satisfied
             TRACE("elim_lit", tout << "clause was satisfied\n";);
             remove_clause(c);
@@ -805,7 +812,7 @@ namespace sat {
             m_sub_counter--;
             TRACE("subsumption", tout << "next: " << c << "\n";);
             if (s.m_trail.size() > m_last_sub_trail_sz) {
-                if (cleanup_clause(c)) {
+                if (cleanup_clause(c, true /* clause is in the use_lists */)) {
                     remove_clause(c);
                     continue;
                 }

src/sat/sat_simplifier.h

@@ -125,7 +125,7 @@ namespace sat {
         void collect_subsumed0(clause const & c1, clause_vector & out);
         void back_subsumption0(clause & c1);
 
-        bool cleanup_clause(clause & c);
+        bool cleanup_clause(clause & c, bool in_use_list);
         bool cleanup_clause(literal_vector & c);
         void propagate_unit(literal l);
         void elim_lit(clause & c, literal l);
@@ -136,7 +136,7 @@ namespace sat {
         void subsume();
         
         void cleanup_watches();
-        void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated);
+        void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists);
 
         bool is_external(bool_var v) const;
         bool was_eliminated(bool_var v) const;

src/tactic/core/ctx_simplify_tactic.cpp

@@ -21,7 +21,7 @@ Notes:
 #include"goal_num_occurs.h"
 #include"cooperate.h"
 #include"ast_ll_pp.h"
-#include"ast_smt2_pp.h"
+#include"ast_pp.h"
 
 struct ctx_simplify_tactic::imp {
     struct cached_result {
@@ -105,6 +105,7 @@ struct ctx_simplify_tactic::imp {
     }
 
     bool shared(expr * t) const { 
+        TRACE("ctx_simplify_tactic_bug", tout << mk_pp(t, m) << "\n";);
         return t->get_ref_count() > 1 && m_occs.get_num_occs(t) > 1;
     }
 
@@ -242,12 +243,13 @@ struct ctx_simplify_tactic::imp {
     }
 
     void assert_expr(expr * t, bool sign) {
+        expr * p = t;
         if (m.is_not(t)) {
             t    = to_app(t)->get_arg(0);
             sign = !sign;
         }
         bool mk_scope = true;
-        if (shared(t)) {
+        if (shared(t) || shared(p)) {
             push();
             mk_scope  = false;
             assert_eq_core(t, sign ? m.mk_false() : m.mk_true());
@@ -457,7 +459,7 @@ struct ctx_simplify_tactic::imp {
             if (visit.is_marked(s)) {
                 continue;
             }
-			visit.mark(s, true);
+            visit.mark(s, true);
             ++sz;
             for (unsigned i = 0; is_app(s) && i < to_app(s)->get_num_args(); ++i) {
                 todo.push_back(to_app(s)->get_arg(i));