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

/*++
Copyright (c) 2011 Microsoft Corporation

Module Name:

    simplify_tactic.h

Abstract:

    Apply simplification and rewriting rules.

Author:

    Leonardo (leonardo) 2011-11-20

Tactic Documentation:

## Tactic simplify

### Short Description:

The tactic performs algebraic simplifications on formulas

### Long Description

The simplify tactic invokes z3's main rewriting engine. 
The rewriting engine contains support for theory specific simplifications.
The set of simplifications invoked is open ended. Useful algebraic simplifications
are added to the rewrite engine as they are discovered to be useful.

Note that the simplifier does not ensure that equivalent formulas are simplified to the same form.
In other words it does not guarantee canonicity. This contrasts with BDD packages where BDDs constructed
from two equivalent formulas are guaranteed to be equal.

### Example
 
```z3
  (declare-const x Int)
  (declare-const y Int)
  (assert (> x (+ x y)))
  (apply simplify)
```

The simplifier is also exposed as a stand-alone command.
There are several options to control its behavior.

```z3
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const u Int)
(declare-fun p (Int) Bool)
(assert (p (* (+ x y) (+ z u))))
(apply simplify)
(apply (with simplify :som true))

(simplify (* (+ x y) (+ z u)) :som false)
(simplify (* (+ x y) (+ z u)) :som true)
```

### Notes

* supports unsat cores, proof terms

--*/
#pragma once

#include "tactic/tactic.h"
#include "tactic/tactical.h"

class simplify_tactic : public tactic {
    bool       m_clean = true;
    struct     imp;
    imp *      m_imp;
    params_ref m_params;
public:
    simplify_tactic(ast_manager & m, params_ref const & ref = params_ref());
    ~simplify_tactic() override;

    void updt_params(params_ref const & p) override;

    static void get_param_descrs(param_descrs & r);
    
    void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); }

    void collect_statistics(statistics& st) const override;
    
    void operator()(goal_ref const & in, goal_ref_buffer & result) override;
    
    void cleanup() override;

    unsigned get_num_steps() const;

    tactic * translate(ast_manager & m) override { return alloc(simplify_tactic, m, m_params); }

    char const* name() const override { return "simplify"; }

};

tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
tactic * mk_elim_and_tactic(ast_manager & m, params_ref const & p = params_ref());

/*
  ADD_TACTIC("simplify", "apply simplification rules.", "mk_simplify_tactic(m, p)")
  ADD_TACTIC("elim-and", "convert (and a b) into (not (or (not a) (not b))).", "mk_elim_and_tactic(m, p)")
*/