mirror of
https://github.com/Z3Prover/z3
synced 2025-08-22 11:07:51 +00:00
80 lines
2.1 KiB
C++
80 lines
2.1 KiB
C++
/*++
|
|
Copyright (c) 2006 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
preprocessor_params.h
|
|
|
|
Abstract:
|
|
|
|
Preprocess AST before adding them to the logical context
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2008-01-17.
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "params/pattern_inference_params.h"
|
|
#include "params/bit_blaster_params.h"
|
|
|
|
enum class lift_ite_kind {
|
|
LI_NONE,
|
|
LI_CONSERVATIVE,
|
|
LI_FULL
|
|
};
|
|
|
|
struct preprocessor_params : public pattern_inference_params,
|
|
public bit_blaster_params {
|
|
lift_ite_kind m_lift_ite;
|
|
lift_ite_kind m_ng_lift_ite; // lift ite for non ground terms
|
|
bool m_pull_cheap_ite;
|
|
bool m_pull_nested_quantifiers;
|
|
bool m_eliminate_term_ite;
|
|
bool m_macro_finder;
|
|
bool m_propagate_values;
|
|
bool m_refine_inj_axiom;
|
|
bool m_eliminate_bounds;
|
|
bool m_simplify_bit2int;
|
|
bool m_nnf_cnf;
|
|
bool m_distribute_forall;
|
|
bool m_reduce_args;
|
|
bool m_quasi_macros;
|
|
bool m_restricted_quasi_macros;
|
|
bool m_max_bv_sharing;
|
|
bool m_pre_simplifier;
|
|
bool m_nlquant_elim;
|
|
|
|
public:
|
|
preprocessor_params(params_ref const & p = params_ref()):
|
|
m_lift_ite(lift_ite_kind::LI_NONE),
|
|
m_ng_lift_ite(lift_ite_kind::LI_NONE),
|
|
m_pull_cheap_ite(false),
|
|
m_pull_nested_quantifiers(false),
|
|
m_eliminate_term_ite(false),
|
|
m_macro_finder(false),
|
|
m_propagate_values(true),
|
|
m_refine_inj_axiom(true),
|
|
m_eliminate_bounds(false),
|
|
m_simplify_bit2int(false),
|
|
m_nnf_cnf(true),
|
|
m_distribute_forall(false),
|
|
m_reduce_args(false),
|
|
m_quasi_macros(false),
|
|
m_restricted_quasi_macros(false),
|
|
m_max_bv_sharing(true),
|
|
m_pre_simplifier(true),
|
|
m_nlquant_elim(false) {
|
|
updt_local_params(p);
|
|
}
|
|
|
|
void updt_local_params(params_ref const & p);
|
|
|
|
void updt_params(params_ref const & p);
|
|
|
|
void display(std::ostream & out) const;
|
|
};
|
|
|