1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     elim_bounds2.h
7 
8 Abstract:
9 
10     <abstract>
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2008-06-28.
15 
16 Revision History:
17 
18 --*/
19 #pragma once
20 
21 #include "ast/ast.h"
22 #include "ast/arith_decl_plugin.h"
23 #include "ast/rewriter/rewriter.h"
24 
25 /**
26    \brief Functor for eliminating irrelevant bounds in quantified formulas.
27 
28    Example:
29    (forall (x Int) (y Int) (or (not (>= y x) (not (>= x 0)) (= (select a x) 1))))
30 
31    The bound (>= y x) is irrelevant and can be eliminated.
32 
33    This can be easily proved by using Fourier-Motzkin elimination.
34 
35    Limitations & Assumptions:
36    - It assumes the input formula was already simplified.
37    - It can only handle bounds in the diff-logic fragment.
38 
39    \remark This operation is subsumed by Fourier-Motzkin elimination.
40 */
41 class elim_bounds_cfg : public default_rewriter_cfg {
42     ast_manager &      m;
43     arith_util         m_util;
44     bool is_bound(expr * n, var * & lower, var * & upper);
45     bool is_bound(expr * n);
46 public:
47     elim_bounds_cfg(ast_manager & m);
48 
49     bool reduce_quantifier(quantifier * old_q,
50                            expr * new_body,
51                            expr * const * new_patterns,
52                            expr * const * new_no_patterns,
53                            expr_ref & result,
54                            proof_ref & result_pr);
55 };
56 
57 /**
58    \brief Functor for applying elim_bounds2 in all
59    universal quantifiers in an expression.
60 
61    Assumption: the formula was already skolemized.
62 */
63 class elim_bounds_rw : public rewriter_tpl<elim_bounds_cfg> {
64 protected:
65     elim_bounds_cfg  m_cfg;
66 public:
elim_bounds_rw(ast_manager & m)67     elim_bounds_rw(ast_manager & m):
68         rewriter_tpl<elim_bounds_cfg>(m, m.proofs_enabled(), m_cfg),
69         m_cfg(m)
70     {}
71 
~elim_bounds_rw()72     ~elim_bounds_rw() override {}
73 };
74 
75 
76