mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
connected smt_params with new parameter infrastructure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
5057257e40
commit
773f82a44c
|
|
@ -323,7 +323,7 @@ namespace api {
|
|||
|
||||
smt::kernel & context::get_smt_kernel() {
|
||||
if (!m_solver) {
|
||||
// PARAM-TODO: copy config_params -> fparams
|
||||
m_fparams.updt_params(m_params);
|
||||
m_solver = alloc(smt::kernel, m_manager, m_fparams);
|
||||
}
|
||||
return *m_solver;
|
||||
|
|
|
|||
32
src/smt/params/preprocessor_params.cpp
Normal file
32
src/smt/params/preprocessor_params.cpp
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
preprocessor_params.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Preprocess AST before adding them to the logical context
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-12-02.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"preprocessor_params.h"
|
||||
#include"smt_params_helper.hpp"
|
||||
|
||||
void preprocessor_params::updt_local_params(params_ref const & _p) {
|
||||
smt_params_helper p(_p);
|
||||
m_macro_finder = p.macro_finder();
|
||||
}
|
||||
|
||||
void preprocessor_params::updt_params(params_ref const & p) {
|
||||
pattern_inference_params::updt_params(p);
|
||||
bv_simplifier_params::updt_params(p);
|
||||
arith_simplifier_params::updt_params(p);
|
||||
updt_local_params(p);
|
||||
}
|
||||
|
|
@ -56,7 +56,7 @@ struct preprocessor_params : public pattern_inference_params,
|
|||
bool m_nlquant_elim;
|
||||
|
||||
public:
|
||||
preprocessor_params():
|
||||
preprocessor_params(params_ref const & p = params_ref()):
|
||||
m_lift_ite(LI_NONE),
|
||||
m_ng_lift_ite(LI_NONE),
|
||||
m_pull_cheap_ite_trees(false),
|
||||
|
|
@ -77,36 +77,12 @@ public:
|
|||
m_max_bv_sharing(true),
|
||||
m_pre_simplifier(true),
|
||||
m_nlquant_elim(false) {
|
||||
updt_local_params(p);
|
||||
}
|
||||
|
||||
#if 0
|
||||
void register_params(ini_params & p) {
|
||||
pattern_inference_params::register_params(p);
|
||||
bit_blaster_params::register_params(p);
|
||||
bv_simplifier_params::register_params(p);
|
||||
arith_simplifier_params::register_params(p);
|
||||
p.register_int_param("lift_ite", 0, 2, reinterpret_cast<int&>(m_lift_ite), "ite term lifting: 0 - no lifting, 1 - conservative, 2 - full");
|
||||
p.register_int_param("ng_lift_ite", 0, 2, reinterpret_cast<int&>(m_ng_lift_ite), "ite (non-ground) term lifting: 0 - no lifting, 1 - conservative, 2 - full");
|
||||
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("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("refine_inj_axiom", m_refine_inj_axiom);
|
||||
p.register_bool_param("elim_bounds", m_eliminate_bounds, "cheap Fourier-Motzkin");
|
||||
|
||||
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("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);
|
||||
p.register_bool_param("pre_simplifier", m_pre_simplifier);
|
||||
}
|
||||
#endif
|
||||
void updt_local_params(params_ref const & p);
|
||||
|
||||
void updt_params(params_ref const & p);
|
||||
};
|
||||
|
||||
#endif /* _PREPROCESSOR_PARAMS_H_ */
|
||||
|
|
|
|||
37
src/smt/params/qi_params.cpp
Normal file
37
src/smt/params/qi_params.cpp
Normal file
|
|
@ -0,0 +1,37 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
qi_params.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-12-02.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"qi_params.h"
|
||||
#include"smt_params_helper.hpp"
|
||||
|
||||
void qi_params::updt_params(params_ref const & _p) {
|
||||
smt_params_helper p(_p);
|
||||
m_mbqi = p.mbqi();
|
||||
m_mbqi_max_cexs = p.mbqi_max_cexs();
|
||||
m_mbqi_max_cexs_incr = p.mbqi_max_cexs_incr();
|
||||
m_mbqi_max_iterations = p.mbqi_max_iterations();
|
||||
m_mbqi_trace = p.mbqi_trace();
|
||||
m_mbqi_force_template = p.mbqi_force_template();
|
||||
m_qi_profile = p.qi_profile();
|
||||
m_qi_profile_freq = p.qi_profile_freq();
|
||||
m_qi_max_instances = p.qi_max_instances();
|
||||
m_qi_eager_threshold = p.qi_eager_threshold();
|
||||
m_qi_lazy_threshold = p.qi_lazy_threshold();
|
||||
m_qi_cost = p.qi_cost();
|
||||
m_qi_max_eager_multipatterns = p.qi_max_multi_patterns();
|
||||
}
|
||||
|
|
@ -20,6 +20,7 @@ Revision History:
|
|||
#define _QI_PARAMS_H_
|
||||
|
||||
#include"util.h"
|
||||
#include"params.h"
|
||||
|
||||
enum quick_checker_mode {
|
||||
MC_NO, // do not use (cheap) model checking based instantiation
|
||||
|
|
@ -53,7 +54,7 @@ struct qi_params {
|
|||
|
||||
bool m_instgen;
|
||||
|
||||
qi_params():
|
||||
qi_params(params_ref const & p = params_ref()):
|
||||
/*
|
||||
The "weight 0" performance bug
|
||||
------------------------------
|
||||
|
|
@ -93,49 +94,17 @@ struct qi_params {
|
|||
m_qi_max_instances(UINT_MAX),
|
||||
m_qi_lazy_instantiation(false),
|
||||
m_qi_conservative_final_check(false),
|
||||
#ifdef _EXTERNAL_RELEASE
|
||||
m_mbqi(true), // enabled by default
|
||||
#else
|
||||
m_mbqi(false), // to avoid Rustan whining that the models are not partial anymore.
|
||||
#endif
|
||||
m_mbqi_max_cexs(1),
|
||||
m_mbqi_max_cexs_incr(1),
|
||||
m_mbqi_max_iterations(1000),
|
||||
m_mbqi_trace(false),
|
||||
m_mbqi_force_template(10),
|
||||
m_instgen(false) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
#if 0
|
||||
void register_params(ini_params & p) {
|
||||
p.register_unsigned_param("qi_max_eager_multi_patterns", m_qi_max_eager_multipatterns,
|
||||
"Specify the number of extra multi patterns that are processed eagerly. By default, the prover use at most one multi-pattern eagerly when there is no unary pattern. This value should be smaller than or equal to PI_MAX_MULTI_PATTERNS");
|
||||
p.register_unsigned_param("qi_max_lazy_multi_pattern_matching", m_qi_max_lazy_multipattern_matching, "Maximum number of rounds of matching in a branch for delayed multipatterns. A multipattern is delayed based on the value of QI_MAX_EAGER_MULTI_PATTERNS");
|
||||
p.register_string_param("qi_cost", m_qi_cost, "The cost function for quantifier instantiation");
|
||||
p.register_string_param("qi_new_gen", m_qi_new_gen, "The function for calculating the generation of newly constructed terms");
|
||||
p.register_double_param("qi_eager_threshold", m_qi_eager_threshold, "Threshold for eager quantifier instantiation");
|
||||
p.register_double_param("qi_lazy_threshold", m_qi_lazy_threshold, "Threshold for lazy quantifier instantiation");
|
||||
p.register_bool_param("qi_profile", m_qi_profile);
|
||||
p.register_unsigned_param("qi_profile_freq", m_qi_profile_freq);
|
||||
p.register_int_param("qi_quick_checker", 0, 2, reinterpret_cast<int&>(m_qi_quick_checker), "0 - do not use (cheap) model checker, 1 - instantiate instances unsatisfied by current model, 2 - 1 + instantiate instances not satisfied by current model");
|
||||
p.register_bool_param("qi_lazy_quick_checker", m_qi_lazy_quick_checker);
|
||||
p.register_bool_param("qi_promote_unsat", m_qi_promote_unsat);
|
||||
p.register_unsigned_param("qi_max_instances", m_qi_max_instances);
|
||||
p.register_bool_param("qi_lazy_instantiation", m_qi_lazy_instantiation);
|
||||
p.register_bool_param("qi_conservative_final_check", m_qi_conservative_final_check);
|
||||
|
||||
|
||||
p.register_bool_param("mbqi", m_mbqi, "Model Based Quantifier Instantiation (MBQI)");
|
||||
p.register_unsigned_param("mbqi_max_cexs", m_mbqi_max_cexs, "Initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation", true);
|
||||
p.register_unsigned_param("mbqi_max_cexs_incr", m_mbqi_max_cexs_incr, "Increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI", true);
|
||||
p.register_unsigned_param("mbqi_max_iterations", m_mbqi_max_iterations, "Maximum number of rounds of MBQI", true);
|
||||
p.register_bool_param("mbqi_trace", m_mbqi_trace, "Generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied.", true);
|
||||
p.register_unsigned_param("mbqi_force_template", m_mbqi_force_template, "Some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= MBQI_FORCE_TEMPLATE are forced to be used as a template", true);
|
||||
|
||||
p.register_bool_param("inst_gen", m_instgen, "Enable Instantiation Generation solver (disables other quantifier reasoning)", false);
|
||||
}
|
||||
#endif
|
||||
|
||||
void updt_params(params_ref const & p);
|
||||
};
|
||||
|
||||
#endif /* _QI_PARAMS_H_ */
|
||||
|
|
|
|||
|
|
@ -17,105 +17,33 @@ Revision History:
|
|||
|
||||
--*/
|
||||
#include"smt_params.h"
|
||||
#include"trace.h"
|
||||
|
||||
#if 0
|
||||
void smt_params::register_params(ini_params & p) {
|
||||
dyn_ack_params::register_params(p);
|
||||
qi_params::register_params(p);
|
||||
theory_arith_params::register_params(p);
|
||||
theory_array_params::register_params(p);
|
||||
theory_bv_params::register_params(p);
|
||||
theory_datatype_params::register_params(p);
|
||||
|
||||
p.register_bool_param("check_proof", m_check_proof);
|
||||
p.register_bool_param("display_proof", m_display_proof);
|
||||
p.register_bool_param("display_dot_proof", m_display_dot_proof);
|
||||
p.register_bool_param("display_unsat_core", m_display_unsat_core);
|
||||
p.register_bool_param("eq_propagation", m_eq_propagation);
|
||||
p.register_bool_param("bin_clauses", m_binary_clause_opt);
|
||||
p.register_unsigned_param("relevancy", m_relevancy_lvl, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant", true);
|
||||
p.register_bool_param("relevancy_lemma", m_relevancy_lemma, "true if lemmas are used to propagate relevancy");
|
||||
p.register_unsigned_param("random_seed", m_random_seed, "random seed for Z3");
|
||||
p.register_percentage_param("random_case_split_freq", m_random_var_freq, "frequency of random case splits");
|
||||
p.register_int_param("phase_selection", 0, 6, reinterpret_cast<int&>(m_phase_selection), "phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences");
|
||||
p.register_bool_param("minimize_lemmas", m_minimize_lemmas, "enable/disable lemma minimization algorithm");
|
||||
p.register_unsigned_param("max_conflicts", m_max_conflicts, "maximum number of conflicts");
|
||||
|
||||
p.register_unsigned_param("recent_lemma_threshold", m_recent_lemmas_size);
|
||||
p.register_unsigned_param("tick", m_tick);
|
||||
|
||||
PRIVATE_PARAMS({
|
||||
p.register_bool_param("theory_resolve", m_theory_resolve, "Apply theory resolution to produce auxiliary conflict clauses", true);
|
||||
});
|
||||
|
||||
p.register_int_param("restart_strategy", 0, 4, reinterpret_cast<int&>(m_restart_strategy), "0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic");
|
||||
p.register_unsigned_param("restart_initial", m_restart_initial,
|
||||
"inital restart frequency in number of conflicts, it is also the unit for the luby sequence");
|
||||
p.register_double_param("restart_factor", m_restart_factor, "when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold");
|
||||
p.register_bool_param("restart_adaptive", m_restart_adaptive, "disable restarts based on the search 'agility'");
|
||||
p.register_percentage_param("restart_agility_threshold", m_restart_agility_threshold);
|
||||
|
||||
p.register_int_param("lemma_gc_strategy", 0, 2, reinterpret_cast<int&>(m_lemma_gc_strategy), "0 - fixed, 1 - geometric, 2 - at every restart");
|
||||
p.register_bool_param("lemma_gc_half", m_lemma_gc_half, "true for simple gc algorithm (delete approx. half of the clauses)");
|
||||
p.register_unsigned_param("lemma_gc_initial", m_lemma_gc_initial, "lemma initial gc frequency (in number of conflicts), used by fixed or geometric strategies");
|
||||
p.register_double_param("lemma_gc_factor", m_lemma_gc_factor, "used by geometric strategy");
|
||||
p.register_unsigned_param("lemma_gc_new_old_ratio", m_new_old_ratio);
|
||||
p.register_unsigned_param("lemma_gc_new_clause_activity", m_new_clause_activity);
|
||||
p.register_unsigned_param("lemma_gc_old_clause_activity", m_old_clause_activity);
|
||||
p.register_unsigned_param("lemma_gc_new_clause_relevancy", m_new_clause_relevancy);
|
||||
p.register_unsigned_param("lemma_gc_old_clause_relevancy", m_old_clause_activity);
|
||||
|
||||
p.register_bool_param("simplify_clauses", m_simplify_clauses);
|
||||
|
||||
p.register_int_param("random_initial_activity", 0, 2, reinterpret_cast<int&>(m_random_initial_activity));
|
||||
|
||||
PRIVATE_PARAMS({
|
||||
|
||||
p.register_double_param("inv_decay", m_inv_decay);
|
||||
p.register_unsigned_param("phase_caching_on_duration", m_phase_caching_on);
|
||||
p.register_unsigned_param("phase_caching_off_duration", m_phase_caching_off);
|
||||
});
|
||||
|
||||
p.register_bool_param("smtlib_dump_lemmas", m_smtlib_dump_lemmas);
|
||||
p.register_string_param("smtlib_logic", m_smtlib_logic, "Name used for the :logic field when generating SMT-LIB benchmarks");
|
||||
p.register_bool_param("display_features", m_display_features);
|
||||
|
||||
p.register_bool_param("new_core2th_eq", m_new_core2th_eq);
|
||||
p.register_bool_param("ematching", m_ematching, "E-Matching based quantifier instantiation");
|
||||
|
||||
p.register_bool_param("profile_res_sub", m_profile_res_sub);
|
||||
#ifndef _EXTERNAL_RELEASE
|
||||
p.register_bool_param("display_bool_var2expr", m_display_bool_var2expr);
|
||||
p.register_bool_param("display_ll_bool_var2expr", m_display_ll_bool_var2expr);
|
||||
p.register_bool_param("abort_after_preproc", m_abort_after_preproc, "abort after preprocessing step, this flag is only useful for debugging purposes");
|
||||
p.register_bool_param("display_installed_theories", m_display_installed_theories, "display theories installed at smt::context", true);
|
||||
#endif
|
||||
p.register_int_param("case_split", 0, 5, reinterpret_cast<int&>(m_case_split_strategy), "0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal");
|
||||
p.register_unsigned_param("rel_case_split_order", 0, 2, m_rel_case_split_order, "structural (relevancy) splitting order: 0 - left-to-right (default), 1 - random, 2 - right-to-left");
|
||||
p.register_bool_param("lookahead_diseq", m_lookahead_diseq);
|
||||
|
||||
p.register_bool_param("delay_units", m_delay_units);
|
||||
p.register_unsigned_param("delay_units_threshold", m_delay_units_threshold);
|
||||
|
||||
p.register_bool_param("model", m_model, "enable/disable model construction", true);
|
||||
p.register_bool_param("model_validate", m_model_validate, "validate the model", true);
|
||||
p.register_bool_param("model_on_timeout", m_model_on_timeout, "after hitting soft-timeout or memory high watermark, generate a candidate model", true);
|
||||
p.register_bool_param("model_on_final_check", m_model_on_final_check, "display candidate model (in the standard output) whenever Z3 hits a final check", true);
|
||||
|
||||
p.register_unsigned_param("progress_sampling_freq", m_progress_sampling_freq, "frequency for progress output in miliseconds");
|
||||
|
||||
|
||||
p.register_bool_param("user_theory_preprocess_axioms",
|
||||
m_user_theory_preprocess_axioms,
|
||||
"Apply full pre-processing to user theory axioms",
|
||||
true);
|
||||
|
||||
p.register_bool_param("user_theory_persist_axioms",
|
||||
m_user_theory_persist_axioms,
|
||||
"Persist user axioms to the base level",
|
||||
true);
|
||||
#include"smt_params_helper.hpp"
|
||||
|
||||
void smt_params::updt_local_params(params_ref const & _p) {
|
||||
smt_params_helper p(_p);
|
||||
m_auto_config = p.auto_config();
|
||||
m_ematching = p.ematching();
|
||||
m_phase_selection = static_cast<phase_selection>(p.phase_selection());
|
||||
m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
|
||||
m_restart_factor = p.restart_factor();
|
||||
m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
|
||||
m_delay_units = p.delay_units();
|
||||
m_delay_units_threshold = p.delay_units_threshold();
|
||||
}
|
||||
|
||||
void smt_params::updt_params(params_ref const & p) {
|
||||
preprocessor_params::updt_params(p);
|
||||
qi_params::updt_params(p);
|
||||
theory_arith_params::updt_params(p);
|
||||
theory_bv_params::updt_params(p);
|
||||
updt_local_params(p);
|
||||
}
|
||||
|
||||
void smt_params::updt_params(context_params const & p) {
|
||||
m_auto_config = p.m_auto_config;
|
||||
m_soft_timeout = p.m_timeout;
|
||||
m_model = p.m_model;
|
||||
m_model_validate = p.m_validate_model;
|
||||
m_proof_mode = p.m_proof ? PGM_FINE : PGM_DISABLED;
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -27,6 +27,7 @@ Revision History:
|
|||
#include"theory_bv_params.h"
|
||||
#include"theory_datatype_params.h"
|
||||
#include"preprocessor_params.h"
|
||||
#include"context_params.h"
|
||||
|
||||
enum phase_selection {
|
||||
PS_ALWAYS_FALSE,
|
||||
|
|
@ -209,23 +210,7 @@ struct smt_params : public preprocessor_params,
|
|||
proof_gen_mode m_proof_mode;
|
||||
bool m_auto_config;
|
||||
|
||||
#if 0
|
||||
unsigned m_memory_high_watermark;
|
||||
unsigned m_memory_max_size;
|
||||
|
||||
bool m_auto_config;
|
||||
|
||||
bool m_debug_ref_count;
|
||||
|
||||
m_well_sorted_check(true),
|
||||
m_memory_high_watermark(0),
|
||||
m_memory_max_size(0),
|
||||
|
||||
m_auto_config(true),
|
||||
m_debug_ref_count(false) {
|
||||
#endif
|
||||
|
||||
smt_params():
|
||||
smt_params(params_ref const & p = params_ref()):
|
||||
m_display_proof(false),
|
||||
m_display_dot_proof(false),
|
||||
m_display_unsat_core(false),
|
||||
|
|
@ -294,7 +279,14 @@ struct smt_params : public preprocessor_params,
|
|||
m_dump_goal_as_smt(false),
|
||||
m_proof_mode(PGM_DISABLED),
|
||||
m_auto_config(true) {
|
||||
updt_local_params(p);
|
||||
}
|
||||
|
||||
void updt_local_params(params_ref const & p);
|
||||
|
||||
void updt_params(params_ref const & p);
|
||||
|
||||
void updt_params(context_params const & p);
|
||||
};
|
||||
|
||||
#endif /* _SMT_PARAMS_H_ */
|
||||
|
|
|
|||
38
src/smt/params/smt_params_helper.pyg
Normal file
38
src/smt/params/smt_params_helper.pyg
Normal file
|
|
@ -0,0 +1,38 @@
|
|||
def_module_params(module_name='smt',
|
||||
class_name='smt_params_helper',
|
||||
description='smt solver based on lazy smt',
|
||||
export=True,
|
||||
params=(('auto_config', BOOL, True, 'automatically configure solver'),
|
||||
('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
|
||||
('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
|
||||
('phase_selection', UINT, 4, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
|
||||
('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
|
||||
('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'),
|
||||
('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal'),
|
||||
('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
|
||||
('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
|
||||
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
|
||||
('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
|
||||
('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),
|
||||
('mbqi.max_iterations', UINT, 1000, 'maximum number of rounds of MBQI'),
|
||||
('mbqi.trace', BOOL, False, 'generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied'),
|
||||
('mbqi.force_template', UINT, 10, 'some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template'),
|
||||
('qi.profile', BOOL, False, 'profile quantifier instantiation'),
|
||||
('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'),
|
||||
('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'),
|
||||
('qi.eager_threshold', DOUBLE, 10.0, 'threshold for eager quantifier instantiation'),
|
||||
('qi.lazy_threshold', DOUBLE, 20.0, 'threshold for lazy quantifier instantiation'),
|
||||
('qi.cost', STRING, '(+ weight generation)', 'expression specifying what is the cost of a given quantifier instantiation'),
|
||||
('qi.max_multi_patterns', UINT, 0, 'specify the number of extra multi patterns'),
|
||||
('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
|
||||
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
|
||||
('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination'),
|
||||
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'),
|
||||
('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'),
|
||||
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),
|
||||
('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic'),
|
||||
('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'),
|
||||
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
|
||||
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
|
||||
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
|
||||
('arith.ignore_int', BOOL, False, 'treat integer variables as real')))
|
||||
|
|
@ -16,63 +16,22 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#include"theory_arith_params.h"
|
||||
#include"smt_params_helper.hpp"
|
||||
|
||||
#if 0
|
||||
void theory_arith_params::register_params(ini_params & p) {
|
||||
#ifdef _EXTERNAL_RELEASE
|
||||
p.register_int_param("arith_solver", 0, 3, reinterpret_cast<int&>(m_arith_mode), "select arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination");
|
||||
#else
|
||||
p.register_int_param("arith_solver", 0, 4, reinterpret_cast<int&>(m_arith_mode), "select arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination, 4 - model guided arith_solver");
|
||||
#endif
|
||||
p.register_bool_param("arith_force_simplex", m_arith_auto_config_simplex, "force Z3 to use simplex solver.");
|
||||
p.register_unsigned_param("arith_blands_rule_threshold", m_arith_blands_rule_threshold);
|
||||
p.register_bool_param("arith_propagate_eqs", m_arith_propagate_eqs);
|
||||
p.register_int_param("arith_propagation_mode", 0, 2, reinterpret_cast<int&>(m_arith_bound_prop));
|
||||
p.register_bool_param("arith_stronger_lemmas", m_arith_stronger_lemmas);
|
||||
p.register_bool_param("arith_skip_big_coeffs", m_arith_skip_rows_with_big_coeffs);
|
||||
p.register_unsigned_param("arith_max_lemma_size", m_arith_max_lemma_size);
|
||||
p.register_unsigned_param("arith_small_lemma_size", m_arith_small_lemma_size);
|
||||
p.register_bool_param("arith_reflect", m_arith_reflect);
|
||||
p.register_bool_param("arith_ignore_int", m_arith_ignore_int);
|
||||
p.register_unsigned_param("arith_lazy_pivoting", m_arith_lazy_pivoting_lvl);
|
||||
p.register_unsigned_param("arith_random_seed", m_arith_random_seed);
|
||||
p.register_bool_param("arith_random_initial_value", m_arith_random_initial_value);
|
||||
p.register_int_param("arith_random_lower", m_arith_random_lower);
|
||||
p.register_int_param("arith_random_upper", m_arith_random_upper);
|
||||
p.register_bool_param("arith_adaptive", m_arith_adaptive);
|
||||
p.register_double_param("arith_adaptive_assertion_threshold", m_arith_adaptive_assertion_threshold, "Delay arithmetic atoms if the num-arith-conflicts/total-conflicts < threshold");
|
||||
p.register_double_param("arith_adaptive_propagation_threshold", m_arith_adaptive_propagation_threshold, "Disable arithmetic theory propagation if the num-arith-conflicts/total-conflicts < threshold");
|
||||
p.register_bool_param("arith_dump_lemmas", m_arith_dump_lemmas);
|
||||
p.register_bool_param("arith_eager_eq_axioms", m_arith_eager_eq_axioms);
|
||||
p.register_unsigned_param("arith_branch_cut_ratio", m_arith_branch_cut_ratio);
|
||||
|
||||
p.register_bool_param("arith_add_binary_bounds", m_arith_add_binary_bounds);
|
||||
p.register_unsigned_param("arith_prop_strategy", 0, 1, reinterpret_cast<unsigned&>(m_arith_propagation_strategy), "Propagation strategy: 0 - use agility measures based on ration of theory conflicts, 1 - propagate proportional to ratio of theory conflicts (default)");
|
||||
|
||||
p.register_bool_param("arith_eq_bounds", m_arith_eq_bounds);
|
||||
p.register_bool_param("arith_lazy_adapter", m_arith_lazy_adapter);
|
||||
p.register_bool_param("arith_gcd_test", m_arith_gcd_test);
|
||||
p.register_bool_param("arith_eager_gcd", m_arith_eager_gcd);
|
||||
p.register_bool_param("arith_adaptive_gcd", m_arith_adaptive_gcd);
|
||||
p.register_unsigned_param("arith_propagation_threshold", m_arith_propagation_threshold);
|
||||
|
||||
p.register_bool_param("nl_arith", m_nl_arith, "enable/disable non linear arithmetic support. This option is ignored when ARITH_SOLVER != 2.");
|
||||
p.register_bool_param("nl_arith_gb", m_nl_arith_gb, "enable/disable Grobner Basis computation. This option is ignored when NL_ARITH=false");
|
||||
p.register_bool_param("nl_arith_gb_eqs", m_nl_arith_gb_eqs, "enable/disable equations in the Grobner Basis to be copied to the Simplex tableau.");
|
||||
p.register_bool_param("nl_arith_gb_perturbate", m_nl_arith_gb_perturbate, "enable/disable perturbation of the variable order in GB when searching for new polynomials.");
|
||||
p.register_unsigned_param("nl_arith_gb_threshold", m_nl_arith_gb_threshold, "Grobner basis computation can be very expensive. This is a threshold on the number of new equalities that can be generated.");
|
||||
p.register_bool_param("nl_arith_branching", m_nl_arith_branching, "enable/disable branching on integer variables in non linear clusters");
|
||||
p.register_unsigned_param("nl_arith_rounds", m_nl_arith_rounds, "threshold for number of (nested) final checks for non linear arithmetic.");
|
||||
p.register_unsigned_param("nl_arith_max_degree", m_nl_arith_max_degree, "max degree for internalizing new monomials.");
|
||||
PRIVATE_PARAMS({
|
||||
p.register_bool_param("arith_fixnum", m_arith_fixnum);
|
||||
p.register_bool_param("arith_int_only", m_arith_int_only);
|
||||
p.register_bool_param("arith_enum_const_mod", m_arith_enum_const_mod, "Create axioms for the finite set of equalities for (mod x k) where k is a positive numeral constant");
|
||||
p.register_bool_param("arith_int_eq_branching", m_arith_int_eq_branching, "Determine branch predicates based on integer equation solving");
|
||||
});
|
||||
p.register_bool_param("arith_euclidean_solver", m_arith_euclidean_solver, "");
|
||||
void theory_arith_params::updt_params(params_ref const & _p) {
|
||||
smt_params_helper p(_p);
|
||||
m_arith_random_initial_value = p.arith_random_initial_value();
|
||||
m_arith_mode = static_cast<arith_solver_id>(p.arith_solver());
|
||||
m_nl_arith = p.arith_nl();
|
||||
m_nl_arith_gb = p.arith_nl_gb();
|
||||
m_nl_arith_branching = p.arith_nl_branching();
|
||||
m_nl_arith_rounds = p.arith_nl_rounds();
|
||||
m_arith_euclidean_solver = p.arith_euclidean_solver();
|
||||
m_arith_propagate_eqs = p.arith_propagate_eqs();
|
||||
m_arith_branch_cut_ratio = p.arith_branch_cut_ratio();
|
||||
m_arith_int_eq_branching = p.arith_int_eq_branch();
|
||||
m_arith_ignore_int = p.arith_ignore_int();
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@ Revision History:
|
|||
#define _THEORY_ARITH_PARAMS_H_
|
||||
|
||||
#include<limits.h>
|
||||
#include"params.h"
|
||||
|
||||
enum arith_solver_id {
|
||||
AS_NO_ARITH,
|
||||
|
|
@ -104,7 +105,7 @@ struct theory_arith_params {
|
|||
bool m_arith_euclidean_solver;
|
||||
|
||||
|
||||
theory_arith_params():
|
||||
theory_arith_params(params_ref const & p = params_ref()):
|
||||
m_arith_mode(AS_ARITH),
|
||||
m_arith_auto_config_simplex(false),
|
||||
m_arith_blands_rule_threshold(1000),
|
||||
|
|
@ -149,7 +150,10 @@ struct theory_arith_params {
|
|||
m_nl_arith_branching(true),
|
||||
m_nl_arith_rounds(1024),
|
||||
m_arith_euclidean_solver(false) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p);
|
||||
};
|
||||
|
||||
#endif /* _THEORY_ARITH_PARAMS_H_ */
|
||||
|
|
|
|||
25
src/smt/params/theory_bv_params.cpp
Normal file
25
src/smt/params/theory_bv_params.cpp
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
theory_bv_params.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-12-02.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"theory_bv_params.h"
|
||||
#include"smt_params_helper.hpp"
|
||||
|
||||
void theory_bv_params::updt_params(params_ref const & _p) {
|
||||
smt_params_helper p(_p);
|
||||
m_bv_reflect = p.bv_reflect();
|
||||
}
|
||||
|
|
@ -19,6 +19,8 @@ Revision History:
|
|||
#ifndef _THEORY_BV_PARAMS_H_
|
||||
#define _THEORY_BV_PARAMS_H_
|
||||
|
||||
#include"params.h"
|
||||
|
||||
enum bv_solver_id {
|
||||
BS_NO_BV,
|
||||
BS_BLASTER
|
||||
|
|
@ -31,24 +33,17 @@ struct theory_bv_params {
|
|||
bool m_bv_cc;
|
||||
unsigned m_bv_blast_max_size;
|
||||
bool m_bv_enable_int2bv2int;
|
||||
theory_bv_params():
|
||||
theory_bv_params(params_ref const & p = params_ref()):
|
||||
m_bv_mode(BS_BLASTER),
|
||||
m_bv_reflect(true),
|
||||
m_bv_lazy_le(false),
|
||||
m_bv_cc(false),
|
||||
m_bv_blast_max_size(INT_MAX),
|
||||
m_bv_enable_int2bv2int(false) {}
|
||||
#if 0
|
||||
void register_params(ini_params & p) {
|
||||
p.register_int_param("bv_solver", 0, 2, reinterpret_cast<int&>(m_bv_mode), "0 - no bv, 1 - simple");
|
||||
p.register_unsigned_param("bv_blast_max_size", m_bv_blast_max_size, "Maximal size for bit-vectors to blast");
|
||||
p.register_bool_param("bv_reflect", m_bv_reflect);
|
||||
p.register_bool_param("bv_lazy_le", m_bv_lazy_le);
|
||||
p.register_bool_param("bv_cc", m_bv_cc, "enable congruence closure for BV operators");
|
||||
p.register_bool_param("bv_enable_int2bv_propagation", m_bv_enable_int2bv2int,
|
||||
"enable full (potentially expensive) propagation for int2bv and bv2int");
|
||||
}
|
||||
#endif
|
||||
m_bv_enable_int2bv2int(false) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p);
|
||||
};
|
||||
|
||||
#endif /* _THEORY_BV_PARAMS_H_ */
|
||||
|
|
|
|||
|
|
@ -179,7 +179,9 @@ namespace smt {
|
|||
}
|
||||
|
||||
void updt_params(params_ref const & p) {
|
||||
params2smt_params(p, fparams());
|
||||
// We don't need params2smt_params anymore. smt_params has support for reading params_ref.
|
||||
// The update is performed at smt_kernel "users".
|
||||
// params2smt_params(p, fparams());
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
// PARAM-TODO copy p --> m_params
|
||||
m_params.updt_params(p);
|
||||
if (m_context == 0)
|
||||
return;
|
||||
m_context->updt_params(p);
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ Notes:
|
|||
#include"rewriter_types.h"
|
||||
|
||||
class smt_tactic : public tactic {
|
||||
smt_params m_params;
|
||||
smt_params m_params;
|
||||
params_ref m_params_ref;
|
||||
statistics m_stats;
|
||||
std::string m_failure;
|
||||
|
|
@ -63,9 +63,7 @@ public:
|
|||
virtual void updt_params(params_ref const & p) {
|
||||
TRACE("smt_tactic", tout << this << "\nupdt_params: " << p << "\n";);
|
||||
updt_params_core(p);
|
||||
m_params_ref = p;
|
||||
// PARAM-TODO update params2smt_params p ---> m_params
|
||||
params2smt_params(m_params_ref, fparams());
|
||||
fparams().updt_params(p);
|
||||
SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config);
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue