1 /*++ 2 Copyright (c) 2010 Microsoft Corporation 3 4 Module Name: 5 6 quant_hoist.h 7 8 Abstract: 9 10 Quantifier hoisting utility. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2010-02-19 15 16 Revision History: 17 18 Hoisted from quant_elim. 19 20 --*/ 21 22 #pragma once 23 24 #include "ast/ast.h" 25 26 class quantifier_hoister { 27 class impl; 28 impl* m_impl; 29 public: 30 quantifier_hoister(ast_manager& m); 31 32 ~quantifier_hoister(); 33 34 /** 35 \brief Pull top-most quantifier up. 36 Create fresh constants for the bound variables. 37 Return the constants, the quantifier type (forall or exists), and 38 the sub-formula under the quantifier. 39 40 The list of variables is empty if the formula is quantifier free or 41 if the existing quantifiers occur under a connective other than 42 or, and, implies, ite (then and else branch only). 43 */ 44 45 void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true); 46 47 /** 48 \brief Pull top-most existential quantifier up. 49 50 The list of variables is empty if there are no top-level existential quantifier. 51 */ 52 void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true); 53 54 55 /** 56 \brief Pull top-most universal (is_forall=true) or existential (is_forall=false) quantifier up. 57 58 The list of variables is empty if there are no top-level universal/existential quantifier. 59 */ 60 void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh = true, bool rewrite_ok = true); 61 62 /** 63 \brief Pull top-most universal (is_forall true) or existential (is_forall=false) quantifier up. 64 Return an expression with de-Bruijn indices and the list of names that were used. 65 Return index of maximal variable. 66 */ 67 68 unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh = true, bool rewrite_ok = true); 69 70 }; 71 72