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