mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Merge pull request #1797 from c-cube/conf-dt-lazy-split

Browse source 
expose the configuration param for datatype case splits
This commit is contained in:
Nikolaj Bjorner 2018-08-10 16:09:13 -07:00 • committed by GitHub
commit a13b6a99d6
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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_bv_params::updt_params(p);
theory_pb_params::updt_params(p); theory_pb_params::updt_params(p);
// theory_array_params::updt_params(p); // theory_array_params::updt_params(p);
theory_datatype_params::updt_params(p);
updt_local_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', 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_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'), ('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_ #ifndef THEORY_DATATYPE_PARAMS_H_
#define THEORY_DATATYPE_PARAMS_H_ #define THEORY_DATATYPE_PARAMS_H_
#include "smt/params/smt_params_helper.hpp"
struct theory_datatype_params { struct theory_datatype_params {
unsigned m_dt_lazy_splits; unsigned m_dt_lazy_splits;
@ -26,11 +28,10 @@ struct theory_datatype_params {
m_dt_lazy_splits(1) { m_dt_lazy_splits(1) {
} }
#if 0 void updt_params(params_ref const & _p) {
void register_params(ini_params & p) { smt_params_helper p(_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"); 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; } void display(std::ostream & out) const { out << "m_dt_lazy_splits=" << m_dt_lazy_splits << std::endl; }
}; };