# z3 / src / ast / simplifier / elim_bounds.h

 ``` 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``` ```/*++ Copyright (c) 2006 Microsoft Corporation Module Name: elim_bounds.h Abstract: Author: Leonardo de Moura (leonardo) 2008-06-28. Revision History: --*/ #ifndef _ELIM_BOUNDS_H_ #define _ELIM_BOUNDS_H_ #include"ast.h" #include"arith_decl_plugin.h" #include"simplifier.h" /** \brief Functor for eliminating irrelevant bounds in quantified formulas. Example: (forall (x Int) (y Int) (or (not (>= y x) (not (>= x 0)) (= (select a x) 1)))) The bound (>= y x) is irrelevant and can be eliminated. This can be easily proved by using Fourier-Motzkin elimination. Limitations & Assumptions: - It assumes the input formula was already simplified. - It can only handle bounds in the diff-logic fragment. \remark This operation is subsumed by Fourier-Motzkin elimination. */ class elim_bounds { ast_manager & m_manager; arith_util m_util; bool is_bound(expr * n, var * & lower, var * & upper); bool is_bound(expr * n); public: elim_bounds(ast_manager & m); void operator()(quantifier * q, expr_ref & r); }; /** \brief Functor for applying elim_bounds in all universal quantifiers in an expression. Assumption: the formula was already skolemized. */ class elim_bounds_star : public simplifier { protected: elim_bounds m_elim; virtual bool visit_quantifier(quantifier * q); virtual void reduce1_quantifier(quantifier * q); public: elim_bounds_star(ast_manager & m):simplifier(m), m_elim(m) { enable_ac_support(false); } virtual ~elim_bounds_star() {} }; #endif /* _ELIM_BOUNDS_H_ */ ```