z3-src 416.0.2

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

/*++
Copyright (c) 2020 Microsoft Corporation

Module Name:

    int_cube.cpp

Abstract:

    Cube finder

Author:
    Lev Nachmanson (levnach)
    Nikolaj Bjorner (nbjorner)

Revision History:
--*/

#include "math/lp/int_solver.h"
#include "math/lp/lar_solver.h"
#include "math/lp/int_cube.h"

namespace lp {

    int_cube::int_cube(int_solver& lia):lia(lia), lra(lia.lra) {}

    lia_move int_cube::operator()() {
        lia.settings().stats().m_cube_calls++;
        TRACE(cube,
              for (unsigned j = 0; j < lra.number_of_vars(); ++j)
                  lia.display_column(tout, j);
              tout << lra.constraints();
              );
        
        lra.push();
        if (!tighten_terms_for_cube()) {
            lra.pop();
            lra.set_status(lp_status::OPTIMAL);
            return lia_move::undef;
        }
        
        lp_status st = lra.find_feasible_solution();
        if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) {
            TRACE(cube, tout << "cannot find a feasible solution";);
            lra.pop();
            lra.move_non_basic_columns_to_bounds();
            // it can happen that we found an integer solution here
            return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef;
        }
        lra.pop();
        lra.round_to_integer_solution();
        lra.set_status(lp_status::FEASIBLE);
        SASSERT(lia.settings().get_cancel_flag() || lia.is_feasible());
        TRACE(cube, tout << "success";);
        lia.settings().stats().m_cube_success++;
        return lia_move::sat;
    }
// i is the column index having the term
    bool int_cube::tighten_term_for_cube(unsigned i) {
        if (!lra.column_associated_with_row(i))
            return true;
        const lar_term& t = lra.get_term(i);
        impq delta = get_cube_delta_for_term(t);
        TRACE(cube, lra.print_term_as_indices(t, tout); tout << ", delta = " << delta << "\n";);
        if (is_zero(delta))
            return true;
        return lra.tighten_term_bounds_by_delta(i, delta);
    }
    
    bool int_cube::tighten_terms_for_cube() {
        for (const lar_term* t: lra.terms())
            if (!tighten_term_for_cube(t->j())) {
                TRACE(cube, tout << "cannot tighten";);
                return false;
            }
        return true;
    }

    void int_cube::find_feasible_solution() {
        lra.find_feasible_solution();
        SASSERT(lp_status::OPTIMAL == lra.get_status() || lp_status::FEASIBLE == lra.get_status());
    }

    impq int_cube::get_cube_delta_for_term(const lar_term& t) const {
        if (t.size() == 2) {
            bool seen_minus = false;
            bool seen_plus = false;
            for(lar_term::ival p : t) {
                if (!lia.column_is_int(p.j()))
                    goto usual_delta;
                const mpq & c = p.coeff();
                if (c == one_of_type<mpq>()) {
                    seen_plus = true;
                } else if (c == -one_of_type<mpq>()) {
                    seen_minus = true;
                } else {
                    goto usual_delta;
                }
            }
            if (seen_minus && seen_plus)
                return zero_of_type<impq>();
            return impq(0, 1);
        }
    usual_delta:
        mpq delta = zero_of_type<mpq>();
        for (lar_term::ival p : t)
            if (lia.column_is_int(p.j()))
                delta += abs(p.coeff());
        
        delta *= mpq(1, 2);
        return impq(delta);
    }

}