void expr_context_simplifier::reduce_fix(expr * m, expr_ref & result) {
    expr_ref tmp(m_manager);
    result = m;
    do {
        tmp = result.get();
        reduce(tmp.get(), result);
    }
    while (tmp.get() != result.get());
}

    br_status dl_rewriter::mk_app_core(
        func_decl * f, unsigned num_args, expr* const* args, expr_ref& result) {
        ast_manager& m = result.get_manager();
        uint64 v1, v2;
        switch(f->get_decl_kind()) {
		case datalog::OP_DL_LT:
            if (m_util.is_numeral_ext(args[0], v1) &&
                m_util.is_numeral_ext(args[1], v2)) {
                result = (v1 < v2)?m.mk_true():m.mk_false();
                return BR_DONE;
            }
            // x < x <=> false
            if (args[0] == args[1]) {
                result = m.mk_false();
                return BR_DONE;
            }
            // x < 0 <=> false
            if (m_util.is_numeral_ext(args[1], v2) && v2 == 0) {
                result = m.mk_false();
                return BR_DONE;
            }
            // 0 < x <=> 0 != x
            if (m_util.is_numeral_ext(args[1], v1) && v1 == 0) {
                result = m.mk_not(m.mk_eq(args[0], args[1]));
                return BR_DONE;
            }
            break;

        default:
            break;
        }
        return BR_FAILED;
    }

bool expr_delta::delta_dfs(unsigned& n, expr* e, expr_ref& result) {
    ast_manager& m = m_manager;
    if (m.is_true(e) || m.is_false(e)) {
        return false;
    }
    if (n == 0 && m.is_bool(e)) {
        result = m.mk_true();
        return true;
    }
    else if (n == 1 && m.is_bool(e)) {
        result = m.mk_false();
        return true;
    }
    else if (is_app(e)) {
        if (m.is_bool(e)) {
            SASSERT(n >= 2);
            n -= 2;
        }
        return delta_dfs(n, to_app(e), result);
    }
    else if (is_quantifier(e)) {
        SASSERT(n >= 2);
        n -= 2;
        quantifier* q = to_quantifier(e);
        if (delta_dfs(n, q->get_expr(), result)) {
            result = m.update_quantifier(q, result.get());
            return true;
        }
        else {
            return false;
        }
    }
    return false;
}

    bool push_toplevel_junction_negation_inside(expr_ref& e)
    {
        ast_manager& m = e.get_manager();
        bool_rewriter brwr(m);

        expr * arg;
        if(!m.is_not(e, arg)) { return false; }
        bool is_and = m.is_and(arg);
        if(!is_and && !m.is_or(arg)) { return false; }

        //now we know we have formula we need to transform
        app * junction = to_app(arg);
        expr_ref_vector neg_j_args(m);
        unsigned num_args = junction->get_num_args();
        for(unsigned i=0; i<num_args; ++i) {
            expr_ref neg_j_arg(m);
            brwr.mk_not(junction->get_arg(i), neg_j_arg);
            neg_j_args.push_back(neg_j_arg);
        }
        if(is_and) {
            brwr.mk_or(neg_j_args.size(), neg_j_args.c_ptr(), e);
        }
        else {
            brwr.mk_and(neg_j_args.size(), neg_j_args.c_ptr(), e);
        }
        return true;
    }

 void udoc_relation::to_formula(expr_ref& fml) const {
     ast_manager& m = fml.get_manager();
     expr_ref_vector disj(m);
     for (unsigned i = 0; i < m_elems.size(); ++i) {
         disj.push_back(to_formula(m_elems[i]));
     }
     fml = mk_or(m, disj.size(), disj.c_ptr());
 }

    void mk_interp_tail_simplifier::simplify_expr(app * a, expr_ref& res)
    {
        expr_ref simp1_res(m);
        m_simp(a, simp1_res);
        (*m_rw)(simp1_res.get(), res);

        m_simp(res.get(), res);
    }

void label_rewriter::remove_labels(expr_ref& fml, proof_ref& pr) {
    ast_manager& m = fml.get_manager();
    expr_ref tmp(m);
    m_rwr(fml, tmp);
    if (pr && fml != tmp) {        
        pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp));
    }
    fml = tmp;
}

 br_status pull_ite(expr_ref & result) {
     expr * t = result.get();
     if (is_app(t)) {
         br_status st = pull_ite(to_app(t)->get_decl(), to_app(t)->get_num_args(), to_app(t)->get_args(), result);
         if (st != BR_FAILED)
             return st;
     }
     return BR_DONE;
 }

