mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

feat(smt/dt): expose the configuration param for datatype case splits

Browse source
This commit is contained in:
Simon Cruanes 2018-08-10 17:37:23 -05:00
parent 8b4e1c1209
commit 0aca1ad4c1
3 changed files with 8 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -63,6 +63,7 @@ void smt_params::updt_params(params_ref const & p) {
theory_bv_params::updt_params(p);
theory_pb_params::updt_params(p);
// theory_array_params::updt_params(p);
theory_datatype_params::updt_params(p);
updt_local_params(p);
}

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

@ -94,5 +94,6 @@ def_module_params(module_name='smt',
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'),
('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none')
('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'),
('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy')
))

9
src/smt/params/theory_datatype_params.h
View file

@ -19,6 +19,8 @@ Revision History:
#ifndef THEORY_DATATYPE_PARAMS_H_
#define THEORY_DATATYPE_PARAMS_H_
#include "smt/params/smt_params_helper.hpp"
struct theory_datatype_params {
unsigned m_dt_lazy_splits;
@ -26,11 +28,10 @@ struct theory_datatype_params {
m_dt_lazy_splits(1) {
}
#if 0
void register_params(ini_params & p) {
p.register_unsigned_param("dt_lazy_splits", m_dt_lazy_splits, "How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy");
void updt_params(params_ref const & _p) {
smt_params_helper p(_p);
m_dt_lazy_splits = p.dt_lazy_splits();
}
#endif
void display(std::ostream & out) const { out << "m_dt_lazy_splits=" << m_dt_lazy_splits << std::endl; }
};