z3-src 415.4.4

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

/*++
  Copyright (c) 2017 Microsoft Corporation

  Author:
    Lev Nachmanson (levnach)
    Nikolaj Bjorner (nbjorner)
  --*/
#include "math/lp/nla_basics_lemmas.h"
#include "math/lp/nla_core.h"
namespace nla {

monotone::monotone(core * c) : common(c) {}
    
void monotone::monotonicity_lemma() {
    unsigned shift = random();
    unsigned size = c().m_to_refine.size();
    for (unsigned i = 0; i < size && !done(); i++) { 
        lpvar v = c().m_to_refine[(i + shift) % size];
        monotonicity_lemma(c().emons()[v]);
    }
}
   
void monotone::monotonicity_lemma(monic const& m) {
    SASSERT(!check_monic(m));
    if (c().mon_has_zero(m.vars()))
        return;
    if (c().has_big_num(m)) 
       return;
    const rational prod_val = abs(c().product_value(m));
    const rational m_val = abs(var_val(m));
    bool is_lt = m_val < prod_val;
    
    // Check if this specific combination should be throttled
    if (c().throttle().insert_new(nla_throttle::MONOTONE_LEMMA, m.var(), is_lt))
        return;
    
    if (is_lt)
        monotonicity_lemma_lt(m);
    else if (m_val > prod_val)
        monotonicity_lemma_gt(m);
}

/** \brief enforce the inequality |m| <= product |m[i]| .

    /\_i |m[i]| <= |val(m[i])| => |m| <= |product_i val(m[i])|
    <=>
    \/_i |m[i]| > |val(m[i])| or |m| <= |product_i val(m[i])|

    implied by 
       m[i] > val(m[i])     for val(m[i]) > 0
       m[i] < val(m[i])     for val(m[i]) < 0
       m >= product m[i]    for product m[i] < 0
       m <= product m[i]    for product m[i] > 0

    Example:

    0 >= x >= -2 & 0 <= y <= 3 => x*y >= -6
    0 >= x >= -2 & 0 <= y <= 3 => x*x*y <= 12
    
*/
void monotone::monotonicity_lemma_gt(const monic& m) {
    lemma_builder lemma(c(), "monotonicity > ");
    rational product(1);
    for (lpvar j : m.vars()) {
        auto v = c().val(j);
        lemma |= ineq(j, v.is_neg() ? llc::LT : llc::GT, v);
        lemma |= ineq(j, v.is_neg() ? llc::GT : llc::LT, 0);
        product *= v;
    }
    lemma |= ineq(m.var(), product.is_neg() ? llc::GE : llc::LE, product);
}
    
/** \brief enforce the inequality |m| >= product |m[i]| .

    /\_i |m[i]| >= |val(m[i])| => |m| >= |product_i val(m[i])|
    <=>
    \/_i |m[i]| < |val(m[i])| or |m| >= |product_i val(m[i])|

    Example:

    x <= -2 & y >= 3 => x*y <= -6
*/
void monotone::monotonicity_lemma_lt(const monic& m) {
    lemma_builder lemma(c(), "monotonicity <");
    rational product(1);
    for (lpvar j : m.vars()) {
        auto v = c().val(j);
        lemma |= ineq(j, v.is_neg() ? llc::GT : llc::LT, v);
        product *= v;
    }
    lemma |= ineq(m.var(), product.is_neg() ? llc::LE : llc::GE, product);
}
   

}