<commit_before>/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    qfbv_tactic.cpp

Abstract:

    Tactic for QF_BV based on bit-blasting

Author:

    Leonardo (leonardo) 2012-02-22

Notes:

--*/
#include"tactical.h"
#include"simplify_tactic.h"
#include"propagate_values_tactic.h"
#include"solve_eqs_tactic.h"
#include"elim_uncnstr_tactic.h"
#include"smt_tactic.h"
#include"bit_blaster_tactic.h"
#include"bv1_blaster_tactic.h"
#include"max_bv_sharing_tactic.h"
#include"bv_size_reduction_tactic.h"
#include"aig_tactic.h"
#include"sat_tactic.h"
#include"ackermannize_tactic.h"
#include"ackr_bound_probe.h"

#define MEMLIMIT 300

#define ACKRLIMIT 1000

tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {

    params_ref solve_eq_p;
    // conservative guassian elimination. 
    solve_eq_p.set_uint("solve_eqs_max_occs", 2); 
    
    params_ref simp2_p = p;
    simp2_p.set_bool("som", true);
    simp2_p.set_bool("pull_cheap_ite", true);
    simp2_p.set_bool("push_ite_bv", false);
    simp2_p.set_bool("local_ctx", true);
    simp2_p.set_uint("local_ctx_limit", 10000000);
    simp2_p.set_bool("flat", true); // required by som
    simp2_p.set_bool("hoist_mul", false); // required by som


    params_ref hoist_p;
    hoist_p.set_bool("hoist_mul", true);
    hoist_p.set_bool("som", false);

    return
        and_then(
            mk_simplify_tactic(m),
            mk_propagate_values_tactic(m),
            using_params(mk_solve_eqs_tactic(m), solve_eq_p),
            mk_elim_uncnstr_tactic(m),
            if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
            using_params(mk_simplify_tactic(m), simp2_p),
            //
            // Z3 can solve a couple of extra benchmarks by using hoist_mul
            // but the timeout in SMT-COMP is too small. 
            // Moreover, it impacted negatively some easy benchmarks.
            // We should decide later, if we keep it or not.
            //
            using_params(mk_simplify_tactic(m), hoist_p),
            mk_max_bv_sharing_tactic(m),
            when(mk_lt(mk_ackr_bound_probe(), mk_const_probe(static_cast<double>(ACKRLIMIT))),  mk_ackermannize_tactic(m,p))
            );
}

static tactic * main_p(tactic* t) {
    params_ref p;
    p.set_bool("elim_and", true);
    p.set_bool("push_ite_bv", true);
    p.set_bool("blast_distinct", true);
    return using_params(t, p);
}


tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) {    

    params_ref local_ctx_p = p;
    local_ctx_p.set_bool("local_ctx", true);

    params_ref solver_p;<commit_msg>Adding parameters to Ackermannization in qfbv_tactic.<commit_after>/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    qfbv_tactic.cpp

Abstract:

    Tactic for QF_BV based on bit-blasting

Author:

    Leonardo (leonardo) 2012-02-22

Notes:

--*/
#include"tactical.h"
#include"simplify_tactic.h"
#include"propagate_values_tactic.h"
#include"solve_eqs_tactic.h"
#include"elim_uncnstr_tactic.h"
#include"smt_tactic.h"
#include"bit_blaster_tactic.h"
#include"bv1_blaster_tactic.h"
#include"max_bv_sharing_tactic.h"
#include"bv_size_reduction_tactic.h"
#include"aig_tactic.h"
#include"sat_tactic.h"
#include"ackermannize_tactic.h"
#include"ackr_bound_probe.h"
#include"qfbv_tactic_params.hpp"

#define MEMLIMIT 300

tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {

    params_ref solve_eq_p;
    // conservative guassian elimination. 
    solve_eq_p.set_uint("solve_eqs_max_occs", 2); 
    
    params_ref simp2_p = p;
    simp2_p.set_bool("som", true);
    simp2_p.set_bool("pull_cheap_ite", true);
    simp2_p.set_bool("push_ite_bv", false);
    simp2_p.set_bool("local_ctx", true);
    simp2_p.set_uint("local_ctx_limit", 10000000);
    simp2_p.set_bool("flat", true); // required by som
    simp2_p.set_bool("hoist_mul", false); // required by som


    qfbv_tactic_params my_params(p);

    params_ref hoist_p;
    hoist_p.set_bool("hoist_mul", true);
    hoist_p.set_bool("som", false);

    const double should_ackermannize = static_cast<double>(my_params.div0ackermann());
    const double ackermannize_limit = static_cast<double>(my_params.div0_ackermann_limit());
    probe * const should_ackermann_p = mk_and(
        mk_const_probe(should_ackermannize),
        mk_lt(mk_ackr_bound_probe(), mk_const_probe(ackermannize_limit))
        );


    return
        and_then(
            mk_simplify_tactic(m),
            mk_propagate_values_tactic(m),
            using_params(mk_solve_eqs_tactic(m), solve_eq_p),
            mk_elim_uncnstr_tactic(m),
            if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
            using_params(mk_simplify_tactic(m), simp2_p),
            //
            // Z3 can solve a couple of extra benchmarks by using hoist_mul
            // but the timeout in SMT-COMP is too small. 
            // Moreover, it impacted negatively some easy benchmarks.
            // We should decide later, if we keep it or not.
            //
            using_params(mk_simplify_tactic(m), hoist_p),
            mk_max_bv_sharing_tactic(m),
            when(should_ackermann_p,  mk_ackermannize_tactic(m,p))
            );
}

static tactic * main_p(tactic* t) {
    params_ref p;
    p.set_bool("elim_and", true);
    p.set_bool("push_ite_bv", true);
    p.set_bool("blast_distinct", true);
    return using_params(t, p);
}


tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) {    

    params_ref local_ctx_p = p;
    local_ctx_p.set_bool("local_ctx", true);

    params_ref solver_p;
{'fraction_non_alphanumeric': 0.11138834432364997, 'fraction_numerical': 0.013544822669755837, 'mean_word_length': 3.5294592413236483, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 6, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 2, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1349891', 'n_tokens_mistral': 2270, 'n_tokens_neox': 2123, 'n_words': 352}