mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

User control over qi.quick_checker smt_params option

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-24 11:17:18 -07:00
parent d06f4bd337
commit 1c06229755
2 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/params/qi_params.cpp
View file

@ -35,6 +35,7 @@ void qi_params::updt_params(params_ref const & _p) {
m_qi_lazy_threshold = p.qi_lazy_threshold();
m_qi_cost = p.qi_cost();
m_qi_max_eager_multipatterns = p.qi_max_multi_patterns();
m_qi_quick_checker = static_cast<quick_checker_mode>(p.qi_quick_checker());
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;

1
src/smt/params/smt_params_helper.pyg
View file

@ -36,6 +36,7 @@ def_module_params(module_name='smt',
('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'),
('qi.quick_checker', UINT, 0, 'specify quick checker mode, 0 - no quick checker, 1 - using unsat instances, 2 - using both unsat and no-sat instances'),
('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),