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