mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

Merge branch 'unstable' into contrib

Browse source
This commit is contained in:
Leonardo de Moura 2012-11-22 18:44:24 -08:00
commit 9cc65b6522
93 changed files with 13848 additions and 2383 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/front_end_params/model_params.cpp
View file

@ -21,7 +21,6 @@ Revision History:
void model_params::register_params(ini_params & p) {
p.register_bool_param("MODEL_PARTIAL", m_model_partial, "enable/disable partial function interpretations", true);
p.register_bool_param("MODEL_HIDE_UNUSED_PARTITIONS", m_model_hide_unused_partitions, "hide unused partitions, some partitions are associated with internal terms/formulas created by Z3", true);
p.register_bool_param("MODEL_V1", m_model_v1_pp,
"use Z3 version 1.x pretty printer", true);
p.register_bool_param("MODEL_V2", m_model_v2_pp,
@ -30,8 +29,7 @@ void model_params::register_params(ini_params & p) {
"try to compact function graph (i.e., function interpretations that are lookup tables", true);
p.register_bool_param("MODEL_COMPLETION", m_model_completion,
"assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model", true);
p.register_bool_param("MODEL_DISPLAY_ARG_SORT", m_model_display_arg_sort,
"display the sort of each argument when printing function interpretations", true);
}

6
src/front_end_params/model_params.h
View file

@ -23,21 +23,17 @@ Revision History:
struct model_params {
bool m_model_partial;
bool m_model_hide_unused_partitions;
bool m_model_compact;
bool m_model_v1_pp;
bool m_model_v2_pp;
bool m_model_completion;
bool m_model_display_arg_sort;
model_params():
m_model_partial(false),
m_model_hide_unused_partitions(true),
m_model_compact(false),
m_model_v1_pp(false),
m_model_v2_pp(false),
m_model_completion(false),
m_model_display_arg_sort(true) {
m_model_completion(false) {
}
void register_params(ini_params & p);

2
src/front_end_params/params2front_end_params.cpp
View file

@ -27,7 +27,6 @@ Revision History:
the new strategy framework.
*/
void params2front_end_params(params_ref const & s, front_end_params & t) {
t.m_quant_elim = s.get_bool(":elim-quant", t.m_quant_elim);
t.m_relevancy_lvl = s.get_uint(":relevancy", t.m_relevancy_lvl);
TRACE("qi_cost", s.display(tout); tout << "\n";);
t.m_qi_cost = s.get_str(":qi-cost", t.m_qi_cost.c_str());
@ -40,7 +39,6 @@ void params2front_end_params(params_ref const & s, front_end_params & t) {
t.m_well_sorted_check = s.get_bool(":check-sorts", t.m_well_sorted_check);
t.m_qi_eager_threshold = s.get_double(":qi-eager-threshold", t.m_qi_eager_threshold);
t.m_qi_lazy_threshold = s.get_double(":qi-lazy-threshold", t.m_qi_lazy_threshold);
t.m_solver = s.get_bool(":solver", t.m_solver);
t.m_preprocess = s.get_bool(":preprocess", t.m_preprocess);
t.m_hi_div0 = s.get_bool(":hi-div0", t.m_hi_div0);
t.m_auto_config = s.get_bool(":auto-config", t.m_auto_config);

2
src/front_end_params/pattern_inference_params.cpp
View file

@ -21,7 +21,7 @@ Revision History:
void pattern_inference_params::register_params(ini_params & p) {
p.register_unsigned_param("PI_MAX_MULTI_PATTERNS", m_pi_max_multi_patterns,
"when patterns are not provided, the prover uses a heuristic to infer them. This option sets the threshold on the number of extra multi-patterns that can be created. By default, the prover creates at most one multi-pattern when there is no unary pattern");
p.register_bool_param("PI_BLOCK_LOOOP_PATTERNS", m_pi_block_loop_patterns,
p.register_bool_param("PI_BLOCK_LOOP_PATTERNS", m_pi_block_loop_patterns,
"block looping patterns during pattern inference");
p.register_int_param("PI_ARITH", 0, 2, reinterpret_cast<int&>(m_pi_arith),
"0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms.");

37
src/front_end_params/preprocessor_params.h
View file

@ -31,13 +31,6 @@ enum lift_ite_kind {
LI_FULL
};
enum q_arith_kind {
QA_NONE,
QA_COOPER,
QA_OMEGA,
QA_ALTERNATE
};
struct preprocessor_params : public nnf_params, public cnf_params, public pattern_inference_params,
public bit_blaster_params, public bv_simplifier_params {
lift_ite_kind m_lift_ite;
@ -46,27 +39,20 @@ struct preprocessor_params : public nnf_params, public cnf_params, public patter
bool m_pull_nested_quantifiers;
bool m_eliminate_term_ite;
bool m_eliminate_and; // represent (and a b) as (not (or (not a) (not b)))
bool m_reverse_implies; // translate (implies a b) into (or b (not a))
bool m_macro_finder;
bool m_solver;
bool m_propagate_values;
bool m_propagate_booleans;
bool m_context_simplifier;
bool m_strong_context_simplifier;
bool m_refine_inj_axiom;
bool m_eliminate_bounds;
bool m_quant_elim;
bool m_nlquant_elim;
bool m_der;
bool m_simplify_bit2int;
bool m_nnf_cnf;
bool m_distribute_forall;
bool m_reduce_args;
bool m_pre_demod;
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():
@ -77,25 +63,19 @@ public:
m_eliminate_term_ite(false),
m_eliminate_and(true),
m_macro_finder(false),
m_solver(false),
m_propagate_values(true),
m_propagate_booleans(false), // TODO << check peformance
m_context_simplifier(false),
m_strong_context_simplifier(false),
m_refine_inj_axiom(true),
m_eliminate_bounds(false),
m_quant_elim(false),
m_nlquant_elim(false),
m_der(false),
m_simplify_bit2int(false),
m_nnf_cnf(true),
m_distribute_forall(false),
m_reduce_args(false),
m_pre_demod(false),
m_quasi_macros(false),
m_restricted_quasi_macros(false),
m_max_bv_sharing(true),
m_pre_simplifier(true) {
m_pre_simplifier(true),
m_nlquant_elim(false) {
}
void register_params(ini_params & p) {
@ -109,27 +89,16 @@ public:
p.register_bool_param("ELIM_TERM_ITE", m_eliminate_term_ite, "eliminate term if-then-else in the preprocessor");
p.register_bool_param("ELIM_AND", m_eliminate_and, "represent (and a b) as (not (or (not a) (not b)))");
p.register_bool_param("MACRO_FINDER", m_macro_finder, "try to find universally quantified formulas that can be viewed as macros");
p.register_bool_param("SOLVER", m_solver, "enable solver during preprocessing step", true);
p.register_bool_param("PROPAGATE_VALUES", m_propagate_values, "propagate values during preprocessing step");
p.register_bool_param("PROPAGATE_BOOLEANS", m_propagate_booleans, "propagate boolean values during preprocessing step");
p.register_bool_param("PULL_CHEAP_ITE_TREES", m_pull_cheap_ite_trees);
p.register_bool_param("PULL_NESTED_QUANTIFIERS", m_pull_nested_quantifiers, "eliminate nested quantifiers by moving nested quantified variables to the outermost quantifier, it is unnecessary if the formula is converted into CNF");
p.register_bool_param("CONTEXT_SIMPLIFIER", m_context_simplifier,
"Simplify Boolean sub-expressions if they already appear in context", true);
p.register_bool_param("STRONG_CONTEXT_SIMPLIFIER", m_strong_context_simplifier,
"Simplify Boolean sub-expressions by using full satisfiability queries", true);
p.register_bool_param("REFINE_INJ_AXIOM", m_refine_inj_axiom);
p.register_bool_param("ELIM_BOUNDS", m_eliminate_bounds, "cheap Fourier-Motzkin");
p.register_bool_param("ELIM_QUANTIFIERS", m_quant_elim,
"Use quantifier elimination procedures on Boolean, Bit-vector, Arithmetic and Array variables", true);
p.register_bool_param("ELIM_NLARITH_QUANTIFIERS", m_nlquant_elim,
"Eliminate non-linear quantifiers", true);
p.register_bool_param("DER", m_der);
p.register_bool_param("BIT2INT", m_simplify_bit2int, "hoist bit2int conversions over arithmetical expressions");
p.register_bool_param("DISTRIBUTE_FORALL", m_distribute_forall);
p.register_bool_param("REDUCE_ARGS", m_reduce_args);
p.register_bool_param("PRE_DEMODULATOR", m_pre_demod, "apply demodulators during preprocessing step");
p.register_bool_param("QUASI_MACROS", m_quasi_macros);
p.register_bool_param("RESTRICTED_QUASI_MACROS", m_restricted_quasi_macros);
p.register_bool_param("BV_MAX_SHARING", m_max_bv_sharing);