void bit2int::operator()(expr * m, expr_ref & result, proof_ref& p) {
    flush_cache();
    expr_reduce emap(*this);
    for_each_ast(emap, m);
    result = get_cached(m);
    if (m_manager.proofs_enabled() && m != result.get()) {
        // TBD: rough
        p = m_manager.mk_rewrite(m, result);
    }
    TRACE("bit2int",
          tout << mk_pp(m, m_manager) << "======>\n"
          << mk_pp(result, m_manager) << "\n";);

    void mk_interp_tail_simplifier::simplify_expr(app * a, expr_ref& res)
    {
        expr_ref simp1_res(m);
        m_simp(a, simp1_res);
        (*m_rw)(simp1_res.get(), res);

        /*if (simp1_res.get()!=res.get()) {
            std::cout<<"pre norm:\n"<<mk_pp(simp1_res.get(),m)<<"post norm:\n"<<mk_pp(res.get(),m)<<"\n";
        }*/

        m_simp(res.get(), res);
    }

static void parse_fml(char const* str, app_ref_vector& vars, expr_ref& fml) {
    ast_manager& m = fml.get_manager();
    fml = parse_fml(m, str);
    if (is_exists(fml)) {
        quantifier* q = to_quantifier(fml);
        for (unsigned i = 0; i < q->get_num_decls(); ++i) {
            vars.push_back(m.mk_const(q->get_decl_name(i), q->get_decl_sort(i)));
        }
        fml = q->get_expr();
        var_subst vs(m, true);
        vs(fml, vars.size(), (expr*const*)vars.c_ptr(), fml);
    }
}

void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, expr_ref & result) {
    SASSERT(is_well_sorted(result.m(), n));
    m_reducer.reset();
    if (m_std_order)
        m_reducer.set_inv_bindings(num_args, args);
    else
        m_reducer.set_bindings(num_args, args);
    m_reducer(n, result);
    SASSERT(is_well_sorted(m_reducer.m(), result));
    TRACE("var_subst_bug",
          tout << "m_std_order: " << m_std_order << "\n" << mk_ismt2_pp(n, m_reducer.m()) << "\nusing\n";
          for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m_reducer.m()) << "\n";
          tout << "\n------>\n";
          tout << mk_ismt2_pp(result, m_reducer.m()) << "\n";);

 void sieve_relation::to_formula(expr_ref& fml) const {
     ast_manager& m = fml.get_manager();
     expr_ref_vector s(m);
     expr_ref tmp(m);
     relation_signature const& sig = get_inner().get_signature();
     unsigned sz = sig.size();
     for (unsigned i = sz ; i > 0; ) {
         --i;
         unsigned idx = m_inner2sig[i];
         s.push_back(m.mk_var(idx, sig[i]));
     }
     get_inner().to_formula(tmp);
     get_plugin().get_context().get_var_subst()(tmp, sz, s.c_ptr(), fml);
 }

bool simple_parser::parse(std::istream & in, expr_ref & result) {
	scanner s(in, std::cerr, false);
    try {
        result = parse_expr(s);
        if (!result)
            throw parser_error();
    }
    catch (parser_error) {
        warning_msg("parser error");
        return false;
    } 
    m_exprs.reset();
    return result.get() != 0;
}

