mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

update dependencies

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-30 22:48:10 -08:00
parent 529f116be0
commit 847aec1d30
5 changed files with 17 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_project.py
View file

@ -21,10 +21,10 @@ def init_project_def():
add_lib('hilbert', ['util'], 'math/hilbert') add_lib('hilbert', ['util'], 'math/hilbert')
add_lib('automata', ['util'], 'math/automata') add_lib('automata', ['util'], 'math/automata')
add_lib('params', ['util']) add_lib('params', ['util'])
add_lib('smt_params', ['params'], 'smt/params')
add_lib('realclosure', ['interval'], 'math/realclosure') add_lib('realclosure', ['interval'], 'math/realclosure')
add_lib('subpaving', ['interval'], 'math/subpaving') add_lib('subpaving', ['interval'], 'math/subpaving')
add_lib('ast', ['util', 'polynomial']) add_lib('ast', ['util', 'polynomial'])
add_lib('smt_params', ['ast', 'params'], 'smt/params')
add_lib('parser_util', ['ast'], 'parsers/util') add_lib('parser_util', ['ast'], 'parsers/util')
add_lib('euf', ['ast'], 'ast/euf') add_lib('euf', ['ast'], 'ast/euf')
add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner') add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner')

1
src/smt/params/CMakeLists.txt
View file

@ -12,6 +12,7 @@ z3_add_component(smt_params
theory_str_params.cpp theory_str_params.cpp
COMPONENT_DEPENDENCIES COMPONENT_DEPENDENCIES
params params
ast
PYG_FILES PYG_FILES
smt_params_helper.pyg smt_params_helper.pyg
) )

12
src/smt/params/smt_params.cpp
View file

@ -292,6 +292,18 @@ void smt_params::setup_QF_LIA(static_features const& st) {
} }
} }
void smt_params::setup_QF_UFIDL() {
m_relevancy_lvl = 0;
m_arith_reflect = false;
m_nnf_cnf = false;
m_arith_eq_bounds = true;
m_arith_eq2ineq = true;
// m_params.m_phase_selection = PS_THEORY;
m_restart_strategy = RS_GEOMETRIC;
m_restart_factor = 1.5;
m_restart_adaptive = false;
}
void smt_params::setup_QF_UFLIA() { void smt_params::setup_QF_UFLIA() {
m_relevancy_lvl = 0; m_relevancy_lvl = 0;
m_arith_reflect = false; m_arith_reflect = false;

2
src/smt/params/smt_params.h
View file

@ -274,6 +274,8 @@ struct smt_params : public preprocessor_params,
void setup_QF_LIA(static_features const& st); void setup_QF_LIA(static_features const& st);
void setup_QF_UFIDL();
void setup_QF_UFLIA(); void setup_QF_UFLIA();
void setup_QF_UFLRA(); void setup_QF_UFLRA();

12
src/smt/smt_setup.cpp
View file

@ -377,15 +377,7 @@ namespace smt {
void setup::setup_QF_UFIDL() { void setup::setup_QF_UFIDL() {
TRACE("setup", tout << "setup_QF_UFIDL()\n";); TRACE("setup", tout << "setup_QF_UFIDL()\n";);
m_params.m_relevancy_lvl = 0; m_params.setup_QF_UFIDL();
m_params.m_arith_reflect = false;
m_params.m_nnf_cnf = false;
m_params.m_arith_eq_bounds = true;
m_params.m_arith_eq2ineq = true;
// m_params.m_phase_selection = PS_THEORY;
m_params.m_restart_strategy = RS_GEOMETRIC;
m_params.m_restart_factor = 1.5;
m_params.m_restart_adaptive = false;
setup_lra_arith(); setup_lra_arith();
} }
@ -624,8 +616,6 @@ namespace smt {
} }
} }
void setup::setup_arith() { void setup::setup_arith() {
static_features st(m_manager); static_features st(m_manager);
IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";); IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);