z3-src 503.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

/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    propagate_ineqs_tactic.h
     
Author:

    Leonardo (leonardo) 2012-02-19

Tactic Documentation:

## Tactic propagate-ineqs

### Short Description

Propagate ineqs/bounds, remove subsumed inequalities

### Long Description

This tactic performs the following tasks:

- Propagate bounds using the bound_propagator.
- Eliminate subsumed inequalities.
  - For example:
    `x - y >= 3` can be replaced with true if we know that `x >= 3` and `y <= 0`

 - Convert inequalities of the form `p <= k` and `p >= k` into `p = k`,
   where `p` is a polynomial and `k` is a constant.

This strategy assumes the input is in arith LHS mode.
This can be achieved by using option :arith-lhs true in the simplifier.

### Example
```z3
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const u Int)
(declare-const v Int)
(declare-const w Int)
(assert (>= x 3))
(assert (<= y 0))
(assert (>= (- x y) 3))
(assert (>= (* u v w) 2))
(assert (<= (* v u w) 2))
(apply (and-then simplify propagate-ineqs))
```

--*/
#pragma once


#include "util/params.h"
#include "tactic/tactic.h"
#include "tactic/dependent_expr_state_tactic.h"
#include "ast/simplifiers/bound_simplifier.h"
#include "ast/simplifiers/dependent_expr_state.h"

inline tactic* mk_propagate_ineqs_tactic(ast_manager& m, params_ref const& p = params_ref()) {
    return alloc(dependent_expr_state_tactic, m, p,
                 [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bound_simplifier, m, p, s); });
}

Z3_ADD_TACTIC(propagate_ineqs, "propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", mk_propagate_ineqs_tactic(m, p));
Z3_ADD_SIMPLIFIER(propagate_ineqs, "propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", alloc(bound_simplifier, m, p, s));