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