z3-src 500.0.0

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132

/*++
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 "tactic/tactical.h"
#include "tactic/core/simplify_tactic.h"
#include "tactic/core/propagate_values_tactic.h"
#include "tactic/core/solve_eqs_tactic.h"
#include "tactic/core/elim_uncnstr_tactic.h"
#include "tactic/bv/bit_blaster_tactic.h"
#include "tactic/bv/bv1_blaster_tactic.h"
#include "tactic/bv/max_bv_sharing_tactic.h"
#include "tactic/bv/bv_size_reduction_tactic.h"
#include "tactic/bv/bv_divrem_bounds_tactic.h"
#include "tactic/aig/aig_tactic.h"
#include "sat/tactic/sat_tactic.h"
#include "sat/sat_solver/inc_sat_solver.h"
#include "ackermannization/ackermannize_bv_tactic.h"
#include "tactic/smtlogics/smt_tactic.h"

#define MEMLIMIT 300

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

    params_ref solve_eq_p;
    // conservative gaussian elimination.
    solve_eq_p.set_uint("solve_eqs_max_occs", 2);

    params_ref flat_and_or_p = p;
    flat_and_or_p.set_bool("flat_and_or", false);

    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
    simp2_p.set_bool("flat_and_or", false);

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

    return
        and_then(
            using_params(mk_simplify_tactic(m), flat_and_or_p),
            using_params(mk_propagate_values_tactic(m), flat_and_or_p),
            using_params(mk_solve_eqs_tactic(m), solve_eq_p),
            mk_elim_uncnstr_tactic(m),
            mk_bv_divrem_bounds_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),
            if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_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);
}


static 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);
    local_ctx_p.set_bool("flat", false);
    local_ctx_p.set_bool("flat_and_or", false);

    params_ref solver_p;
    solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.

    tactic* preamble_st = mk_qfbv_preamble(m, p);
    tactic * st = main_p(and_then(preamble_st,
                                  // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function
                                  // symbols. In this case, we should not use the `sat', but instead `smt'. Alternatively,
                                  // the UFs can be eliminated by eager ackermannization in the preamble.
                                  cond(mk_is_qfbv_eq_probe(),
                                       and_then(mk_bv1_blaster_tactic(m),
                                                using_params(smt, solver_p)),
                                       cond(mk_is_qfbv_probe(),
                                            and_then(mk_bit_blaster_tactic(m),
                                                     when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)),
                                                          and_then(using_params(and_then(mk_simplify_tactic(m),
                                                                                         mk_solve_eqs_tactic(m)),
                                                                                local_ctx_p),
                                                                   if_no_proofs(mk_aig_tactic()))),
                                                     sat),
                                            smt))));

    st->updt_params(p);
    return st;

}


tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
    tactic * new_sat = cond(mk_produce_proofs_probe(),
                            and_then(mk_simplify_tactic(m), mk_smt_tactic(m, p)),
                            mk_psat_tactic(m, p));
    return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic(m, p));

}