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
70
71
/*++
Copyright (c) 2010 Microsoft Corporation
Module Name:
quant_hoist.h
Abstract:
Quantifier hoisting utility.
Author:
Nikolaj Bjorner (nbjorner) 2010-02-19
Revision History:
Hoisted from quant_elim.
--*/
#pragma once
#include "ast/ast.h"
class quantifier_hoister {
class impl;
impl* m_impl;
public:
quantifier_hoister(ast_manager& m);
~quantifier_hoister();
/**
\brief Pull top-most quantifier up.
Create fresh constants for the bound variables.
Return the constants, the quantifier type (forall or exists), and
the sub-formula under the quantifier.
The list of variables is empty if the formula is quantifier free or
if the existing quantifiers occur under a connective other than
or, and, implies, ite (then and else branch only).
*/
void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true);
/**
\brief Pull top-most existential quantifier up.
The list of variables is empty if there are no top-level existential quantifier.
*/
void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result, bool use_fresh = true, bool rewrite_ok = true);
/**
\brief Pull top-most universal (is_forall=true) or existential (is_forall=false) quantifier up.
The list of variables is empty if there are no top-level universal/existential quantifier.
*/
void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars, bool use_fresh = true, bool rewrite_ok = true);
/**
\brief Pull top-most universal (is_forall true) or existential (is_forall=false) quantifier up.
Return an expression with de-Bruijn indices and the list of names that were used.
Return index of maximal variable.
*/
unsigned pull_quantifier(bool is_forall, expr_ref& fml, ptr_vector<sort>* sorts, svector<symbol>* names, bool use_fresh = true, bool rewrite_ok = true);
};