void collect_bounds(goal const & g) {
        unsigned sz = g.size();
        numeral  val;
        unsigned bv_sz;
        expr * f, * lhs, * rhs;        
        for (unsigned i = 0; i < sz; i++) {
            bool negated = false;
            f = g.form(i);            
            if (m.is_not(f)) {
                negated = true;
                f = to_app(f)->get_arg(0);
            }

            if (m_util.is_bv_sle(f, lhs, rhs)) {
                bv_sz = m_util.get_bv_size(lhs);
                if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
                    TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
                    // v <= k
                    val = m_util.norm(val, bv_sz, true);
                    if (negated) {
                        val += numeral(1);
                        if (m_util.norm(val, bv_sz, true) != val) {
                            // bound is infeasible.
                        } 
                        else {
                            update_signed_lower(to_app(lhs), val);
                        }
                    }
                    else update_signed_upper(to_app(lhs), val);
                }

bool is_equal(goal const & s1, goal const & s2) {
    if (s1.size() != s2.size())
        return false;
    unsigned num1 = 0; // num unique ASTs in s1
    unsigned num2 = 0; // num unique ASTs in s2
    expr_fast_mark1 visited1;
    expr_fast_mark2 visited2;
    unsigned sz = s1.size();
    for (unsigned i = 0; i < sz; i++) {
        expr * f1 = s1.form(i);
        if (visited1.is_marked(f1))
            continue;
        num1++;
        visited1.mark(f1);
    }
    SASSERT(num1 <= sz);
    SASSERT(0 <= num1);
    for (unsigned i = 0; i < sz; i++) {
        expr * f2 = s2.form(i);
        if (visited2.is_marked(f2))
            continue;
        num2++;
        visited2.mark(f2);
        if (!visited1.is_marked(f2))
            return false;
    }
    SASSERT(num2 <= sz);
    SASSERT(0 <= num2);
    SASSERT(num1 >= num2);
    return num1 == num2;
}

 void solver_exp::assert_goal(goal const & g) {
     SASSERT(&(g.m()) == &m_ext_mng);
     ast_translation translator(m_ext_mng, m, false);
     unsigned sz = g.size();
     for (unsigned i = 0; i < sz; i++) {
         assert_expr_core(g.form(i), translator);
     }
 }

 virtual result operator()(goal const & g) {
     proc p(g.m(), m_bool, m_family);
     unsigned sz = g.size();
     expr_fast_mark1 visited;
     for (unsigned i = 0; i < sz; i++) {
         for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, g.form(i));
     }
     return result(p.m_counter);
 }

void bv2int_rewriter_ctx::collect_power2(goal const& s) {
    ast_manager& m = m_trail.get_manager();
    arith_util arith(m);
    bv_util bv(m);
    
    for (unsigned j = 0; j < s.size(); ++j) {
        expr* f = s.form(j);
        if (!m.is_or(f)) continue;
        unsigned sz = to_app(f)->get_num_args();
        expr* x, *y, *v = 0;
        rational n;
        vector<rational> bounds;
        bool is_int, ok = true;

        for (unsigned i = 0; ok && i < sz; ++i) {
            expr* e = to_app(f)->get_arg(i);
            if (!m.is_eq(e, x, y)) {
                ok = false;
                break;
            }
            if (arith.is_numeral(y, n, is_int) && is_int &&
                (x == v || v == 0)) {
                v = x;
                bounds.push_back(n);
            }
            else if (arith.is_numeral(x, n, is_int) && is_int &&
                     (y == v || v == 0)) {
                v = y;
                bounds.push_back(n);
            }
            else {
                ok = false;
                break;
            }
        }
        if (!ok || !v) continue;
        SASSERT(!bounds.empty());
        lt_rational lt;
        // lt is a total order on rationals.
        std::sort(bounds.begin(), bounds.end(), lt);
        rational p(1);
        unsigned num_bits = 0;
        for (unsigned i = 0; ok && i < bounds.size(); ++i) {
            ok = (p == bounds[i]); 
            p *= rational(2);
            ++num_bits;
        }
        if (!ok) continue;
        unsigned log2 = 0;
        for (unsigned i = 1; i <= num_bits; i *= 2) ++log2;
        if(log2 == 0) continue;
        expr* logx = m.mk_fresh_const("log2_v", bv.mk_sort(log2));
        logx = bv.mk_zero_extend(num_bits - log2, logx);
        m_trail.push_back(logx);
        TRACE("bv2int_rewriter", tout << mk_pp(v, m) << " |-> " << mk_pp(logx, m) << "\n";);
        m_power2.insert(v, logx);
    }

 result operator()(goal const & g) override {
     proc p(g.m());
     unsigned sz = g.size();
     expr_fast_mark1 visited;
     for (unsigned i = 0; i < sz; i++) {
         for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, g.form(i));
     }
     const double total = ackr_helper::calculate_lemma_bound(p.m_fun2terms);
     TRACE("ackr_bound_probe", tout << "total=" << total << std::endl;);

 void collect(goal const & g) {
     m_var2degree.reset();
     expr_fast_mark1 visited;
     unsigned sz = g.size();
     for (unsigned i = 0; i < sz; i++) {
         collect(g.form(i), visited);
     }
     
     TRACE("degree_shift", display_candidates(tout););

// Copy configuration: depth, models/proofs/cores flags, and precision from src.
// The assertions are not copied
goal::goal(goal const & src, bool):
    m_manager(src.m()),
    m_ref_count(0),
    m_depth(src.m_depth), 
    m_models_enabled(src.models_enabled()),
    m_proofs_enabled(src.proofs_enabled()), 
    m_core_enabled(src.unsat_core_enabled()), 
    m_inconsistent(false), 
    m_precision(src.m_precision) {
}

 bool collect_bounds(goal const & g) {
     bool found = false;
     unsigned sz = g.size();
     for (unsigned i = 0; i < sz; i++) {
         expr * t = g.form(i);
         if (process(t))
             found = true;
         else
             m_new_goal->assert_expr(t); // save non-bounds here
     }
     return found;
 }

 bool is_target(goal const & g) const {
     expr_fast_mark1 visited;
     unsigned sz = g.size();
     visitor proc(m_rw.cfg().butil().get_family_id());
     try {
         for (unsigned i = 0; i < sz; i++) {
             expr * f = g.form(i);
             for_each_expr_core<visitor, expr_fast_mark1, false, true>(proc, visited, f);
         }
     }
     catch (not_target) {
         return false;
     }
     return true;
 }

bool is_unbounded(goal const & g) {
    ast_manager & m = g.m();
    bound_manager bm(m);
    bm(g);
    is_unbounded_proc proc(bm);
    return test(g, proc);
}

 void compile(goal const & g) {
     expr * lhs;
     expr * rhs;
     unsigned sz = g.size();
     for (unsigned i = 0; i < sz; i++) {
         expr * f = g.form(i);
         TRACE("diff_neq_tactic", tout << "processing: " << mk_ismt2_pp(f, m) << "\n";);
         if (u.is_le(f, lhs, rhs))
             process_le(lhs, rhs);
         else if (u.is_ge(f, lhs, rhs))
             process_le(rhs, lhs);
         else if (m.is_not(f, f) && m.is_eq(f, lhs, rhs))
             process_neq(lhs, rhs);
         else
             throw_not_supported();
     }

 virtual result operator()(goal const & g) {
     proc p(g.m());
     for_each_expr_at(p, g);
     if (m_avg)
         return p.m_counter == 0 ? 0.0 : static_cast<double>(p.m_acc_degree)/static_cast<double>(p.m_counter);
     else
         return p.m_max_degree;
 }

static bool is_lp(goal const & g) {
    ast_manager & m = g.m();
    arith_util u(m);
    unsigned sz = g.size();
    for (unsigned i = 0; i < sz; i++) {
        expr * f  = g.form(i);
        bool sign = false;
        while (m.is_not(f, f))
            sign = !sign;
        if (m.is_eq(f) && !sign) {
            if (m.get_sort(to_app(f)->get_arg(0))->get_family_id() != u.get_family_id())
                return false;
            continue;
        }
        if (u.is_le(f) || u.is_ge(f) || u.is_lt(f) || u.is_gt(f))
            continue;
        return false;
    }
    return true;
}

 void operator()(goal & g) {
     if (g.inconsistent())
         return;
     tactic_report report("symmetry-reduce", g);
     vector<ptr_vector<app> > P;    
     expr_ref fml(m());
     to_formula(g, fml);
     app_map occs;
     compute_occurrences(fml, occs);
     find_candidate_permutations(fml, occs, P);
     if (P.empty()) {
         return;
     }
     term_set T, cts;        
     unsigned num_sym_break_preds = 0;
     for (unsigned i = 0; i < P.size(); ++i) {
         term_set& consts = P[i];
         if (invariant_by_permutations(fml, consts)) {
             cts.reset();
             select_terms(fml, consts, T);
             while (!T.empty() && cts.size() < consts.size()) {
                 app* t = select_most_promising_term(fml, T, cts, consts, occs);
                 T.erase(t);                    
                 compute_used_in(t, cts, consts);
                 app* c = select_const(consts, cts);
                 if (!c) break;
                 cts.push_back(c);
                 expr* mem = mk_member(t, cts);
                 g.assert_expr(mem); 
                 num_sym_break_preds++;
                 TRACE("symmetry_reduce", tout << "member predicate: " << mk_pp(mem, m()) << "\n";);
                 fml = m().mk_and(fml.get(), mem);
                 normalize(fml);
             }
         }
     }

void goal::copy_to(goal & target) const {
    SASSERT(&m_manager == &(target.m_manager));
    if (this == &target)
        return;

    m().copy(m_forms, target.m_forms);
    m().copy(m_proofs, target.m_proofs);
    m().copy(m_dependencies, target.m_dependencies);

    target.m_depth                = std::max(m_depth, target.m_depth);
    SASSERT(target.m_proofs_enabled == m_proofs_enabled);
    SASSERT(target.m_core_enabled   == m_core_enabled);
    target.m_inconsistent         = m_inconsistent;
    target.m_precision            = mk_union(prec(), target.prec());
}

 virtual result operator()(goal const & g) {
     bool found_non_01 = false;
     bound_manager bm(g.m());
     bm(g);
     rational l, u; bool st;
     bound_manager::iterator it  = bm.begin();
     bound_manager::iterator end = bm.end();
     for (; it != end; ++it) {
         expr * t = *it;
         if (bm.has_lower(t, l, st) && bm.has_upper(t, u, st) && (l.is_zero() || l.is_one()) && (u.is_zero() || u.is_one()))
             continue;
         if (found_non_01)
             return false;
         found_non_01 = true;
     }
     return true;
 }

static bool is_lira(goal const & g) {
    is_non_nira_functor p(g.m(), true, true, true, true);
    return !test(g, p);
}

static bool is_qfnia(goal const & g) {
    is_non_nira_functor p(g.m(), true, false, false, false);
    return !test(g, p);
}

static bool is_qflra(goal const & g) {
    is_non_qflira_functor p(g.m(), false, true);
    return !test(g, p);
}