1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     preprocessor_params.h
7 
8 Abstract:
9 
10     Preprocess AST before adding them to the logical context
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2008-01-17.
15 
16 Revision History:
17 
18 --*/
19 #pragma once
20 
21 #include "params/pattern_inference_params.h"
22 #include "params/bit_blaster_params.h"
23 
24 enum lift_ite_kind {
25     LI_NONE,
26     LI_CONSERVATIVE,
27     LI_FULL
28 };
29 
30 struct preprocessor_params : public pattern_inference_params,
31                              public bit_blaster_params {
32     lift_ite_kind   m_lift_ite;
33     lift_ite_kind   m_ng_lift_ite;  // lift ite for non ground terms
34     bool            m_pull_cheap_ite;
35     bool            m_pull_nested_quantifiers;
36     bool            m_eliminate_term_ite;
37     bool            m_macro_finder;
38     bool            m_propagate_values;
39     bool            m_refine_inj_axiom;
40     bool            m_eliminate_bounds;
41     bool            m_simplify_bit2int;
42     bool            m_nnf_cnf;
43     bool            m_distribute_forall;
44     bool            m_reduce_args;
45     bool            m_quasi_macros;
46     bool            m_restricted_quasi_macros;
47     bool            m_max_bv_sharing;
48     bool            m_pre_simplifier;
49     bool            m_nlquant_elim;
50 
51 public:
52     preprocessor_params(params_ref const & p = params_ref()):
m_lift_itepreprocessor_params53         m_lift_ite(LI_NONE),
54         m_ng_lift_ite(LI_NONE),
55         m_pull_cheap_ite(false),
56         m_pull_nested_quantifiers(false),
57         m_eliminate_term_ite(false),
58         m_macro_finder(false),
59         m_propagate_values(true),
60         m_refine_inj_axiom(true),
61         m_eliminate_bounds(false),
62         m_simplify_bit2int(false),
63         m_nnf_cnf(true),
64         m_distribute_forall(false),
65         m_reduce_args(false),
66         m_quasi_macros(false),
67         m_restricted_quasi_macros(false),
68         m_max_bv_sharing(true),
69         m_pre_simplifier(true),
70         m_nlquant_elim(false) {
71         updt_local_params(p);
72     }
73 
74     void updt_local_params(params_ref const & p);
75 
76     void updt_params(params_ref const & p);
77 
78     void display(std::ostream & out) const;
79 };
80 
81