static void test(app* var, expr_ref& fml) {

    ast_manager& m = fml.get_manager();
    smt_params params;
    params.m_model = true;

    symbol x_name(var->get_decl()->get_name());   
    sort* x_sort = m.get_sort(var);

    expr_ref pr(m);
    expr_ref_vector lits(m);
    flatten_and(fml, lits);

    model_ref md;
    {
        smt::context ctx(m, params);
        ctx.assert_expr(fml);
        lbool result = ctx.check();
        if (result != l_true) return;
        ctx.get_model(md);
    }    
    VERIFY(qe::arith_project(*md, var, lits));
    pr = mk_and(lits);
   
    std::cout << "original:  " << mk_pp(fml, m) << "\n";
    std::cout << "projected: " << mk_pp(pr,  m) << "\n";

    // projection is consistent with model.
    VERIFY(md->is_true(pr));

    // projection implies E x. fml
    {
        qe::expr_quant_elim qelim(m, params);
        expr_ref result(m), efml(m);
        expr* x = var;
        expr_abstract(m, 0, 1, &x, fml, efml);
        efml = m.mk_exists(1, &x_sort, &x_name, efml);
        qelim(m.mk_true(), efml, result);

        smt::context ctx(m, params);
        ctx.assert_expr(pr);
        ctx.assert_expr(m.mk_not(result));
        std::cout << "exists: " << pr << " =>\n" << result << "\n";
        VERIFY(l_false == ctx.check());
    }    

    std::cout << "\n";
}

 void table_base::to_formula(relation_signature const& sig, expr_ref& fml) const {
     // iterate over rows and build disjunction
     ast_manager & m = fml.get_manager();
     expr_ref_vector disjs(m);
     expr_ref_vector conjs(m);
     dl_decl_util util(m);
     bool_rewriter brw(m);
     table_fact fact;
     iterator it = begin();
     iterator iend = end();
     for(; it != iend; ++it) {
         const row_interface & r = *it;   
         r.get_fact(fact);
         conjs.reset();
         for (unsigned i = 0; i < fact.size(); ++i) {
             conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), util.mk_numeral(fact[i], sig[i])));
         }
         brw.mk_and(conjs.size(), conjs.c_ptr(), fml);
         disjs.push_back(fml);
     }
     brw.mk_or(disjs.size(), disjs.c_ptr(), fml);        
 }

 // Return true if t1 and t2 are of the form:
 //   t + a1*x1 + ... + an*xn
 //   t' + a1*x1 + ... + an*xn
 // Store t in new_t1, t' in new_t2 and (a1*x1 + ... + an*xn) in c.
 bool unify_add(app * t1, expr * t2, expr_ref & new_t1, expr_ref & new_t2, expr_ref & c) {
     unsigned num1 = t1->get_num_args();
     expr * const * ms1 = t1->get_args();
     if (num1 < 2)
         return false;
     unsigned num2;
     expr * const * ms2;
     if (m_a_util.is_add(t2)) {
         num2 = to_app(t2)->get_num_args();
         ms2  = to_app(t2)->get_args();
     }
     else {
         num2 = 1;
         ms2  = &t2;
     }
     if (num1 != num2 && num1 != num2 + 1 && num1 != num2 - 1)
         return false;
     new_t1 = 0;
     new_t2 = 0;
     expr_fast_mark1 visited1;
     expr_fast_mark2 visited2;
     for (unsigned i = 0; i < num1; i++) {
         expr * arg = ms1[i];
         visited1.mark(arg);
     }
     for (unsigned i = 0; i < num2; i++) {
         expr * arg = ms2[i];
         visited2.mark(arg);
         if (visited1.is_marked(arg))
             continue;
         if (new_t2)
             return false; // more than one missing term
         new_t2 = arg;
     }
     for (unsigned i = 0; i < num1; i++) {
         expr * arg = ms1[i];
         if (visited2.is_marked(arg))
             continue;
         if (new_t1)
             return false; // more than one missing term
         new_t1 = arg;
     }
     // terms matched...
     bool is_int = m_a_util.is_int(t1);
     if (!new_t1) 
         new_t1 = m_a_util.mk_numeral(rational(0), is_int);
     if (!new_t2)
         new_t2 = m_a_util.mk_numeral(rational(0), is_int);
     // mk common part
     ptr_buffer<expr> args;
     for (unsigned i = 0; i < num1; i++) {
         expr * arg = ms1[i];
         if (arg == new_t1.get())
             continue;
         args.push_back(arg);
     }
     SASSERT(!args.empty());
     if (args.size() == 1) 
         c = args[0];
     else
         c = m_a_util.mk_add(args.size(), args.c_ptr());
     return true;
 }

 expr* get_literal() { return m_literal.get(); }

 unsigned get_decl_id() const { return is_app(m_expr) ? to_app(m_expr)->get_decl()->get_id() : m_expr->get_id(); }

 unsigned get_id() const { return m_expr->get_id();}