Merge branch 'master' of https://github.com/z3prover/z3 into opt

src/smt/smt_case_split_queue.cpp

@@ -51,9 +51,9 @@ namespace smt {
             if (!m_theory_var_priority.find(v2, p_v2)) {
                 p_v2 = 0.0;
             }
-        // add clause activity
-        p_v1 += m_activity[v1];
-        p_v2 += m_activity[v2];
+            // add clause activity
+            p_v1 += m_activity[v1];
+            p_v2 += m_activity[v2];
             return p_v1 > p_v2;
         }
     };
@@ -82,6 +82,7 @@ namespace smt {
 
         virtual void mk_var_eh(bool_var v) {
             m_queue.reserve(v+1);
+            SASSERT(!m_queue.contains(v));
             m_queue.insert(v);
         }
 
@@ -130,10 +131,7 @@ namespace smt {
 
         virtual void display(std::ostream & out) {
             bool first = true;
-            bool_var_act_queue::const_iterator it  = m_queue.begin();
-            bool_var_act_queue::const_iterator end = m_queue.end();
-            for (; it != end ; ++it) {
-                unsigned v = *it;
+            for (unsigned v : m_queue) {
                 if (m_context.get_assignment(v) == l_undef) {
                     if (first) {
                         out << "remaining case-splits:\n";
@@ -143,8 +141,7 @@ namespace smt {
                 }
             }
             if (!first)
-                out << "\n";
-
+                out << "\n";            
         }
 
         virtual ~act_case_split_queue() {};
@@ -166,11 +163,15 @@ namespace smt {
             act_case_split_queue::activity_increased_eh(v);
             if (m_queue.contains(v))
                 m_queue.decreased(v);
+            if (m_delayed_queue.contains(v))
+                m_delayed_queue.decreased(v);
         }
 
         virtual void mk_var_eh(bool_var v) {
             m_queue.reserve(v+1);
             m_delayed_queue.reserve(v+1);
+            SASSERT(!m_delayed_queue.contains(v));
+            SASSERT(!m_queue.contains(v));
             if (m_context.is_searching()) 
                 m_delayed_queue.insert(v);
             else
@@ -1099,8 +1100,6 @@ namespace smt {
 #endif
 
             GOAL_STOP();
-
-            //std::cout << "goal set, time " << m_goal_time.get_seconds() << "\n";
         }
 
         void set_global_generation()

src/smt/smt_context.cpp

@@ -1826,6 +1826,7 @@ namespace smt {
     }
     
     void context::rescale_bool_var_activity() {
+        TRACE("case_split", tout << "rescale\n";);
         svector<double>::iterator it  = m_activity.begin();
         svector<double>::iterator end = m_activity.end();
         for (; it != end; ++it)

src/smt/smt_context.h

@@ -1047,6 +1047,7 @@ namespace smt {
             if (act > ACTIVITY_LIMIT)
                 rescale_bool_var_activity();
             m_case_split_queue->activity_increased_eh(v);
+            TRACE("case_split", tout << "v" << v << " " << m_bvar_inc << " -> " << act << "\n";);
         }
 
     protected:

src/smt/theory_str.cpp

@@ -1549,14 +1549,12 @@ namespace smt {
         expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m);
 
         expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m);
+        assert_axiom(breakdownAssert);
+        
         SASSERT(breakdownAssert);
 
         expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m);
-        SASSERT(reduceToResult);
-
-        expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToResult), m);
-        SASSERT(finalAxiom);
-        assert_axiom(finalAxiom);
+        assert_axiom(reduceToResult);
     }
 
     void theory_str::instantiate_axiom_str_to_int(enode * e) {
@@ -4653,34 +4651,24 @@ namespace smt {
     }
 
     bool theory_str::get_arith_value(expr* e, rational& val) const {
-        if (opt_DisableIntegerTheoryIntegration) {
-            TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;);
-            return false;
-        }
-
         context& ctx = get_context();
         ast_manager & m = get_manager();
-        theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
-        if (!tha) {
+
+	// safety
+	if (!ctx.e_internalized(e)) {
+	  return false;
+	}
+	
+        // if an integer constant exists in the eqc, it should be the root
+        enode * en_e = ctx.get_enode(e);
+        enode * root_e = en_e->get_root();
+        if (m_autil.is_numeral(root_e->get_owner(), val) && val.is_int()) {
+            TRACE("str", tout << mk_pp(e, m) << " ~= " << mk_pp(root_e->get_owner(), m) << std::endl;);
+            return true;
+        } else {
+            TRACE("str", tout << "root of eqc of " << mk_pp(e, m) << " is not a numeral" << std::endl;);
             return false;
         }
-        TRACE("str", tout << "checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;);
-        expr_ref _val(m);
-        enode * en_e = ctx.get_enode(e);
-        enode * it = en_e;
-        do {
-            if (m_autil.is_numeral(it->get_owner(), val) && val.is_int()) {
-                // found an arithmetic term
-                TRACE("str", tout << mk_pp(it->get_owner(), m) << " is an integer ( ~= " << val << " )"
-                      << std::endl;);
-                return true;
-            } else {
-                TRACE("str", tout << mk_pp(it->get_owner(), m) << " not a numeral" << std::endl;);
-            }
-            it = it->get_next();
-        } while (it != en_e);
-        TRACE("str", tout << "no arithmetic values found in eqc" << std::endl;);
-        return false;
     }
 
     bool theory_str::lower_bound(expr* _e, rational& lo) {